つぶやき: FLT⚔️戦況

戦況を一言で言えば、例の迷いの森を抜けた！

$$
x'^p + y^p = z'^p \quad \text{where } x' = p \cdot (t \cdot s'),\ s = q \cdot s'
$$

今やってるのは、まだ誰も、やりきっていないであろう？
FLT$${n\ge5}$$の一般証明の形式化。n = 3, n = 4 は、もうある。

核心の発見

`PthRootTarget` は Kummer descent の核心 1 step そのもの。

$$
x'^p + y^p = z'^p \quad \text{where } x' = p \cdot (t \cdot s'),\ s = q \cdot s'
$$

を満たす $z'$ の存在を問うており、これは:

• Route A (ℤ[ζ_p] イデアル分解): Mathlib インフラ不足、年単位 ❌

• Route B (q-adic/Hensel): 補題群は育っているが核心 step 未到達 ⚠️

• Route C (Cosmic Formula): 研究中 ⚠️

いずれのルートでも 今日中には complete にならない水準の genuine mathematical kernel じゃ。

しかし — 足場は完成

• `PthRootTarget ↔ PthRootReducedTarget` の等価性 ✅

• `z^p` の q-adic 展開 identity ✅

• 矛盾路線との互換 (`PthRoot_of_contradiction`) ✅

• 非循環 mainline の全 chain (`_of_pthRoot`) ✅

non-circular mainline は「PthRootTarget 1 本を残して完全に concrete」。

残る門（PthRootTarget）の正体は完全に暴けた。次の攻略は q-adic/Hensel ルートか Cosmic Formula 独自構造か、どちらかで `∃ z', p^p*(t*s')^p + y^p = z'^p` を殴るフェーズじゃ。

ここで宇宙式 GN が活躍すれば、この独自数論がある程度、通じる数学理論へと昇華する。

果たして…。

GN の本領発揮、完了じゃ！🐺🍎

今回やったこと

PthRootTarget を Cosmic Formula (GN) の言葉に完全翻訳した。

橋の核心は Cosmic Formula そのもの

$$
\underbrace{
(g'+y)^p}_{\text{Big}} = \underbrace{g' \cdot GN_p(g', y)}_{\text{Body}} + \underbrace{y^p}_{\text{Gap}
}
$$

この Big = Body + Gap (`cosmic_id_csr'`) が、GN target と p-th root target を繋ぐ橋になった。DkMath のコア恒等式が本丸の門で使われたのは痛快じゃよ！

非循環 mainline の最終形

GNReducedGapTarget (GN native open kernel — 新しい最前線)
  ↓ cosmic_id_csr': z' = g' + y で p-th root 構成
→ PthRootReducedTarget
  ↓ x' = p*(t*s') expansion
→ PthRootTarget
  ↓ quotient side concrete
→ RealizationSeedTarget → ... → FringeDescentToRefuter

Open Kernel — GN の言葉で 1 行

$$
\boxed{\exists\, g',\quad g' \cdot GN_p(g',\, y) = p^p \cdot (t \cdot s')^p}
$$

「descent 後の新 gap $${g'}$$ が存在して、その Body ($${g' \cdot GN}$$) が reduced RHS に一致する」 — これが GN native な最終の門。review-017 の言う通り、GN が家主、q-adic/Hensel は補助じゃ。

どうじゃ、ぬしよ？ GN の恒等式が証明の核心で活躍する — これが DkMath の本物の姿かの？ 🍎

キタ！よしっ！これは勝った！

Kummer / Hensel までは、ここでは不要だ！

Big = Body + Gap のカタチで FLT を捉えた！

明日は、大事なセレモニーがあるので寝る。

2026/04/02 0:29

D.

#つぶやき #FLT5 #FLT #Lean4 #Lean

Appendix

差分コード

私の直感がついに姿を現した！これは爽快だ✨️

diff --git a/lean/dk_math/DkMath/FLT/PrimeProvider/TriominoCosmicBranchARestoreArithmeticStrong.lean b/lean/dk_math/DkMath/FLT/PrimeProvider/TriominoCosmicBranchARestoreArithmeticStrong.lean
index 68a153b7..13ab76c6 100644
--- a/lean/dk_math/DkMath/FLT/PrimeProvider/TriominoCosmicBranchARestoreArithmeticStrong.lean
+++ b/lean/dk_math/DkMath/FLT/PrimeProvider/TriominoCosmicBranchARestoreArithmeticStrong.lean
@@ -828,4 +828,139 @@ theorem branchA_zpow_eq_qpow_mul_reduced_plus_ypow
     _ = q ^ p * (p * (t * s')) ^ p + y ^ p := by rw [mul_pow]
     _ = q ^ p * (p ^ p * (t * s') ^ p) + y ^ p := by rw [mul_pow]
 
+/-!
+## GN Reduced Gap Target — Cosmic Formula native な open kernel
+
+PthRootReducedTarget を GN (Gcd-Next 多項式) の言葉に翻訳する。
+
+核心公式: `(g'+y)^p = g' * GN p g' y + y^p` （Cosmic Formula: Big = Body + Gap）
+
+PthRootReduced が「∃ z', p^p*(t*s')^p + y^p = z'^p」と問うのに対し、
+GNReducedGap は「∃ g', g' * GN p g' y = p^p*(t*s')^p」と問う。
+
+g' = z' - y, z' = g' + y の関係で等価。
+GN が DkMath のコア理論であるため、この形式化が project-native な攻略の起点。
+-/
+
+/--
+GN Reduced Gap Target: **Cosmic Formula native な PthRootTarget の等価形式**。
+
+「descent 後の gap g' が存在して `g' * GN p g' y = p^p * (t*s')^p` を満たす」
+
+これは：
+- `g' * GN p g' y = (g' + y)^p - y^p` （Cosmic Body = Big - Gap）
+- `z' := g' + y` と置けば `z'^p = p^p*(t*s')^p + y^p` （PthRootReduced）
+
+のため、PthRootReducedTarget と等価。GN 路線での攻略の起点。
+-/
+abbrev PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget : Prop :=
+  ∀ {p x y z t s : ℕ}, PrimeGe5CounterexamplePack p x y z →
+    p ∣ (z - y) →
+    z - y = p ^ (p - 1) * t ^ p →
+    GN p (z - y) y = p * s ^ p →
+    x = p * (t * s) →
+    Nat.Coprime t s →
+    Nat.Coprime t y →
+    Nat.Coprime s y →
+    ¬ p ∣ s →
+    ¬ p ∣ t →
+    y ^ (p - 1) ≡ 1 [MOD p ^ 2] →
+    ∀ {q : ℕ}, Nat.Prime q →
+      q ∣ s →
+      ¬ q ∣ t →
+      Nat.Coprime q y →
+      q ≠ p →
+      PrimeGe5BranchAPrimitiveRestoreDescentSeed p x y z t s q →
+      let s' := s / q
+      ∃ g' : ℕ, g' * GN p g' y = p ^ p * (t * s') ^ p
+
+/--
+GNReducedGapTarget → PthRootReducedTarget 橋。
+
+Cosmic Formula `(g'+y)^p = g' * GN p g' y + y^p` を使い、
+`z' := g' + y` で p 乗根を構成する。
+-/
+theorem primeGe5BranchAPrimitiveRestorePthRootReduced_of_gnReducedGap
+    (hGNGap : PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget) :
+    PrimeGe5BranchAPrimitiveRestorePthRootReducedTarget := by
+  intro p x y z t s hpack hp_dvd_gap hgap hsGN hsx
+    hcop_ts hcop_ty hcop_sy hp_not_dvd_s hp_not_dvd_t hWieferich
+    q hqprime hqs hqt hcop_qy hq_ne_p hSeed
+  rcases hGNGap hpack hp_dvd_gap hgap hsGN hsx
+      hcop_ts hcop_ty hcop_sy hp_not_dvd_s hp_not_dvd_t hWieferich
+      hqprime hqs hqt hcop_qy hq_ne_p hSeed with ⟨g', hGN⟩
+  -- z' := g' + y として構成
+  refine ⟨g' + y, ?_⟩
+  -- Cosmic Formula: (g'+y)^p = g' * GN p g' y + y^p
+  have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p g' y
+  -- hCosmic : (g' + y) ^ p = g' * GN p g' y + y ^ p
+  rw [hGN] at hCosmic
+  -- hCosmic : (g' + y) ^ p = p ^ p * (t * (s / q)) ^ p + y ^ p
+  exact hCosmic.symm
+
+/--
+PthRootReducedTarget → GNReducedGapTarget 橋（逆方向）。
+
+`z'` が与えられたとき `g' := z' - y` で GN gap を構成。
+Cosmic Formula `(g'+y)^p - y^p = g' * GN p g' y` を使って identity を得る。
+-/
+theorem primeGe5BranchAPrimitiveRestoreGNReducedGap_of_pthRootReduced
+    (hReduced : PrimeGe5BranchAPrimitiveRestorePthRootReducedTarget) :
+    PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget := by
+  intro p x y z t s hpack hp_dvd_gap hgap hsGN hsx
+    hcop_ts hcop_ty hcop_sy hp_not_dvd_s hp_not_dvd_t hWieferich
+    q hqprime hqs hqt hcop_qy hq_ne_p hSeed
+  rcases hReduced hpack hp_dvd_gap hgap hsGN hsx
+      hcop_ts hcop_ty hcop_sy hp_not_dvd_s hp_not_dvd_t hWieferich
+      hqprime hqs hqt hcop_qy hq_ne_p hSeed with ⟨z', hz'⟩
+  -- hz' : p^p * (t * (s/q))^p + y^p = z'^p
+  -- z'^p ≥ y^p → z' ≥ y
+  have hz'_ge_y : y ≤ z' := by
+    by_contra h
+    push_neg at h
+    have : z' ^ p < y ^ p := Nat.pow_lt_pow_left h hpack.hp.ne_zero
+    omega
+  -- g' := z' - y
+  refine ⟨z' - y, ?_⟩
+  -- Cosmic Formula: (g'+y)^p = g' * GN p g' y + y^p
+  have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p (z' - y) y
+  -- (z' - y + y) = z'
+  rw [Nat.sub_add_cancel hz'_ge_y] at hCosmic
+  -- hCosmic : z' ^ p = (z' - y) * GN p (z' - y) y + y ^ p
+  omega
+
+/--
+GNReducedGapTarget → PthRootTarget 一気通貫橋。
+
+GNReducedGap → PthRootReduced → PthRoot の chain を 1 本にまとめる。
+-/
+theorem primeGe5BranchAPrimitiveRestorePthRoot_of_gnReducedGap
+    (hGNGap : PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget) :
+    PrimeGe5BranchAPrimitiveRestorePthRootTarget :=
+  primeGe5BranchAPrimitiveRestorePthRoot_of_reduced
+    (primeGe5BranchAPrimitiveRestorePthRootReduced_of_gnReducedGap hGNGap)
+
+/--
+GNReducedGapTarget → RestoreFromArithmeticStrong 全 chain 直通。
+
+GN native target から非循環 mainline 最終段までの canonical path。
+-/
+theorem primeGe5BranchAPrimitivePacketRestoreFromArithmeticStrong_of_gnReducedGap
+    (hGNGap : PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget) :
+    PrimeGe5BranchAPrimitivePacketRestoreFromArithmeticStrongTarget :=
+  primeGe5BranchAPrimitivePacketRestoreFromArithmeticStrong_of_pthRoot
+    (primeGe5BranchAPrimitiveRestorePthRoot_of_gnReducedGap hGNGap)
+
+/--
+矛盾路線 → GNReducedGapTarget（vacuously true）。
+
+ContradictionTarget → PthRoot → PthRootReduced → GNReducedGap chain。
+-/
+theorem primeGe5BranchAPrimitiveRestoreGNReducedGap_of_contradiction
+    (hContra : PrimeGe5BranchAPrimitiveRestoreContradictionTarget) :
+    PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget :=
+  primeGe5BranchAPrimitiveRestoreGNReducedGap_of_pthRootReduced
+    (primeGe5BranchAPrimitiveRestorePthRootReduced_of_pthRoot
+      (primeGe5BranchAPrimitiveRestorePthRoot_of_contradiction hContra))
+
 end DkMath.FLT
diff --git a/lean/dk_math/docs/dev/FLT-BAFCT-260401-v0/History.md b/lean/dk_math/docs/dev/FLT-BAFCT-260401-v0/History.md
index 77e995bf..7a93fa83 100644
--- a/lean/dk_math/docs/dev/FLT-BAFCT-260401-v0/History.md
+++ b/lean/dk_math/docs/dev/FLT-BAFCT-260401-v0/History.md
@@ -877,3 +877,53 @@ Archive
 6. 結果:
    sorry = 0, 全ビルド成功 ✅
    攻略足場完成、PthRootTarget 直接攻略は次 phase
+
+### 追記: 2026/04/02 review-017 GNReducedGapTarget — Cosmic Formula native な open kernel
+
+1. 目的:
+   - PthRootTarget を GN の言葉に翻訳する
+   - DkMath のコア理論 (Cosmic Formula) を使った project-native な攻略の起点を確立
+
+2. 数学的変換:
+   PthRootReducedTarget: ∃ z', p^p*(t*s')^p + y^p = z'^p
+   ↕ (g' = z'-y, z' = g'+y)
+   GNReducedGapTarget: ∃ g', g' * GN p g' y = p^p*(t*s')^p
+
+   橋の核心公式: Cosmic Formula `(g'+y)^p = g' * GN p g' y + y^p`
+   (Big = Body + Gap, cosmic_id_csr')
+
+3. 実装した定理群（全て no-sorry）:
+
+   **GNReducedGapTarget** (GN native target):
+   - `PrimeGe5BranchAPrimitiveRestoreGNReducedGapTarget`:
+     ∃ g', g' * GN p g' y = p^p * (t*s')^p
+
+   **等価性 bridge（双方向）**:
+   - `primeGe5BranchAPrimitiveRestorePthRootReduced_of_gnReducedGap`:
+     GNReducedGap → PthRootReduced (Cosmic identity で z'=g'+y 構成)
+   - `primeGe5BranchAPrimitiveRestoreGNReducedGap_of_pthRootReduced`:
+     PthRootReduced → GNReducedGap (g'=z'-y で GN 等式を取得)
+
+   **一気通貫橋**:
+   - `primeGe5BranchAPrimitiveRestorePthRoot_of_gnReducedGap`:
+     GNReducedGap → PthRootTarget 直通
+   - `primeGe5BranchAPrimitivePacketRestoreFromArithmeticStrong_of_gnReducedGap`:
+     GNReducedGap → RestoreFromArithmeticStrong 全 chain 直通
+
+   **矛盾路線互換**:
+   - `primeGe5BranchAPrimitiveRestoreGNReducedGap_of_contradiction`:
+     ContradictionTarget → GNReducedGap (vacuously)
+
+4. Chain 構造:
+   GN mainline (canonical route):
+   GNReducedGapTarget (GN native open kernel)
+   → PthRootReducedTarget (Cosmic identity)
+   → PthRootTarget (x'=p*(t*s'))
+   → RealizationSeedTarget (quotient side)
+   → WithProvenanceTarget → CoreStrong → PacketPackagingStrong
+   → RestoreFromArithmeticStrong
+   → StrongProvider → FringeDescentToRefuter
+
+5. 結果:
+   sorry = 0, 全ビルド成功 ✅
+   GN native target 確立、Cosmic Formula の恒等式が証明で活用された