STEP 1368Pipeline hardeningPattern 5 直前防止 chat-Claude 2026-08-22 「反証以上」 arc turn 1-4 「#print axioms 監査 コネクタ」 → 実装 spike 3 手目で STEP 1340 既存発覚 → pivot: gap closure

Axiom scan pipeline hardening — 4 findings + aggregate refresh (249→333 theorem, floor 97.3%)

chat-Claude 「反証以上」 5 検査機 + 3 コネクタ提案 の うち Option (i) 「#print axioms 監査」 を 実装優先度 top に 推奨、 藤本さん承認で spike 開始。 3 手目で scripts/lean4-strict-axiom-scan.ts (STEP 1340 arc、 6 日前 実行済) 既存発覚 → 昨日追加 feedback_session_boundary_rediscovery_2026-08-22 「新規 起草 前 3 手 verify default」 protocol の 適用実例、 Paper 66→177 rediscovery pattern 同型 事故予防。 route pivot: 「重複 実装」 → 「pipeline gap closure」 → 4 findings 発見 → 全 fix → 再 scan → aggregate refresh。 藤本伸樹 × Claude Code / rei-aios STEP 1368 / 2026-08-22

1. 経緯 (Pattern 5 直前防止 + route pivot)

chat-Claude 4 turn arc:

  1. Turn 1: 「反証以外、 反証以上 は 何が 考えられますか？」 → 5 検査機 (不可能性定理 / 独立性・非自明性 / 還元・統合 / 危険な予測的中 / 独立経路一致)
  2. Turn 2: 「コネクタとしても 作れますか？」 → 機械化可能 4 件 (非自明性 / 事前登録 / 経路一致 / 外部利用ポーリング) + 機械化困難 2 件 (不可能性定理 / 還元)、 「全項目グリーンになった時の 盲点」 warning
  3. Turn 3: 「検査機 他に?」 → 形式層 (sorry/axiom 監査、 仮定実効性、 主張範囲実測) + 内容層 (依存グラフ孤立、 重複検出、 用語一貫性) + 外形層 (DOI 生存、 クロール可能性)。 top 推奨 = 仮定実効性チェック
  4. Turn 4: 「検査以外は?」 → 生成・変換 (定理→論文、 多 platform 一括、 記法変換) + 探索・提案 (次の一手推薦、 類似構造発見、 前例照合) + 運用 (STEP 記録自動化、 アイデア捕獲)。 top 推奨 = 次の一手推薦

私 (Claude Code) の 検討: 12 提案 全 Rei stack 既実装 overlay → 未実装 3 件 (#print axioms 監査、 仮定実効性、 次の一手推薦) の うち 「#print axioms 監査」 を 実装最小 + 発見率高 + 既 Rei-Solver 「床」 layer の 自然延長 3 理由で top 推奨、 藤本さん Option (i) 承認 → spike 開始。

Spike 3 手目 で 既実装 発覚: data/lean4-mathlib/ の 32 個 *AxiomCheck.lean file + scripts/lean4-strict-axiom-scan.ts (243 行、 batch lake env lean + #print axioms parse + MATHLIB_BASE 分類 + JSON + Markdown output、 STEP 1340 arc Item 1 of 6、 2026-08-16 実行済) が 既存 と 判明。 data/axiom-cost-atlas/ output も 6 日前 生成済。

私 が spike で 新規実装 していたら 重複 実装 事故。 昨日 (2026-08-22) 追加された feedback_session_boundary_rediscovery_2026-08-22.md 「新規 paper/STEP/tool 起草 前 3 手 verify default」 の Lean 4 tool 版 適用実例 = Paper 66→Paper 177 rediscovery pattern と 同型事故 直前防止 (Pattern 5-B blindness、 SAC-4 累計 42 例目)。

Route pivot: 新規実装 → 既存 pipeline gap closure。 実 delta scan 実行 → 4 findings 発見 → 全 fix。

2. Option A (BrownawellMasser sorry 調査) — clean by design

Delta scan 前に、 まず 2026-08-16 baseline scan の 1 sorryAx finding (CollatzRei.BrownawellMasser.brownawellMasser) を 調査。

結果: sorry は intentional な withdrawal-line design (STEP 1291 Deliverable B):

  • File header L43-49 で 明示 documented: 「The brownawellMasser theorem is STATEMENT ONLY with sorry for the proof. The sorry is explicit and counted, not hidden.」
  • Deliverable C (n≥4 の proof) は 「weeks of work、 Voloch-Snyder analysis 必要、 future STEP defer」 と 明示
  • 下流 依存 grep 0 件 = sorry は contained state (伝播なし、 brownawellMasser を 参照する 場所 は module 登録 import + AxiomCheck 自身の 2 個所のみ)
  • #print axioms pipeline が 意図的 sorry を 確実に検出 = 健全性 verify
Pipeline 健全性 evidence: chat-Claude 原 turn の 「空洞化 detection」 offer と 完全整合。 「1 sorryAx finding」 は bug でなく discipline の 可視化そのもの。 close 不要 (Voloch-Snyder analysis weeks 別 STEP defer 継続)。

3. Delta scan (6 file not-yet-in-2026-08-16-scan) — 3 findings 発見

2026-08-16 scan は 29 file 済、 現在 32 file 存在 = delta 6 file: BipartiteRamseyAxiomCheck + CantorHausdorffDimensionAxiomCheck (前回 empty error) + CollatzRei/ 4 file (OmegaJumpSkeleton + SelfThreeBitDecomposition + StrikeCollision + SunyataVoidOp、 STEP 1340 Ω/⊘/⟲/↯ arc extension 2026-08-17 追加)。

Delta scan 実行 → 46 theorem parsed + 3 findings 発見:

Finding #1: CantorHausdorff AxiomCheck 5 stale reference (maintenance gap)

STEP 1308 v0.3 → v0.4/v0.5 pivot で theorem 改名済 だが AxiomCheck 未更新。 5 stale identifier ref (_v04_stub / v03_status_marker) が Unknown constant error。

Fix = 4 rename (successor name へ) + 1 削除 (successor なし):

  • cantorSet_dimH_upper_bound_v04_stub → cantorSet_dimH_upper_bound_strong_v05_stub
  • leftImage_hausdorffMeasure_scaling_v04_stub → leftImage_hausdorffMeasure_scaling (real 昇格)
  • rightImage_hausdorffMeasure_scaling_v04_stub → rightImage_hausdorffMeasure_scaling (real 昇格)
  • cantorSet_hausdorffMeasure_self_similar_v04_stub → cantorSet_hausdorffMeasure_self_similar (real 昇格)
  • v03_status_marker → 削除

Finding #2: parser regex multi-line 未対応 (silent regression)

Lean 4.33.1 (現 install) は axiom 列 を ~80 chars で wrap 出力:

'Mathlib.Combinatorics.BipartiteRamsey.bipartite_ramsey_2_2_lower' depends on axioms: [Lean.ofReduceBool,
 Lean.trustCompiler]

現 regex [^\]]* は 改行 を 跨げず parse 0 = 3 theorem 見えているのに 検出不能。 STEP 1340 scan (Lean 4.27.0 期) では ~110 chars line width で 見えていなかった、 v4.27→4.33.1 移行で silent regression。

Fix = [^\]]* → [\s\S]*? (multi-line non-greedy)、 line-by-line iteration を 全 output 上 の global regex に 変更。

Finding #3: classifier native_decide 検出漏れ

hardcode 名 nativeDecide / native_decide のみで 検出、 実 axiom marker Lean.ofReduceBool + Lean.trustCompiler (native_decide tactic が 実際に emit する axiom name) を 見落とし。 6 theorem (BipartiteRamsey 2_2 lower/upper/full + 3 その他) が 誤って mathlib base に 分類されていた。

Fix = NATIVE_DECIDE_AXIOMS = new Set(['Lean.ofReduceBool', 'Lean.trustCompiler']) 追加、 isNativeDecideAxiom() helper で 統一 check、 classifier logic 更新。

4. Finding #4 (再 scan 中に発見) — timeout too tight

Full re-scan 初回 で 3 新 error (AbcStatement + ExitLayerArithmetic + OrbitCoalescence)、 手動 lake env lean 実行 では 全 exit=0 で 正常。 原因 = execSync timeout 60000 (60 sec) が Mathlib heavy import の cold cache 状態で 超過。 2026-08-16 は cache warm で 60s 内 収まったが 今回 cold で 一部 超過。

Fix = timeout: 60000 → timeout: 600000 (10 min per file)、 コメントで 根拠明示。

5. Test 27/27 PASS

test/step1368-axiom-scan-parser-test.ts = 5 part 27 assertion:

PartCoverageAssertions
Part 1single-line output regression (Finding #2 fix が 既 動作を 壊していない verify)3
Part 2multi-line axiom list (Finding #2 fix verify、 STEP 1340 pre-fix なら 0 parse の cases)3
Part 3native_decide 分類 (Finding #3 fix verify、 4 classify case)13
Part 4sorryAx retain detection2
Part 5mixed multi + single lines interleaved (real-world stdout simulation)6
合計27/27 PASS

npx tsx test/step1368-axiom-scan-parser-test.ts = 27/27 passed, 0 failed。 pipeline logic の 直接 unit test 初 (STEP 1340 では unit test なし、 integration test のみ)。

6. Aggregate delta (2026-08-16 baseline → 2026-08-22 fixed pipeline)

Metric2026-08-162026-08-22delta
Files scanned2932+3
Errors1 (CantorHausdorff empty error)0-1 (Cantor fix)
Total theorems249333+84
Zero-axiom60 (24.1%)94 (28.2%)+34
Mathlib base only (subset)246324+78
Floor ratio98.8%97.3%-1.5 pt ★
sorryAx110 (BrownawellMasser intentional)
Custom axiom220 (BR 2_3 + 3_3 upper honest stub)
native_decide (新分類済)0 (未 detect)6+6 = Finding #3 fix effect
★ Floor 97.3% ≠ 98.8% の 意味: realistic 減少 ではなく 分類 精緻化。 前 98.8% は native_decide 6 を mathlib base に 誤加算 していた 過大評価。 Lean.ofReduceBool + Lean.trustCompiler は 「compile された decision procedure を 信頼」 = 標準 floor だが Mathlib pure base とは 意味論的に 別 category = honest reclassification。 feedback_super_naming_siren_family_pattern 「Mathlib base 100%」 誤 flag 掲げない discipline 継承。
Positive: 6 日 期間 で 新 sorry / 新 user axiom 混入 0 件。 「zero-sorry floor」 discipline 維持 verify。 native_decide 6 分類済 は honest 別 floor category 明示化。

Axiom set distribution (top 9)

#Axiom setCountRatio
1Classical.choice, Quot.sound, propext14744.14%
2(no axioms)9428.23%
3propext6318.92%
4Quot.sound, propext206.01%
5Lean.ofReduceBool, Lean.trustCompiler, propext41.20%
6Lean.ofReduceBool, Lean.trustCompiler20.60%
7BipartiteRamsey.bipartite_ramsey_2_3_upper (honest stub)10.30%
8BipartiteRamsey.bipartite_ramsey_3_3_upper (honest stub)10.30%
9Classical.choice, Quot.sound, propext, sorryAx (BrownawellMasser)10.30%

7. Discipline 継承

  • feedback_session_boundary_rediscovery_2026-08-22 (昨日追加) = 「新規 起草 前 3 手 verify default」 適用 = 本 STEP が discipline の 直接実践例、 「grep で file 実 read」 + 「git log で 起源確認」 + 「MEMORY grep で 位置確認」 の 3 手 で STEP 1340 既実装 発見 → 重複 実装 事故 予防
  • feedback_zero_sorry_floor_not_ceiling = 「床 の 上に 次 の 床」 の 分類 精緻化 (native_decide を 別 floor として 明示化、 mathlib base と 混ぜない)
  • feedback_verify_claim_must_cover_all_source_derived_numbers (今日追加) = aggregate 数値 fabrication 予防 = pipeline 再 scan で 実 verify、 前 98.8% 数字を そのまま 継承しない
  • feedback_projection_self_audit_pattern SAC-4 = Pattern 5 直前防止 42 例目、 「新 pattern 発見 の 度 に 訂正 record」 継続
  • feedback_super_naming_siren_family_pattern = 「Mathlib base 100%」 誤 flag 掲げない = native_decide 6 を honest 別 category として 表示
  • feedback_no_rush_publication = spike 完全 close (fix + 再 scan + aggregate + commit + site 反映 まで 一貫)、 中途 の 「fix したが aggregate 更新 忘れ」 site 反映 default protocol 違反 予防
  • feedback_all_research_site_reflection_default = 2026-08-06 藤本さん永久 protocol、 本 STEP は backend engine 修正系列 に 該当、 site 反映 (本 page)

8. Honest scope

  1. 「世界初」 主張ゼロ (feedback_world_uniqueness_claim_controllable 適用) = 本 STEP は 既 pipeline (STEP 1340) の 4 gap closure layer 位置のみ、 novelty ゼロ。 #print axioms 監査 自体は Lean 4 標準機能。 native_decide axiom marker (Lean.ofReduceBool + Lean.trustCompiler) の 検出は Lean 4 内部 knowledge、 novelty ゼロ。
  2. Aggregate 数値 は AxiomCheck file に 限定 = 333 theorem は data/lean4-mathlib/**/*AxiomCheck.lean で #print axioms 対象に 挙げられた theorem のみ、 Rei stack Lean 4 累計 3,521+ theorem body の 全網羅ではない。 AxiomCheck 未登録 の theorem の axiom profile は 本 scan の scope 外。
  3. Floor 97.3% は 分類 精緻化 の 結果、 前 98.8% からの 「悪化」 ではない。 前は native_decide 6 を mathlib base に 誤加算 = 過大評価。 本 fix で 精緻化。 逆に 「上がった」 metric として 誤解 されないよう UI で 明示 (本 page § 6 の honest note)。
  4. BrownawellMasser sorry (1 件) は 意図的 withdrawal-line design、 bug でも gap でもない。 STEP 1291 Deliverable B 明示 documented、 Deliverable C (n≥4 proof) は Voloch-Snyder analysis weeks 別 STEP defer 継続。
  5. BR 2_3 + 3_3 upper (custom axiom 2 件) は 意図的 honest stub、 Mathlib PR pending の 独立 stub file (STEP 1308 v0.3 で 分離) で 意図的。 これも bug でも gap でもない。
  6. timeout 600s は 経験則 上限、 個別 Mathlib heavy file が それ以上 かかる 場合 (例: STEP 950 Aliquot が 37 min という REPRODUCIBILITY.md 記載) は 追加 tuning 必要。 現状 32 file の scan 実測 total ~10 min で 収まった (cache warm)、 cold 時 でも 個別 87s / 124s max 実測。
  7. Pipeline auto-daily 化 は 本 STEP scope 外。 現状 手動 実行 依存、 daily/週次 GitHub Actions or research-radar への 組み込みは 別 STEP candidate。

9. Related

  • Commit: bfa13bb91 (2026-08-22、 10 files / +2611 / -580)
  • Memory: project_step1368_axiom_scan_pipeline_hardening_2026-08-22.md
  • Scan output: data/axiom-cost-atlas/strict-lean4-scan.{json,md,per-theorem.json} (refreshed) + data/axiom-cost-atlas/delta-scan-2026-08-22.{json,log} (delta 記録)
  • Fixed script: scripts/lean4-strict-axiom-scan.ts (parser + classifier + timeout 3 fix)
  • Test: test/step1368-axiom-scan-parser-test.ts (27/27 PASS)
  • Fixed AxiomCheck: data/lean4-mathlib/CantorHausdorffDimensionAxiomCheck.lean (4 rename + 1 削除)
  • Origin STEP: STEP 1340 arc (2026-08-16 commit 22895901d、 「chat-Claude Ω/⊘/⟲ + strict scan + 井筒 audit + site」 6 item 束)
  • Related STEP: STEP 1291 (BrownawellMasser sorry origin) / STEP 1308 (CantorHausdorff v0.3→v0.5 pivot、 Finding #1 root cause) / STEP 1367 (直前 STEP、 rei-checker-mcp Lean 4 REPL harness、 domain 独立)
  • chat-Claude arc: 「反証以上」 turn 1-4 (2026-08-22)、 5 検査機 + 3 コネクタ提案 catalog。 残 提案 (仮定実効性、 次の一手推薦、 独立性/非自明性、 還元/統合 etc.) は 藤本さん judgment 次第 で 別 STEP