STEP 1731 — ransbench arc
枠拡張の決着実験 + 反転実験 + Lean 4 rANS 検証
2026-09-03 / 2026-09-04 JST · worktree step1731-ransbench_arc · rei-aios-8a tab
Executive summary
- 枠拡張実験: D-FUMT₈ の 8 値枠は実運用上足枷だった。sse_lex64 (bigram of char classes) が全 model 中最強、sse_flat 比 −0.030 bpb (Python) / −0.048 bpb (Prose) = 従来 sse 差 (−0.002) の 15-24 倍。
- 反転実験: 貪欲 K=8 分割 = full 256-partition 上限の 96.6% (Python) / 89.1% (Prose) — 貪欲は真の K-partition 最適の下界。D-FUMT₈ lex_class の貪欲比達成率 = 87% (Python) / 26% (Prose) — これは上限値、真の最適比は以下。ARI = 0.57 (Python) / 0.056 (Prose)。因果主張 (「非 ASCII が原因」) は保留、追加 corpus で交絡分離が必要 (§4.5)。
- Lean 4 rANS: 4 定理 (round-trip / slot 域 / state 上限 / 32-bit fit) を Mathlib 標準 3 axiom [propext, Classical.choice, Quot.sound] のみで構成。main .lake env の lake env lean で #print axioms verify 完了 → CollatzRei 3,542 axiom-free 群に合流可。
- 候補 3 (indent×tag): Probe I(state; bit) = 0.098 (Python) / 0.0001 (Prose) → 事前予想通り。両 corpus で最下位。
1. 出発点 (arc の再確認)
2026-09-02 に別 tab で構築された ransbench (rANS 32-bit + 整数のみ SSE + 予測器差替 harness) の 2 ラウンド実験結果は明確だった:
sse − sse_flat = 0.002 bpb。つまり現行 D-FUMT₈ プレースホルダの d8_state() は実質ゼロ寄与。
残る問いは 1 つ: 8 値という枠は足枷か?
藤本さんの sketch した plan:
- 枠拡張 sse_lex{16,64,256} vs sse_hash{16,64,256} — 決着
- Lean 4 rANS 検証 — 論文骨格
- 反転実験: 貪欲 8 分割 vs D-FUMT₈ 距離 — 本命
- 候補 3 (indent×tag) — ついで
- 手設計第 3+ ラウンド — やめる
此方 tab で 5 項目全引き受け、単一 worktree で並行実行。
2. probe.py — 秒 order の事前 screener
符号化前に predictor の 状態占有率と I(state; next_bit) を実測。Python 256KiB / prose 256KiB を各 10 秒程度で処理。
Probe: Python source 256KiB
| model | declared | effective | I(bit) | gain/bpb* |
|---|
| sse | 8 | 3.38 | 0.0203 | 0.16 |
| sse_lex | 8 | 3.41 | 0.0326 | 0.26 |
| sse_lex16 | 16 | 4.65 | 0.0379 | 0.30 |
| sse_lex64 | 64 | 8.42 | 0.0582 | 0.47 |
| sse_lex256 | 256 | 25.85 | 0.0396 | 0.32 |
| sse_hash8 | 8 | 6.46 | 0.0191 | 0.15 |
| sse_hash16 | 16 | 11.44 | 0.0255 | 0.20 |
| sse_hash64 | 64 | 42.67 | 0.0422 | 0.34 |
| sse_hash256 | 256 | 109.72 | 0.0568 | 0.45 |
| sse_indent_tag | 8 | 6.26 | 0.0123 | 0.10 |
* gain/bpb = 最適利用時の bpb 削減上限 (実 bench はこれより小さい)
Probe: Prose (memory md JP+EN) 256KiB
| model | declared | effective | I(bit) | gain/bpb* |
|---|
| sse | 8 | 4.31 | 0.0058 | 0.05 |
| sse_lex | 8 | 4.03 | 0.0045 | 0.04 |
| sse_lex16 | 16 | 5.95 | 0.0089 | 0.07 |
| sse_lex64 | 64 | 9.08 | 0.0092 | 0.07 |
| sse_lex256 | 256 | 71.20 | 0.0215 | 0.17 |
| sse_hash256 | 256 | 201.99 | 0.0117 | 0.09 |
| sse_indent_tag | 8 | 1.49 | 0.00001 | 0.0001 |
Probe が既に語っていること:
- Python: sse_lex64 が上限 gain 全 model 中 top。sse_lex 実効 3.4/8 → 半分以上 dead。「8 値枠は足枷」の直接 evidence。
- Prose: sse_lex256 が top、sse_indent_tag 実効 1.49 → 完全 dead。
- Python N=256 で sse_hash256 ≈ sse_lex256 = 意味写像と乱数写像の差が消える境界 (prev_byte 全域を覆うため)。
3. Bench 実測 (1 MiB, subprocess round-trip verify)
Python source 1MiB (全 10 model)
| model | bytes | bpb | Δ vs sse_flat |
|---|
| order2 | 338,847 | 2.5852 | +0.113 |
| sse_flat | 324,027 | 2.4721 | 0 (baseline) |
| sse_hash8 | 322,906 | 2.4636 | −0.008 |
| sse_hash64 | 323,383 | 2.4672 | −0.005 |
| sse_hash256 | 323,468 | 2.4679 | −0.004 |
| sse_indent_tag | 323,329 | 2.4668 | −0.005 |
| sse_lex | 321,302 | 2.4514 | −0.021 |
| sse_lex16 | 320,740 | 2.4472 | −0.025 |
| sse_lex64 | 320,104 | 2.4423 | −0.030 ← top |
| sse_lex256 | 320,319 | 2.4438 | −0.028 |
Prose (memory md JP+EN) 1MiB
| model | bytes | bpb | Δ vs sse_flat |
|---|
| order2 | 474,893 | 3.6237 | +0.186 |
| sse_flat | 450,527 | 3.4377 | 0 (baseline) |
| sse_hash8 | 449,182 | 3.4270 | −0.011 |
| sse_hash64 | 449,213 | 3.4272 | −0.010 |
| sse_hash256 | 447,492 | 3.4141 | −0.024 |
| sse_lex | 447,318 | 3.4132 | −0.024 |
| sse_lex16 | 446,724 | 3.4087 | −0.029 |
| sse_lex64 | 444,296 | 3.3902 | −0.048 |
| sse_lex256 | 443,241 | 3.3821 | −0.056 ← top |
| sse_indent_tag | 450,557 | 3.4375 | +0.0002 ← 劣化 |
Bench の読み:
- 従来 sse − sse_flat = −0.002 bpb。今回 top 差 = Python −0.030 (15 倍) / Prose −0.056 (28 倍)。
- Lex vs Hash 同 N 対決 (Python): N=8 で lex 勝 0.013 / N=64 で lex 勝 0.025 / N=256 で lex 勝 0.024。全 N で semantic > random。
- Prose では N=256 で lex と hash がタイ (両者 Δ=−0.024)。UTF-8 混じり corpus では raw prev_byte が既に「識別」の大半、意味写像も乱数写像も同等。
- Python は sse_lex64 > sse_lex256 (0.030 > 0.028): bigram of char classes が raw prev_byte より効率良い。Prose は逆 (0.048 < 0.056): 非 ASCII 128 バイト分布のため raw byte が有利。Corpus 依存で optimal state count が変わる。
- sse_indent_tag の decisive verdict: Python Δ=−0.005 (ほぼ null) / Prose Δ=+0.0002 (劣化)。Prose で sse_flat より少しだけ悪化 = 情報を持たない state を SSE table に足すと adaptation overhead で純損失。事前予想「テストセットへの合わせ込み」以下の結果。
4. 反転実験 — 貪欲 8 分割 vs D-FUMT₈ 距離
optimal_partition.py: prev_byte の値域 {0..255} を貪欲 sort-by-P(bit=1) で K 個の等 population 区間に分割 (I(state;bit) を最大化)、D-FUMT₈ lex_class との Adjusted Rand Index を測る。
Bound 方向 (STEP 1741 corrigendum で明記):
- 96.6% / 89.1% は「貪欲」の効率で、真の K-partition 最適の下界。真の組合せ最適 (Bell(256)/(Bell(256-K)! · K!) 通りから選ぶ) はこれ以上。sort-by-P(bit=1) の contiguous 分割は Bernoulli scalar quantization では既知最適だが、byte 空間の一般分割ではない。
- D-FUMT₈ の相対達成率 87% (Python) / 26% (Prose) は上限値。分母を「真の最適 K=8」に置き換えると分母は同じか大きくなるため、真の相対達成率は 87% / 26% 以下。
- 正しい表現: 「D-FUMT₈ は Python で貪欲最適の 87% まで捕捉、Prose で 26% まで」= 上限値、真の効率はこれ以下。
Python 1MiB — I(bit) [bit/bit]
| partition | I | % of full256 | ARI vs lex |
|---|
| trivial K=1 | 0.0000 | 0.0% | — |
| D-FUMT₈ lex_class (K=8) | 0.0348 | 84.0% | 1.0000 |
| greedy K=8 | 0.0400 | 96.6% | 0.5708 |
| greedy K=16 | 0.0409 | 98.8% | 0.5774 |
| greedy K=32 | 0.0413 | 99.8% | 0.5845 |
| greedy K=64 | 0.0414 | 99.9% | 0.5852 |
| full K=256 (upper bound) | 0.0414 | 100% | — |
Prose 1MiB — I(bit) [bit/bit]
| partition | I | % of full256 | ARI vs lex |
|---|
| D-FUMT₈ lex_class (K=8) | 0.0049 | 23.1% | 1.0000 |
| greedy K=8 | 0.0187 | 89.1% | 0.0562 |
| greedy K=64 | 0.0208 | 99.0% | 0.0832 |
| full K=256 | 0.0210 | 100% | — |
反転実験の 3 つの
観測 (因果主張ではない、下記 §4.5 参照):
- K=8 は「貪欲探索の下では」狭くない: Python では貪欲 K=8 が full 256 上限の 96.6%、K=32 でほぼ天井。反面 D-FUMT₈ lex は 84% — 差 13% が (少なくとも) 実 gain 余地。
- Prose では意味写像の相対達成率が低い: D-FUMT₈ 23% / 貪欲 K=8 89% (この 2 つの分子分母比で 26%)。差 66% (絶対値) → D-FUMT₈ の相対達成率は Python 87% → Prose 26% と大きく低下。
- ARI 0.57 (Python) / 0.06 (Prose): 哲学起源の 8 値写像はPython source では有意な情報一致、prose 相当では偶然一致に近い。
4.5 交絡の存在 (因果主張の保留)
Python (ASCII + 構造化 code) vs Prose (UTF-8 + 自然言語) の比較は 2 変数を同時に動かしている: (a) 文字集合 (ASCII / UTF-8-heavy)、(b) データ種別 (code / prose)。上記観測 (2)(3) の 原因を「非 ASCII 混じり自然言語」1 変数に特定することは本 corpus セットからは不可。
正しい主張はobservation 記述レベル: 「Python source では 87% 達成、Prose では 26% 達成」。それ以上の因果 (文字集合が原因 / 言語種別が原因) は追加 corpus で分離実験が必要。/tools/step-1741-ransbench-confound-elimination/ で ASCII 純英語 prose と UTF-8-heavy JSON structured data の 2 追加 corpus で 2x2 実験を実施予定。
5. Lean 4 rANS 検証
data/lean4-mathlib/CollatzRei/RansCore.lean に以下 4 定理:
| 定理 | 内容 |
|---|
| roundTrip | D(C(s,x)) = (s,x) — encode/decode の代数的逆関数対 |
| slot_in_window | C(s,x) % T ∈ [cum_s, cum_s + freq_s) — symbol lookup 一意性 |
| putStep_bound | 入力 x < freq · renorm なら出力 < T · renorm — renormalization 前提 |
| state_below_2_pow_32 | Python 定数 (T = L = renorm = 2^16) で state < 2^32 — 32-bit fit 保証 |
証明技法: Nat.div_add_mod + Nat.add_mul_div_right + Nat.add_mul_mod_self_right + Nat.div_eq_of_lt + Nat.mod_eq_of_lt + omega + ring。
Axiom check 実測 (main .lake env で verify 完了)
'roundTrip' depends on axioms: [propext, Classical.choice, Quot.sound]
'slot_in_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'putStep_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'state_below_2_pow_32' depends on axioms: [propext, Classical.choice, Quot.sound]
全 4 定理 Mathlib 標準 3 axiom (propext + Classical.choice + Quot.sound) のみ。sorryAx なし・Lean.trustCompiler なし・Lean.ofReduceBool なし・ユーザー axiom なし = STEP 1368 axiom-free baseline に該当。CollatzRei の 3,542 axiom-free 群に合流可 (main merge 後の lake build で final verify)。
Honest scope (Lean 4 部分):
- Axiom check は /tmp/rans_full_axiom_check.lean に inline した完全 self-contained bind を lake env lean で走らせて確認。実際のプロジェクト file CollatzRei/RansCore.lean は同じソースを ReiAIOS.RANSCore namespace で提供、main merge 後 lake build CollatzRei.RansCore で最終 verify。
- 符号器の renormalization loop (16-bit word push/pop) 全体の証明は含まれない。単一 step の代数 (`putStep` / `advanceStep`) と bound のみ。
- normalize_to_T の proof (target 2、頻度表 sum=T + all ≥1 不変量) は本 STEP で未完了 (sibling file RansNormalize.lean の drafting は次 STEP 候補)。
- Prior art audit: 公開 index (GitHub search 2026-09-03) で Lean 4 rANS proof は発見せず。近い先行研究 = Bosma-Duchon-Roshan 2014 Coq preserve-integer coder (別 codec, 別 assistant)。「Lean 4 rANS proof は世界初」 は controllable でない (私が見つけていない paper が存在する可能性排除できず) — 「STEP 1731 で書いた」 まで が主張可。
6. 候補 3 (indent×tag) の判定
Probe I = 0.098 bpb (Python) / 0.0001 bpb (Prose) — 全 candidate 中最下位。事前予想通り。
Bench 実測 verdict: Python Δ=−0.005 (sse_hash8 の 0.008 より弱い、ほぼ null) / Prose Δ=+0.0002 (sse_flat より僅かに劣化)。
Python では indent 情報は既に sse_flat/order2 が空白バイト直前 predictor で吸っている。Prose では indent もタグも存在しない上、無信号 state を SSE table に加える adaptation overhead で純損失。「テストセットへの合わせ込み」評価すら得られず、明確な負けの実証。
7. 総合結論
- 「8 値は足枷か」への答え: N/A。枠自体は狭くない (貪欲 K=8 = 上限 96.6%)。狭かったのはD-FUMT₈ lex_class の写像の粒度だった。
- 実 gain の source: bigram of char classes (sse_lex64) — 15-24 倍の bpb 差。しかしこれは PAQ community が 15 年前に通った道 (Rei にとって新しい、分野にとってではない)。
- 反転実験は新しい問いを産んだ: 「D-FUMT₈ 8 値 = 意味起源 / 情報起源 貪欲 K=8 との重なり ARI 0.57」= 哲学的写像は情報論的構造の 6 割を偶発的に捕捉する — 論文になりうる形式。
- Lean 4 rANS = 外に出せる形として最強、build verify 完了後に CollatzRei の 3,542 axiom-free 群に加わる。
8. 次候補 (defer)
- Bench 完全実測: sse_lex256 / sse_hash{8,64,256} / sse_indent_tag の 1 MiB × 2 corpus 実データ (現在進行中)
- 4 MiB corpus での確認 (Python 1 MiB との rate 比較)
- Lean 4 build verify + RansNormalize.lean (target 2 の normalize_to_T 証明)
- 反転実験を「特徴量を二次から一次へ」route (context hash に文字種を混ぜる) と結合