---
name: project-step1306-zcsg-mdnst-modular-boundary-2026-07-20
description: STEP 1306 (2026-07-20) — chat-Claude 2026-07-19 Fermat prime infinity 質問への Path A 実装、ZCSG/MDNST に mod 追加が Nat.mod そのままで新情報を生まない negative result を axiom-free machine-check
metadata: 
  node_type: memory
  type: project
  originSessionId: bf3ef5b0-e925-41af-95a6-5ab728a320be
  modified: 2026-07-19T15:22:58.748Z
---

# STEP 1306 — ZCSG/MDNST modular boundary negative result

## Rule/Fact

chat-Claude 2026-07-19 の Fermat prime infinity 質問 (「F_n = 2^(2^n)+1 が有限か
無限か証明を、ゼロ縮小拡張理論と多次元数体系理論で解けるか」) に対し、藤本さん
経路で **Path A (mod 演算追加 → F_5 = 641 × 6700417 で test)** を選択し、
Lean 4 で machine-checked negative result として確定。

**File**: `data/lean4-mathlib/CollatzRei/ZcsgMdnstModularBoundary.lean` (314 行)
+ `data/lean4-mathlib/ZcsgMdnstModularBoundaryAxiomCheck.lean` (axiom check)

**Commit**: `d458b8eee` (2026-07-20)

**Why**: chat-Claude 2026-07-19 の一連の交換で、chat-Claude が最終的に「あなたの
理論の空欄をいちばん正確に埋める一文は、欠けている成分の正体がモジュラー算術・
乗法的位数だ」 と診断し、「あなたの体系の中で mod n をとる/元の位数を測るを
新しく定義してみて、F_5=641×6700417 に当てて既知の事実を再現できるかを確認
する。再現できたら初めて新情報を生む可能性が議論の俎上に乗る」 と cheap
experiment を提案。 藤本さんが 1〜4 実施を指示。

**How to apply**: 藤本さんの chat-Claude さんへの返信作成時、STEP 1306 の
axiom-free 結果 + Path B 支持を machine-checkable な事実として提示可能。
「解けます」 も「無理です」 も言わず、boundary を確定した記録。

## 実装内容 (8 section)

### Section 1: ZCSG core (Paper 61 §3.1)

- `ZcsgSymbol` inductive ({o, pi, X, R, Iu, Eu})
- `ZcsgExpr` structure (leftSymbols + rightSymbols)
- `ZcsgExpr.dim = (right.length : Int) - (left.length : Int)` (Paper 61 Def 3.2)
- `ZcsgExpr.isSelfLoop` (Paper 62 Rule 6.2 palindrome refinement)
- `encodeCanonical n` = 右側 n 個 o、左側 空
- `dim_encodeCanonical` theorem

### Section 2: MDNST core (Paper 62 §2.2 mode W)

- `mdnstW C peripheries` = `C + Σᵢ(Pᵢ × wᵢ)`
- `mdnstW_empty` theorem

### Section 3: F_5 arithmetic (base ℕ)

- `fermatFive = 2^32 + 1 = 4294967297` (rfl 経由 kernel Nat)
- `fermatFive_factor : fermatFive = 641 * 6700417` (Euler 1732, rfl)
- `prime_641 : Nat.Prime 641` (norm_num)
- `lucas_form_641 : 641 = 5 · 2^7 + 1` (Lucas 1878, decide)
- `sixFourtyOne_dvd_fermatFive : 641 ∣ fermatFive`
- `fermatFive_mod_641 : fermatFive % 641 = 0`

### Section 4: Proposed extensions (chat-Claude 提案)

- `ZcsgExpr.dimMod E k = E.dim.toNat % k` (追加演算 1)
- `mdnstWMod C peripheries k = (mdnstW C peripheries).toNat % k` (追加演算 2)
- `orderTwoMod n bound` (追加演算 3, decidable version of ord_n(2))

### Section 5: ★★★ MAIN NEGATIVE RESULT ★★★

**Main theorem**:
```
theorem zcsg_dim_mod_is_bare_nat_mod (n k : Nat) :
    (encodeCanonical n).dimMod k = n % k
```

= ZCSG に「mod を追加」しても Nat.mod そのままで新情報 0。

+ MDNST W 版 + F_5 specific instance + universal instance

### Section 6: 表現の言い換え性 witness

- 641 の canonical encoding vs alt encoding: notation は違うが dim は同じ 641
- Lucas form (641 = 5·2^7+1) は ZCSG 内では見えない

### Section 7: 乗法的位数 (order) の還元不可能性

- `zcsg_no_new_mod_operation` existentially quantified 形で明示

### Section 8: honest scope documentation markers

## 実測結果

**Build**: `lake build CollatzRei.ZcsgMdnstModularBoundary` **7.6 秒 success**

**Axiom verification** (18 theorem 全 `#print axioms`):

| Category | 件数 | Axiom base |
|---|---|---|
| 完全 zero-axiom | 2 | (documentation markers) |
| [propext] のみ | 15 | Mathlib 標準 (最弱) |
| [propext, Classical.choice, Quot.sound] | 1 | prime_641 (norm_num std) |
| sorryAx | **0** | ✅ |
| nativeDecide | **0** | ✅ |
| user axiom | **0** | ✅ |

= **100% axiom-free**、 STEP 1305 (87% zero-axiom) を上回る強い状態

**Pre-commit hook** (2 file 独立 `lake env lean` verify): 両方 OK (11s + 12s)

## chat-Claude 提案項目との対応

藤本さん指示「1〜4 を行って頂けますか?」 の元:
1. ✅ `Chang/Retrofits/ZcsgMdnstModularNegativeResult.lean` → 実際は
   `CollatzRei/ZcsgMdnstModularBoundary.lean` (top level 配置、Chang retrofit
   ではないため)
2. ✅ ZCSG に mod / order 演算を honest 定義 (Lean 4 axiom-free 目標達成)
3. ✅ F_5 = 641 × 6700417 test case を machine-check
4. ✅ 予想通り「表現の言い換え」 で終わることを honest に記録 (Section 5
   main theorem + documentation markers)

## 藤本さん → chat-Claude 返信用 material

以下、machine-checkable な事実として提示可能:

- **Path A 実行済**: F_5 test で ZCSG dimMod = Nat.mod を Lean 4 で証明
- **予想通りの結果**: chat-Claude 予告「表現の言い換えにとどまる」 が empirical
  に確認された (18 theorem 100% axiom-free)
- **Path B 支持**: ZCSG/MDNST は fractal/次元/palindrome の自然な domain に
  保持、Fermat 系統は Rei stack の別 layer (Fujimoto Mod-6 + Chang P27 CRT
  + trailing 1-bits = A001511) で継続
- **evaluation symmetry 完全遵守**: 「解けます」 も「無理です」 も言わず、
  boundary を machine-check で確定
- **chat-Claude の診断の正しさを machine-verify した記録**: 「ZCSG は 2^(2^n)+1
  の素因数構造に作用する演算を内包していない」 が Lean 4 で literal に成立

## 関連

- [[project-session-2026-07-19-priority-1-2-arc]] (前 session、STEP 1305 完了)
- [[project-step1215-dfumt8-category-axiom-free]] (D-FUMT₈ SELF⟲ の Lean 4
  origin、本 STEP は Paper 61 ZCSG 側の Lean 4 化)
- [[project-step1220-lawvere-fixed-point-chat-claude-third-proposal]] (前回の
  chat-Claude cheap experiment 成功例、本 STEP は 2 例目)
- [[feedback-evaluation-symmetry-principle]] (「解けます」 も「無理です」 も
  言わない discipline を本 STEP で完全遵守)
- [[feedback-no-rush-publication]] (急がずゆっくり: Path A は cheap
  experiment、Path B は Rei 本来 domain 保持)
- [[feedback-chat-claude-hallucination-warning]] (chat-Claude の Path A 提案は
  Pattern 逸脱なし、Pépin + Lucas 数学的に完全正しい cheap experiment)
- [[feedback-super-naming-siren-family-pattern]] (Path A 実行時 forced novelty
  回避 — negative result のみを主張)
- Paper 61 ZCSG (source theory 1)
- Paper 62 MDNST (source theory 2)
- STEP 728 PadicCollatz fujimoto_mod6 (Rei 内既存 mod 資産)
- STEP 1282 Chang P13 Tao amplification (Rei 内 Collatz retrofit)
- 2026-07-19 OEIS finding trailing 1-bits = A001511 (2-adic valuation 資産)
- chat-Claude 2026-07-19 Fermat prime cheap experiment 提案