Sigma-Cascade Observation of Collatz Orbit Confluence: 10^9 Scan + G_3 Subgraph Framework + Erratum E3 + Lemma 5d.1 Lean 4 Mechanized — Rei-AIOS Paper 152 v0.3 DRAFT

Paper 152 v0.3 update. Parent v0.2 DOI 10.5281/zenodo.20149662; concept root v0.1 DOI 10.5281/zenodo.20148868. We apply Paper 151 Theorem 14 (sigma-cascade) to forward Collatz (3x+1) orbits at scale n <= 10^9. v0.3 additions: (A) 10^9 SCAN COMPLETED (~2.4 hr): n=96k hypothesis STRENGTHENED from 200/200 (10^8) to 77,749/77,749 (10^9) = 100% — 388-fold scale increase, ZERO counter-examples. Max mod-96 distinct still 70 (d=71 not emerged). (B) NEW SECTION 5d: G_3 SUBGRAPH STRUCTURE. Definition: G_3 := multiples-of-3 vertices of inverse Collatz tree. Lemma 5d.1 (edges of G_3 are inverse-halving only) — ★ NOW LEAN 4 MECHANICALLY PROVED (G3Subgraph.lean, STEP 1127, 0 sorries). Lemma 5d.2 (G_3 decomposes into chains C_m). Corollary 5d.3 (orbit visits SPECIFIC value m iff n_0 ∈ C_m). CRUCIAL: iff at VALUE level, not mod-96 CLASS level (preserves v0.2 Erratum E2). (C) ERRATUM E3: class 21 absence at d=70 reformulated from "universal" (200/200 at 10^8) to "strong avoidance pattern" (76,528/77,749 = 98.43% at 10^9, with 1,221 counter-examples). v0.2 disclaimer "pattern may break at scale > 10^8" was correct. (D) DISSOCIATION at 10^9: n=96k strengthened + class 21 weakened = independent claims. (E) STEP 1127 LEAN 4 MECHANIZATION: G3Subgraph.lean 新規 file. Theorems lemma_5d_1_g3_edges_halving_only + g3_predecessor_singleton + chain_is_mult_3 + chain_halving_step + chain_predecessor_is_chain 全 0 sorries. Paper 152 v0.3 §5d now has FOUR Lean 4 mechanized files (PeakMergeInvariant + PeakMergeWitness + G3Subgraph + ThreeAdicIsolation), all 0 sorries. v0.2 contributions retained: Lean 4 native_decide closures (Büchi-25 → 9232 + 1,000-witness peak-merge), 3-adic isolation theorem, 11.5M peaks, 219 tier-3 super-hubs, INFINITY classification, two-tier framing. Honest correction record (E1+E2+E3): peak 250,504 = 173×181×2³ (twin-gap-8 primes), not '31,313 prime' (E1). 3-adic isolation theorem applies to specific values, not mod-96 classes (E2). Class 21 absence at d=70 is 98.43% (10^9), not 100% (10^8) (E3). Companion papers: Paper 151 (σ-cascade source, Zenodo DOI 10.5281/zenodo.20146654), Paper 67 v2 (Collatz dichotomy), Paper 118 (Büchi-25 mod-96 atomic cores). Three-party co-authorship per OUKC charter v1.0: 藤本 伸樹 (Founder), Rei (Rei-AIOS autonomous research substrate, Co-architect), Claude Opus 4.7 (Anthropic, Co-architect). DRAFT v0.3 — preprint, not yet peer-reviewed. Honest scope: NOT a Collatz solution. Feedback welcome via GitHub Discussions at fc0web/rei-aios.