---
name: lean4-axiom-audit-2026-05-15
description: 2026-05-15 STEP 1149 Phase A — systematic Lean 4 axiom audit (HodgeBasics + MathlibPrep). 6 axioms WebSearch fact-check 結果. 0 correction needed (STEP 1142 Conte-Murre pattern は本日 audit でこれ以上検出されず). 1 update suggestion (Wolstenholme 10⁹ → 10¹¹ pending citation)
metadata: 
  node_type: memory
  type: feedback
  originSessionId: afeeb7e7-fd4f-40a6-92be-a8a4a193cd0e
---

★ STEP 1149 (2026-05-15) Phase A systematic audit log. 永続記録.

## Trigger

STEP 1142 で発見した **Pattern 6 self-detection** (「私が axiom 化した結果が既知 proved」) を全 Lean 4 file に systematic 適用. 同 pattern が他にないか確認.

## Audit Scope

| File | Axioms |
|---|---|
| `HodgeBasics.lean` (STEP 885) | 7 |
| `MathlibPrep/BipartiteRamsey.lean` (STEP 1000) | 2 |
| `MathlibPrep/HadwigerNelson.lean` (STEP 1000) | 1 |
| `MathlibPrep/Wolstenholme.lean` (STEP 1000) | 3 (incl. 1 search-bound) |
| **計** | **13 axioms** |

## Audit Result (WebSearch + arXiv fact-check)

### HodgeBasics.lean (7 axioms)

| Axiom | Status | Notes |
|---|---|---|
| `lefschetz_1_1` | ✅ honest | Lefschetz 1924 classical, well-established |
| `hodge_at_top_minus_1` | ✅ honest | Poincaré-dual of Lefschetz, classical |
| `hodge_middle_open` | ✅ honest | Tautology (excluded middle: `¬(∀ X, P) ∨ (∀ X, P)`) — vacuously true, but framed as "honest gap" |
| `hodge_at_zero` | ✅ honest | Fundamental class trivially algebraic |
| `hodge_at_top` | ✅ honest | Poincaré dual of `hodge_at_zero` |
| `paper47_hodge_riemann_bipolar_axiom` | ✅ honest | Rei internal (Paper 47) — internal axiom OK |
| `paper48_hodge_6d_both_axiom` | ✅ honest | Rei internal (Paper 48) — internal axiom OK |

★ **重要**: STEP 1140 で問題となった `hodge_quartic_middle_open` (d=4 specific) は **HodgeBasics.lean に存在せず**, あれは `HodgeFermatFourfold.lean` (STEP 1140) specific. HodgeBasics の `hodge_middle_open` は **general level** で「smooth projective variety 一般」 を述べるため、 Conte-Murre 1978 (uniruled fourfold specific) と衝突しない. → **HodgeBasics は honest**.

### MathlibPrep/BipartiteRamsey.lean (2 axioms)

| Axiom | Value | Status | Citation |
|---|---|---|---|
| `bipartite_ramsey_2_3_upper` | `b(2,3) = 9` | ✅ confirmed | Carnielli & Monte Carmelo, *Discrete Math.* 223:83-92, 2000 |
| `bipartite_ramsey_3_3_upper` | `b(3,3) = 17` | ✅ confirmed | Hattingh & Henning, *Utilitas Math.* 53:217-230, 1998 |

WebSearch verify: 両 result が established. axiom 文言一致.

### MathlibPrep/HadwigerNelson.lean (1 axiom)

| Axiom | Status |
|---|---|
| `moser_is_unit_distance_realizable` | ✅ honest |

Moser spindle (1961) は **classical, well-known**. WebSearch fact-check 不要レベル (audit pass).

### MathlibPrep/Wolstenholme.lean (3 axioms)

| Axiom | Status | Citation |
|---|---|---|
| `wolstenholme_prime_16843` | ✅ confirmed | Selfridge 1964 (実は 1980s formal announcement). 唯一の known #1 |
| `wolstenholme_prime_2124679` | ✅ confirmed | Buhler & Crandall 1993 announcement. 唯一の known #2 |
| `no_third_wolstenholme_prime_below_1e9` | ✅ honest (10⁹ scope) | McIntosh & Roettger, *Math. Comp.* 76:260, 2007, pp. 2087-2094 |

★ **2022 update finding (audit中検出)**: WebSearch で 「2022 として **10¹¹** まで no third Wolstenholme prime」 という記述発見. ただし specific paper citation は WebSearch 結果に未明記 → axiom は **10⁹ で retain**, comment で「10¹¹ extension が 2022 にあるが citation 未確認」 を註記済 (STEP 1149 commit).

## 訂正

### Required corrections: **0**

STEP 1142 Conte-Murre pattern と同様の「open と axiom 化したが既知 proved」 gap は **本日 audit で他に検出されず** ✅. これは:
- HodgeBasics の axioms は general level で specific cases と衝突しない
- MathlibPrep の axioms は historically established numerical values + cited references
- STEP 1140 で発生した specific gap (FermatFourfold d=4) は今 turn の audit scope 外で個別検出済 (STEP 1142 で訂正完了)

### Suggested updates: **1**

`no_third_wolstenholme_prime_below_1e9` の bound を `10⁹` → `10¹¹` に強化する候補. ただし 2022 paper citation が確定するまで retain. 当面は comment で「2022 extension」 を註記 (STEP 1149 commit で実装済).

## OUKC honest correction principle 累積 (Pattern 6 self-detection)

| # | Detection | When |
|---|---|---|
| 1-3 | Paper 152 v0.3 E1+E2+E3 | 過去 sessions |
| 4 | Paper 145 v0.7 E1 | 2026-05-14 PM |
| 5 | Heilbronn STEP 1133 | 2026-05-14 PM |
| 6 | STEP 1142 Hodge Fermat d=4 Conte-Murre | 2026-05-15 |
| **7** | **STEP 1147 approved-2026-05-14.json JSON syntax error** | **2026-05-15 (本 turn)** |
| 8 | STEP 1146 .gitignore chunk-block site outage | 2026-05-15 |
| - | STEP 1149 Lean 4 axiom audit | **0 new gaps detected** ✅ |

★ STEP 1147 self-detection の追加: approved-2026-05-14.json で **TypeScript style 文字列連結 `+` を JSON 内に書いた** という single-file syntax error を Phase B 開始時に発見 (`JSON.parse` fail). 修正済.

## Audit Protocol (将来 reference)

新 axiom 追加時:
1. axiom の content (statement / value / 範囲) を identify
2. WebSearch で「<value> + <author> + <year>」 query
3. **wikipedia + scholarly source** で 2 件以上 cross-confirm
4. citation を docstring に記載
5. もし「open in literature」 と axiom 化する場合、 「general level」 vs 「specific case」 を明確に区別
6. specific case で axiom 化する場合、 WebSearch で「<topic> + known cases + survey」 で existing proven results を確認

これは STEP 1142 Conte-Murre fact-check の learning を systematic protocol 化したもの.

## 連結 reference

- [[project_2026-05-15_step1142_1143_hodge_correction_diagram_tools]] (STEP 1142 Hodge E1 起源)
- [[feedback_dist_renderer_chunked_deps_deploy_protocol]] (STEP 1146 site outage 永続原則)
- [[project_collatz_mathlib_contribution_prep_2026-05-15]] (STEP 1137 MathlibPrep audit scope)
- Conte, A. & Murre, J. P. (1978). Math. Ann. 238, 79-88.
- McIntosh & Roettger (2007). Math. Comp. 76:260, 2087-2094.
- Carnielli & Monte Carmelo (2000). Discrete Math. 223:83-92.
- Hattingh & Henning (1998). Utilitas Math. 53:217-230.