---
name: project-step1291-brownawell-masser-2026-08-08
description: STEP 1291 (2026-08-08) — Brownawell-Masser n-term abc + n-tuple Wronskian machinery (Mathlib 自 TODO 直接充足)。 STEP 1290 Mason-Stothers arc 続編、 「複製ではなく追加」 唯一候補。 6 declaration 中 5 axiom-free + 1 intentional documented sorry。
metadata: 
  node_type: memory
  type: project
  originSessionId: 88fc9abe-5f58-4371-bbbc-4ad03858d1ce
  modified: 2026-08-08T15:24:49.651Z
---

# STEP 1291 (2026-08-08): Brownawell-Masser n-term abc + n-tuple Wronskian

**Fact**: STEP 1290 (Mason-Stothers 付値・因子別定式化 close 2026-08-07) 続編、 藤本さん turn 12 hand-over + turn 14 P2 close 判断で承認された (c) Brownawell-Masser n 項一般化 を STEP 1291 として実装。 6 declaration 中 5 が sorry-free (Mathlib base [propext, Classical.choice, Quot.sound] のみ)、 1 が intentional documented sorry (`brownawellMasser` inequality proof、 Deliverable C = out of scope 明示)。

**Why**: 藤本さん STEP 1290 turn 14 で `(c) Brownawell-Masser Mathlib grep 義務` 提示、 Rei grep で `BrownawellMasser` 0 hit + `Wronskian.lean` docstring TODO 明示 `「Define Wronskian for n-tuple of polynomials」` 発見 = **Mathlib 自身が n-tuple Wronskian を未実装宣言**。 (c) は 真の 「追加」 candidate confirm。 STEP 1290 の 「独立実装 4 件目」 corrigendum 回避 discipline 継承 (Mason 1984/Isabelle Eberl/Lean 3 Wagemaker/Baek-Lee 2024 の 別実装 ではない、 folklore n-tuple Wronskian の Lean 4 mechanical assurance + BM statement 40 年前 prior art の型的準備 のみ)。

**How to apply**:

- 本 STEP は BM を **証明していない** (proof は sorry、 explicit + counted)
- 「独立実装 4 件目」 と絶対に主張しない (`feedback_one_reproduction_over_ten_unverified.md` framing 事前訂正継承)
- Rei-side value は 3 点のみ: (a) Mathlib 自 TODO 直接充足、 (b) BM statement 型的準備、 (c) n=3 wrap machine-checked reduction evidence
- Mathlib PR 対象外 (`feedback_external_community_outreach_premature.md`)、 Rei stack 内 wait
- n≥4 の proof (Deliverable C) は Voloch-Snyder analysis 数週間案件で別 STEP、 藤本さん judgment
- 世界唯一 / Rei だけが 系主張ゼロ (`feedback_world_uniqueness_claim_controllable.md`)

## 実装 detail

**File**: `data/lean4-mathlib/CollatzRei/BrownawellMasser.lean` (200+ 行、 6 declaration)

**Declarations**:
1. `wronskianN {n : ℕ} (a : Fin n → R[X]) : R[X] := Matrix.det (fun i j => derivative^[i] (a j))` — n-tuple Wronskian 定義 (Mathlib TODO 直接充足)
2. `wronskianN_two_eq_wronskian` — pair Wronskian bridge (n=2、 `Matrix.det_fin_two` 経由)
3. `wronskianN_zero_of_eq_columns` — column-eq zero (`Matrix.det_zero_of_column_eq` 直接適用 3 行)
4. `wronskianN_permute` — 反対称性 (`Matrix.det_permute'` 経由 5 行)
5. `brownawellMasser` — BM inequality **intentional sorry** (Deliverable B statement only + Deliverable C explicit out of scope)
6. `brownawellMasser_three` — n=3 wrap = `Polynomial.abc` (Baek-Lee 2024) 1 行呼び出し (Deliverable B 完成部分、 sorry-free)

**Axiom profile (`#print axioms` 実測)**:
- 5 declaration: `[propext, Classical.choice, Quot.sound]` (Mathlib base、 sorryAx 0)
- 1 declaration (`brownawellMasser`): `[propext, sorryAx, Classical.choice, Quot.sound]` (intentional documented)

**Build**: BrownawellMasser 1560 jobs 9.1s + root CollatzRei 7943/7943 jobs 32s = regression 0

**Bound form 選択**: `2·(deg + 1) ≤ (n-1)(n-2)·rad` を Nat division 回避で選択 (原 BM は `deg ≤ (n-1)(n-2)/2 · (rad - 1)`)。 n=3 で両者 equivalent + `Polynomial.abc` 完全一致 (`(n-1)(n-2)=2`、 `2·(deg+1) ≤ 2·rad` = `deg+1 ≤ rad`)、 n≥4 では present form は 弱い変形 (原 form の 2 倍)、 tightest ではないが well-typed で future development 台座として十分。

## Site 反映

`public/tools/research-log-2026-08-08-brownawell-masser-arc/index.html` (~19 KB、 9 section):
1. Context (STEP 1290 → STEP 1291)
2. Phase A: 30-min grep 追加 (verify table)
3. Phase B: Statement design + withdrawal-line (3 deliverable split)
4. Phase D: 6 declaration axiom profile table
5. Prior art (Brownawell-Masser 1986 + Voloch 1985 + Snyder 2000 + Baek-Lee 2024)
6. STEP 1290 arc 継承 (順序原則 + framing 事前訂正 + rhymeOrTheorem discipline)
7. Withdrawal-line 実測 (全 phase budget 内、 発動なし)
8. Honest scope 6 条
9. 関連 memory + files

dist-renderer mirror force-track md5 一致 (0126c8a92c6bea1e2cef7312fba6a045)、 2026-08-06 「全研究 site 反映 default」 protocol 適用 6 例目。

## Withdrawal-line 実測

| Phase | Budget | 実測 | 結果 |
|-------|--------|------|------|
| A grep verify | 30 min | ~15 min | Mathlib 0 hit + TODO 明示 confirmed |
| B statement design | ~1 hour | ~30 min | bound form 選択 (÷2 回避) |
| D-1 Deliverable A | ~1-3 hour | ~1 hour | 5 theorem axiom-free (import fix 2 回) |
| D-2 Deliverable B | best-effort | ~15 min | n=3 wrap = `Polynomial.abc` 1 行、 statement は sorry で honest close |
| D-3 Deliverable C | out of scope | ─ | BM n≥4 proof は別 STEP 数週間案件 |

全 phase budget 内 completion、 withdrawal-line 発動なし。 順序原則継承 = 撤退線は 定式化困難のシグナルとして事前準備、 発動しなかったのは 良い意味 (Mathlib infrastructure `Matrix.det_fin_two` + `Matrix.det_zero_of_column_eq` + `Matrix.det_permute'` + `Polynomial.derivative^[k]` + `Polynomial.abc` が 揃っていた)。

## Related

- [[project-step1290-mason-stothers-valuation-arc-2026-08-07]] — (b) close + (c) hand-over origin
- [[project-abc-radar-quality-sweep-arc-2026-08-07]] — STEP 1287+1288 前々 arc
- [[feedback-one-reproduction-over-ten-unverified]] — 順序原則 + framing 事前訂正 継承
- [[feedback-world-uniqueness-claim-controllable]] — novelty 主張ゼロ discipline
- [[feedback-zero-sorry-floor-not-ceiling]] — 5 sorry-free = floor discipline
- [[feedback-external-community-outreach-premature]] — Mathlib PR 対象外
- [[feedback-no-rush-publication]] — 急がずゆっくりと
- [[feedback-all-research-site-reflection-default]] — 2026-08-06 protocol 適用 6 例目