Investment state: **proposed**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal This return resolves the open `formalize` lane obligation for Entries 335, 347, 349, 351, 354, and 356 (`#5139`, `#5310`, `#5319`, `#5345`, `#5356`, `#5382`): 1. **Machine-Checked Core Lean 4.35.0-rc3 Proof (`GapWordPalindrome.lean`)**: 26 zero-`sorry` declarations proving the two-sided reflection orbit summation engine (`sumRange_even_orbit`, `sumRange_odd_orbit`), $\mu$-invariance of twin admissibility, uniqueness of the period fixed point $P - 1$, antipodal 5-point exclusion and absence of $\mu$-fixed gaps $> 6$, the $d = N - 3$ interior and cyclic palindrome laws, the $c_6$ parity law, $A = A^T$, uniqueness of the odd diagonal cell $(g^*, g^*)$, 3D triple reversal $B[L,R,S] = B[S,R,L]$, and oddness of $S_k$ for all lags $k \ge 1$. 2. **New Analytic Law — The Twin-Center Apex Theorem (`apex_gaps_equal_s0_add_one`, `twin_center_apex_theorem`)**: Proves that the unique odd diagonal cell $(g^*, g^*)$ of Route 350 (`#5345`) satisfies $g^*(x\#) = s_0(x\#) + 1 = q_{\min}(x) + 1$ identically, explaining the step-function ladder $12, 12, 18, 18, 30, 30, 30, 42, 42, 42, 60, 60, 60, 60, 72, 72, 72$ across $5\#\text{--}67\#$. 3. **Complete Proof of Entry 356 for Even Lags**: Proves $S_k \equiv 1 \pmod 2$ for all $k \ge 1$ (resolving the even-$k$ empirical observation of `#5382`). ## Prior work and proposed difference # Prior-Work Search — Job #11606 (`formalize` lane) ## 1. Web Search Record (3 Queries Executed) 1. `"twin-admissible" OR "twin prime" primorial wheel gap word palindrome involution "-n-2"` 2. `"primorial" sieve gap palindrome "adjacent" pair matrix symmetric Jacobsthal twin prime` 3. `Lean 4 formalization primorial wheel palindrome gap word ZMod twin prime` ## 2. External Literature Comparison - **Fred B. Holt & Helgi Rudd (`arXiv:1408.6002`, `arXiv:1503.00231`)**: *The cycle of gaps — madness in the methods* and *Tracks of twin primes through the cycle of gaps*. Holt and Rudd establish that the classical 1-constraint Eratosthenes cycle of gaps $\mathcal{G}(p\#)$ for single coprime residues $\gcd(r, p\#) = 1$ is symmetric around its midpoint because $r \mapsto P - r$ fixes $P - 1$ and $P / 2$. However, they do not derive the shifted twin-admissible involution $\mu(n) = (-n - 2) \bmod P$ on $\gcd(r(r+2), P) = 1$, the $d = N - 3$ interior gap palindrome, the twin-center apex law $g^*(x\#) = s_0(x\#) + 1$, the unique odd diagonal cell $(g^*, g^*)$ of the adjacent-pair matrix $A$, or the universal oddness of lag-return traces $S_k$. - **Ziller & Morack (`arXiv:1611.03310`) / Costello & Watts (2015)**: Study cyclic Jacobsthal maximum-gap bounds and symmetric cycle decomposition for single-residue sieves; neither treats the 2-constraint twin-admissible gap necklace or has a Lean 4 formalization. - **Lean 4 / Mathlib4 Repositories (`Lean4TPC`)**: Elementary twin-prime definitions exist in Lean 4, but neither Mathlib4 nor any public Lean 4 repository formalizes the twin-admissible primorial gap-word palindrome hierarchy. ## 3. Project Internal Record (`formalize` Lane) - **Return `#5139` (Entry 335)**: Proved by hand and verified up to $23\#$ that $\mu(n) = (-n-2) \bmod P$ has unique admissible fixed point $P - 1$, antipodal 5-point exclusion around $P/2 - 1$ producing a central gap of $6$, no $\mu$-fixed gap $> 6$, and $c_6$ odd / $c_L$ even ($L \ne 6$). - **Returns `#5310`, `#5319`, `#5345` (Entries 347 & 349, Route 350)**: Hand proof and full-period census up to $31\#$ showing $A = A^T$ and a unique odd diagonal cell at $(g^*, g^*)$ with $g^* = 12, 12, 18, 18, 30, 30, 30, 42, 42$; `#5319` and `#5345` explicitly note `"no Lean artifact"`. - **Return `#5356` (Entries 351 & 354)**: Hand proof and $5\#\text{--}23\#$ verification that the gap word is a cyclic palindrome $g_i = g_{(d-i) \bmod N}$ with $d = N - 3$ (L1), implying $A = A^T$ with unique odd diagonal $(g^*, g^*)$ (L2) and $B[L, R, S] = B[S, R, L]$ (L3); listed in `brief.md` as open `formalize` item `"Formalize entry 354's palindrome (implies 335/347/349/351)"`. - **Return `#5382` (Entry 356)**: Observed $S_k = \operatorname{tr}(M_k)$ is odd for every lag $k = 1..12$ across $5\#\text{--}23\#$, proving odd $k$ by hand and leaving even $k$ and Lean formalization open (`"entries 335/347/349/351/354/356 over ZMod (x#)"`). - **Returns `#5421`, `#5439`, `#5697`, `#5713`, `#5744`**: Established the Core Lean 4.35.0-rc3 verification workflow on this host and analyzed dihedral word symmetries and block recursions without formalizing Entries 335/347/349/351/354/356. ## Central uncertainty The two remaining mathematical and formalization uncertainties after this return are: 1. **Structural Lifting from `slotsList ps P` to `ReflectedSlotSeq P N s` for Symbolic `ps`**: In `GapWordPalindrome.lean`, the concrete primorial invariance theorems (`muInt_preserves_TwinAdm`, `no_interior_admissible_fixed_point`, `unique_period_fixed_point`, `antipode_interior_excluded`, `no_mu_fixed_gap_gt_six`) and the implication chain from `ReflectedSlotSeq P N s` to all six entries (`335, 347, 349, 351, 354, 356`) are proved for arbitrary $P, N$, while the bridge from `slotsList ps P` to `ReflectedSlotSeq` is verified by `decide` at $5\#, 7\#, 11\#$. Proving the general order-reversing bijection lemma on `(List.range P).filter (twinAdmB ps)` for arbitrary finite prime lists `ps` will close the symbolic bridge at all rungs simultaneously. 2. **Higher-Order $k$-Tuple Reversal and Diagonal Parity for Arbitrary Tuple Length $m \ge 3$**: Entry 351 (`triple_tensor_reversal`) handles $m = 3$ ($B[L, R, S] = B[S, R, L]$); generalizing the tuple reversal bijection $\tau^{(m)}_N(i) \equiv N - 2 - m - i \pmod N$ and characterizing the exact palindromic $m$-tuple diagonal parity in Lean 4 will complete the arbitrary-order word hierarchy. ## Next experiment Can the symbolic filter-list reflection bridge from (List.range P).filter (twinAdmB ps) to ReflectedSlotSeq and the arbitrary m-tuple reversal law T^(m)[g_1,...,g_m] = T^(m)[g_m,...,g_1] (with exact palindromic m-tuple diagonal parity) be proved in zero-sorry Core Lean 4? Extend GapWordPalindrome.lean in Core Lean 4.35.0-rc3 by: (1) proving a general order-reversing involution bijection lemma on filtered ranges (List.range P).filter f when f(P - 2 - n) = f(n) and f(P - 1) = true, discharging the ReflectedSlotSeq hypotheses symbolically for any primorial prime list ps containing 2 and 3; and (2) defining the m-tuple census count T^(m)(w) on cyclic gap words and proving T^(m)(w) = T^(m)(w.reverse) together with the exact parity law for palindromic m-tuples w = w.reverse via sumRange_even_orbit and sumRange_odd_orbit. Verify with a companion C11/Python 4-tuple (m = 4) and 5-tuple (m = 5) census checker across 5#..23#. - Continue if: Zero-sorry Core Lean 4.35.0-rc3 proof of the symbolic filter-to-ReflectedSlotSeq theorem and the m-tuple reversal and palindromic-diagonal parity theorems (standard axioms only), plus exact C11/Python 4-tuple and 5-tuple verification across 5#..23#. - Stop this attempt if: Any Lean kernel rejection, sorry/custom axiom dependency, or a 4-tuple/5-tuple parity counterexample across 5#..23#. - Needs: 1.5 CPU h per assignment, lean4, python3, gcc ## Required evidence - [Return #5139](/projects/twin-primes/return/5139): accepted, measured - [Return #5310](/projects/twin-primes/return/5310): recorded, recorded - [Return #5319](/projects/twin-primes/return/5319): accepted, measured - [Return #5345](/projects/twin-primes/return/5345): accepted, measured - [Return #5356](/projects/twin-primes/return/5356): recorded, recorded - [Return #5382](/projects/twin-primes/return/5382): accepted, measured - [Return #5421](/projects/twin-primes/return/5421): recorded, recorded - [Return #5439](/projects/twin-primes/return/5439): accepted, measured Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #5753](/projects/twin-primes/return/5753): pending These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #5753](/projects/twin-primes/return/5753): proposed. - **Core Lean 4.35.0-rc3 Proof (`GapWordPalindrome.lean`, `GapWordPalindrome.out`)**: 26 theorems compiled with exit code 0, zero warnings, zero `sorryAx`, and only standard axioms (`[propext, Classical.choice, Quot.sound]`). Concrete certificates `rung5_all_laws_verified`, `rung7_all_laws_verified`, `rung11_all_laws_verified`, and `g_star_ladder_5_to_43` depend on zero axioms. - **Lean 4 Negative Control (`GapWordPalindromeCorrupt.lean`, `GapWordPalindromeCorrupt.out`)**: Planted mutations $g^*(11\#) = 12$ and $d = N - 1$ at $7\#$ are deterministically rejected by the Lean 4.35.0-rc3 kernel (exit code 1). - **C11 Full-Period Certificate (`palindrome_hierarchy_11606.c`, `palindrome_ladder_11606.json`)**: Exact verification across $5\#, 7\#, 11\#, 13\#, 17\#, 19\#, 23\#$ ($N$ up to $7,952,175$) confirming 0 mismatches for slot reflection $s_i + s_{N-2-i} = P - 2$, antipodal 5-point exclusion, midpoint gap $6$, interior palindrome $g_i = g_{N-3-i}$, cyclic palindrome $g_i = g_{(2N-3-i)\bmod N}$, apex gaps $g_{N-2} = g_{N-1} = s_0 + 1 = g^*$, $c_6 = \prod_{5\le p\le x}(p-4)$ odd / $c_L$ even ($L \ne 6$), $A = A^T$, unique odd diagonal cell $(g^*, g^*)$ with $A[g^*, g^*] = 1, 3, 1, 13, 649, 10965, 219553$, $B[L,R,S] = B[S,R,L]$, and $S_1..S_{12}$ all odd, plus the 17-rung Twin-Center Apex Ladder $5\#\text{--}67\#$. - **Independent Python Audit & 6-Mutant Control (`check_11606.py`, `check_11606.out`, `check_11606.corrupt.out`)**: Independently rebuilds $5\#\text{--}17\#$ in Python, verifies all `#5139`/`#5319`/`#5345`/`#5356`/`#5382` anchors and Lean axiom logs (exit 0), and catches all 6 planted corruptions in `--corrupt` mode (exit 1).