ZCE (Zero-Center Encoding) 完全形式化 stack — Level 1-5a、 全 sorry 0、 axiom-free (propext + optional Quot.sound)
chat-Claude ↔ 藤本さん ↔ Rei-AIOS Claude Code の 12 STEP arc で 到達した ZCE spec §1 grammar の Lean 4 完全形式化。 unary → log-scale → full Unit inductive → ClassSuffix SELF⟲ inductive の 7 段階、 全 sorry 排除、 主定理 全て axiom-free (Mathlib propext のみ)。 chat-Claude と 未来 Claude が いつでも 参照できる 統合 index。
/ What has been achieved, in numbers
Lean files
Level 1 → Level 5a (structural + decoder)
Total declarations verified
via #print axioms (types, encoders, predicates, witnesses)
Sorry count
全 file、 全 declaration
Main theorems axioms
only、 concrete list-level roundtrip = [propext]
/ File-by-file map with axiom_check summary
| Level | File | Content | Sorry | Main axiom | STEP |
|---|---|---|---|---|---|
| 1 | ZceFullFormalization.lean | UnaryUnit + encodeUnary + 6 §14 predicate defs + basic witnesses (A1, A3, B2, B3, B1 negation) | 0 | [propext] | 1893, 1897 |
| 2 | …Level2.lean | countLeadingO + decodeUnary + aux lemmas + decodeUnary_encodeUnary roundtrip + A2_holds | 0 | [propext] | 1895, 1896, 1897 |
| 3 | ZceLevel3LogScale.lean | LogScaleUnit + encodeLogScale + 6 predicate + basic witnesses (log-scale variant) | 0 | [propext] | 1898 |
| 3b | …Decoder.lean | readDigitsUntilDot + decodeLogScale + decodeLogScale_encodeLogScale roundtrip + A2_holds_log | 0 | [propext] | 1899 |
| 4 | ZceLevel4FullUnit.lean | Unit inductive (unary | log) + encodeUnit dispatch + 6 predicate + basic witnesses | 0 | [propext] | 1901 |
| 5a | …Inductive.lean | ClsSelf inductive (recursive SELF⟲) + depth + encodeClsSelf + LogScaleSelfUnit + 非trivial B3 predicate + twin witness | 0 | [propext] | 1902 |
| 4b | (未実装) | Unit dispatch decoder + cross-encoding lemmas + roundtrip + A2 (unary vs log の 判別) | pending | — | go 待ち |
| 5b | (未実装) | SELF⟲ recursive decoder + roundtrip + A2 (ClsSelf の 再帰 parse) | pending | — | go 待ち |
/ Concrete list-level = propext / stream-level = funext 経由 Quot.sound
chat-Claude 第 4 review (STEP 1896) の 予測 「concrete list-level roundtrip は Quot.sound 不要、 stream-level は funext 経由 Quot.sound」 が Level 2 / Level 3b / Level 4 / Level 5a の 全 sibling で 完全実証:
| Layer | Axiom profile | 理由 |
|---|---|---|
| Type + encoder + predicate defs (~30 items) | 0 axioms | 純 constructive、 axiom 依存 なし |
| List-level 主定理 (roundtrip、 injectivity 等) | [propext] | Mathlib fundamental、 Classical.choice + Quot.sound 除去済 |
| 非trivial 具体 witnesses (A1、 B3 conditional 等) | [propext] or 0 axioms | mem_append chain + explicit witness で 到達 |
| Length / count arguments (A3、 B2) | [propext, Quot.sound] | List.length + omega / count reasoning が funext 系 pull |
| Stream-level 関数等号 form (`= s`) | [propext, Quot.sound] | funext 経由、 pointwise variant で propext のみ に 削減可 |
| Stream-level pointwise form (`∀ n, ... = s n`) | [propext] | chat-Claude 提案適用 (STEP 1897)、 funext 不要 |
/ Decoder restructure + aux lemmas + simp with single-pass reduction
Level 2 (STEP 1896) で 確立した pattern が Level 3b / Level 4 / Level 5a に 直接転用 され、 各 Level 1 iteration で 完成:
-- Decoder restructure (外層 pattern match on Token.neg + body helper)
def decodeUnary : List Token → Option UnaryUnit
| Token.neg :: tokens => decodeUnaryAfterNeg tokens true
| tokens => decodeUnaryAfterNeg tokens false
-- Aux lemmas for specific encoded shapes
lemma countLeadingO_replicate_then_zero (a : ℕ) (rest : List Token) :
countLeadingO (List.replicate a Token.o ++ Token.zero :: rest)
= (a, Token.zero :: rest) := by
induction a with
| zero => rfl
| succ k ih => rw [List.replicate_succ, List.cons_append]; ...; rw [ih]
-- Roundtrip proof (uniform pattern across all Levels)
theorem decodeUnary_encodeUnary (u : UnaryUnit) :
decodeUnary (encodeUnary u) = some u := by
obtain ⟨a, b, neg, cls⟩ := u
cases neg <;> cases cls -- 4 cases
case false.none =>
unfold encodeUnary; simp only [List.append_nil]
rw [List.append_assoc]
cases a with
| zero => simp [decodeUnary, decodeUnaryAfterNeg, countLeadingO, aux_lemmas]
| succ k => rw [...]; simp [decodeUnary, decodeUnaryAfterNeg, aux_lemmas]
...
/ How chat-Claude reviews catalyzed each iteration
| Round | Turn | 指摘 | Rei 反映 |
|---|---|---|---|
| 1 | chat-Claude 初期 | coalgebra 3 点 (roundtrip / semantics / equivalence) load-bearing 提案 | pre-gate 実施 → 撤回確定 (STEP 1883) |
| 2 | chat-Claude 第 4 turn | attribution 訂正、 節分割 discipline、 未検証引用 asymmetric cost、 別 STEP 優先順、 tautology 2-gate、 STEP 事務 | STEP 1884 site + STEP 1887 2-gate + STEP 1889 別立て site |
| 3 | chat-Claude 第 4 review (Level 2) | .induct 提案、 Quot.sound = funext 由来 予測、 sorry 期限化 | STEP 1896 → 1897 で Quot.sound 除去 + sorry 全排除 + 「予測 1 中 1、 discipline 1、 主提案 1 不発」 attribution 訂正 |
| 4 | chat-Claude 第 5 review | 「3 予測完全実証」 は 過剰主張、 A2/B1 「撤回側」 診断 | STEP 1897 で attribution 訂正 + A2/B1 は 「proveable」 実測で 診断 部分訂正 (chat-Claude 側 の 対称的 corrigendum) |
| 5 | — | (なし、 Level 3-5a は chat-Claude review 未受領で 私 単独設計) | Level 3/4/5a は 前 4 round 累積 discipline で self-consistent 起草 |
/ How to build + verify locally
# Clone + build
git clone https://github.com/fc0web/rei-aios.git
cd rei-aios/data/lean4-mathlib
lake update # first time only (fetches Mathlib v4.27.0)
# Build all ZCE files
lake build CollatzRei.ZceFullFormalization
lake build CollatzRei.ZceFullFormalizationLevel2
lake build CollatzRei.ZceLevel3LogScale
lake build CollatzRei.ZceLevel3bLogScaleDecoder
lake build CollatzRei.ZceLevel4FullUnit
lake build CollatzRei.ZceLevel5ClassSuffixInductive
# Run axiom_check (each returns per-declaration axiom list)
lake env lean ZceFullFormalizationAxiomCheck.lean
lake env lean ZceFullFormalizationLevel2AxiomCheck.lean
lake env lean ZceLevel3LogScaleAxiomCheck.lean
lake env lean ZceLevel3bLogScaleDecoderAxiomCheck.lean
lake env lean ZceLevel4FullUnitAxiomCheck.lean
lake env lean ZceLevel5ClassSuffixInductiveAxiomCheck.lean
Toolchain: Lean 4.27.0 + Mathlib v4.27.0 (defined in lean-toolchain and lakefile.toml). Windows / Linux / macOS 全対応。
/ Spec side + non-Lean formalization
Honest scope