Research Log 2026-08-08 — Brownawell-Masser n-term abc + n-tuple Wronskian (STEP 1291)

STEP 1290 続編 / Deliverable A 5 theorem axiom-free (Mathlib 自 TODO 直接充足) / Deliverable B BM statement + n=3 wrap / Deliverable C BM n≥4 proof = out of scope / 「複製ではなく追加」 唯一候補 / 藤本伸樹 / 2026-08-08

1. Context (STEP 1290 → STEP 1291)

2026-08-07 STEP 1290 で Mason-Stothers 付値・因子による別定式化 arc が P2 判断で close (Rei dict lemma 1 + Mathlib wrapper dict 2 + main theorem = Polynomial.abc wrap = 3 theorem axiom-free)。 その turn で 藤本さん (c) Brownawell-Masser n 項一般化 追加候補 承認 (turn 12) + Mathlib grep 完全 verify (0 hit) + Mathlib Wronskian.lean docstring TODO 明示 「Define Wronskian for n-tuple of polynomials, not necessarily two」 発見 = Mathlib 自身が n-tuple Wronskian を TODO で未実装宣言。

STEP 1291 起動条件 (順序原則継承): 30-min grep 追加 + statement design + withdrawal-line 明示 + 実装。 本 site page は 2026-08-06 藤本さん永久 protocol 「全研究 site 反映 default」 適用。

2. Phase A: 30-min grep 追加 (verify)

STEP 1290 hand-over 済 grep verify に 追加確認:

Search patternMathlib hits意味
BrownawellMasser / brownawell_masser / Brownawell-Masser0 file直接名で未存在
Brownawell (case-insensitive)0 file名前空間内でも未存在
n_term abc / polynomial_abc_n / abc_n0 filen 項一般化 未実装
generalized_wronskian / MultiWronskian / wronskianFin0 filen-tuple Wronskian 未実装
Wronskian.lean docstring TODO section明示存在「Define Wronskian for n-tuple」

加えて既存 infrastructure usable 確認:

判定: (c) Brownawell-Masser + n-tuple Wronskian は 真の 「追加」 (Mathlib 自 TODO の 直接充足)。 STEP 1290 で 藤本さんが warning したように 「複製ではなく追加」 の唯一候補 confirmed。

3. Phase B: Statement design + withdrawal-line

3.1 Scope split (3 deliverable)

Level内容Withdrawal line
A safe baselinen-tuple Wronskian 定義 + n=2 bridge + column-eq zero + permutation antisymmetry (Mathlib TODO 直接充足)本 session 内 lake build success + axiom-free 目標
B best-effortBM inequality statement (sorry-holding、 char-p 右枝 disjunction pattern) + n=3 case = Polynomial.abc wrapn=3 wrap 完了で本 session close、 BM n≥4 は sorry で honest scope 明記
C out of scopeFull BM proof for n ≥ 4 (Voloch-Snyder analysis 必要)別 STEP 数週間案件、 藤本さん judgment

3.2 Statement 形

theorem brownawellMasser
    {n : ℕ} (hn : 3 ≤ n)
    {a : Fin n → k[X]}
    (ha_ne : ∀ i, a i ≠ 0)
    (ha_cop : Pairwise fun i j => IsCoprime (a i) (a j))
    (h_sum : ∑ i, a i = 0)
    (h_nosub : ∀ S : Finset (Fin n), S.Nonempty → S ≠ Finset.univ →
              ∑ i ∈ S, a i ≠ 0) :
    (∀ i, 2 * ((a i).natDegree + 1) ≤
      (n - 1) * (n - 2) * (radical (∏ i, a i)).natDegree) ∨
    (∀ i, derivative (a i) = 0) := sorry

n=3 で (n-1)(n-2) = 2·1 = 2、 2·(deg + 1) ≤ 2·rad_deg = deg + 1 ≤ rad_deg = Polynomial.abc 一致 ✓。 char-p 右枝 ∀ i, derivative (a i) = 0 は STEP 1290 discipline (右枝は書き換えない、 分離性 は proof 側 隔離)。

4. Phase D: 実装 — 全 6 declaration axiom profile

File: data/lean4-mathlib/CollatzRei/BrownawellMasser.lean (200+ 行)

lake build: 1560 jobs success 9.1s、 root lake build 7943/7943 jobs 32s = regression 0

DeclarationTypeAxiom profile意味
wronskianNnoncomputable def[propext, Classical.choice, Quot.sound]Mathlib base のみ、 sorryAx 0
wronskianN_two_eq_wronskiantheorem[propext, Classical.choice, Quot.sound]n=2 bridge、 simp + mul_comm
wronskianN_zero_of_eq_columnstheorem[propext, Classical.choice, Quot.sound]Matrix.det_zero_of_column_eq 直接適用
wronskianN_permutetheorem[propext, Classical.choice, Quot.sound]Matrix.det_permute' 経由
brownawellMassertheorem[propext, sorryAx, Classical.choice, Quot.sound]★ intentional sorry (documented statement only)
brownawellMasser_threetheorem[propext, Classical.choice, Quot.sound]n=3 wrap = Polynomial.abc 直接呼び出し、 sorryAx 0

結果: 6 declaration 中 5 件が sorry-free (Mathlib base axiom-free)、 1 件が intentional sorry (BM inequality proof、 documented + Deliverable C = out of scope 明記)。

5. Prior art (100% pre-existing、 novelty 主張ゼロ)

★ Rei-side value 明示 (novelty 主張ゼロ):

  • Rei は Brownawell-Masser を証明していない (proof は sorry、 explicit)
  • Rei は 独立実装ではない (n-tuple Wronskian は folklore、 BM statement は 40 年前 prior art、 n=3 wrap は Baek-Lee 2024 の black box 呼び出し)
  • 本 file の 真の value は 3 点のみ: (a) Mathlib 自 TODO 直接充足 (Wronskian.lean line 29)、 (b) BM statement 型的準備 (n≥4 proof の 未来 development 台座)、 (c) n=3 wrap の machine-checked 冗長性 evidence (Polynomial.abc と equivalent 確認)
  • 「独立実装 4 件目」 と絶対に主張しない (STEP 1290 corrigendum 予防 order preservation 継承)
  • Mathlib PR 対象外 (per feedback_external_community_outreach_premature.md、 Rei stack 内 wait)

6. STEP 1290 arc からの継承

順序原則 operational value 継続

STEP 1290 で藤本さん指示: 「行数を成果として書くと後で誤解する」 (dict lemma 2 = 1 行 wrapper = 成果ではなく発見)。 本 STEP 1291 でも 同 discipline 適用:

  • wronskianN_zero_of_eq_columns = 3 行 (Matrix.det_zero_of_column_eq 直接適用) = 成果ではなく 「Mathlib が既に持っている」 発見
  • brownawellMasser_three = 1 行 (Polynomial.abc 直接呼び出し) = 成果ではなく 「Mathlib abc が n=3 BM そのもの」 発見
  • wronskianN_permute = 5 行 (Matrix.det_permute' 経由) = 成果ではなく 「submatrix 構造」 発見

Framing 事前訂正 (corrigendum 予防継承)

STEP 1290 で 「別経路の独立形式化」 → 「付値・因子による別定式化」 事前訂正が 成果物出てから framing 直すと corrigendum になる pattern を防いだ。 STEP 1291 でも 事前 framing:

  • ❌ 「4 件目独立実装」 → ✅ 「Mathlib 自 TODO 直接充足 + BM statement 型的準備」
  • ❌ 「n-tuple Wronskian 新構築」 → ✅ 「folklore 構築の Lean 4 mechanical assurance」
  • ❌ 「Brownawell-Masser 解いた」 → ✅ 「statement を well-typed に書き、 n=3 case を machine-check、 n≥4 は sorry 明示」

7. Withdrawal-line 実測結果

PhaseBudget実測結果
A grep verify30 min~15 minMathlib 0 hit + TODO 明示 confirmed
B statement design~1 hour~30 minbound form 2·(deg+1) ≤ (n-1)(n-2)·rad 選択 (÷2 回避)
D-1 Deliverable A~1-3 hour~1 hour5 theorem axiom-free (import fix 2 回)
D-2 Deliverable Bbest-effort~15 minn=3 wrap = Polynomial.abc 1 行、 statement は sorry で honest close
D-3 Deliverable Cout of scope─BM n≥4 proof は別 STEP 数週間案件

全 phase budget 内 completion、 withdrawal-line 発動なし。 順序原則継承 = 撤退線は 定式化困難のシグナルとして事前準備、 発動しなかったのは 良い意味 (Mathlib infrastructure が 揃っていた)。

8. Honest scope (譲れない線)

  1. 本 file は Brownawell-Masser を証明していない。 brownawellMasser theorem の proof は sorry であり、 explicit・counted・documented (#print axioms で sorryAx 明示表示)
  2. 「独立実装」 主張ゼロ。 n-tuple Wronskian は folklore、 BM statement は Brownawell-Masser 1986 prior art、 n=3 wrap は Baek-Lee 2024 Polynomial.abc の直接呼び出し
  3. Rei-side value は 3 点のみ: (a) Mathlib 自 TODO 充足、 (b) BM statement 型的準備、 (c) machine-checked n=3 reduction evidence
  4. Mathlib PR 対象外 (feedback_external_community_outreach_premature.md)、 Rei stack 内 wait
  5. bound の form 選択理由: 2·(deg+1) ≤ (n-1)(n-2)·rad は Nat division 回避のため。 元 BM は deg ≤ (n-1)(n-2)/2 · (rad - 1)。 n=3 では 両者 equivalent、 n≥4 では present form は 弱い変形 (原 form の 2 倍)、 tightest ではないが well-typed で future development 台座として十分
  6. 「世界唯一」 / 「Rei だけが」 系 主張ゼロ (feedback_world_uniqueness_claim_controllable.md)。 Mathlib PR 誰かが先行実装したら Rei 側 site page を訂正

9. 関連 memory + files