---
name: project-step1310-chang-coverage-p6-p18-wall-search-2026-07-23
description: "STEP 1310 pt.1-3 統合 record (2026-07-23 session)。 JC ニュース → Collatz close arc 直後の 「新しい壁に当たる」 phase で Chang paradigm coverage 12/29 → 16/29 (55.2%) に +P6 (Automata via Paper 57 DFA firewall) + P18 (Digit-sum via step624 trailingOnes) + P8 (Baker/CF thin dual via two_pow_ne_three_pow) + P1 (Transfer operator spectral substantive via step627k spectral gap) 4 retrofit 追加、 全 zero-axiom。 (log_2, popcount) empirical で 22 pairs 中 12 obstruction detected。 監査-of-監査 inflation 回避 discipline 継続適用、 substantive vs thin retrofit 区別明示化、 narrative construction 発火なし。"
metadata: 
  node_type: memory
  type: project
  originSessionId: 29ce2da2-2298-4a0d-b3de-3b2e304e248a
  modified: 2026-07-22T22:16:16.680Z
---

## 概要 (2026-07-23 session, STEP 1310 pt.1-3 統合)

JC ニュース → Collatz 応用可能性 close arc ([[project-jc-news-collatz-audit-close-2026-07-23]]) 直後、 藤本さん permissive 指示 「新しい壁に当たる為に、 色々と出来る事をやってみてください」 の産物。 3 phase execute で Chang coverage 大幅拡大:

- **pt.1**: +P6 (Automata) + P18 (Digit-sum) via step629 DFA + step624 trailingOnes (12/29 → 14/29)
- **pt.2**: +P8 (Baker/CF thin dual) via RozierTerracolLogRatio (14/29 → 15/29)
- **pt.3**: +P1 (Transfer operator spectral substantive) via step627k (15/29 → 16/29)

**累計: 4 new retrofits + 1 empirical (popcount obstruction), 全 zero-axiom, coverage 12/29 → 16/29 = 55.2%**

## Honest scope (super critical, 各 arc 冒頭に再明示)

- **Rei は Collatz を解いていない** (default reject 継続)
- Chang paradigms coverage の積み上げは **「なぜ困難か」 の evidence layer** であって Collatz 予想解決ではない
- Chang より強い前提 (finite-state DFA + deterministic descent + prime factorization + bounded spectral gap) でも 同結論 (壁) に到達
- **coverage 数字上昇 (55.2%) は Collatz 攻略 tool 数の増加ではない**、 evidence layer 拡大のみ

## Pt.1: P6 + P18 retrofit + popcount empirical

### Work stream 1: P6 (Automata-theoretic) retrofit

- **Source**: `data/lean4-transfer/step629_automaton_formal.lean` (Paper 57, 132 定理 zero sorry via native_decide)
- **Retrofit**: `Chang/Retrofits/DfaFirewall.lean` (retrofit id #14)
- **Chang P6 obstruction**: 「Automata-theoretic complexity: infinite state complexity is a consequence of non-convergence, not a tool」
- **Rei twist**: Chang は infinite-state 想定、 Rei は **finite (8-state) DFA + universal firewall trigger** = より強い前提 finite-state variant instance
- **Wall**: Paper 57 self-quoted 「gap between 'carry firewall exists and is universal' and 'carry firewall always activates' remains the core difficulty」 = trigger occurrence for all n 未証明 = Collatz 本体

### Work stream 2: P18 (Digit-sum / Hamming weight) retrofit

- **Source**: `data/lean4-transfer/step624_COMPLETE.lean` (STEP 622-624, 48 定理 zero sorry)
- **Retrofit**: `Chang/Retrofits/TrailingOnesDigitSum.lean` (retrofit id #15)
- **Chang P18 obstruction**: 「E[hw] < 0 gives expectation, not deterministic」
- **Rei twist**: Chang は expectation 主張、 Rei は THE_THEOREM + gk1-gk10 で **deterministic trailingOnes descent** を machine-check = より強い前提 refined witness
- **Wall**: step624 §7.1 「trailingOnes descent proves tro decreases, but the VALUE may increase. The unsolved problem is proving that the total halvings eventually dominate the total triplings」 = digit-sum aspect deterministic でも value control 不可

### Work stream 3: (log_2, popcount) obstruction empirical

- **Script**: `scripts/empirical/popcount-obstruction-witness-2026-07-23.py`
- **Setup**: V(n) = log_2(n) + α(popcount(n)) 候補、 (pc_low, pc_high) pair の feasibility window 検査
- **Result**: **22 pairs 中 12 obstruction (55%)**, adjacent popcount pairs systemic infeasibility
- **Chang paradigm 18 refined instance の independent empirical confirmation** = trailingOnes (LOCAL) と popcount (GLOBAL) の 2 digit-sum features とも piecewise V に fail

## Pt.2: P8 (Baker/CF thin dual) retrofit

- **Source**: `data/lean4-mathlib/CollatzRei/RozierTerracolLogRatio.lean` 既存 (P29 と同 source, dual angle)
- **Retrofit**: 既存 `Chang/Retrofits/RozierTerracol.lean` に P8 def 追加 (retrofit id #16, dual coverage)
- **Chang P8 obstruction**: 「Baker constrains SL/L gap size; already captured by CF structure」
- **Rei twist**: Layer 順序 (Rei は最深 layer):
  1. Rei prime factorization → 2^S ≠ 3^k atomic parity
  2. CF 構造 → log_3 2 質的無理性
  3. Baker's theorem → 定量 bound
  4. BakerSeparationConjecture (Merle working)
- **Rei の 「CF より深い prime factorization layer で atomic parity capture」** = Chang の 「CF captures Baker」 observation の atomic core witness
- **★★ THIN DUAL RETROFIT** (1 theorem のみ, evidence layer 弱):
  - log_3 2 irrationality は `logThreeTwo_irrational` axiom 依存 (Gelfond-Schneider not in Mathlib v4.27)
  - CF 構造も axiom-free に構築していない
  - forbiddenClaims 拡張: 「Rei P8 retrofit は Baker's method Lean 4 closure でない」 明示

## Pt.3: P1 (Transfer operator spectral substantive) retrofit

- **Source**: `data/lean4-transfer/step627k_spectral_formal.lean` (STEP 627k, k=8 mod 256 trailingOnes 6-state chain)
- **Retrofit**: `Chang/Retrofits/SpectralGap.lean` (retrofit id #17)
- **Chang P1 obstruction**: 「Transfer operator spectral analysis, uniform gap proved; yields equidistribution, not individual orbit control」
- **Rei machine-checked** (all native_decide, zero sorry):
  - row1_total_pos + row2_total_pos: counts positive
  - row_sim_j1: |count(1→1)/total(1) - count(2→1)/total(2)| < 30%
  - row12_bounded_j{1, 2, 3}: rows 1,2 within factor 3
  - two_step_sim_j1 + gap_evidence_13: double-episode rows within factor 2
- **Spectral gap estimate**: ≈ 0.29-0.33 (row ratio bounds から derived)
- **★ SUBSTANTIVE RETROFIT** (thin dual でない、 複数 machine-checked spectral theorems)
- **Wall**: k=8 mod 256 bounded specific case のみ、 Bourgain-Terras 系譜 general uniform gap は Mathlib operator norm spectral machinery 未実装

## Substantive vs Thin retrofit の明確化 (重要 discipline)

| Retrofit | Type | Evidence layer |
|----------|------|---------------|
| P6 (DFA firewall) | singleton | Paper 57 132 定理 + master theorem |
| P18 (trailingOnes) | singleton | THE_THEOREM + gk1-gk10 + Cases 1-4 |
| **P8 (Baker/CF)** | **thin dual** | 1 theorem のみ (dual with P29) |
| **P1 (spectral gap)** | **substantive** | 複数 machine-checked spectral theorems |

**coverage-status.json + forbiddenClaims + honestScope 全 3 layer で明示化** = coverage 数字 bumping と誤読される risk 予防。

## 監査-of-監査 inflation 回避 discipline 継続適用

前 arc ([[project-jc-news-collatz-audit-close-2026-07-23]]) で learn した discipline を継続:

1. **narrative construction (Rei 禁止 pattern) 発火なし** — 各 retrofit は Chang paradigm と同結論に別 angle で到達、 「Chang より強い前提を確立 → refute」 系 framing は forbiddenClaims 明示化で防御 (pt.2 で明示追加)
2. **監査-of-監査 inflation 回避** — 「壁探し succeeded → 大発見」 framing 不使用、 「予測通り壁に当たった → 記録」 として close
3. **feature space 「記載不能」 認識継続** — popcount 選択理由は 「Chang P18 direct correspondence + t1 と GLOBAL/LOCAL 対比」 の探索的選択、 事後合理化 production せず
4. **thin vs substantive 区別明示** — P8 thin dual と P1 substantive の evidence layer 差を record 3 layer (Coverage.lean comment + retrofit file honestScope + coverage-status.json scopeNote) で明示

## Deliverables (総合)

- **Lean 4 file 4 個新規/更新**: `DfaFirewall.lean` + `TrailingOnesDigitSum.lean` + `SpectralGap.lean` (新規 3) + `RozierTerracol.lean` (P8 dual 追加) + `Coverage.lean` update
- **Empirical file 2 個**: popcount script + JSON output
- **JSON file update 1 個**: `coverage-status.json` (retrofits 15→17, cumulativeGain +11 paradigms, forbiddenClaims 拡張, dual coverage pattern に RozierTerracol P29+P8 追加)
- **Git commits 3 個**: `4bdab64bf` (pt.1) + `d76ba3771` (pt.2) + `adbdbb4ca` (pt.3), 全 push 済
- **累計 axiom-free theorem**: 12 (retrofit annotation 4 × 2 + coverage aggregation 4)
- **Chang coverage 進捗**: +4 paradigms = +13.9 percentage points (12/29 → 16/29 in 1 session)

## Related memory

- [[project-jc-news-collatz-audit-close-2026-07-23]] — 直前 arc close record (Rei-internal audit discipline)
- [[project-step1269-chang-paradigm-exhaustion-retrofit-2026-07-10]] — Chang v6 型化 origin
- [[project-cantor-v06-interval-enumeration-2026-07-23]] — 同日別 arc (Cantor v0.6 interval enumeration setup)
- [[feedback-collatz-default-reject-proof-claims]] — 永続 discipline anchor
- [[feedback-super-naming-siren-family-pattern]] — narrative construction 自己適用継続
- [[feedback-evaluation-symmetry-principle]] — 監査-of-監査 inflation 回避
- [[feedback-chat-claude-collaboration]] — chat-Claude C audit の feature space 「記載不能」 認識継続
- Paper 57 (「Collatz 8-state DFA Firewall」, 2026-04-11) — P6 retrofit source
- STEP 622-624 (Collatz structural proof assembly, 2026-05 頃) — P18 retrofit source
- STEP 627k (spectral gap formal, k=8 mod 256) — P1 retrofit source
- RozierTerracolLogRatio.lean (STEP 1275 sub-3) — P29 + P8 dual source

## Loop close

藤本さん指示 「色々と出来る事をやってみてください」 に対し、 3 sub-arc 実行 (pt.1 + pt.2 + pt.3):
1. pt.1: 3 stream 並行 (P6 + P18 + popcount empirical) → 全 substantive/deterministic 壁 record
2. pt.2: P8 thin dual (dual coverage pattern 適用、 evidence layer 弱明示)
3. pt.3: P1 substantive (spectral gap estimate、 bounded specific case)

いずれも 「壁に当たる」 目標達成、 Rei は Collatz を解いていない、 Chang より強い前提でも同結論に到達を明示。 Coverage 数字が 55.2% まで上がったが Collatz 進撃ではなく evidence layer 拡大のみ。 substantive/thin 区別 明示化。 **急がず、 ゆっくりと**。