仕様圧縮 ・ SPEC COMPRESSION
Proof Sketch Compression TOSHNOTATION × LEAN 4 ・ SHANNON でなく仕様 OVERHEAD を畳む
Lean 4 の proof script を、 ToshNotation の 6 glyph で「証明の意図」 だけに畳む。
bit を減らすのではない — 受け手の Lean toolchain と ToshNotation 辞書を共有していれば、 glyph 列だけで proof obligation pattern が復元できる。
思弁的 / SPECULATIVE
Lean 4 proof script
ToshNotation sketch
Lean script bytes
— B
UTF-8
Glyph sketch bytes
— B
UTF-8 (multi-byte)
仕様意図 圧縮率
— ×
lines ratio
Naive byte 圧縮率
— ×
←要 honest scope
★ Honest scope (read first):
PROVEN Shannon entropy floor は破れない (情報理論既知)。
PROVEN ToshNotation glyph は UTF-8 で multi-byte (↯=3B, ⟲=3B) のため、 **naive byte 圧縮率は時に <1.0 (むしろ膨張)**。
真の節約 は: 「証明書本体を receiver の Lean toolchain に repoint」 した分の spec overhead。 これは Wadler 1990 linear types + Lucassen-Gifford 1988 effect systems + Honda 1993 session types と同 paradigm。
NOT 「Shannon 限界を超えた」 — 圧縮されているのは bit でなく 「仕様記述に必要な記号 count」。
PROVEN Shannon entropy floor は破れない (情報理論既知)。
PROVEN ToshNotation glyph は UTF-8 で multi-byte (↯=3B, ⟲=3B) のため、 **naive byte 圧縮率は時に <1.0 (むしろ膨張)**。
真の節約 は: 「証明書本体を receiver の Lean toolchain に repoint」 した分の spec overhead。 これは Wadler 1990 linear types + Lucassen-Gifford 1988 effect systems + Honda 1993 session types と同 paradigm。
NOT 「Shannon 限界を超えた」 — 圧縮されているのは bit でなく 「仕様記述に必要な記号 count」。
仕組み — どこで bit が減っていないか / どこで意図が畳まれているか
ToshNotation の ↔ ⇝ ↯ ⊥ ⊢ ⟲ はそれぞれ proof obligation の型 を担う:
- ↔ Rev (両側逆 / bijection) — `structure Rev` instance を要求
- ⇝ Approx (誤差 ≤ ε) — `Approx d f g ε` proposition
- ↯ Irrev (衝突対 witness) — `∃ a₁ a₂, a₁ ≠ a₂ ∧ f a₁ = f a₂`
- ⊥ Collapse (定値 witness) — `∃ b, ∀ a, f a = b`
- ⊢ Entail (含意, Curry-Howard) — `P → Q`
- ⟲ SelfRef (不動点 / Lawvere) — `∃ a, f a = a`
本体 (proof term) は receiver の Lean toolchain にあり、 glyph 列は どの kind の obligation を期待するか を 1 字で指す。 これは関数名が処理本体を指すのと同じ shared-codebook 機構。
★ chat-Claude 2026-06-29 articulation: 「圧縮しているのは bit でなく型注釈・仕様説明の overhead」 + 「展開先は receiver 側の codebook (model weights, Lean toolchain, mathlib)」。