SsmQuant broken import audit + fix STEP 1777 STEP 1783

2026-09-06 · 3 週間 root build red 常態化 の 発見 + 起点特定 + 「なぜ 気づかれなかったか」 構造分析 (7 因子) + 修復 実施 (root green 化 3 週間ぶり)

1. なぜ このページか

2026-09-06 4e session の STEP 1774 (ZCE partition-conservation Lean 4) build 中に、 root lake build CollatzRei が CollatzRei/SsmQuantErrorBounded.lean file 不在で fail 発見。 私 (Claude) が 「pre-existing、 私の 変更起因ではない、 別 arc scope」 と 判定して 別 arc 扱い → 藤本さん 明示訂正: 「root build が 赤い 常態化 = 次に 本物の regression が 入っても 気づけない、 d8_verify の 緑と 同じ構図の 裏返し。 いつから 赤いのか、 誰の担当か を notepad に 残しておいてください」。

★ 本題: 「ファイルを 1 本足せば 直る 話」 として だけ 記録すると、 構造の問題が 消える。 本 page は 表面 fix (STEP 1783) + 「なぜ 3 週間気づかれなかったか」 の 構造分析 (STEP 1777) 両方を 保存する。 藤本さん directive: 「d8_verify の 緑と 同じ構図の 裏返しで、 こちらの ほうが 本題」。

2. 一次 audit — 起点 + 経過 (STEP 1777)

broken importdata/lean4-mathlib/CollatzRei.lean:237 = import CollatzRei.SsmQuantErrorBounded
起点 commit3f14557ce0 (2026-08-16 01:08:04 JST, author fc0web, co-author Claude Opus 4.7)
commit messagefeat(step-1338): Antihydra Bridge Lean 4 axiom-free + chat-Claude λ arc archival
経過期間2026-08-16 → 2026-09-06 = 21 日 (約 3 週間)
file 状態CollatzRei/SsmQuantErrorBounded.lean = git log --diff-filter=A/D 両方 空 = 一度も add されず / delete されず

2.1 真の起源 arc = 別 session (2 日前)

STEP 1338 memory (project_step1338_antihydra_bridge_2026-08-16.md) は Antihydra Bridge 主 arc で、 SsmQuant 一切言及なし。 真の 起源 = 2 日前 (2026-08-14) の SSM Phase 2 (c) 別 session (0fbf78aa-...、 memory project_ssm_phase2cd_lean4_and_mlir_2026-08-14.md)。 SSM Phase 2 (c) は SsmQuantErrorBounded.lean + AxiomCheck.lean 両方 作成予定と 記録、 実際は 両 file とも 一度も commit されず、 root CollatzRei.lean への import 行のみ 2 日後 の 別 arc (STEP 1338 Antihydra Bridge) の commit に working tree cross-arc pollution で 混入。

3. ★★★ 本題 — なぜ 3 週間気づかれなかったか (STEP 1777 構造分析)

藤本さん directive: 「root build が 赤いまま 各 tab が 個別の lake build (667/667 PASS など) で 作業を 続けられているなら、 root が 赤いことを 誰にも 通知しない 構造」

3.1 7 因子

#因子効果
1Pre-commit hook は module-level 個別 verify のみroot build は 走らず、 STEP 1774 commit 出力 も Verifying 3 staged Lean file(s) のみ
2CI/CD で root build gate なし定期 root build 実行 + fail 通知 の 仕組み なし (要 verify)
3各 arc の 「build OK」 主張は module-level のみnotepad / memory / commit message で 「build 通過」 と 記録される 際、 root build は 対象外
4Local dev workflow が module-focusedroot build 数分 vs module build 数秒、 効率 trade-off が 効率側に 常態的に 寄る
5Root build fail の 影響が module-level 作業に 現れないbroken import は 孤立 file 化、 他 module から 参照されず、 root 以外では 起動しない
6Notepad TEMPLATE.md に root build 状態 記録 慣習なし「Build」 section は default で module-level、 root 状態 記録が 制度化されていない
7Discovery bias (default state 化 + 「pre-existing」 shrug pattern)positive event は notepad される、 negative absence (「root が 赤い」) は 誰も notepad しない → 気づく機会 を feedback loop で 減らす

3.2 d8_verify の 緑と 対称構造

事例信号実際の内容意味喪失 pattern
d8_verify (STEP 1397-1772)「緑 6/6 PASS」TS side self-check のみ、 cross-impl drift 未検出緑 が 「整合」 の 意味を 失う
root build (STEP 1338-1774)「赤い」 or 「知らない」各 module 個別 OK、 root 状態 誰も monitor せず赤 が 「壊れている」 の 意味を 失う (default state 化)

両方 = 「意味を 持つ 信号 が 意味を 持たない 状態に 常態化」 の 対称構造。 藤本さん 「こちらの ほうが 本題」 明示。

4. 修復 実施 (STEP 1783)

4.1 判断 — 修復案 3 択

私の 推奨 = import 削除 (SSM arc 実質 abandoned + 3 週間 誰も 困っていない + memory に spec 残存)。 藤本さん AskUserQuestion 経由で 「STEP 1777 audit の 修復実施」 選択 → 実施。

4.2 実施内容

-- data/lean4-mathlib/CollatzRei.lean:237 削除
- import CollatzRei.SsmQuantErrorBounded

CLAUDE.md rule 準拠: 「// removed comments 追加禁止、 unused なら 完全削除」 → 説明 comment code 内一切なし、 why は commit message + notepad + memory 3 層 保存。

4.3 Build 結果

★ lake build CollatzRei = 7954/7955 jobs PASS (20s) = 3 週間ぶり root build green 化達成

5. Honest scope

本 STEP 1783 は 表面 fix のみ。 STEP 1777 audit で 指摘した 7 因子 構造問題 は 未修復:
  1. Pre-commit hook module-level のみ (root build gate 追加は 別 arc)
  2. CI/CD root build gate なし (要 verify + 追加は 別 arc)
  3. 各 arc の 「build OK」 主張は module-level のみ
  4. Local dev workflow が module-focused
  5. Root build fail の 影響が module-level 作業に 現れない
  6. Notepad TEMPLATE.md に root build 状態 記録 慣習なし
  7. Discovery bias + 「pre-existing」 shrug pattern
次回 root build red 再発時、 7 因子 が 依然として 3 週間 silent を 再生産する 可能性。 根本治療 は 藤本さん 運用見直し STEP scope (未 claim、 material 提供済)。
SSM Phase 2 (c) 定理 spec (trajectory_abs_le + trajectory_bound_independent_of_time) は memory project_ssm_phase2cd_lean4_and_mlir_2026-08-14.md に 保存継続、 将来 復元必要なら 別 STEP。

6. Collision material for 藤本さん 運用見直し STEP

本 STEP 1777 claim 過程で atomic counter vs 発話予約 mismatch 事例 が 発生:

藤本さん 一般化: 「私の 指示が machine-readable な 形で 残っていない」 = 発話 directive は cross-session log に 残らず、 tab は 受信 text しか 持たず、 「同じ指示を 別 tab に 出した」 「発話予約が 別 tab に 取られた」 「発話予約と 実 claim が drift した」 が 全て 検出困難。

藤本さん の 運用見直し STEP で 参照可能な 4 material

  1. 本 audit (STEP 1777/1783) = 機械 signal 意味喪失
  2. STEP 1777 claim collision = Human directive non-machine-readability
  3. STEP 1775 誤 read + STEP 1776/1777 二重発注 = cross-tab draft 誤認 + Human 指示追跡欠落
  4. d8_verify 緑 (a6 arc 進行中) = 機械 signal 意味喪失 対称事例

4 事例 は 全て 「信号 (機械 or 人) と 実 内容 の drift」 pattern の 変奏。

7. 参照