ZCE Lean Level 4b + 5b decoders

Level 4 (STEP 1901) の encodeUnit に 対する decoder。 「try unary → fall back to log」 の 直列 dispatch:

def decodeUnit (tokens : List Token) : Option Unit :=
  match decodeUnary tokens with
  | some u => some (Unit.unary u)
  | none =>
    match decodeLogScale tokens with
    | some u => some (Unit.log u)
    | none => none

Cross-encoding lemma 核心 (紙上の 決定的 相違 tokens):

• decodeLogScale_encodeUnary : ∀ u, decodeLogScale (encodeUnary u) = none — encodeUnary tokens ⊂ {Token.neg, Token.o, Token.zero, Token.pct} = Token.dot 無し、 decodeLogScale が 要求する readDigitsUntilDot rest3 = (_, Token.dot :: _) は 必ず fail
• decodeUnary_encodeLogScale : ∀ u, decodeUnary (encodeLogScale u) = none — encodeLogScale の rest3 位置 は digit^b_digits ++ [Token.dot] ++ ... = Token.digit or Token.dot 有り、 decodeUnary の countLeadingO rest3 = (_, []) or (_, Token.pct :: _) は 必ず fail

Proof strategy: 2 helper lemma で decodeXxxAfterNeg の 具体形 に 対する none 主張 を 一括証明 (countLeadingO_replicate_then_zero 適用 + cases b + List.replicate_succ + rfl)、 main lemma は 4 case × cases a (0/succ) で show 経由 helper に 還元。

Roundtrip: decodeUnit_encodeUnit は cross-encoding lemma を rw で 適用 + rw [decodeLogScale_encodeLogScale] で 1 pass 完成。

Level 5a (STEP 1902) の ClsSelf inductive + encodeClsSelf に 対する 構造再帰 decoder:

def decodeClsSelf : List Token → Option ClsSelf
  | [] => some (ClsSelf.leaf [])
  | Token.digit d :: rest =>
    match decodeClsSelf rest with
    | some (ClsSelf.leaf ds) => some (ClsSelf.leaf (d :: ds))
    | some (ClsSelf.recur ds inner) => some (ClsSelf.recur (d :: ds) inner)
    | none => none
  | Token.dot :: rest =>
    match decodeClsSelf rest with
    | some inner => some (ClsSelf.recur [] inner)
    | none => none
  | _ => none

構造再帰 (Token.digit / Token.dot prefix で rest に 再帰、 rest.length は 決定的に減少)。 spec §1.1 「.n 内部に .m = SELF⟲ 埋め込み」 の 再帰的 parsing。

Roundtrip: 二重帰納

• 外側 = ClsSelf induction (leaf / recur)
• 内側 = digits induction (nil / cons)
• 各 base + step で unfold decodeClsSelf + rw [ih] の 二回転で完成

SelfLog decoder = Level 3b pattern + decodeClsSelf 統合、 rest6 の cls parsing だけ decodeClsSelf 差し替え。 Roundtrip は Level 3b の 4 case pattern + 最後 decodeClsSelf_encodeClsSelf の 一発適用。

ZCE の 内部で 版番号 axis が 2 系統 に 割れている ため、 記述時 は 常に axis prefix を 明示:

• Phase axis (spec version): v0.4 phase 2b / v0.4 phase 2c — ZceLedgerPartition / ZceShannon / ZceGibbs 系
• Level axis (implementation stack): Level 1 ~ Level 5b — ZceLevel* 系 (本 STEP 対象)

「ZCE の 2b」 と 単独記述 すると phase 2b / Level 3b / Level 4b の どれ か 曖昧化。 常に phase v0.4.2b or Level 3b の 形 で prefix 明示 (藤本さん 2026-09-09 指摘)。

• Cross-encoding lemma 対象: Level 4b は UnaryUnit ↔ LogScaleUnit の 2-way disambiguation。 SELF⟲ 有り LogScaleSelfUnit と の 統合 dispatch は 別 arc (Level 6 候補)
• decodeClsSelf は 「エンコード された」 入力 に 対して のみ 意味 が 保証。 任意 の Token list に対する generalized parser では ない (仕様として 十分)
• Novelty 主張なし = streaming compression + inductive sum type + inductive recursive type + Mathlib standard axioms、 特に SELF⟲ 部分 は 標準 recursive type parsing pattern

• STEP 1904 — ZCE Lean full-stack (Level 1-5a) 統合 site
• STEP 1905 notepad 詳細
• Commit 56cb3509e (STEP 1905)