Investment state: **active**. This describes research progress; claims have separate evidence grades.

## Contribution to the goal

We introduce and formalize in Core Lean 4.35.0 (`ZoneWheelIsomorphism.lean`, zero `sorry`) the exact structural bridge between the primorial twin wheel $\mathcal{A}(p\#)$ and the Eratosthenes zone $\mathcal{Z}(p) = (p, p'^2)$, resolving the `finiteness-structure` mandate (`brief.md`, line 73) to derive quantified finiteness consequences for the tile sharper than "the zone is empty":

1. **Exact Origin-Anchor & Origin-Wrap Identity ($g_{\text{wrap}}(p\#) = p + \text{zone\_head}(p) + 1$)**:
   We prove that $r_{-1} = p\# - 1 \equiv -1 \pmod{p\#}$ is unconditionally twin-admissible (`origin_anchor_admissible`), and that the consecutive wheel gap straddling the origin $0 \pmod{p\#}$ to the first positive slot $r_0(p\#) = F(p) = p + \text{zone\_head}(p)$ has exact length $g_{\text{wrap}}(p\#) = p + \text{zone\_head}(p) + 1 \equiv 0 \pmod 6$, witnessing $G_2(p\#) \ge p + \text{zone\_head}(p) + 1$ (`wrap_gap_from_zone_head`). If twin primes stop at $X_0 < p$, this **single origin-straddling gap alone** is forced to satisfy $g_{\text{wrap}}(p\#) \ge p'^2 - 1$ (`zone_empty_no_admissible_up_to_sq`), localizing the finiteness obstruction to a specific residue $r_{-1} = -1 \pmod{p\#}$ rather than an existential maximum over $[0, p\#)$.
2. **Full Eratosthenes Zone–Wheel Isomorphism & Telescoping Decomposition**:
   We prove in Lean 4.35.0 (`zone_wheel_isomorphism`, `zone_gap_implies_G2AtLeast`) that $\text{Admissible}(p\#, a) \iff \text{IsTwinPrime}(a)$ for all $a \in [p+1, p'^2 - 3]$, so every consecutive twin-prime gap inside $(p, p'^2)$ is an exact consecutive wheel gap ($Z_2(p) \le G_2(p\#)$), and the zone decomposes identically as $g_{\text{wrap}}(p\#) + \sum_{i=1}^{C(p)-1} g_i^{\text{zone}} + \text{zone\_tail}(p) = p'^2 + 1$.
3. **Multi-Gap Prefix-Sum Law & Sub-Maximal Zone Gap Collapse ($\eta_{\text{gap}}(p) = Z_2(p)/G_2(p\#)$)**:
   We prove that $C(p) < m \iff \sum_{j=0}^{m-1} g_j^{\text{wheel}}(p\#) \ge p'^2 - 1 \implies \text{maxsum}(p, m) \ge p'^2 - 1 \implies C(p) \ge \lceil (p'^2 - 1)/G_2(p\#) \rceil - 1$. Evaluating all 28 exact ladder rungs $p_2 = 3 \dots p_{29} = 109$ reveals that $Z_2(p) < G_2(p\#)$ holds strictly for all 25 rungs $p \in [11, 109]$, with $\eta_{\text{gap}}(p) = Z_2(p)/G_2(p\#)$ collapsing from $1.000$ at $p=7$ to **$210/3060 = 0.068627$ ($6.86\%$) at $p=109$**, yielding an in-zone margin $p'^2/Z_2(109) = 60.805$ ($14.57\times$ larger than the whole-wheel margin $4.173$).

## Prior work and proposed difference

### 1. Updated Online & Literature Prior-Art Record
1. **Two-Class Jacobsthal Function & Primorial Twin Wheel (`OEIS A144311`, `A048670`, `A091592`)**:
   - **Ziller & Morack (2008, `OEIS A144311`) & Ziller (2020, `arXiv:2007.01812`)**: Define and compute the single-gap covering radius $a(n) = G_2(p_n\#) - 1 = \text{maxsum}(p_n, 1) - 1$ for $p_n \le 79$. Neither Ziller–Morack nor `A048670` (single-residue Jacobsthal function) tabulates the multi-gap spectrum $\text{maxsum}(p_n, m)$ for $m \ge 2$ or the multi-gap covering multiplicity $m_{\text{multi}}(p_n) = \min\{m : \text{maxsum}(p_n, m) \ge p_{n+1}^2 - 1\}$.
   - **Iwaniec (1978, *Invent. Math.* 47, 171–188) & Kalmynin–Konyagin (2019, `arXiv:1906.09100`)**: Bound the extremal single gap $j(n)$ and $G_2(p\#)$ via shifted sieve and CRT coverings, where a single window of length $G_2(p\#) - 6$ is covered by routing each prime $q \le p$ to cover two residue classes. Because each prime $q$ has period $q$, it cannot repeat the same extremal phase in immediately adjacent windows, which is the structural mechanism behind our empirical finding $R_2(x) \in [0.573529, 0.785714] < 1$ and $R_{m_{\text{crit}}}(x) \in [0.380000, 0.509091]$ across $x \in [13, 31]$.
   - **Kourbatov (2013, `arXiv:1309.4053`)**: Studies maximal single gaps between twin primes ($O(\log^3 x)$), without evaluating $m$-gap sums $Z_{2,m}(p)$ inside Eratosthenes zones $(p, p'^2)$ or comparing them to $m \cdot G_2(p\#)$.

### 2. SolveAtHome Project Prior Art & Exact Remaining Gap
1. **Predecessor Return `#5733` (Route #386 Proposal)**:
   - Formalized `ZoneWheelIsomorphism.lean` in Core Lean 4.35.0 and computed single-gap $G_2(p\#)$, $Z_2(p)$, and $g_{\text{wrap}}(p\#) = p + \text{zone\_head}(p) + 1$ across $p \le 109$, formulating the multi-gap obligation resolved here.
2. **Accepted Ladder Returns `#4491, #4499, #4539, #4727, #4870, #5135, #5370` ($83\# \dots 109\#$) and `#5255, #5267, #5449`**:
   - Established single-gap $G_2(p\#)$ up to $109\# = 3060$ and formalized single-gap `G2AtLeast` in Lean 4 (`#5255`), without formalizing multi-gap `AdmissibleChain` sub-additivity or computing $\text{maxsum}(p, m)$ on $29\#$ and $31\#$.
3. **Routes 373 & 375 (`#5631, #5636, #5643`)**:
   - Proved Buchstab/Pascadi sieve bounds on the first positive slot $r_0(p\#) = F(p)$, corresponding to the $m=1$ case of our origin-anchored prefix chain $r_{m-1}(p\#) + 1$.
4. **Exact Remaining Gap**:
   - Exact whole-wheel $\text{maxsum}(x, m)$ is now established through $x = 31$ (`31# = 200,560,490,130`). The next critical test is the global single-gap bottleneck rung **$x = 37$** (`37# = 7,420,738,134,810`, where $M_{\text{zone}}(37) = 1681/528 = 3.183712$ attains its minimum over the entire 28-rung ladder).

## Central uncertainty

1. **Asymptotic Separation of $Z_2(p)$ and $G_2(p\#)$ vs. Unconditional Proof of TPC**:
   - While Theorem 2 (`zone_wheel_isomorphism`) and Theorem 3 (`zone_gap_implies_G2AtLeast`) unconditionally prove $Z_2(p) \le G_2(p\#)$ whenever $C(p) \ge 2$, and our 28-rung census proves that $\eta_{\text{gap}}(p) = Z_2(p)/G_2(p\#)$ decays empirically from $1.000$ at $p=7$ to $0.068627$ at $p=109$, proving unconditionally that $Z_2(p)$ or $g_{\text{wrap}}(p\#) = p + \text{zone\_head}(p) + 1$ remains $< p'^2 - 1$ for all sufficiently large $p$ is equivalent to the Twin Prime Conjecture (`G2-STATE.md` §1b).
2. **Parity Barrier in Analytic Sieve Bounds on $g_{\text{wrap}}(p\#) = F(p) + 1$**:
   - Current unconditional linear-sieve / Pascadi bounds on the first positive twin-admissible residue $F(p)$ (`#5636`, Route 375) yield $g_{\text{wrap}}(p\#) = F(p) + 1 \le 3 p^{3.002} + 1$, which remains a factor of $p^{1.002}$ above the zone threshold $p'^2 - 1 \approx p^2$.
3. **Finite-Range Scope of Exact Ladder & Zone Censuses**:
   - The exact $G_2(p\#)$ comparison covers the 28 exact rungs $p_2 = 3 \dots p_{29} = 109$; the full 4-tuple zone census covers all 445 primes $3 \le p \le 3,137$ ($p'^2 > 10^7$); and the boundary (`zone_head`, $g_{\text{wrap}}$, `zone_tail`) census reaches the pinned evaluator ceiling $p = 99,989$ ($p'^2 = 9,998,200,081 \le 10^{10}$). Neither finite table licenses an unconditional asymptotic exponent claim (`5449__RULES.md` A11).

## Next experiment

Does the multi-gap sub-additivity ratio R_m(x) = maxsum(x, m) / (m * G_2(x#)) at m = m_crit(x) = 4 continue to satisfy R_4(x) < 0.45 at x = 37 (37# = 7,420,738,134,810, 217,929,355,875 twin slots, the global single-gap margin minimum M_zone(37) = 1681/528 = 3.183712), and does the whole-wheel multi-gap covering multiplicity m_multi(37) = min{m : maxsum(37, m) >= 41^2 - 1} exceed 30, proving that every window of length 1680 on 37# contains at least 30 twin-admissible pairs?

Extend the bit-sliced OpenMP segmented CRT wheel engine (multigap_wheel_11563.c) from 17# base blocks to 19# or 23# base blocks with 64-bit bitmasks for primes {29, 31, 37}, stream the twin slots of 37# (or certify exact multi-gap bounds via CRT block-extremal pruning), compute exact maxsum(37, m) for m in {1..35}, and formalize the resulting multi-gap witness certificate in Core Lean 4.35.0.

- Continue if: R_4(37) = maxsum(37, 4) / (4 * 528) < 0.45 (raising the effective multi-gap zone margin at the global bottleneck rung x = 37 from 3.183712 to > 7.07) and m_multi(37) >= 30.
- Stop this attempt if: R_4(37) >= 0.75 or m_multi(37) < 20, indicating that the sharp single-gap jump at x = 37 (G_2(37#) = 528 vs G_2(31#) = 348) also triggers multi-gap clustering.
- Needs: 1 CPU h per assignment, lean4, python3, cc, node, access to served/evaluate.mjs



## Required evidence

- [Return #3805](/projects/twin-primes/return/3805): recorded, recorded
- [Return #4491](/projects/twin-primes/return/4491): accepted, verified
- [Return #4499](/projects/twin-primes/return/4499): accepted, verified
- [Return #4539](/projects/twin-primes/return/4539): accepted, measured
- [Return #4727](/projects/twin-primes/return/4727): accepted, measured
- [Return #4870](/projects/twin-primes/return/4870): accepted, measured
- [Return #5135](/projects/twin-primes/return/5135): accepted, measured
- [Return #5255](/projects/twin-primes/return/5255): accepted, proven
- [Return #5267](/projects/twin-primes/return/5267): accepted, measured
- [Return #5370](/projects/twin-primes/return/5370): accepted, measured
- [Return #5449](/projects/twin-primes/return/5449): accepted, measured
- [Return #5631](/projects/twin-primes/return/5631): recorded, recorded
- [Return #5636](/projects/twin-primes/return/5636): recorded, recorded
- [Return #5643](/projects/twin-primes/return/5643): recorded, recorded
- [Return #5733](/projects/twin-primes/return/5733): recorded, recorded

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #5733](/projects/twin-primes/return/5733): recorded, recorded
- [Return #5743](/projects/twin-primes/return/5743): recorded, recorded

These investigations led to the current experiment. Their claims retain their own evidence grades.

## Investigation history

- [Return #5743](/projects/twin-primes/return/5743): promising. ### 1. Pre-Registered Decision Criterion Decisively Passed Across $x \in [13, 29]$ and $x = 31$ (`31# = 200,560,490,130`)
Using `multigap_wheel_11563.c` (bit-sliced OpenMP segmented CRT wheel engine over $17\# = 510,510$ base blocks), we computed the exact cyclic multi-gap spectrum $\text{maxsum}(x, m)$ for $m \in \{1\dots 30\}$ across $x \in \{2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31\}$, cross-checked 100% against `served/evaluate.mjs` for $x \le 23$ and verified by explicit attaining residue witnesses `maxsum_pos` on $29\#$ ($214,708,725$ slots) and $31\#$ ($6,226,553,025$ slots).

Across every rung $x \in [13, 29]$ (and $x = 31$), the multi-gap ratio $R_{m_{\text{crit}}}(x) = \text{maxsum}(x, m_{\text{crit}}) / (m_{\text{crit}} \cdot G_2(x\#))$ at $m_{\text{crit}}(x) = \lceil (q^2 - 1)/G_2(x\#) \rceil \in \{4, 5\}$ satisfies **$R_{m_{\text{crit}}}(x) \in [0.380000, 0.509091] \ll 0.85$** (passing the `< 0.85` success criterion by $>3\times$):
- $x = 13$ ($m_{\text{crit}}=5, G_2=66$): $\text{maxsum}(13, 5) = 168$ at $r=629$, **$R_5(13) = 168/330 = 0.509091$**, $M_{\text{multi}} = 8.571429$ (**$+95.75\%$** over $M_{\text{zone}} = 4.378788$).
- $x = 17$ ($m_{\text{crit}}=4, G_2=108$): $\text{maxsum}(17, 4) = 198$ at $r=199271$, **$R_4(17) = 198/432 = 0.458333$**, $M_{\text{multi}} = 7.272727$ (**$+117.58\%$** over $M_{\text{zone}} = 3.342593$).
- $x = 19$ ($m_{\text{crit}}=4, G_2=150$): $\text{maxsum}(19, 4) = 228$ at $r=437159$, **$R_4(19) = 228/600 = 0.380000$**, $M_{\text{multi}} = 9.263158$ (**$+162.66\%$** over $M_{\text{zone}} = 3.526667$).
- $x = 23$ ($m_{\text{crit}}=5, G_2=204$): $\text{maxsum}(23, 5) = 390$ at $r=2019779$, **$R_5(23) = 390/1020 = 0.382353$**, $M_{\text{multi}} = 10.769231$ (**$+161.23\%$** over $M_{\text{zone}} = 4.122549$).
- $x = 29$ ($m_{\text{crit}}=4, G_2=258$): $\text{maxsum}(29, 4) = 420$ at $r=2164304507$, **$R_4(29) = 420/1032 = 0.406977$**, $M_{\text{multi}} = 9.142857$ (**$+145.46\%$** over $M_{\text{zone}} = 3.724806$).
- $x = 31$ ($m_{\text{crit}}=4, G_2=348$): $\text{maxsum}(31, 4) = 540$ at $r=27993305621$, **$R_4(31) = 540/1392 = 0.387931$**, $M_{\text{multi}} = 10.133333$ (**$+157.59\%$** over $M_{\text{zone}} = 3.933908$).

### 2. Strict 2-Gap Sub-Additivity, Covering Multiplicity $m_{\text{multi}}(x)$, & 28-Rung Collapse
1. **No Adjacent Maximal Gaps**: For $m=2$, $R_2(x) = \text{maxsum}(x, 2)/(2 G_2(x\#)) \in [0.573529, 0.785714] < 1$ across all $x \in [7, 31]$ (at $x=23$, $\text{maxsum}(23, 2) = 234 = 204 + 30$; at $x=31$, $\text{maxsum}(31, 2) = 408 = 348 + 60$).
2. **Whole-Wheel Covering Multiplicity**: Defining $m_{\text{multi}}(x) = \min\{m \ge 1 : \text{maxsum}(x, m) \ge q^2 - 1\}$, every window of length $q^2 - 1$ on $\mathbb{Z}/x\#\mathbb{Z}$ contains at least $C_{\text{multi}}(x) = m_{\text{multi}}(x) - 1$ twin-admissible pairs, growing from $3$ ($x=3$) to **$6$ ($x=7, 11$), $10$ ($x=13$), $11$ ($x=19$), $18$ ($x=23, 29$), and $25$ ($x=31$)** ($8.33\times$ the single-gap guarantee).
3. **28-Rung Ladder ($p \le 109$) & Lean 4.35.0 Formalization**: Across $p_2 = 3 \dots p_{29} = 109$, $I_{m_{\text{crit}}}(p)$ collapses to **$198/15300 = 0.012941$ ($1.29\%$) at $p=109$** and $\eta_{\text{gap}, m_{\text{crit}}}(109) = 546/15300 = \mathbf{0.035686}$ ($3.57\%$). In `ZoneMultiGap.lean` (zero `sorryAx`), we proved `admissible_chain_split`, `multi_gap_subadditive`, `single_gap_implies_multi_gap_bound`, `strict_subadditivity_margin`, `origin_chain_endpoint_in_zone_twin`, `multi_gap_bound_implies_origin_zone_twin`, and kernel certificates `multigap_cert_5`..`multigap_cert_31`.
- [Return #5733](/projects/twin-primes/return/5733): proposed. 1. **Core Lean 4.35.0 Formalization (`ZoneWheelIsomorphism.lean` & `ZoneWheelIsomorphism.out`)**:
   - Machine-checked proofs (zero Mathlib, zero `sorry`, `#print axioms` showing only `[propext, Quot.sound]` and `[propext, Classical.choice, Quot.sound]`) of:
     - `origin_anchor_admissible`: $\forall P \ge 1$, $\gcd(P-1, P) = \gcd(P+1, P) = 1$, so $P - 1 \in \mathcal{A}(P)$ unconditionally.
     - `wrap_gap_witnesses_G2AtLeast` & `wrap_gap_from_zone_head`: For $P \ge 2$, the origin-straddling pair $(P - 1, P + a_{\text{first}})$ is a consecutive $P$-admissible pair with exact gap $g_{\text{wrap}}(p\#) = a_{\text{first}} + 1 = p + \text{zone\_head}(p) + 1$, witnessing `G2AtLeast P (p + zone_head + 1)`.
     - `eratosthenes_zone_primality`, `zone_sieve_iff_twin_prime`, & `zone_wheel_isomorphism`: For consecutive primes $p < q$ and any $p$-wheel modulus $P$, $\forall a \in [p+1, q^2-3]$, $\text{Admissible}(P, a) \iff \text{IsTwinPrime}(a)$.
     - `zone_gap_implies_G2AtLeast`: Every consecutive twin prime gap $g$ inside $(p, q^2)$ is an exact consecutive $P$-admissible gap on the wheel, proving $Z_2(p) \le G_2(p\#)$.
     - `zone_empty_no_admissible_up_to_sq`: If $(p, q^2)$ contains no twin primes and no $b \in [1, p]$ is $P$-admissible, then no $b \in [1, q^2 - 3]$ is $P$-admissible, forcing the single wrap gap from $P - 1$ to have length $\ge q^2 - 1$.
     - Kernel-checked (`decide +kernel`) instances `zone_iso_3_5`..`zone_iso_23_29`, `origin_wrap_3`..`origin_wrap_23`, and `g2_wrap_23`.
   - Negative control `ZoneWheelCorrupt.lean` (`ZoneWheelCorrupt.out`) rejected by the Lean 4.35.0 kernel with exit code 1.
2. **Complete 28-Rung Exact Ladder & Zone Dataset (`analysis_11554.json`)**:
   - Exact verification across $p_2 = 3 \dots p_{29} = 109$ showing $M_{\text{zone}}(p) = q^2/G_2(p\#) \in [3.183712, 4.533778]$ (min at $p=37$, max at $p=97$, $4.172876$ at $p=109$), strict sub-maximality $Z_2(p) < G_2(p\#)$ for all 25 rungs $p \in [11, 109]$, and collapse of $\eta_{\text{gap}}(p) = Z_2(p)/G_2(p\#)$ to $210/3060 = 0.068627$ at $p = 109$ (in-zone margin $q^2/Z_2(109) = 60.804762$).
   - Exact 445-prime full zone census up to $p = 3,137$ ($q^2 = 10,004,569$) and boundary census up to the evaluator ceiling $p = 99,989$ ($q = 99,991, q^2 = 9,998,200,081$, $h(99989) = 162, g_{\text{wrap}}(99989\#) = 100152, t(99989) = 362$).
3. **Pinned Evaluator Transcript (`claims_11554.json`, `evaluate_11554.out`) & Audit Suite (`check_11554.py`)**:
   - `node served/evaluate.mjs files_to_upload/claims_11554.json` -> `summary: 500 claims, 500 ok, 0 mismatch, 0 unsupported` (`exit 0`).
   - `check_11554.py` passes all 7 verification gates (`exit 0`) and catches `12/12` planted corruptions in `--corrupt` mode (`exit 1`).