Inter-universal geometryとABC予想(シン応援スレ) 92

Inter-universal geometryとABC予想(シン応援スレ) 92 (376ﾚｽ)
上下前次 1-新
通常表示 512ﾊﾞｲﾄ分割ﾚｽ栞

243: １３２人目の素数さん [] 2026/07/17(金) 20:06:51.79 ID:zMIRi+X7

つづき

なお、6で我々は(A)(B)(C)のいずれかが供給されればLEANの形式化と接続して機械検証すると言ってるが、俺は中身はほとんど理解してないので、これは我々と言うよりは純粋にFable5の言い分となる
もし7月17日にLANAプロジェクトでGithubが公開されなければ公開するかもしれんが、Fable5が利用クレジットでの利用じゃなく、再度月額プランのみで使えるようになったらでないとFable5でやるつもりはない他のモデルではやるかもしれん

ちなみに3.11までは特に問題なくLEAN化は成功して、3.11を認めた上でのCor3.12の証明も機械検証は難なく通った
問題はそれがトートロジー的閉ループを構築していることに帰着すること
しかしそれは望月が論文内で言及していて問題ないとする部分でもある

4要請の前の0〜3は以下
0. 一行要旨
IUT 4論文の主張のうち、機械検証(Lean 4)で正しさを確認できた部分と確認できなかった部分の境界が、 [IUTchIV] Thm 1.10 証明 Step (v) の一入力 —— λ := ord(q^{j²}) を受信側正規化の体積計算に適用してよいこと —— に正確に一致した。この入力の導出(定義的措定ではなく)の所在をご教示いただきたい。

1. 背景: 何を検証済みで、何を疑っていないか
我々は IUT 4論文([IUTchI–IV])+星裕一郎『宇宙際 Teichmüller 理論入門』を底本に、 Lean 4 + Mathlib による形式化(67モジュール、sorry/axiom 0、標準公理のみ)を行った。 以下は証明として再構成でき、正しさを確認した部分である(疑義はない):

[IUTchIV] Prop 1.1–1.4 の台帳計算: different の上界(不分岐 d=0、順分岐 d=e−1、 暴分岐 d ≤ e−1+e·v_p(e))、対数殻の半径定数 a, b、殻の包含と体積公式。 (順分岐上界など、Mathlib に存在しない定量評価は新規に証明した。)
p 進 exp/log の解析理論: 収束・加法性・ノルム保存(等長性)・全単射性 (Newton 反復による全射性)。すなわち log-link の単数部 (O^×μ) は体積を保存する —— [IUTchIII] Prop 3.9 の体積両立性と整合する。
Kummer 理論の機構: 両立的巾根系・Kummer 類のコサイクル律・well-definedness、 円分剛性関連の非自明性、「1 の巾根 ↦ 0(不定性なし)」条項([IUTchIII] Thm 3.11 (ii))。
containment 側の導出([IUTchIII] Cor 3.12 証明 Step (xi-d)–(xi-f)): q-標対象の像が可能な像の包に含まれることから −|log(q)| ≤ −|log(Θ)| が 「follows formally」に従うこと。ℝ の同一視を用いずに検証した。
[IUTchIV] Thm 1.10 の最終算術: C_Θ ≥ −1 から高さ不等式への初等的演繹、 および Thm 1.10 → Cor 2.2 → Szpiro/abc 型不等式の連鎖。

つづく

http://rio2016.5ch.io/test/read.cgi/math/1781308317/243

上下前次 1-新書関写板覧索設栞歴

あと 133 ﾚｽあります
ｽﾚ情報赤ﾚｽ抽出画像ﾚｽ抽出歴の未読ｽﾚ AAｻﾑﾈｲﾙ

ぬこの手ぬこTOP 0.360s*