---
name: project-step1368-axiom-scan-pipeline-hardening-2026-08-22
description: "STEP 1368 — chat-Claude 「反証以上」 arc B \"#print axioms 監査\" spike → Pattern 5 blindness 直前防止 (STEP 1340 既実装発見) → 3 findings 発見 + 4th (timeout) 発見 → 全 fix → 再 scan → aggregate refresh (249→333 theorem、 floor 97.3%、 native_decide 6 分類済)"
metadata: 
  node_type: memory
  type: project
  originSessionId: 455ea334-b212-4768-ae25-75bc985b2196
  modified: 2026-08-22T03:04:55.707Z
---

# STEP 1368 — Axiom scan pipeline hardening (2026-08-22)

## 起点

chat-Claude 「反証以上」 arc (turn 1-4) で 提示された 5 検査機 + 3 コネクタ提案 の うち、 私が Option (i) 「#print axioms 監査」 を 実装優先度 top と 推奨、 藤本さん 承認 → 実装 spike 開始。

## Pattern 5 blindness 直前防止 (SAC-4 subtype 32 例目)

Spike 着手 3 手目 で `scripts/lean4-strict-axiom-scan.ts` (243 行) が STEP 1340 arc Item 1 of 6 (2026-08-16 commit `22895901d`) で **既 完成 + 6 日前 実行済** と 判明。 32 個の `*AxiomCheck.lean` file と `data/axiom-cost-atlas/` output も 既 存在。 私 が spike で 新規実装 していたら 重複 = 昨日追加 [[feedback-session-boundary-rediscovery-2026-08-22]] Paper 66→177 rediscovery pattern と 同型 事故。

「新規 paper/STEP/tool 起草 前 3 手 verify」 protocol の Lean 4 tool 版 適用実例、 pivot 「重複 実装」 → 「既 pipeline の gap closure」。

## 2026-08-16 baseline 発見 3 gap

Option A (BrownawellMasser sorry 調査) を まず 実行:
- `CollatzRei.BrownawellMasser.brownawellMasser` の sorry は **intentional withdrawal-line design** (STEP 1291、 Deliverable B 明示、 Voloch-Snyder analysis weeks の 別 STEP defer)
- 下流 依存 grep 0 件 = contained state
- `#print axioms` が **意図的 sorry を 確実に検出** = pipeline 健全性 verify
- 「1 sorryAx finding」 は bug でなく discipline の 可視化

Option B (6 file delta scan) を 続けて 実行 = **副次 3 findings 発見**:

### Finding #1 — CantorHausdorff AxiomCheck 5 stale reference

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 出力。 現 regex `[^\]]*` は 改行を 跨げず parse 0。 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 更新。

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

初回 full re-scan で 3 新 error (AbcStatement + ExitLayerArithmetic + OrbitCoalescence)、 手動 実行 では 全 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)、 コメントで 根拠明示。

## Test 27/27 PASS

`test/step1368-axiom-scan-parser-test.ts` = 5 part 27 assertion:
- Part 1: single-line output regression (3 result)
- Part 2: multi-line axiom list (Finding #2 fix verify、 STEP 1340 pre-fix なら 0 parse となる cases)
- Part 3: native_decide 分類 (Finding #3 fix verify、 4 classify case)
- Part 4: sorryAx retain detection
- Part 5: mixed multi + single lines interleaved

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

## Aggregate 更新 (2026-08-16 baseline → 2026-08-22 fixed pipeline)

| Metric | 2026-08-16 | 2026-08-22 | delta |
|---|---:|---:|---:|
| Files scanned | 29 | 32 | +3 (BipartiteRamsey + CantorHausdorff 復活 + 6 new file 網羅済 3) |
| Errors | 1 (CantorHausdorff empty error) | **0** | -1 (Cantor fix) |
| Total theorems | 249 | 333 | +84 |
| Zero-axiom | 60 (24.1%) | 94 (28.2%) | +34 |
| Mathlib base only | 246 | 324 | +78 |
| **Floor ratio** | 98.8% | **97.3%** | **-1.5 pt** (native_decide 6 が 別 category 分類 = honest reclassification) |
| sorryAx | 1 (BrownawellMasser intentional) | 1 (unchanged) | 0 |
| Custom axiom | 2 (BR 2_3 + 3_3 upper) | 2 (unchanged) | 0 |
| **native_decide (新分類済)** | 0 (未 detect) | **6** | +6 = Finding #3 fix effect |

**Positive**: 6 日 期間で **新 sorry / 新 user axiom 混入 0 件**。 「zero-sorry floor」 discipline 維持されている。 native_decide 6 分類済 は honest 別 floor category (Lean.ofReduceBool + Lean.trustCompiler = 「compile された decision procedure を 信頼」 = 標準 floor だが Mathlib pure base とは 意味論 別)。

Floor 97.3% ≠ 98.8% は **realistic 減少 でなく 分類 精緻化**。 前 98.8% は native_decide 6 を mathlib base に 誤加算 していた 過大評価。

## Discipline との 整合

- [[feedback-zero-sorry-floor-not-ceiling]] operational 実践 = 「床 の 上に 次 の 床」 の 分類 精緻化
- [[feedback-verify-claim-must-cover-all-source-derived-numbers]] (今日 追加) = aggregate 数値 fabrication 予防 = pipeline 再 scan で 実 verify
- [[feedback-session-boundary-rediscovery-2026-08-22]] (今日 追加) = 3 手 verify で STEP 1340 既実装 発見 = 重複 実装 事故 予防
- [[feedback-chat-claude-hallucination-warning]] Pattern 5 subtype = 「既実装 の 認知盲点」 34 例目 予防、 私 initial spike route 反省
- [[feedback-projection-self-audit-pattern]] SAC-4 = 「新 pattern 発見 の 度 に 訂正 record」 継続
- [[feedback-no-rush-publication]] = spike 完全 close、 中途 の 「fix したが aggregate 更新 忘れ」 site 反映 default protocol 違反 予防

## Commit 内容

- `scripts/lean4-strict-axiom-scan.ts` (parser + classifier + timeout 3 fix、 8 行 diff)
- `data/lean4-mathlib/CantorHausdorffDimensionAxiomCheck.lean` (4 rename + 1 削除、 6 行 diff)
- `test/step1368-axiom-scan-parser-test.ts` (新規 130 行、 27 assertion)
- `package.json` (test:step1368 entry 追加)
- `data/axiom-cost-atlas/strict-lean4-scan.{json,md,per-theorem.json}` (refresh、 249→333)
- `data/axiom-cost-atlas/delta-scan-2026-08-22.{json,log}` (delta scan 単独記録、 pipeline hardening 経緯 evidence)

明示 除外 (auto data files): `data/{arxiv-*,crypto,buddy,manifold,ligo-events,nasa-sdo,jquants,hf-models,edu-news,eric,gbif-recent,github-edu,inspection-snapshot,learning-log-*,harness-sync*,autonomous-learning-status}.json` 等 cron 生成物 559 file。

## Site 反映 (完了 2026-08-22)

2026-08-06 「全研究 site 反映 default」 protocol 適用、 藤本さん (a) 新規 page 承認で 実行:
- URL: https://rei-aios.pages.dev/tools/step-1368-axiom-scan-hardening/
- Size: 25,004 bytes (public/dist-renderer 両 md5 一致 `0d20abcac380dd8634b9f54eada3f6d3`)
- 9 section: 経緯 + Option A BrownawellMasser 調査 + Delta 3 findings + Finding #4 timeout + Test 27/27 + Aggregate delta + Discipline 7 link + Honest scope 7 条 + Related
- Deploy verify: HTTP 200 + content marker 「STEP 1368 — Axiom scan pipeline hardening」 + 「333 theorem」 + 「97.3%」 全 検出
- Commit: `3aff47356` (site page) + `2bf6ac4a6` (verify status ✅)
- SITE_COVERAGE_MAP.md 新規 subsection 「2026-08-22 STEP 1368 site 化」 追加

## 関連

- [[project-step1367-lean4-repl-harness-v021-stage1-spike-2026-08-22]] — 直前 STEP、 rei-checker-mcp 別 repo、 domain 独立
- [[project-step1291-brownawell-masser-2026-08-08]] — brownawellMasser sorry の 起源 (Deliverable B intentional withdrawal-line design)
- STEP 1340 arc — 既実装 origin (commit `22895901d`、 2026-08-16、 「chat-Claude Ω/⊘/⟲ + strict scan + 井筒 audit + site」 6 item 束)
- STEP 1308 v0.3 → v0.5 (CantorHausdorff pivot 由来、 Finding #1 root cause)
- chat-Claude 「反証以上」 arc turn 1-4 = 本 STEP 起点、 5 検査機 + 3 コネクタ提案 catalog
- [[feedback-super-naming-siren-family-pattern]] = 「果たせない約束を 名乗らない」 discipline、 native_decide 6 「別 floor category」 明示は siren-family 回避 (「Mathlib base 100%」 という 誤 flag を 掲げない)