Research Log 2026-08-07 — Mason-Stothers 付値・因子による別定式化 (STEP 1290 close)

1. Context (STEP 1287+1288 → STEP 1290)

STEP 1287+1288 arc (abc quality sweep c ≤ 10⁵ + research-radar abc topic +47 keywords) の直後、 藤本さんが「進めている abc 証明」 の Rei 内 file 実体が statement + folklore + 経験的 のみ = 実質未着手と指摘。 item 2 replace として Mason-Stothers Lean 4 formalization を STEP 1290 で着手。

藤本さん承認 (turn 8) + 4 条件:

1. 標数扱いを statement に先入れ (disjunction pattern = 右枝 `derivative = 0` で char p 破綻吸収、 [CharZero k] 追加せず Mathlib 同型維持)
2. 撤退線 = 3 日 for dictionary lemma 2 のみ (dict 1 は撤退線外)
3. Isabelle Eberl + Lean 3 Wagemaker signature 精読 は 今 skip (独立性汚染回避線を薄化しないため)
4. 符号紙作業 = 「右枝をどう書くか」 でなく 「v_p(f') の case-split point」

turn 12 で追加 3 訂正:

1. (a) Mason 1984 棄却: 対数微分 ≡ Wronskian の同一恒等式の別記法 (a+b=c を微分して a/c·(a'/a − c'/c) + b/c·(b'/b − c'/c) = 0 = W(a,b))、 補題共有 → 4 件目独立実装にならない
2. (b) k(X) 付値経路 選択 = Stothers 経路の生き残り (P¹ = 種数 0 で分岐 → 付値 退化)、 但し 独立性見積もり訂正: Stothers を種数 0 に落とすと φ' 分子は W(a,c) そのもの → 「別経路」 ではなく 「付値・因子による別定式化」 の公算高 (Framing 事前訂正、 語を先に直す)
3. (c) Brownawell-Masser n 項一般化 追加候補 = Mathlib になし (仮定) = 唯一の 「複製ではなく追加」 候補、 順序 (b) → (c) 維持、 (b) 完了報告に 「独立実装 4 件目」 と書かない

turn 12 の 3rd 訂正: 右枝 statement 書き換えない (Mathlib 同型絶対最優先) + 分離性は proof 側隔離 + 反例側探索余力振替。

turn 14 で P2 close 判断 + 「予測の的中として記録」 + 順序原則 corrigendum 予防 feedback 化 + (c) Brownawell-Masser Mathlib grep 義務。

2. 実装 (3 theorem 全 axiom-free)

File: data/lean4-mathlib/CollatzRei/MasonStothersValuation.lean (~200 行)

3. ★ 留保付き推測が結果的に当たった (「予測の的中」 は校正で撤回)

今回の発見 (実装中): dict 2 で Mathlib pow_sub_one_dvd_derivative_of_pow_dvd が 局所は Wronskian-free 5 行 で v_p(f') 関係を提供と判明 (任意 q ∈ R[X] + 標数仮定なし)。 加えて main theorem の global combining step (a·b' − a'·b ↔ radical(abc)) で必ず Wronskian に戻ると判明。

= 局所と大域の境目に、 微分と分岐の同一性が現れた。 P1 (global Wronskian-free attempt) に賭ける理由なし = P2 (Mathlib wrap で close + (c) 直行) が Recommended。

4. ★ Framing 事前訂正の観測事実 (校正 2026-08-07 藤本さん turn 15)

順序原則 (「十本の未検証より一本の再現」) の operational 実例、 但し 厳密には 反実仮想部分を明示。 Feedback として永久保存 (memory/feedback_one_reproduction_over_ten_unverified.md update 2026-08-07 section、 記録校正も順序原則適用対象として保存)。

5. ★ 反例側探索結果 retain (右枝設計妥当性の裏側支持)

初期候補: char 2, k = F_2, (a, b, c) = (X², X²+1, 1) triple

• a + b = X² + X² + 1 = 1 = c (char 2 で 2X² = 0) ✓
• gcd(X², X²+1) = 1 (pairwise coprime) ✓
• a' = b' = c' = 0 (全 derivative = 0)
• → Mathlib 右枝で吸収
• (b) approach で v_p(f') 書けない (全 f' = 0 で v_p(f') = ∞ = well-defined でない)

6. (c) Brownawell-Masser hand-over — grep verify 済

藤本さん turn 14 義務: 「Brownawell-Masser が Mathlib に無いことを、 実際に grep で確認してください。 私は 『無いはず』 と書きましたが、 これは確認していません。 今回の一連で潰れた四つのうち二つは、 私の側の見積もり誤りでした。」 = 順序原則の 藤本さん側 self-check 適用。

Grep 実測

## TODO
- Define Wronskian for n-tuple of polynomials, not necessarily two.

判定: 藤本さん assertion 「Mathlib になし」 = grep で verify 済確定。 (c) は 真の 「追加」 confirm、 加えて n-tuple Wronskian machinery も STEP 1291 scope に含む (Mathlib TODO 実装が hand-over 前提条件)。

7. STEP 1291 (c) 着手前条件 (順序原則継承)

• 30-min grep 追加: 関連 generalized derivative / higher Wronskian concepts の partial coverage 見落とし check
• Paper work: statement design、 char-p condition (Mathlib pattern 右枝 disjunction で inseparable 吸収)
• Withdrawal-line design: analogous to STEP 1290 (generalized Wronskian construction 3 日 / n-term bound 追加 7 日)

8. Honest scope

• 本 STEP は Mason-Stothers の 独立実装ではない (「独立実装 4 件目」 と称さない)
• 「付値・因子による別定式化」 も 限定的 = 局所は Rei wrapper、 global は Mathlib wrap
• Rei 独自成果 = dict lemma 1 の場所 (rad natDegree ↔ place count) のみ (他は Mathlib wrap)
• (c) が真の 「追加」 target = Brownawell-Masser n 項一般化 + generalized Wronskian machinery = 別 STEP 1291
• dict 2 の 「1 行 wrapper」 は 成果ではなく発見 (行数を成果として書くと後で誤解する、 価値は探索の側)
• 藤本さん総括: 「これは撤退ではありません。 予測の的中です」

9. ★ 選択肢の並べ方 訂正 (7 例目、 藤本さん turn 17)

Close 後、 藤本さんに 「少しだけでも進める事は可能ですか?」 と 問われ、 私は (A)-(E) の 5 選択肢を提示。 (E) 「今日は close 継続」 を 「距離変わらず」 の 列に並べたが、 これは 藤本さん turn 17 で訂正:

本件は 記録校正 (5+6 例目、 認定語 先確定 + 反実仮想撤回) に続く 7 例目 = 「選択肢を並べる際の軸の統一 or 分離」 として 学習対象。 順序原則の 適用領域が また一段 拡がった。

10. 今日の実質 = 位置を実測した日 (藤本さん turn 17)

私の 「(A) Letendre 精読」 Recommendation 押しは 過剰でした。 藤本さんの 「少しだけでも進めたい」 気持ちは、 今日が 訂正ばかりの一日 (419 + 実装数 + 経路 + framing + 記録の書き方まで、 全部正しい訂正) で 「前に進んでいない感覚」 が残ったから 出た問い、 という 分析が正確。

11. Close 意思