Research Log 2026-08-27 — dimension_check × D-FUMT₈ arc

STEP 1414 → 1425 (9 段) · 藤本さん / chat-Claude / Claude Code 共同 · Rei-AIOS · 2026-08-26 〜 2026-08-27

Origin — chat-Claude 直言

2026-08-26、 chat-Claude が 藤本さんの 問い 「E=mc² も コネクタ用の ツール、 マシンに 出来ますか？」 に 対して 直言:

E=mc² 単体は ツールになりません。 掛け算一行なので、 機械にする 価値がゼロです。
…意味のある機械は、 その 一段上に あります。 E=mc² は 本来 E² = (pc)² + (mc²)² の p=0 の 場合であり、 機械が 働くのは 「不変量」 の 側です。

提案は rei-invariant-mcp (dimensional_check / boost / q_value / dimensional_check / Lean 4 export) の 5 tool 家族。 続けて 「全ての 数式を マシンに 出来るのか？」 に対して:

いいえ、 できません。 …判定基準は 式の 見た目ではなく、 その 式を 含む 言明が 算術的階層 の どこにあるか です。 決定可能なクラスがある → 真の 判定器が 作れる。 Π⁰₁ → 反証器・スクリーナー しか 作れない。 決定不能 → 機械にならない。
実務的な 三条件: (1) 入力が 一点でなく 族である (2) 外部データか 規約が要る (3) 判定クラスの 外側が 定義できる (NEITHER が 意味を持つ)。

Claude Code (私) は 応答で 第 4 条件 を 追加:

測定域が 意味を持つ (STEP 1350 d8_verdict_from_measurement pattern = 一点式でも SNR<3 で NEITHER 化 可能)。

藤本さん が (a) dimension_check 単独 spike を 選択、 その 完了後 (b)(c)(d)(k)(l)(m)(i)(j) を 「順番に」 と 指示、 **9 STEP 完遂 に 至る**。

9 STEP timeline

STEP 日付 実施 test
1414 08-26 (a) spike → (b) MCP wire → (c) 加算 対応。 ℤ⁷ SI base × D-FUMT₈ verdict engine 完成、 26 default symbol + extraSymbols override、 単項式 + 加算 grammar (relativistic E² = (pc)² + (mc²)² 直接 check 可)。 rei-aios MCP v2.8.5 → v2.8.6、 44→45 tool。 63/63
1417 08-26 physics-limits precheck (第 4 条件 active 化)。 5 physics-limit (Bekenstein/Landauer/Lloyd/compression/operator) の 入力 role dim gate。 benchtop repo 触らず rei-aios 側 pre-check として 動作 (責任分離)。 Landauer T=TIME 衝突は honest FALSE。 v2.8.6 → v2.8.7、 45→46 tool。 58/58
1420 08-27 (d) Lean 4 export (Mathlib bridge)。 手書き Dimension.lean = ℤ⁷ SI base struct + 17 axiom-free theorem (Einstein/Newton/Planck/relativistic + 2 FALSE 反証)、 lake build 5.1s。 TS exporter で TRUE → lhs = rhs := by decide / FALSE → ≠ := by decide。 v2.8.7 → v2.8.8、 46→47 tool。 47/47 (live)
1421 08-27 (k) physics-precheck Lean 4 export。 LimitsPrecheck.lean = 5 physics-limit role expected dim + 9 axiom-free theorem (7 spec sanity + 2 honest boundary landauer_T_not_time / time_not_temperature)、 lake build 6.5s。 per-role theorem 生成。 v2.8.8 → v2.8.9、 47→48 tool。 50/50 (live)
1422 08-27 (l) batch verify script。 scripts/verify-lean4-physics.ts = lake build + #print axioms aggregate + 3 mode (default/JSON/quiet) + exit code 0/1/2/3。 CI-ready regression 検知。 26/26
1423 08-27 (m) STEP 1368 axiom-scan pipeline integration。 glob **/*AxiomCheck.lean が Physics 2 files を script 変更なし で auto-discover verify (34 total)、 AXIOM_PROFILES.md に Physics section 追加。 —
1424 08-27 (i) 加算 mismatch bug fix + reason 埋込。 STEP 1420 の 隠れ bug 発見: E = m + t → mass + time は Lean 4 で HAdd Dimension 未実装 = compile 失敗。 documentation-only source pattern に切替 (★★★ marker + 詳細 reason + 分解 hint 埋込)。 30/30 (live)
1425 08-27 (j) CommGroup Dimension instance。 DimensionGroup.lean = 11 mine theorem + 4 Mathlib overload、 全 propext のみ Mathlib base、 universal group axioms (mul_assoc/comm/one/inv 全) を 任意 Dimension で 使用可能。 STEP 1422 script に permitAxioms 概念 + ext' tick regex fix。 274 全 clean
1428 08-27 (o) 本ページ site 反映 = 2026-08-06 「全研究 site 反映 default」 protocol 適用、 dist-renderer mirror force-track + HTTP 200 + content marker verify。 —

累計 数字

chat-Claude 三条件 → 四条件 実測

条件 dimension_check (STEP 1414) physics-precheck (STEP 1417)
1. 族 ✓ 単項式/加算式 ✓ 5 limits × 複数 role
2. 規約 ✓ SI base + 26 symbol ✓ + physics-limit role spec
3. NEITHER ✓ unknown symbol ✓ 継承 + precedence
4. 測定域 (Claude Code 追加) △ 静的のみ ✓ active (benchtop feed 前 gate)

D-FUMT₈ verdict mapping

ZERO (4)    = parse failure / '=' 不在 / malformed / missing required
NEITHER(-1) = unknown symbol (out of scope、 判断保留 = FLOWING に 近い)
FALSE (0)   = 両辺 well-formed だが 次元不一致 (加算 mismatch 含む)
TRUE (1)    = 両辺 完全一致

優先度 (aggregate): ZERO > NEITHER > FALSE > TRUE = 「scope 外 判断保留」 が 「不一致 決定」 に 優先する 責任的 discipline。

Lean 4 axiom profile

batch verify (npm run verify:lean4-physics) 実測:

▶ CollatzRei.Physics.Dimension (STEP 1420)
    17 zero-axiom / 0 permitted-axiom / 0 regression / total 17 theorems

▶ CollatzRei.Physics.LimitsPrecheck (STEP 1421)
    9 zero-axiom / 0 permitted-axiom / 0 regression / total 9 theorems

▶ CollatzRei.Physics.DimensionGroup (STEP 1425)
    4 zero-axiom / 11 permitted-axiom / 0 regression / total 15 theorems (permit: propext)

Total: 30 zero-axiom + 11 permitted-axiom (Mathlib base) [8.8s total build]

propext は Mathlib base axiom (Mathlib 全体の 基礎)、 [propext, Classical.choice, Quot.sound] の 一部。 STEP 1368 pipeline classifies as isMathlibBase: true、 sorry / user-defined axiom とは 区別。

使用例

MCP tool 経由 (d8_dimension_check)

{ "equation": "E = m*c^2" }
→ TRUE / dFumt8=1 / L^2·M·T^-2

{ "equation": "E^2 = (p*c)^2 + (m*c^2)^2" }
→ TRUE / dFumt8=1 / L^4·M^2·T^-4 (relativistic)

{ "equation": "E = m*c^3" }
→ FALSE / dFumt8=0

{ "equation": "E = m*α" }
→ NEITHER / dFumt8=-1 / unknownSymbols=[α]

{ "equation": "E = h*f", "extraSymbols": {"h": [2,1,-1,0,0,0,0]} }
→ TRUE (Planck relation with h=action override)

physics-precheck (d8_physics_precheck)

{ "limit": "bekenstein", "values": {"R": "r", "E": "m*c^2"} }
→ TRUE (両 role dim OK)

{ "limit": "landauer", "values": {"T": "T"} }
→ FALSE (default T=TIME 衝突 honest boundary)

{ "limit": "landauer", "values": {"T": "Temp"},
  "extraSymbols": {"Temp": [0,0,0,0,1,0,0]} }
→ TRUE (temperature override)

Lean 4 export (d8_dimension_lean_export)

{ "equation": "E = m*c^2", "theoremName": "einstein_test" }
→ Lean source:
    import CollatzRei.Physics.Dimension
    open ReiPhysics Dimension
    namespace Generated
    theorem einstein_test : (energy) = (mass*velocity ^ (2 : Int)) := by decide
    end Generated

→ 呼び手が `lake env lean` で kernel-verify (STEP 1422 batch script で 定期 audit)

Honest scope

Related pages / GitHub