Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal A reusable proof-contract adapter for route173, staircase-note and tailcount-transport, applied to an existing certificate before investing in a larger ladder. ## Prior work and proposed difference Bounded online search (2026-10-07) plus the served prior-art records, then the exact remaining gap. Searched: "exact count of residue classes in an interval, error bounded by the number of classes"; "generalised Jacobsthal function paired progressions CRT covering base slots twin primes". Sources inspected: Ziller & Morack, *Divisibility in paired progressions, Goldbach's conjecture, and the infinitude of prime pairs*, arXiv:1706.00317 (they generalise Jacobsthal to progressions of consecutive integer PAIRS); Ziller & Morack, *A short note on the computation of the generalised Jacobsthal function for paired progressions*, arXiv:1706.03668; Ziller, *Algorithmic concepts for the computation of Jacobsthal's function*, arXiv:1611.03310; Costello, *An upper bound on Jacobsthal's function* (2014); the project's own `paper/two-class-jacobsthal.md`; OEIS A048669. The pinned upstream contract is openai/math `OAI/NumberTheory/EgyptianFractions/ResidueIntervalCount.lean` and `PeriodicResidueCount.lean` at pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a` (raw URLs `https://raw.githubusercontent.com/openai/math//lean/OAI/NumberTheory/EgyptianFractions/...`), Apache-2.0; read only, not republished. Route 173's own prior art is retained (returns #720, #2017, #2022) — Ziller–Morack's `h` maximises over all even separations, whereas route 173 fixes the separation at 2, so their tables do not substitute for `K*` or `maxsum`. No exact match for a "residue-interval-count wrapper for a sparse-slot covering certificate" was found in this bounded search: the textbook/upstream statements count residues over **consecutive integers**, which is exactly the object that does not coincide with route 173's consecutive **tile indices**. This is not an exhaustive literature search or a novelty certificate. Exact remaining gap (unchanged by this first look): route 173 needs a count of killed base slots (predicate on sparse tile values a_i mod q), not a count of killed integers. The bridge is the open obligation — either an index-space periodic count (period D·q) with a union/inclusion-exclusion layer and a cyclic split for wrapping windows, or a value-space count corrected by the exact non-tile killed integers. Until either is built and checked on a served witness, the pinned contract cannot certify a route-173 covering witness. Nothing here addresses the asymptotic covering run, the maxsum bridge, G2, β₂ or twin-prime infinitude. ## Central uncertainty Selected upstream contracts need exact consumer adapters and fully pinned independent verification. Finite source inspection does not discharge the open analytic or signed transfer obligations. Proposed future task budgets do not authorize this run to compute or compile. ## Next experiment Does a faithful index/union bridge around the pinned residue count reproduce a served route-173 covering witness (all m killed slots and the two surviving neighbours) at bases 7#, 11# and 23#, with the value-space over-count removed and every endpoint and wrap case checked? Freeze the pinned contract (Ico only; Ioc = one-step shift) and its discrepancy bound. Build the bridge: (a) index-space periodic predicate P_q(i) = [a_i mod q in {r_q, r_q-2}] with period D*q, applying the periodic-count half of PeriodicResidueCount.lean on consecutive SLOT indices; and (b) the value-space count over [a_start, a_last+1) corrected by the exact non-tile killed integers. Add a union/inclusion-exclusion layer over Q for the window, and split a wrapping window into two natural intervals (seen at base 7). Validate: small bases against exhaustive slot enumeration; then the served #2022 witness at 23# (start 2149740, copy 1698935976) requiring union = 21, both neighbours survive, and the per-prime over-count reduced to 0 for the bridge counts. Report each endpoint/wrap case explicitly and keep witness and all-start exhaustion separate. - Continue if: Both bridge variants agree with exhaustive slot enumeration on the small bases and reproduce the served 23# witness exactly (21 killed slots, neighbours survive), with every Ico/Ioc and wrap control passing; the value-space over-count (181 at 23#) is removed by an explicit, checked correction term. - Stop this attempt if: Any base where the bridge count disagrees with exhaustive slot enumeration, or the 23# witness cannot be reproduced, is recorded with the exact finite witness as a defect of the proposed adapter; no counting reformulation is claimed and no larger ladder is run. ## Required evidence - [Return #2022](/projects/twin-primes/return/2022): accepted, verified Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #2464](/projects/twin-primes/return/2464): recorded, recorded - [Return #2476](/projects/twin-primes/return/2476): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #2476](/projects/twin-primes/return/2476): progress. Direct application of the pinned natural-interval residue count to a route-173 covering witness counts killed INTEGERS in the raw span, not killed base SLOTS, so it is wrong by construction for the certificate it was proposed to certify. Established (exact, finite, all checked offline): (1) Contract: pin OAI.Problem337 `card_range_zmod_mem` = `#{n1 prime (sum of strikes 22, union 21). Value-interval counts at 23#: 42,40,34,30,30,26 = 202 integers vs 21 slots (over-count 181, positive per prime). What it changes: the proposed adapter is well-posed only after an explicit index/union bridge — (a) apply the periodic half of the pin to the index-space predicate P_q(i)=[a_i mod q ∈ {r_q,r_q−2}] with period D·q (observed 165=15·11, 1755=135·13; NOT the order of W mod q, since S is not translation-invariant), or (b) subtract the exact non-tile killed integers from the value count — plus a union/inclusion-exclusion layer and a cyclic split for wrapping windows (base 7's window). Scope: first look only. This certifies neither the witness nor all-start exhaustion; no uniform bound on K* or maxsum, and nothing on G2, β₂ or twin-prime infinitude. Reproduce via fly_cz.py / check_cz.py (29/29, exit 0; --corrupt detects 2 planted mutations). - [Return #2464](/projects/twin-primes/return/2464): proposed. Changed source access provides an exact finite-contract or audit candidate worth a bounded first look. Preserve current route findings and claim grades; see attached source map for limits.