つぶやき: FLT⚔️戦況 #2

#FLT #一般化証明 #形式化 のための #無限降下法 の種を探した結果。
「 #Kummer理論 」と「 #宇宙式 」を繋ぐことになってしまった。

結局、芯の部分を探り当てたら…

`2m-pure` という呼称した芯が見つかって、それは結果的に
`DkMath.CosmicFormulaBinom.cosmic_id_csr'` つまり GN核 構造と同値。
という定理の証明がビルドを通って✅️しまった。

/--
`2m-pure` の GN 等式と descent existence の同値性。

Cosmic Formula 恒等式 `(g' + y)^p = g' * GN(p, g', y) + y^p` により、
`g' * GN(p, g', y) = (x/q)^p` ↔ `(g' + y)^p = (x/q)^p + y^p`。

つまり `2m-pure` は **descent existence そのもの** である。
-/
theorem descentExistence_iff_gnReduction (p g' y xq : ℕ) :
    g' * GN p g' y = xq ^ p ↔ (g' + y) ^ p = xq ^ p + y ^ p := by
  constructor
  · intro h
    have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p g' y
    omega
  · intro h
    have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p g' y
    omega

ここに書いてあるだけの内容ならば、通って当然な記述だけだけど。
何やらいろんな前提を見直し解釈すれば、こういう事だろうという定理か？

これをさらに深堀りしたら、#Kummer理論 の形式化をする必要はめになった。

#Mathlib に Kummer の定理が形式化されているならば、それを使えば済む。
無ければ、書き上げて最終定理に繋げる必要がある。

という感じであろうか。

ABC予想 でも、結局なんとか理論の形式化をせざるを得なくて、それを待つことにして止めた経緯がある。 FLT もそんな感じだなあ。

証明を形式化100%とするのが主体ではなく、どういう原理で成り立たないのか、成り立つのか。という根本原因をロジカルに探るのが目的なので、既存理論をそのまま形式化するのであれば、あまり面白みがなく、何と繋がって同値なのかを見られることが主体。そこに恒等式の宇宙式が出てくると、私的には非常に面白い話になる。

だけど、宇宙式って飛び飛びな離散構造でなく連続化された構造なので、離散を説明するのは不得手なのよねぇ…。だから、別の観点の理論で説明せざるを得ない。

$$
(P+u)^d
$$

この $${u > 0 \in \R}$$ が連続になって可変なので、固定視点で得られる定理群を構成しないと説明しにくいという事かな。Gcd 補題だけでは足りない。

Kummer 着手前に、宇宙式定理を増やしておくか…。✍️

2026/04/05 17:28

D.

Appendix

2m-pure

/-!
### §20.1. `2m-global` の仮定監査と `2m-pure` の切り出し

`2m-global` の結論 `∃ g', g' · GN(p, g', y) = (x/q)^p` は
witness `R : ZMod (q^p)` に **依存しない**。
右辺 `(x/q)^p` は pack + `q ∣ x` だけで決まり、
左辺 `GN p g' y` も `g'` と `y` だけで決まる。

したがって、witness R の仮定を完全に除去した `2m-pure` を定義できる。
`2m-pure → 2m-global` は自明に成り立つ（R を受け取って捨てるだけ）。
逆方向 `2m-global → 2m-pure` は **一般には成立しない**。
`2m-pure` は `2m-global` より **真に強い** 主張。

### §20.1.1. `2m-global` と `2m-pure` の gap の正体

分析の結果、`2m-global → 2m-pure` が成立しない正確な理由が判明した:

`R = z · y⁻¹ mod q^p` とする。pack の `Coprime x y` と `q ∣ x` から `gcd(y,q) = 1` が出て、
y は `ZMod (q^p)` で可逆なので R は一意に定まる。`z ≡ R·y (mod q^p)` は定義から成立。
しかし `Φ_p(R) = 0 (mod q^p)` が成り立つかは q と gap の関係に依存する:

- **`q ∤ gap`** (= `q ∤ (z-y)`): R ≢ 1 (mod q)。
  `R^p ≡ 1 (mod q^p)` と `R - 1` が `ZMod q` で可逆であることから、
  `Φ_p(R) ≡ 0 (mod q^p)` が **自動的に成立**。
  このケースで `2m-global` は非 vacuous な情報を与える。

- **`q | gap` かつ `q ≠ p`**: R ≡ 1 (mod q)。
  `Φ_p(R) ≡ Φ_p(1) = p (mod q)` で、`q ≠ p` なら `Φ_p(R) ≢ 0 (mod q)`。
  よって `Φ_p(R) = 0 (mod q^p)` を満たす R が **存在しない**。
  `2m-global` は vacuously true になり、何の情報も与えない。

- **`q = p` かつ `p | gap`**: `Φ_p(R) ≡ 0 (mod p)` だが `mod p^p` かは非自明
  （Wieferich/Kummer 理論に依存）。

重要: DescentChain の actual usage path では、q は `CyclotomicExistenceTarget` から来る
**distinguished prime** であり、`¬ q ∣ (z-y)` が保証される（= 第1ケース）。
したがって **actual chain 上では `2m-global` の witness 条件は自動的に充足される**。

**結論**: `2m-pure` と `2m-global` の formal な gap は `q | gap` ケースで生じるが、
このケースは DescentChain 本線では起きない。`2m-global` を攻める A ルートが正しい。
-/

/--
2m-pure: witness R を完全に除去した最鋭 target。

pack + `Prime q` + `q ∣ x` だけから reduced gap `g'` の存在を要求する。
`2m-global` より **厳密に強い**（witness R を仮定しない）。
`2m-pure → 2m-global` は自明だが、逆は一般には不成立。
-/
abbrev PrimeGe5BranchAPrimitiveQAdicGapReductionPureTarget : Prop :=
  ∀ {p x y z : ℕ}, PrimeGe5CounterexamplePack p x y z →
    ∀ {q : ℕ}, Nat.Prime q →
      q ∣ x →
      ∃ g' : ℕ, g' * GN p g' y = (x / q) ^ p

/--
`2m-pure` の GN 等式と descent existence の同値性。

Cosmic Formula 恒等式 `(g' + y)^p = g' * GN(p, g', y) + y^p` により、
`g' * GN(p, g', y) = (x/q)^p` ↔ `(g' + y)^p = (x/q)^p + y^p`。

つまり `2m-pure` は **descent existence そのもの** である。
-/
theorem descentExistence_iff_gnReduction (p g' y xq : ℕ) :
    g' * GN p g' y = xq ^ p ↔ (g' + y) ^ p = xq ^ p + y ^ p := by
  constructor
  · intro h
    have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p g' y
    omega
  · intro h
    have hCosmic := DkMath.CosmicFormulaBinom.cosmic_id_csr' (R := ℕ) p g' y
    omega

/-- `2m-pure` → `2m-global`（witness を受け取って捨てるだけ）。 -/
theorem qAdicGapReductionGlobal_of_pure
    (hPure : PrimeGe5BranchAPrimitiveQAdicGapReductionPureTarget) :
    PrimeGe5BranchAPrimitiveQAdicGapReductionGlobalTarget := by
  intro p x y z hpack q hq hq_dvd_x R _hphi _hzRy
  exact hPure hpack hq hq_dvd_x

/-
`2m-global` → `2m-pure`（結論が R-free なので witness 仮定は不要）。

注意: この方向は **一般には成立しない**。
`2m-global` は「witness R が与えられたとき `g'` が存在する」と言い、
`2m-pure` は「witness R なしに `g'` が存在する」と言う。
`2m-pure` は `2m-global` より **真に強い** 主張。

ただし `2m-local` (concrete) が witness R を構成できる文脈では
`2m-global` から `2m-pure` を得ることは可能。
その経路は `pthRootCore_of_qAdicGapReductionGlobal` を参照。
-/