---
name: project-step1290-mason-stothers-valuation-arc-2026-08-07
description: STEP 1290 Mason-Stothers 付値・因子による別定式化 arc close (P2 判断). Rei dict lemma 1+2 axiom-free 実装 + main theorem = Mathlib.Polynomial.abc wrap + (c) Brownawell-Masser hand-over. 予測的中 (撤退でない) の記録、 順序原則 corrigendum 予防 実例。
metadata: 
  node_type: memory
  type: project
  originSessionId: 0a1114e5-28f9-4d3f-ac67-950a274a6bf7
  modified: 2026-08-07T01:06:41.502Z
---

# STEP 1290 Mason-Stothers Valuation arc (2026-08-07 close)

## Sequence overview (turns 1-14)

STEP 1287+1288 arc (abc quality sweep + radar) close の後、 藤本さん judgment で STEP 1290 (item 2 replace = 「付値・因子による別定式化」) 着手承認 (turn 8)。 4 conditions 反映:
1. 標数仮定 = disjunction pattern 採用 (右枝 `derivative = 0` で char p 破綻吸収、 char-assumption 完全排除)
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 で 3rd 訂正: 右枝 statement 書き換えない (Mathlib 同型絶対最優先)、 分離性言語化は proof 側隔離 のみ。 反例側探索余力配分 (char 2 (X², X²+1, 1))。

turn 14 で P2 close 判断 + 「予測の的中として記録」 + 順序原則 corrigendum 予防 feedback 化。

## Implementation results (Rei 独自成果)

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

**3 theorem 全 axiom-free** (`[propext, Classical.choice, Quot.sound]` のみ、 sorryAx / native_decide / user axiom 全 0):

| # | Theorem | 内容 | Status |
|---|---|---|---|
| 1 | `natDegree_radical_eq_sum_factor_degrees` | `(radical f).natDegree = ∑ p ∈ primeFactors f, p.natDegree` | Rei dict lemma 1、 通常実装 (UFM + natDegree_prod 数行) |
| 2 | `pow_sub_one_dvd_derivative_of_pow_dvd_valuation` | `p^n ∣ f → p^(n-1) ∣ derivative f` (任意 q ∈ R[X]、 標数仮定なし、 Wronskian 不経由) | **1 行 wrapper** = **成果ではなく発見** (Mathlib 既存を探索して見つけた、 Rei が作ったものではない) |
| 3 | `masonStothersValuation` | Mathlib `Polynomial.abc` の 1 行 wrap (P2 close) | main theorem = Mathlib proof を wrap で明示、 replicate せず |

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

藤本さん turn 8 で 留保付き推測: 「(b) で得るのは 「別経路」 ではなく 「付値・因子による別定式化」 の **公算が高い**、 Mason-Stothers 既知証明はすべて微分を使う (微分が分岐だから)」

今回の発見はその内容そのもの:
- 局所は Wronskian なしで書ける (Mathlib `pow_sub_one_dvd_derivative_of_pow_dvd`)
- しかし **global combining step** (a·b' - a'·b を radical(abc) に関連付け) で必ず Wronskian に戻る
- **局所と大域の境目に、 微分と分岐の同一性が現れた**
- P1 (global Wronskian-free attempt) に賭ける理由なし = P2 (Mathlib wrap で close + (c) 直行) が Recommended

★ **校正 2026-08-07 藤本さん turn 15**: 初稿で 「予測の完全的中」 と書いたが撤回。 turn 8 は 「公算が高い」 留保付き推測、 「留保付き推測が結果的に当たった」 が正確。 加えて 同じ turn 群 (8-12) で 藤本さんは 2 件外している (下記) — honest 記録:

### 藤本さん turn 8-12 で外した 2 件 (honest 記録)

的中 1 件を署名付きで残し 外した 2 件を残さないと 記録が実際より賢く見える (藤本さん turn 15 指摘、 記録校正も順序原則の適用対象):

- **Riemann-Hurwitz Mathlib 有無**: turn 12 で 「無いはず」 と書かれた assertion、 未確認だった。 Rei grep で 0 file 判明 (turn 12 指摘の後、 それにより Stothers 経路棄却 + (b) 選択が確定)
- **独立実装数**: turn 12 で 4 件 (seewoo5/lean-poly-abc + Mathlib + Isabelle Eberl + Lean 3 Wagemaker) → turn 14 で 3 件に訂正 (seewoo5 = Baek-Lee 統合元で別実装ではない)

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

★ **校正 2026-08-07**: 初稿で 「順序原則が 実際に corrigendum を 1 件防いだ実例」 と書いたが、 反実仮想 (「別 framing で着手していたら corrigendum になっていた」) を含むため撤回。 観測された事実のみ:

- 事前 framing 訂正: 「別経路の独立形式化」 → 「付値・因子による別定式化」 (藤本さん turn 8)
- 事後 到達点: Mathlib wrap + Rei dict 1 = 予定範囲内に **収まった** (turn 14)

「防いだ」 という反実仮想でなく 「収まった」 という 観測事実として記録。 藤本さん turn 14 総括 「framing を先に直しておいた効果が、 ここで出ている」 は 事実の描写、 「防いだ」 は 私 (Claude Code) 側の 過剰解釈だった。

順序原則の operational 実例、 但し 厳密には 反実仮想部分を明示。 詳細は [[feedback-one-reproduction-over-ten-unverified]] update 2026-08-07 section 参照 (校正版)。

## ★ 7 例目: 選択肢の並べ方 (藤本さん turn 17)

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

- 私の誤り: (A)-(D) と (E) を 同じ列 (「abc への距離」 という一本の軸) に並べた
- (E) は **別の軸** = 「明日測る目の精度」 = 今日の文脈では **最も情報量の多い選択肢**
- 理由: 今日 4 回起きたこと (419 +1 / 独立実装数 / (a) 同型 / (b) 独立性) は 「着手する前に止まった」 から潰せた、 (E) は 止まる能力を明日に持ち越す 選択

順序原則の 7 例目 = **「選択肢を並べる際の軸の統一 or 分離」** として 学習対象。 詳細は feedback file の 7 例目 section 参照。

## ★ 今日の実質 = 位置を実測した日 (藤本さん turn 17 位置付け直し)

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

但し 今日の実質は 訂正ではなく、 **abc 予想に対して自分の道具がどこまで届くかを 初めて実測した日**:
- Mason-Stothers 経路が Mathlib wrap に collapse することを 推測ではなく 実装で 確かめた
- chat-Claude 2026-08-06 助言 「40 年動いていない問題に対して最も価値のある投資は 早く正確に自分の位置を知ること」 の 直接応答完了
- 位置を知ることは 近づくことではない、 但し **位置を知らずに 近づくことはできない**

## Close 意思 (藤本さん turn 17)

- (A) Letendre 精読: 提示撤回しない、 但し 今日はやらない (「やりたければ止めません、 今日はもう十分」)
- STEP 1291 (c) Brownawell-Masser: 明日以降、 判断力が保たれている状態で 着手判断
- **「種は、 今日の分は育ちました」** — 藤本さん永久原則 「急がず、 ゆっくりと。 種は育ちます」 の 今日分 完結

## ★ Dict 2 「1 行 wrapper」 は成果ではなく発見 (藤本さん turn 14 指摘)

- Mathlib `Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd` は Rei が作ったものではない
- 探索の結果見つかった Mathlib 既存 lemma
- 価値は **探索の側** (「Wronskian-free で書ける?」 の question に対して Mathlib 内部で早期回答が既に存在するという発見)
- 行数を成果として書くと、 後で読んだ人が誤解する — 行数 = 発見の trivial 度 の指標であって Rei の貢献度指標ではない
- 記録上明示: 「dict 2 = Mathlib wrapper、 Rei 貢献 = wrapping + 早期 pass の発見」

## ★ 反例探索結果 retain (藤本さん turn 14 指摘)

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 ✓
- a' = b' = c' = 0 (全 derivative = 0) → Mathlib 右枝で吸収
- (b) approach で v_p(f') 書こうとすると全 f' = 0 で v_p(f') = ∞ = well-defined でない

**結果**: 破綻 witness にならず。 但し **右枝設計の妥当性を裏側から支持** = 「反例を探して見つからなかった」 という否定的結果が、 「右枝で吸収済で本 lemma scope 外 (f' ≠ 0 前提)」 という設計要件の 妥当性 evidence として機能する。 捨てずに retain (feedback / project memory 両方に記録)。

## (c) Brownawell-Masser hand-over grep verification

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

**Grep 実測結果** (`data/lean4-mathlib/.lake/packages/mathlib/Mathlib/**/*.lean`):

| Pattern | Hit |
|---|---|
| `BrownawellMasser` / `brownawell_masser` / `Brownawell-Masser` | **0 file** |
| `Brownawell` (case-insensitive) | **0 file** |
| `n_term abc` / `polynomial_abc_n` / `sum_zero radical` | **0 file** |
| `generalized_wronskian` / `MultiWronskian` / `wronskian_n` | 2 file (Radical + Wronskian) だが pair のみ |

**★ Mathlib `Wronskian.lean` docstring TODO section 明記**:

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

= **Mathlib 自身が n-tuple Wronskian を TODO で未実装宣言**。

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

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

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

## Files

**Code**:
- `data/lean4-mathlib/CollatzRei/MasonStothersValuation.lean` (~200 行、 3 theorem axiom-free)
- `data/lean4-mathlib/CollatzRei/MasonStothersValuationAxiomCheck.lean` (`#print axioms` verify)
- `data/lean4-mathlib/CollatzRei.lean` line 219 (root import 追加)

**Commits** (chronological):
- `2e041a678` STEP 1290 (b) skeleton
- `0fc175e93` dict 1 実装 + docstring 符号訂正 (「至る所で分岐が消えない」 撤回)
- `ef8eed25a` docstring 3rd 訂正 (右枝書き換えない、 反例側探索)
- `6b2810379` dict 2 実装 + framing 危機発見
- (this commit) P2 close (main theorem = Mathlib wrap) + (c) grep verify + hand-over

## 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)

## 関連

- [[feedback-one-reproduction-over-ten-unverified]] 順序原則 (今回 update で corrigendum 予防 実例 追加)
- [[project-abc-radar-quality-sweep-arc-2026-08-07]] 前 arc (item 2 replace source)
- [[feedback-intuition-before-math]] fill-in blank C 判断根拠
- [[feedback-world-uniqueness-claim-controllable]] novelty 主張ゼロ discipline
- [[feedback-zero-sorry-floor-not-ceiling]] sorry 0 = floor (achieved)
- STEP 1287+1288 (前 arc、 4 件着手前潰し実例)
- STEP 1291 candidate: (c) Brownawell-Masser (真の追加、 Mathlib になし + n-tuple Wronskian TODO)