# STEP 1777 — ssm-quant-error-bounded-root-fail-audit

**Timestamp**: 2026-09-06T01:15 (JST)
**Tab worktree**: main (rei-aios-4e session)
**Commit**: `<hash>` (commit 後追記)

## 一行 summary

`SsmQuantErrorBounded.lean` broken import (2026-08-16 STEP 1338 commit で 混入、 3 週間 root build red 常態化) の audit — 起点 特定 + **「なぜ 3 週間気づかれなかったか」構造分析** (root build が 誰にも 通知されない 構造 = d8_verify 緑と 対称)

## 主要 finding / evidence

### (1) 一次 audit — 起点 + 経過

- **broken import 行**: `data/lean4-mathlib/CollatzRei.lean:237` = `import CollatzRei.SsmQuantErrorBounded`
- **起点 commit**: `3f14557ce0` (2026-08-16 01:08:04 JST, author fc0web, co-author Claude Opus 4.7)
- **commit message**: `feat(step-1338): Antihydra Bridge Lean 4 axiom-free + chat-Claude λ arc archival`
- **経過期間**: 2026-08-16 → 2026-09-06 = **約 3 週間** (21 日)
- **現在の担当**: 明示 evidence なし (別 tab の 修復進行 grep 該当なし、 git status で `SsmQuantErrorBounded` 無出現)
- **file 状態**: `CollatzRei/SsmQuantErrorBounded.lean` は git log --diff-filter=A/D 両方 空 = **一度も add されず / delete されず**

### (2) 起源 arc audit — STEP 1338 は 実は 別 arc

- **STEP 1338 memory** (`memory/project_step1338_antihydra_bridge_2026-08-16.md`): AntihydraBridge 主 arc、 `SsmQuantErrorBounded` 一切言及なし
- **真の 起源**: `memory/project_ssm_phase2cd_lean4_and_mlir_2026-08-14.md` = 2 日前 (2026-08-14) の SSM Phase 2 (c) arc、 別 session `0fbf78aa-...` で 実行予定
- **SSM Phase 2 (c) の 予定**: `SsmQuantErrorBounded.lean` (2 定理 `trajectory_abs_le` + `trajectory_bound_independent_of_time`、 Mathlib base axiom-free) + `SsmQuantErrorBoundedAxiomCheck.lean` **両方 作成予定**
- **実際**: 両 file とも 一度も commit されず、 root `CollatzRei.lean` への import 行のみ **2 日後 の 別 arc (STEP 1338 Antihydra Bridge) の commit に 巻き込まれた**
- **推定 mechanism**: SSM Phase 2 (c) session で 作業中 (working tree に import 行 + file 未 write)、 別 session に 移行、 STEP 1338 commit 時に `git add data/lean4-mathlib/CollatzRei.lean` で import 行が staging に混入、 file 本体は untracked のまま commit されず。 pre-commit hook は staged Lean file を verify するが、 root build までは gate せず → 通過

### (3) ★★★ **なぜ 3 週間気づかれなかったか — 構造分析 (本題側)**

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

具体的な 「通知欠落」 の 7 因子:

1. **Pre-commit hook は module-level 個別 verify のみ** — 私 STEP 1774 の commit 出力: `Verifying 3 staged Lean file(s) with 'lake env lean'... OK CollatzRei.lean OK CollatzRei/ZceLedgerPartition.lean OK ZceLedgerPartitionAxiomCheck.lean`。 root `lake build CollatzRei` は 走らず。 他 tab も 同じ。

2. **CI/CD で root build gate なし** — repo に GitHub Actions / 定期 CI が root build を 走らせる 仕組み なし (要 verify)。 「build 状態を 誰も 見ていない」 が構造。

3. **各 arc の 「build OK」 主張は module-level のみ** — notepad / memory で 「build 通過」 と 記録される 際、 root build は 対象外。 STEP 1774 も その 一例 (「build 667/667 PASS 7.4s」 は `lake build CollatzRei.ZceLedgerPartition` の 結果、 root ではない)。

4. **Local dev workflow が module-focused** — 開発中は 該当 module を lake build するのが 効率的 (数秒〜数十秒)、 root build は 数分 かかる ため 頻繁には 走らない。 「作業効率」 と 「root health monitoring」 の trade-off が 効率側に 常態的に 寄っている。

5. **Root build fail の 影響が module-level 作業に 現れない** — 私 STEP 1774 の build 中も `Mathlib.Algebra.BigOperators.Group.Finset` 誤 import は STEP 1774 module で detect されて 修正、 root の broken import (`SsmQuantErrorBounded`) は 独立して 影響せず、 module 開発は 完結。 broken import は 「他 module から 参照されない孤立 file」 に 化けている ため、 root build 以外では 起動しない。

6. **Notepad TEMPLATE.md に root build 状態 記録 慣習なし** — 「Build」 section は default で module-level (「lake build <MyModule> N/M PASS」)。 root 状態 (「root build 前提として red、 私の 変更起因ではない」) を 明示的に 書く 慣習が確立されていない。 STEP 1774 notepad も root fail を 「詳細参照」 section の 一言 (「Regression note: pre-existing」) で 済ませていた = 記録 弱い。

7. **Discovery bias (default state 化)** — 「新 feature 追加」 は notepad で record される (positive event)、 「root が 赤い」 は 誰も notepad しない (default state と 認識される、 negative absence)。 STEP 1774 の 私も 「pre-existing broken import、 私の 変更起因ではない、 別 arc scope」 と 判断して すぐ 手放した = default state 化 の 一 example。 「気づく機会」 を さらに 減らす feedback loop。

### (4) D-FUMT₈ 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 化) |

**両方とも 信号の 意味喪失 = 「意味を 持つ 信号 が 意味を 持たない 状態に 常態化」 pattern**。 対称構造 = 藤本さん指摘 「d8_verify の 緑と 同じ構図の 裏返し、 こちらの ほうが 本題」。

## Honest scope

- **主張しないこと**:
  - この audit で 修復は 一切していない (broken import 削除 or file 追加 判断は 別 STEP)
  - CI/CD 状態 の 完全 verify は 未実行 (「GitHub Actions で root build gate なし」 は grep での 明示 evidence 未収集、 要 verify)
  - 3 週間中 に 別 tab が root build 実行して 気づいた 可能性は 排除しきれない (memory 全 grep で 「SsmQuantErrorBounded」 該当 = 本 audit と 元 SSM Phase 2 (c) memory のみ、 他 tab の 気づき 記録なし = 誰も notepad にしていない side)
- **確認していないこと**: `dist-renderer/assets/*` の 大量 delete 状態 (git status) との 関連 (別 tab の build 済 の 可能性、 SsmQuantErrorBounded とは 独立と 推定 だが 未確認)
- **前提**: root build 「7944/7945」 (STEP 1338 memory 記録) → 「667/667」 (現在 module-level) の 数字差 は module 数 統計の 変化 (STEP 1338 → 1774 の 3 週間で 追加削除 の 累計)、 直接 audit 対象ではない

## Failure mode (未来 Claude dataset)

- **What could go wrong**:
  - (a) **Structural silent failure pattern**: 各 tab が module-level で 個別 verify、 root は 誰も 監視せず → root broken 状態が 数週間 気づかれない (実 事例 21 日 記録済)
  - (b) **Working tree cross-arc pollution**: session A で 作業中の staging (未完 file + partial import) が session B の commit に 巻き込まれる → import 行だけ commit + file 未 commit → root broken (実 事例 STEP 1338 commit に SSM Phase 2 (c) 途中作業混入 記録済)
  - (c) **Default state discovery bias**: 「新 feature 追加」 は notepad で 記録、 「壊れている」 は 誰も notepad しない → negative state が 発見されにくい → 慢性化
  - (d) **「Pre-existing」 shrug pattern**: broken 状態を 別 arc で 発見しても 「pre-existing、 私の scope 外」 と 手放して 記録もしない (私 の STEP 1774 が まさに この pattern を していた、 藤本さん 明示指摘で 訂正)
- **Prevention**:
  - (a): (i) Pre-commit hook に root build gate 追加 (時間 cost 大、 trade-off 判断要)、 (ii) CI/CD で 定期 root build 実行 + fail 通知、 (iii) notepad TEMPLATE.md に 「Root build 状態」 section を default 追加 (低コスト)
  - (b): Pre-commit hook で 「staged import 行が 参照する module が commit tree に 存在するか」 check (可能性は あるが 未実装)
  - (c): 「Root build red」 状態を **積極的に record** する 慣習 = 発見時 に 必ず notepad audit を 追加 (本 STEP 1777 が その 第 1 例)
  - (d): 「Pre-existing で 私の 起因ではない」 と 判定した 事項も、 audit として 記録する (別 arc 修復 前提 でも 起点 特定 + 経過 期間 + 構造分析は record)
- **Recovery**:
  - 本 audit 自体が (c)(d) の recovery instance
  - (a)(b) の 予防策 実装は 別 arc = 藤本さん の 運用見直し STEP scope

## ★ 修復方針 propose (別 STEP 実施 前提)

3 択:
- **修復案 1: import 行 削除** — `data/lean4-mathlib/CollatzRei.lean:237` の `import CollatzRei.SsmQuantErrorBounded` を 削除 or コメントアウト。 3 週間 誰も 困っていない = 実質 不要と 見なせる。 最も 保守的 (対応 file の 存在に 依存する 別 file なし = grep verify)。
- **修復案 2: file 追加** — SSM Phase 2 (c) memory (`project_ssm_phase2cd_lean4_and_mlir_2026-08-14.md`) に 定理 spec + proof 記録あり、 これを Lean 4 file として 復元。 SSM Phase 2 arc の 意図 (bounded state proof の formal 化) を 尊重。
- **修復案 3: 一時 stub file 追加** — 空 namespace + placeholder proof で file を 追加、 root build を green 化、 実 content は 別 STEP で 追加。 短期 fix。

**私の 推奨**: **修復案 1 (import 削除)**。 根拠:
- SSM Phase 2 (c) arc は 2 日 後 に AntihydraBridge arc に 上書きされた (別 session 移行) = 実 実装意図が 中断 = arc 自体が 未完 の まま abandoned の 可能性
- 3 週間 誰も 困っていない = 該当 定理を 他 module が 参照していない = 実 使用の evidence なし (要 grep verify)
- SSM Phase 2 (c) の 定理 spec は memory に 記録されている = 将来 復元 要 なら memory から reconstruct 可能、 broken import 常態化 より 明示的 削除 が clean
- STEP 1338 co-author の Claude Opus 4.7 session (`018nbciAGaGNXGijhheSatK9`) と 元 SSM session (`0fbf78aa-8dcf-4dd5-8e62-89880c1846c6`) いずれ も 現在 offline (grep 該当なし)、 意図確認は memory 記録のみ

**修復判断は 藤本さん judgment** — 上記 3 案 + 推奨、 実 修復は 別 STEP で 別 tab or 4e 別 arc で 実施。

## ★ Collision material for 運用見直し STEP (藤本さん directive)

藤本さん 指摘: 「今回の collision 自体が 運用見直しの 材料。 私が 口頭で 『次は 1777、 担当は a6』 と 言ったことが、 counter にも file にも 残らず、 別 tab が 同じ番号を 取った。 95 と a6 への 二重発注と 同じ根。 私の 指示が machine-readable な 形で 残っていない」

本 STEP 1777 arc で 発生した 実 collision:
- 2026-09-05T15:26:55 STEP 1774 claim (私、 zce_partition_total_exclusive)
- 2026-09-05T16:07:19 STEP 1777 release (私、 藤本さん発話予約 respect)
- 2026-09-05T16:07:22 STEP 1777 claim (私、 3秒後 に 同 slug 再取得 = counter は skip なし)
- 2026-09-05T16:08:22 STEP 1778 claim (a6、 slug `step1776_phrasing_corrigendum_headline_overreach` — 拡張案 a ではない、 別 arc)
- 2026-09-05T16:10:33 STEP 1779 claim (別 tab、 slug `d8verify_cross_impl_drift_claim`)

**Pattern (発話予約 vs atomic counter mismatch)**:
- 藤本さん 発話: 「次は 1777、 担当は a6」 → **counter は 発話を 認識せず**
- 4e が atomic claim → 1777 取得 (発話予約 violation)
- 藤本さん judgment (A-1) で 私 1777 使用確定、 a6 は 1778 に 実装 continue
- **a6 が 実際に 取った 1778 は 藤本さん が 想定した 「拡張案 a」 とも 異なる slug** = 藤本さん 発話予約と actual claim が 更に 二重 drift

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

**藤本さん の 運用見直し STEP で 参照可能な material 4 種**:
- (i) `SsmQuantErrorBounded` 3 週間 silent root fail = 「機械的 signal の 意味喪失」 の 事例
- (ii) STEP 1777 claim collision = 「Human directive の non-machine-readability」 の 事例
- (iii) STEP 1775 誤 read + STEP 1776/1777 二重発注 (前 turn 記録) = 「cross-tab draft 誤認 + Human 指示追跡欠落」 の 事例
- (iv) d8_verify 緑 (a6 arc 進行中) = 「機械的 signal の 意味喪失」 の 対称事例

4 事例 は 全て 「信号 (機械 or 人) と 実 内容 の drift」 pattern の 変奏。 運用見直し STEP は 4 事例を 統一的に 材料化可能。

## 詳細参照

- 詳細 memory: `memory/project_step1777_ssm_quant_error_bounded_root_fail_audit_2026-09-06.md`
- 前 STEP notepad: `docs/notepad/2026-09-06T00-54_STEP-1774_zce-partition-conservation.md` (root fail は「Regression note」 一行で 済ませていた、 本 STEP で 補完)
- 起点 commit: `3f14557ce0` (git show)
- 起源 arc memory: `project_step1338_antihydra_bridge_2026-08-16.md` + `project_ssm_phase2cd_lean4_and_mlir_2026-08-14.md`
- 関連 STEP: STEP 1338 (Antihydra Bridge、 巻き込まれ commit)、 STEP 1774 (直前 arc、 4e、 root fail 発見)、 藤本さん 運用見直し STEP (未 claim、 別 tab or 藤本さん directive)、 未定 修復 STEP (別 tab or 4e 別 arc)