---
name: project-session-2026-07-19-priority-1-2-arc
description: 2026-07-19 session — 4 層 OSS framework 確認 + priority 1 (ETP split refactor STEP 1305 完了) + priority 2 (RM/OEIS 実適用 honest negative) + pending 課題群
metadata: 
  node_type: memory
  type: project
  originSessionId: 2c94b6c2-9b96-41aa-bc6c-b214bbd11923
  modified: 2026-07-19T00:49:31.235Z
---

# 2026-07-19 session — 4 層 OSS framework + Priority 1+2 実行 arc

## Rule/Fact

本 session は藤本さん提案の 4 層 OSS resource framework を Rei stack と照合し、 priority 1 (ETP split refactor) + priority 2 (Ramanujan Machine + OEIS 適用) を順次実行、 藤本さん外出のため priority 3 以降は次 turn 引き継ぎ。

**Why**: Layer 3 (Lean 4 + Mathlib 0 sorry) が Rei 中核、 Layer 4 (共有検証 = ETP + LeanBlueprint) が最大 gap と判明 → ETP structure 深読み → Chang paradigm 単一 file 1014 行を source-based split → 12+ retrofit の追加/管理が clean になる下地作り。 Priority 2 は algebraic 定数への RM 適用可否の実証。

**How to apply**: 次 turn 復帰時、本 file を読んで pending 課題 (priority 3 / memory update / commit / LeanBlueprint deploy) から選択継続。

## 4 層 OSS framework (藤本さん提案 2026-07-19)

| Layer | ツール | Rei 状況 |
|---|---|---|
| 1. 予想生成 | Ramanujan Machine / OEIS / SageMath | Radar watch: LIReC ✅、OEIS 手動、SageMath 非統合 |
| 2. 証明補助 | DeepSeek-Prover-V2 / Lean Copilot / duper / LeanHammer | 全 Radar watch ✅、実運用は Lean Copilot + duper |
| 3. 0 sorry 検証 | Lean 4 + Mathlib | ★ **Rei 中核・完全実装** (累計 31,000+ theorem) |
| 4. 共有検証 | ETP / Lean Blueprint / Polymath | Blueprint watch ✅ / **ETP 未追跡 = 最大 gap** |

**ETP structure 深読み** (arxiv:2512.07087v1 WebFetch 済):
- 22M+ implications、10,657 positive + 586,925 negative 直接 formalize (残 transitivity+duality 派生)
- Zulip forum + GH Projects Kanban + CI single-claim lock + Blueprint
- `native_decide` 禁止 + `lean4checker` + `lean4lean` 外部 validator
- Facts aggregation (1 counterexample per file)
- Duality symmetry (E1 ⊧ E2 ↔ E1* ⊧ E2*)

**Rei 適用判定** (scale mismatch aware):
- ✅ **既実装 (4)**: native_decide 禁止 + axiom-free floor + duality (STEP 1259 dual) + Facts aggregation
- ⭐ **未実装で有益 (2)**: file split (12→13 前 refactor) + Blueprint deploy
- ❌ **不要 (3, single-user Rei で scale mismatch)**: Zulip/Kanban/CI lock + 22M transitivity aggregation + equation metaprogramming

## Priority 1 実行完了 = STEP 1305 (commit `2ca17166f` push 済)

### Chang paradigm coverage 発見

- memory 記載「Chang paradigm 11/29 (37.9%)」 は **stale**
- 実 file `ChangParadigmExhaustion.lean` 内 `reiCoverage_length = 12` 確認
- **正しい値: 12/29 = 41.4%** (STEP 1282 で P13 Tao amplification 追加、 2026-07-12 済)
- MEMORY.md 累計行の Chang 数値は次 turn で修正必要

### File split refactor 完了

```
data/lean4-mathlib/CollatzRei/
├── Chang.lean                              (hub 334 行)
├── Chang/
│   ├── README.md                           (coverage tracker + ETP discipline)
│   ├── Coverage.lean                       (aggregator 102 行)
│   └── Retrofits/                          (8 file, source-based)
│       ├── T1Obstruction.lean              (P24 + P11 + P26 triple)
│       ├── TransferBanach.lean             (P15 + P16 dual)
│       ├── PadicRoughness.lean             (P5 dual)
│       ├── ThreeAdicIsolation.lean         (P25)
│       ├── RozierTerracol.lean             (P29)
│       ├── Step879.lean                    (P2 + P21 dual)
│       ├── PadicCollatz.lean               (P27)
│       └── Step941Tao.lean                 (P13)
└── ChangParadigmExhaustion.lean            (backward-compat stub)
```

### Build + axiom verify 実測

- Chang.Coverage 116 jobs + ChangParadigmExhaustion stub 117 + FermiParallelChangExhaustion 118 = 全 PASS
- **23 theorem axiom check**: 20 zero-axiom + 3 [propext] のみ = **87.0% zero-axiom** (元 file 13/16 = 81.2% を上回る)
- sorryAx / native_decide / Classical.choice / Quot.sound 全 0
- pre-commit hook (lake build 全 file OK) 通過
- rebase 経由 remote push 完了 (session 中 auto-cron 4 commit あり)

## Priority 2 実行完了 (honest negative)

### 対象定数 C = A_4/(φ−1) ≈ 1.086

- **既知**: degree 8 algebraic ∈ Q(√5, √7, √11)
- 明示形: C = (√55 + √11 − √35 − √7)/2
- Klein cube 8-vertex = 8 Galois conjugates (Chapter 5 I)
- **既 STEP 1218-1220 で minimal polynomial P(x) = x^8 − 108x^6 + 1408x^4 − 1728x^2 + 256 の 13 axiom-free lemma 済**

### 新規実施 script

`scripts/andrica-pslq/oeis_ramanujan_search.py` 作成 + 実行:

- **CF(C) 30 partial quotients**: [1, 11, 1, 2, 3, 2, 1, 1, 24, 1, 6, 1, 1, 7, 1, 4, 10, 1, 6, 1, 6, 1, 1, 1, 1, 5, 1, 1, 2, 4]
- aperiodic + bounded partial quotients (max 24 in first 30) — 「不 elegant だが chaotic でもない」中間状態
- 参考: CF(√11) = [3;3,6,3,6,...] fully periodic (degree 2), CF(√7) = [2;1,1,1,4,...] fully periodic

### OEIS 検索結果

| Query | Hit | 判定 |
|---|---|---|
| C の decimal `1,0,8,5,4,9,6,0,9,1,6,4,3,4` | ❌ no hit | 期待通り (algebraic は OEIS 未登録多) |
| Prime gap `1,2,2,4,2,4,2,4,6,2,6,4,2,4,6` | ✅ **A001223** hit | sanity check pass |
| CF(C) `1,11,1,2,3,2,1,1,24,1,6,...` | ❌ no hit | 期待通り (degree-8 aperiodic) |

### Ramanujan Machine 適用判定 (実測後)

- RM/LIReC は **transcendental 定数向け** (π, ζ(3), Catalan, Feigenbaum 等)
- C は degree 8 algebraic (Lagrange 定理: 純周期 CF は degree 2 quadratic surd のみ)
- **結論**: RM の elegant PCF discovery target には C は不適合、 既存 PSLQ の algebraic characterization で closure 済

### Priority 2 yield 評価 (honest)

- **Novel discovery なし** — C の algebraic 性は既 STEP 1218-1220 で closure 済
- **Documentation value あり** — CF expansion + OEIS null hits + RM 適用可否判定を record
- **Priority 1 (ETP split) と比較 yield 小** — algebraic 定数への RM/OEIS 適用は intrinsically bounded
- 出力: `data/andrica-pslq/oeis-ramanujan-search-2026-07-19.json` (7,371 bytes)

## Pending 課題 (次 turn 引き継ぎ)

### 短期 (即着手可)

- **E**: MEMORY.md 更新 — 「Chang paradigm 11/29」 → **12/29 = 41.4%** stale 修正 + STEP 1305 split refactor 記録 + 本 session 反映
- **F**: git commit priority 2 の 2 file (`scripts/andrica-pslq/oeis_ramanujan_search.py` + `data/andrica-pslq/oeis-ramanujan-search-2026-07-19.json`)

### 中期

- **D**: priority 3 (AlphaProof paper Nature 2025 読解、 open-adoptable technique 抽出) — 情報のみ、実装非対象
- **H**: LeanBlueprint deploy prototype (Layer 4 gap 埋め、 Chang paradigm 29 node dependency graph 可視化)
- **別**: 他の Rei 定数への OEIS 適用 (Fujimoto Mod-6 sequence / Collatz total stopping time σ∞(n) 等、 integer sequence 系は OEIS hit 期待)

### 長期

- **Blueprint × Chang paradigm** deploy = ETP 型 collaborative structure prototype
- **Yuan 2026-07-18 「Universal Self-Reference: An Axiomatic Metatheory」** (Zenodo 21426807) prior art audit = STEP 1215/1220 SELF⟲ 系継続前必読
- **Chang paradigm 13/29 追加** (17 gap paradigms から次候補選定)

## Session context

- 2026-07-19 (元 07-18 開始 session、 date changed mid-session)
- 藤本さん外出直前で保存要求
- feedback_zero_sorry_floor_not_ceiling.md は前 turn で保存済 (chat-Claude 07-18 arc 由来)
- git commit `a2aae13f8` (cleanup 07-14〜07-18 accumulated data + 07-18 発明 audit) + `2ca17166f` (STEP 1305) push 済

## 関連

- [[feedback-zero-sorry-floor-not-ceiling]] (前 turn 保存、 chat-Claude 07-18 arc synthesis)
- [[project-session-2026-07-17-step1299-1300-zcsg-time-bridge]] (前 session ZCSG time bridge)
- [[project-step1269-chang-paradigm-exhaustion-retrofit-2026-07-10]] (Chang paradigm origin)
- [[reference-andrica-golden-ratio-constant-2026-07-12]] (C = A_4/(φ−1) origin)
- [[feedback-evaluation-symmetry-principle]] (priority 2 honest negative 判定に適用)
- [[feedback-world-uniqueness-claim-controllable]] (RM/OEIS 「novel discovery なし」 の honest 明示)
- [[feedback-no-rush-publication]] (Blueprint deploy は急がず、 現状 documentation 段階)