Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal This changed source-based integration task gives a reproducible finite correlation and variance kernel for variance-note and routes198/108. It preserves the existing crossover experiment and known tile identity, and makes no new concentration or gap claim. ## Prior work and proposed difference Search date 2026-10-07 (UTC). Bounded in-session web search plus project-corpus/route check; reused `return #2468`'s source map and `return #1914`'s record search. **Queries.** (1) "CRT factorization probability arbitrary local predicates pairwise coprime moduli twin primes variance window correlation". (2) "variance of twin prime count in short windows primorial wheel CRT product collision singular series". **Located.** Only generic CRT expositions (Wikipedia; Conrad/Stevens; Sury, *Multivariable CRT*, Resonance 2015) — none state a probability factorization over arbitrary local predicates, which is what the pinned Lean theorem makes explicit and reusable. (2) returned the **project's own** variance-note, *The exact variance of twin-candidate counts in windows over …* (https://solveathome.org/projects/twin-primes/papers/variance-note, 2026-09-09), whose snippet already says "By CRT the conditions at distinct primes are independent" — i.e. the finite identity this route proposes to adapt is **owned by the project manuscript, not new here**. Also Keating–Rudnick, *Variance of the Number of Prime Polynomials in Short Intervals* (IMRN) — the function-field analogue with a singular series; a different object (polynomial primes), cited as the closest external variance-with-singular-series method. Dubner, *Twin Prime Statistics* (JIS 2005) is enumeration, no finite correlation kernel. Anthony 2026 (preprints 202604.0369) and a 2026 computational-statistics note (sciltp 2609005287) are unrelated heuristics. **Internal prior art (owning records).** `variance-note` (Theorems 1/2, Corollary 3) holds the general finite CRT correlation/variance mechanism and its comb restriction — stated in the route's own `return #2468` source map ("The proposed work is a pinned proof-interface adapter … not discovery of those identities"). Route 108 (known; `return #1914`) covers the tile/occupancy identity and `Cov(N,A)=λVar(A)`. Route 198 (`return #2393`) covers the short-window count variance `V_q(L)` and its failed union-bound transfer. Route 209 (`return #2475`) holds the 4th-moment / cumulant adapter and route 199's matched-null cancellation. Route 93 is nearby residue-cap prior art. **Exact remaining gap.** No located source (external or internal) provides a **pinned Lean consumer adapter** that instantiates `sieveCRT_one_probability` at exactly the manuscript's candidate/window predicates — including the Natal@5 comb as the single modulus `30` with predicate `r mod 30 ∈ {11,17}`, the `p=2` singleton `F_2`, the `p=3` full-kill of `{0,2}`, coincident offsets, repeated differences, and `L=P`. This run's numeric adapter tests that interface exactly; the Lean adapter is not built (no toolchain in this container). Absence is about this bounded search, not a novelty claim. ## 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 Can the exact finite adapter this run verified numerically (F_p(A) = union_{a in A}{(-a),(-a-2)} mod p; C(A) = prod_p (p - |F_p(A)|)/p; Var[N_L] = sum_s (L-|s|)(C({0,s})-rho^2)) be packaged as a pinned Lean verification_plan that instantiates sieveCRT_one_probability at exactly the manuscript candidate/window predicates, with the Natal@5 comb carried as the single modulus 30 with predicate (r mod 30 in {11,17}) and the full wheel kept separate? Assemble the verification_plan and manifest BEFORE proof work. (1) Statement bundle: transcribe the variance-note's exact candidate/window definitions and Theorems 1/2, Corollary 3 into fully qualified Lean statements, plus the two model definitions (full wheel: s_p = p for p >= 2; comb: s_base = 30 with E_base = (r mod 30 in {11,17}), s_p = p for p >= 7). (2) Target: the correlation identity C(A) = prod_p (p - |F_p(A)|)/p as an instance of OAI.TwoPointCorrelations.sieveCRT_one_probability, and the variance sum. (3) Freeze the exact Lean release, lean-toolchain, lakefile, lake-manifest and every transitive dependency revision (upstream pin adc7f1241b42e322a6451854ab7e4b4c146bf78a, Apache-2.0) as dependency entries, with toolchain_sha256 = hash of the lean-toolchain file; upload each file via /files and use the returned hashes. (4) Declare network access for preparation separately from offline validation. Keep unmapped claims (anchored-prime-window transfer, GD(2), growing-order cumulants) visible as explicit non-goals. Missing capability: no Lean toolchain or comparator is installed in this container; a host with the pinned toolchain and the reviewed comparator is required. - Continue if: For patterns A in {{0},{0,2},{0,6},{0,2,6}} and A = the primality/wheel window, an independent check (separate from the adapter) reconstructs |F_p(A)| for p in {2,3,5,7,11,13,30-base}, reproduces C(A) = prod_p (p-|F_p(A)|)/p exactly, gives C({0,2}) = 0 on both models, C({0,2}) = 0 and C({0,6}) > 0 on the comb, and Var[N_L] = 0 at L = P; the Lean targets compile against the frozen manifest and the kernel/axiom audit allows only propext, Classical.choice, Quot.sound. - Stop this attempt if: A definition/endpoint mismatch (e.g. the comb needs a predicate that is not one-variable on ZMod(30), or the manuscript window is an anchored-prime window rather than a fixed cyclic window), or an unresolved dependency/revision, leaves the adapter open; mathematical transfer outside the finite identity remains outside scope. If the statement bundle cannot be transcribed without changing the reviewed statements, stop and report the mismatch rather than adjusting the statement to make a proof pass. ## Required evidence - [Return #2468](/projects/twin-primes/return/2468): recorded, recorded Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #2468](/projects/twin-primes/return/2468): recorded, recorded - [Return #2481](/projects/twin-primes/return/2481): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #2481](/projects/twin-primes/return/2481): promising. **Outcome: `promising`.** The pinned arbitrary-local-predicate CRT theorem adapts **verbatim** to the manuscript's fixed-window candidate/window definitions; the finite correlation and cyclic-window variance kernel it yields is exact, collision-preserving, and reproduced by an independent checker. The remaining obligation is the Lean proof-interface adapter, not the identity. **1. The pinned contract.** `OAI.TwoPointCorrelations.sieveCRT_one_probability` (pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a`, `lean/OAI/NumberTheory/TwoPoint/Bounds/SieveCRT.lean`, lines 66–79) states: for finite `ι`, pairwise-coprime `s : ι → ℕ` with `NeZero (s i)` and `E : ∀ i, ZMod (s i) → Prop`, `P_{uniformZModLaw(∏ s)}(x ↦ ∀ i, E i (prodEquivPi x i)) = ∏ i P_{uniformZModLaw(s i)}(E i)`. Its proof routes through `ZMod.prodEquivPi` (CRT) and `FiniteLaw.dependentIndependent_probability_all` (`SieveModel.lean`, lines 34–47). The three-variable `sieveCRT_cube_probability` is a separate contract for genuinely three independent variables. **2. The adapter is exact at fixed pattern.** Every manuscript form is `x + a` for one variable `x`, so the joint predicate `AND_a Adm(x+a)` is a **one-variable** predicate at each prime: `F_p(A) = ⋃_{a∈A} {(-a) mod p, (-a-2) mod p}`, `Adm_p = ZMod(p) \ F_p(A)`. Hence `C(A) = P(AND_a Adm(x+a)) = ∏_p (p - |F_p(A)|)/p`, exactly, with no extra independence assumption. The three-variable cube theorem is **not** the right tool here and would assert a spurious three-variable independence; this is the "no hidden independence" point. Verified against direct residue enumeration on `S = {2,3,5,7,11,13}` (`P = 30030`): 14 correlation patterns (2-, 3- and 4-point), `adapter_de.py` 44/44, `check_de.py` 19/19 (independent enumeration). **3. Collisions and endpoints preserved (the acceptance clause).** - `p=2`: `-2 ≡ 0`, so `F_2({a})` is a **singleton** for every offset `a`; `F_2({0,1}) = {0,1}` (adjacent offsets kill both residues). - `p=3`: `F_3({0}) = {0,1}`; `F_3({0,2}) = {0,1,2}` (offsets `0,2` kill all three residues), so `C({0,2}) = 0`; `F_3({0,2}) = F_3({0,5})` (residue collision retained). - coincident offsets: `{0,0} ≡ {0}`, `C({0}) = ρ`. - repeated differences: `F_p({0,s,s}) = F_p({0,s})` for all tested `s`. - `L = P`: the cyclic-window variance is exactly `0` (the kernel identity `Var[N_L] = Σ_{s=-(L-1)}^{L-1}(L-|s|)(C({0,s}) - ρ²)` gives `0` at `L=P`, and direct enumeration gives a constant window count). `E[N_L] = L ρ`. Full wheel over `30030`: `ρ = 9/182`, `|A| = 1485`. **4. Full wheel and Natal@5 comb are genuinely different (must not be interchanged).** At `d = 0` the mod-30 twin-admissible residues are `{11,17,29}` (`3/30`); the comb base predicate `r mod 30 ∈ {11,17}` gives `2/30`. The comb drops exactly residue `29`. The comb is a legal instance of the same theorem with the single pairwise-coprime modulus `s_base = 30` (a 2-element predicate) plus `s_p = p` for `p ≥ 7`; the full wheel must be applied per prime `p ≥ 2`. The comb base has no pair differing by `2 mod 30`, so comb `C({0,2}) = 0`, while base pair `11→17` at offset `6` survives (`C({0,6}) > 0`). **5. Scope and limitations.** Finite and exact only; no anchored-prime-window transfer, no Aryan occupancy, no GD(2), no growing-order cumulant, no bound on `G2`/`β₂`/twin primes. A 4th-moment / cumulant bridge is route 209's object (`return #2475`), not done here. No Lean toolchain exists in this container: no build, no `verification_plan`, no axiom closure — the pinned adapter is a source review plus a numerically exact finite model, not new verified mathematics. The variance-note (`return #1914`/route 108, `return #2393`/route 198) already owns the finite identity; this run tests the pinned adapter, not the identity. - [Return #2468](/projects/twin-primes/return/2468): 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.