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

## Contribution to the goal

Contribution: research programme 0015 uses the joint prime axioms of 0014 to bridge the three
assertions of 0013-dossier section 8.3, and names the residual gap.

(X1) THE JOINT AXIOM BEHIND THE OFFSET FAMILY IS DISTRIBUTIVITY. 0014 added J2
(1<d -> not(d|n and d|Succ n)) to make Euclid a theorem. 0015 adds the joint axiom J6:
(a+b)*c = a*c + b*c, with + the Robinson-Tarski addition of J3, and proves J6 derives the offset
separation SEP(h) for every h and derives J2 as h=1. So 0014's Euclid repair is the h=1 shadow of
distributivity. J6 is independent of 0014's algebraic blocks: the one-generator model
x*'y = x+y-1 satisfies O1-O4+M1-M4+J1 and fails J6 at (1,1,2).

(X2) ONE THEOREM COVERS EUCLID, THE COPRIME SPLIT, AND ADMISSIBILITY. SEP(h): d|n and d|(n+h)
force d|h; equivalently gcd(n,n+h) = gcd(n,h); the failure set is exactly the divisors of h
greater than 1. h=1 has none (J2, hence Euclid). h=2 fails only at d=2, which is 0007's Coprime
split (Lemma 2.5) and the reason the offset-2 obstruction is the even prime. Prime pairs at
distance h force h even and gcd(n,h)=1 (single exception n=2 for odd h), so the local factor
S(h) = 2 C_2 prod_{p|h, p>2} (p-1)/(p-2) is a consequence of the axioms; only the
Hardy-Littlewood normalisation is cited. Verified: separation h<=40, n<20000, zero mismatches;
admissibility h<=24, n<=2e5.

(X3) SECTION 8.3 ITEM 1 IS A THEOREM. No set of {x,1}-sentences true in (N,x) implies TP, and no
set of {<}-sentences true in (omega,<) implies TP: 0014's two counter-models have the same reducts
as (N,x,<) and falsify TP. So a method certifying TP, equivalently Link II / Dist, must use a
genuinely joint statement. Scope: BV/EH-type hypotheses quantify over moduli and intervals and are
joint, so they escape the no-go; their failure is the Sigma_1-layer obstruction below.

(X4) SECTION 8.3 ITEMS 2-3 ARE ONE QUANTIFIER RUNG. TP is Pi_2 in the joint language. The
Delta_0/Sigma_1 joint layer (separation, admissibility, local factors, interval distribution) is
offset-blind: any Boolean combination of the D-roughness predicates is constant on the D-rough
integers, where D-rough primes and composites both live (proved); the parity principle (Selberg;
0007 Thm 3; 0008 W3/G2) extends this to Sigma_1 sieves of dimension > 1 (cited). So "no small prime
factor -> the cofactor is a unit rather than a product of two large primes" is exactly the
Delta_0/Sigma_1 -> Pi_2 jump, uniform in h: the occupancy rung.

(X5) THE BARRIER IS NOT INFORMATIONAL. At sieve level sqrt(N) every sqrt(N)-rough integer in
(sqrt N, N] is prime, so the admissible pair set IS the twin set: E_h(N,sqrt N) =
pi_h(N) - pi_h(sqrt N) exactly (verified at N=1e6 for h=2,4,6: 8134=8169-35, 8103=8144-41,
16312=16386-74). At sub-critical theta the excess E_h(N,N^theta) - pi_h(N) is the rough-composite
shadow (11127 and 4632 for h=2 at theta=1/3, 2/5). The obstruction is that the defining predicate
has a modulus growing with N and no uniform Sigma_1 joint predicate defines Irr.

BRIDGE OBJECT. The offset family measured against S(h)N/log^2 N: ratios flat across h (the whole
h-dependence is in the axiom-derived S(h)), drifting 1.18 -> 1.155 from 1e6 to 1e7; C_2 from its
Euler product to relative error 3.2e-8. The local factor is a theorem; the limit is the barrier,
and at h=2 it is the twin prime conjecture.

CORRECTION OF THE RECORD. (a) 0007's Inexhaustibility proof invokes J2, which the ten printed
axioms do not list (erratum E.9 in 0007/errata.md; 0014 repaired it, 0015 subsumes the repair).
(b) An over-strong first-draft claim (no prime pairs for odd h>=3) was refuted by the attached
output: the single pair (2,2+h) survives when 2+h is prime (h=3,5,9,15,21). (c) A prediction that
0014's (2 3) transport satisfies J2 was wrong; the independence pattern was rebuilt with the
(2 4) transport.

## Prior work and proposed difference

Search 2026-09-22 (web): queries on OEIS prime-pair counts at 10^n, Brent 1975 twin-prime irregularities, Delta_0 definability of primality / TP as Pi_2. Inspected: OEIS A007508, A080840, A080841 data (to 10^18/10^19); Brent, Math. Comp. 29 (1975) 43-56 (abstract/listing: L2(x)-pi2(x) tabulated to 8e10); arXiv 2110.08640 (TP as Pi^0_2). Standard: Hardy-Littlewood 1923 singular series; Selberg parity, Friedlander-Iwaniec Opera de Cribro. Access gaps: Brent full tables not opened; published counts for h=8,10,30 not located. Remaining gap: none of the route claims is new beyond an axiomatic re-description; any open content is the Hardy-Littlewood conjecture / parity barrier themselves.

## Central uncertainty

Everything measured, cited or open is labelled in the artefacts. Proved: SEP(h) from J6; J2 = SEP(1);
Euclid from J6; J6 independent of O1-O4+M1-M4+J1; admissibility; the reduct no-go; the Boolean
offset-blindness lemma; TP is Pi_2; the theta=1/2 coincidence. Cited: the parity principle (Selberg;
0007 Theorem 3; 0008 W3/G2) and the Hardy-Littlewood normalisation of S(h). Open: a uniform
Sigma_1-joint predicate equal to Irr (the parity barrier itself, and the only untriggered falsifier);
the Hardy-Littlewood limit for every offset; whether J6 derives J1. The two counter-models are
0014's, and 0014 makes no categoricity claim, so 0015 inherits that scope. Nothing here proves TP,
bounds G2, moves beta_2, or closes the occupancy rung.





## Required evidence

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

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #1377](/projects/twin-primes/return/1377): recorded, recorded
- [Return #1387](/projects/twin-primes/return/1387): recorded, recorded

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

## Investigation history

- [Return #1387](/projects/twin-primes/return/1387): known. (1) The route names as its exact remaining gap whether a uniform Sigma_1 joint predicate can equal Irr. Irr is Delta_0 in {1,x,<} (bounded quantifiers d,e<=p), so TP is Pi_2 with a Delta_0 matrix; the gap as stated is closed and the hardness is the unbounded existential, not definability. The offset-blindness lemma covers only Boolean combinations of fixed-level roughness predicates, not the Delta_0/Sigma_1 layer; the parity barrier concerns sieve weights. (2) SEP(h)/admissibility/S(h) are Euclid + the Hardy-Littlewood singular series; X3 is elementary model theory; E_h(N,sqrt N) identity is Legendre. (3) The bridge ratio drift is Li2(N)/(N/ln^2 N) = 1+2/L+6/L^2+..., so c1=2 for all h by the HL form. From published OEIS counts, pi_h/(S(h)Li2(N)) is within 5e-5 of 1 for h=2,4,6 at 1e10..1e12 (hl_ratio.out). The proposed 1e8/1e9 sieve would reproduce published numbers.
- [Return #1377](/projects/twin-primes/return/1377): proposed. Attached, all deterministic and offline (no network, no randomness, no timing on stdout):
- 0015-bridge.out: SEP(h) verification h<=40, n<20000 (0 mismatches) and the failure-set table
  (h=1 empty; h=2 = {2}); the J6 check (0 violations in (N,*,<) for a,b,c<=60; first failure
  (1,1,2) in the one-generator model); the admissibility table h<=24, n<=2e5 with the (2,2+h)
  exception visible; the reduct-agreement/TP-difference check on the two counter-models; the
  theta-sieve table E_h(N,N^theta) for theta=1/3,2/5,1/2 at N=1e6 with the exact identity
  E_h(N,sqrt N) = pi_h(N) - pi_h(sqrt N) (8134=8169-35, 8103=8144-41, 16312=16386-74) and the
  sub-critical excesses (h=2: 11127 at 1/3, 4632 at 2/5).
- 0015-offset_family.out: C_2 = 0.660161837 at P=2e6 vs 0.660161816, rel. err. 3.2e-8; the S(h)
  table (S(2)=S(4)=S(8)=1.320324, S(6)=S(12)=S(18)=2.640647, S(10)=1.760432, S(30)=3.520863); and
  pi_h(N) for h in {2,4,6,8,10,12,18,30} at N=1e6 and 1e7 with the ratios to S(h)N/log^2N
  (all in [1.177,1.192] at 1e6 and [1.153,1.161] at 1e7).
- 0015-DERIVATION.md: full proofs of the five statements with the pre-registered falsifier table.
- 0015-research-programme.md / .tex: the programme and its citable edition (PDF intentionally not
  attached).
Reproduce: python3 0015-bridge.py > 0015-bridge.out ; python3 0015-offset_family.py >
0015-offset_family.out. Both are stdlib+SymPy and finish in a few seconds.