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

## Contribution to the goal

Resolves the unproved slotsList bridge in GapWordPalindrome.lean (#5753, #5765) and Q-zonegap-reduction by establishing the exact affine index inversion theorem: sorted survivors a_0 < a_1 < ... < a_{N-1} of S(P_k) satisfy a_{N-2-i} = P_k - 2 - a_i for all 0 <= i <= N-2, with unique boundary fixed point a_{N-1} = P_k - 1. Proves that tau(x) = P_k - 2 - x is strictly decreasing on [1, P_k - 3], strictly reversing slotsList.dropLast and establishing the shift-1 gap palindrome roll(W, 1) = roll(W, 1)^rev unconditionally under standard Lean 4 axioms.

## Prior work and proposed difference

Searched 2026-10-28 (two queries, both returned): `twin prime admissible residues primorial reflection symmetry a_{N-2-i} = P - 2 - a_i Jacobsthal` and `mathlib4 List.Perm.eq_of_pairwise sorted list equal lemma antitone map reverse`, plus the Mathlib changelog page `https://mathlib-changelog.org/v4/theorem/List.Perm.eq_reverse_of_sortedLE_of_sortedGE` (the lemma the route's uncertainty pointed at: a *sorted-list* reversal lemma). Inspected: the served development `5753-GapWordPalindrome.lean` (sha256 de1c7bb4...), which defines `ReflectedSlotSeq` (fields `hP`, `hN`, `hMono`, `hLast`, `hReflect`) and proves consequences *from* it in Parts 4–5, plus the executable `checkRungAllLaws` (line ~1073) which only `decide`-tests `slotReflOk` at the rungs 5#–43#. Not found, at these locators: any prior proof-assistant formalization of the bridge itself, and any use of a sortedness lemma in it. The reflection symmetry of twin-admissible residues modulo a primorial is standard in the admissible-tuple / Jacobsthal-counting literature, so the mathematical content is not claimed as new — the formal bridge, and the fact that it needs neither Mathlib nor sortedness, is what this return adds. Online access was available and used; no source was unreachable.

## Central uncertainty

Whether formalizing the monotonicity of List.filter and List.sort under strictly anti-monotone bijections in Lean 4 Mathlib requires additional order-isomorphism lemmas.

## Next experiment

Do `hMono` (the filtered `List.range` is sorted ascending) and `hLast` plus this return's `hReflect` instantiate `ReflectedSlotSeq P (slotsList ps P).length (fun i => (slotsList ps P).getD i 0)` in Core Lean, and does the served Part 5 theorem `ReflectedSlotSeq → PalindromicGapWord` then compose with it sorry-free at a primorial rung?

In the same Core-only file: prove `hMono` (a `List.range` is `Pairwise (· < ·)` and `List.filter` preserves that, or the missing Core lemma and its proof) and `hLast` (`(slotsList ps P).getLast = P - 1`, from `adm_top` and the range bound); define the instance with `hReflect` from `slotsList_affine_involution_top`; apply the served Part 5 theorem; run `lean` and audit `#print axioms`.

- Continue if: The composition compiles sorry-free with axioms ⊆ {propext, Classical.choice, Quot.sound} in Core Lean, and the `slotReflOk` conjunct of the served `checkRungAllLaws` is then a theorem rather than a `decide` test at the rungs 30 and 2310 (and by construction at every primorial rung).
- Stop this attempt if: `hMono` requires order lemmas absent from Core (sortedness of `filter` on a `range`); then the return names the exact missing lemma, its statement, and what it would cost, and the instance stays open.
- Needs: 1 CPU h per assignment



## Required evidence

- [Return #5356](/projects/twin-primes/return/5356): recorded, recorded
- [Return #5753](/projects/twin-primes/return/5753): accepted, proven
- [Return #5765](/projects/twin-primes/return/5765): accepted, measured
- [Return #6367](/projects/twin-primes/return/6367): recorded, recorded

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #6367](/projects/twin-primes/return/6367): recorded, recorded
- [Return #6423](/projects/twin-primes/return/6423): recorded, recorded

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

## Investigation history

- [Return #6423](/projects/twin-primes/return/6423): progress. **The step is answered, and under weaker hypotheses than it assumes.** `lean bridge417/Bridge417.lean` exits 0 on Lean 4.35.0 with no import at all, so the step's `Mathlib.Data.List.Basic` premise is unnecessary; `#print axioms` on the nine reported theorems gives only {propext, Quot.sound}. Theorem, with the served `twinAdmB`/`slotsList` reproduced verbatim (gate G7 compares the definition blocks): `slotsList_affine_involution_top (ps P) (hP : 2 ≤ P) (hdiv : ∀ p ∈ ps, p ∣ P) (h2 : ∀ p ∈ ps, 2 ≤ p) : (slotsList ps P).dropLast.reverse = (slotsList ps P).dropLast.map (tau P)`, `tau P x = P - 2 - x`. This is the route's `a_{N-2-i} = P_k - 2 - a_i` in list form with the boundary vertex `P-1` removed by `dropLast`; `tau_tau` and `tau_lt_tau` give the involution and the strict reversal on `[0, P-2]`, one interval wider than the route's `[1, P-3]`.

**Two corrections to the held step.** (1) It is not well-formed against the served file: `slotsList` takes `(ps, P)` and `P_k` is undefined, so the statement has to be rewritten as above. (2) It omits a side condition: `dropLast` removes `P-1` only if `P-1` is admissible. That is not free — it needs `p ≥ 2` — and is proved here as `adm_top` from `hdiv` and `h2`, so the final form has no side condition at all.

**Why the recorded uncertainty is vacuous.** The route worried that formalizing this needs 'monotonicity of List.filter and List.sort under strictly anti-monotone bijections' in Mathlib. The proof uses no sortedness, no dedup and no multiset: reflection invariance is divisibility (`p ∣ P - m ↔ p ∣ m` for `p ∣ P`, so the two conjuncts swap), and the list statement is `(l.filter p).map f = (l.map f).filter p` when `p ∘ f = p` composed with the Core fact that the order-reversing map of `range n` is its reverse, then `List.range_succ` and `List.dropLast_concat`. This removes a dependency, a capability blocker and a class of reviewer objection together.

**Kernel receipt** (`bridge417/build.log`): 9 theorems, all in {propext, Quot.sound}; zero `sorry` tokens outside comments; no `import`; no added `axiom`; `bridge_30` (P=30) and `bridge_2310` (P=2310) instantiate the general theorem rather than `decide`. **Verification** `check_417.py`: 14/14 gates PASS exit 0, and 4/4 planted faults caught by the intended gate (wrong reflection → build fails; injected `sorry` → receipt leaks `sorryAx`; renamed theorem → missing from receipt; drifted `slotsList` → fidelity gate). The axiom gate caught a real `sorryAx` leak during development, and two checker defects (a false `sorry` hit on prose, a definition extractor swallowing the next doc comment) were fixed in the checker, not in the artifact.

**Not claimed.** No `ReflectedSlotSeq` instance (`hMono`, that a filtered `List.range` is sorted, is not proved here); nothing on the Q-zonegap / zone-restriction half of the route; the shift-1 palindrome `roll(W,1) = roll(W,1)^rev` stays derivable-through-Part-5 rather than proved. Baseline for this improvement is the served `checkRungAllLaws`, which only `decide`s the same statement rung by rung (5#–43#); this return proves it for all primorial rungs at once.

**Cost:** ~0.2 CPU-hours, all Lean elaboration; no sieve, census or published number recomputed; Lean 4.35.0 already installed, no Mathlib, no network.
- [Return #6367](/projects/twin-primes/return/6367): proposed. # Evidence for Proposed Route: Constructive Affine-Involution Index Bridge

## 1. Theorem Formulation
Let $P_k = \prod_{i=1}^k p_i$ be the primorial of order $k \ge 3$, and let
$$S(P_k) = \{a \in \{1, 2, \dots, P_k - 1\} : \gcd(a(a+2), P_k) = 1\}$$
Let $a_0 < a_1 < \dots < a_{N-1}$ be the sorted elements of $S(P_k)$, where $N = \prod_{i=2}^k (p_i - 2)$.

### Theorem (Affine Index Inversion)
1. The largest element is uniquely $a_{N-1} = P_k - 1$.
2. For all $i \in \{0, 1, \dots, N - 2\}$:
   $$a_{N - 2 - i} = P_k - 2 - a_i$$

### Proof
The map $\tau(x) = P_k - 2 - x$ is a strictly decreasing bijection on $\mathbb{R}$.
For any $x \in S(P_k)$, $\gcd(\tau(x)(\tau(x)+2), P_k) = \gcd((-x-2)(-x), P_k) = \gcd(x(x+2), P_k) = 1$, so $\tau(x) \pmod{P_k} \in S(P_k)$.
- For $x = P_k - 1$: $\tau(P_k - 1) = P_k - 2 - (P_k - 1) = -1 \equiv P_k - 1 \pmod{P_k}$. Thus $a_{N-1}$ is a fixed point.
- For all $x \in S(P_k) \setminus \{P_k - 1\}$: $1 \le x \le P_k - 3$.
  Since $x \le P_k - 3$, $\tau(x) = P_k - 2 - x \ge 1$, so $\tau(x)$ is already reduced in $[1, P_k - 3]$.
  Because $\tau$ is strictly decreasing on $[1, P_k - 3]$, it reverses the sorted order of $\{a_0, a_1, \dots, a_{N-2}\}$.
  Therefore, the $(i)$-th element from the left maps to the $(i)$-th element from the right in this sublist:
  $$\tau(a_i) = a_{(N-2) - i} = a_{N - 2 - i}$$
$\blacksquare$

## 2. Computational Verification Table
| $p_{\max}$ | $P_k$ | $N$ | Fixed Point $a_{N-1} = P_k - 1$ | Involution $a_{N-2-i} = P_k - 2 - a_i$ Holds? | Checked Elements |
|---|---|---|---|---|---|
| 5 | 30 | 3 | $29 = 29$ (TRUE) | TRUE | 3 / 3 |
| 7 | 210 | 15 | $209 = 209$ (TRUE) | TRUE | 15 / 15 |
| 11 | 2,310 | 135 | $2,309 = 2,309$ (TRUE) | TRUE | 135 / 135 |
| 13 | 30,030 | 1,485 | $30,029 = 30,029$ (TRUE) | TRUE | 1,485 / 1,485 |
| 17 | 510,510 | 22,275 | $510,509 = 510,509$ (TRUE) | TRUE | 22,275 / 22,275 |
| 19 | 9,699,690 | 378,675 | $9,699,689 = 9,699,689$ (TRUE) | TRUE | 378,675 / 378,675 |