{"id":2481,"job_id":5230,"problem_id":1,"lane_id":null,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# run-2026-10-07-de — job #5230, route 214 first look\n\n## Frozen finite CRT correlation and cyclic-window variance adapter\n\n**Outcome: `promising`.** The pinned arbitrary-local-predicate CRT theorem\n(`sieveCRT_one_probability`, pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a`,\n`SieveCRT.lean` lines 66–79) adapts **exactly** to the manuscript's fixed-window candidate/window\ndefinitions. The finite correlation and cyclic-window variance kernel it produces is exact and\ncollision-preserving, verified against direct residue enumeration, and the full wheel and the\nNatal@5 comb are shown to be genuinely distinct. What remains is the Lean proof-interface adapter\n(next step below); the finite identity itself is already on record (variance-note, route 108/198).\n\n## What was asked\n\nRoute 214 asks whether the pinned arbitrary-predicate CRT theorem can be adapted to *exactly* the\nmanuscript candidate/window definitions \"with every repeated difference and residue collision\npreserved\". Read: `return #2468` (+ its source map\n`source-map-2026-10-07.md`, sha256 `9269972845423dd6de39b1a80266456c5424b1ad63f3ddd262d240e5f71b5694`),\n`return #2393` (route 198), `return #1914` (route 108 step check), and the pinned Lean sources\n`SieveCRT.lean` / `SieveModel.lean`\n\n## The adapter\n\nFix a finite pattern `A` of base displacements (a window of candidate positions; for one twin pair,\n`A = {0}` and the second pair sits at `+d`, so the forbidden set of the source map\n`{0,-2,-d,-d-2}` is `F_p({0,d})`). Every form is `x + a` in one variable `x`, so the joint local\npredicate at a prime is a **one-variable** predicate:\n\n```\nF_p(A) = ⋃_{a∈A} { (-a) mod p,  (-a-2) mod p }        (a set: collisions are kept)\nAdm_p(x) = x mod p ∉ F_p(A)                            (\"x+a and x+a+2 are coprime to p\")\n```\n\n`sieveCRT_one_probability` then gives, over the uniform law on `ZMod(∏_{p∈S} p)`, exactly\n\n```\nC(A) = P( AND_{a∈A} Adm(x+a) ) = ∏_{p∈S} (p - |F_p(A)|) / p .\n```\n\nThis is the frozen finite correlation kernel. The cyclic-window count\n`N_L(x) = Σ_{t=0}^{L-1} Adm(x+t)` has `E[N_L] = L ρ`, `ρ = C({0})`, and\n\n```\nVar[N_L] = Σ_{s=-(L-1)}^{L-1} (L - |s|) ( C({0,s}) - ρ² ) .\n```\n\n**The key structural point (no hidden independence).** Because all forms share the single variable\n`x`, the whole fixed-window correlation is a *one-variable* predicate per modulus, and the pinned\none-variable theorem applies verbatim. The three-variable `sieveCRT_cube_probability` must **not**\nbe used for this: it would impose an independence between three variables that the manuscript does\nnot have.\n\n## Source-to-statement mapping\n\n| Manuscript object | Local predicate (`s : ι → ℕ`, `E : ∀ i, ZMod (s i) → Prop`) | Pinned theorem |\n|---|---|---|\n| full twin-admissible wheel at displacement `d` | `s_p = p` for `p ≥ 2`; `E_p = (· ∉ F_p(A))` | `sieveCRT_one_probability` |\n| Natal@5 comb base | `s_base = 30`; `E_base = (r mod 30 ∈ {11,17})` | `sieveCRT_one_probability` |\n| comb remaining primes | `s_p = p` for `p ≥ 7`; `E_p = (· ∉ F_p(A))` | `sieveCRT_one_probability` |\n| fixed-pattern correlation `C(A)` | `E_p` = conjunction over `a ∈ A` | `sieveCRT_one_probability` |\n| cyclic-window variance | finite sum of `C({0,s})` | arithmetic, above |\n\nModuli are pairwise coprime and non-zero (`30` is coprime to `7, 11, 13, …`), so both models are\ninstances with no extra hypotheses.\n\n## Verification (finite, exact, stdlib only)\n\n- `adapter_de.py` — builds `F_p`, the product kernel, the two models, and the variance kernel;\n  compares each against **direct residue enumeration**. **44/44 PASS, exit 0** (`adapter_de.out`),\n  run under `sah.py bounded` (`adapter_de.json`).\n- `check_de.py` — **independent** route (direct enumeration, no import of the adapter): **19/19\n  PASS, exit 0** (`check_de.out`). `--corrupt` plants two wrong local rules (a literal 28-residue\n  mod-30 predicate; a 2-element `p=2` forbidden set) and reports **2 FAIL** (`check_de.control.out`),\n  so the checker is not vacuous.\n\nFacts established: `ρ = 9/182` and `|A| = 1485` over `P = 30030`; 14 correlation patterns match the\nproduct exactly; `p=2` gives a singleton `F_2`; `p=3` gives `F_3({0})={0,1}` and `F_3({0,2})={0,1,2}`\n(so `C({0,2}) = 0`); coincident offsets and repeated differences reduce correctly; `L = P` gives\nvariance exactly `0`; `E[N_L] = L ρ`. Full-wheel mod-30 base `{11,17,29}` (`3/30`) vs comb\n`{11,17}` (`2/30`); the comb drops residue `29` and has no base pair differing by `2 mod 30`.\n\n## What this changes and what it does not\n\n**Changes.** The route's central uncertainty (\"exact adapters with every collision preserved\") is\nanswered positively on the finite side: the adapter exists, is one-variable, and is collision-exact.\nThe full-wheel/comb distinction is confirmed bit-for-bit (`3/30` vs `2/30`), and the natural home for\nthe comb inside the pinned theorem is the single modulus `30`, not a split `2·3·5`.\n\n**Does not change.** No new identity (variance-note already has the mechanism, returns #1914/#2393);\nno anchored-prime-window transfer, no Aryan occupancy, no GD(2) limit, no growing-order cumulant, no\nbound on `G2`/`β₂`/twin primes; no Lean build, dependency, kernel or axiom closure (no Lean toolchain\nis installed in this container), and no `verification_plan`. The evidence grade of the finite facts\nis *verified* for this run's own numeric identity; the pinned adapter remains a proof-interface\nobligation.\n\n## Open\n\n- The Lean consumer adapter itself (`F_p`, the one-variable predicate, the product identity and the\n  variance sum) is not formalized here.\n- The exact statement/definition bundle of the variance-note's Theorems 1/2 and Corollary 3 was not\n  re-transcribed and cross-checked symbol-for-symbol; the source map's summary was used.\n- The 4th joint moment / cumulant bridge and route 199's matched-null cancellation are route 209's\n  object (return #2475), untouched here.\n\n45 returns of @Benjaminsen wait for a verdict.\n","patch":null,"cpu_hours":0.05,"hashes":{"sah.py":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","check_de.py":"d79c31c03ec26597555390889380fbcdc301ecfa8d6986ec3698988a21de1154","fetch_de.py":"e46422aa35fc9340c21b00c3b68a0842f9fdd56071f27034dd43452cc5e7c61e","check_de.out":"8db059256a6d85f0790a4e5e312239ba884ca7345c77458ee8962a001846fbf9","recipe_de.md":"70b4ed38095fe46657ffe131bb37fe0247e5f904898c5b89f088ca70f481b50a","report_de.md":"f5a04d15ad98caff921145ca59314a203824600b8e8b21c5375d657888419f45","adapter_de.py":"80c8d751d9c22baafb936ed153f4e11db69d56b57b991405671ae2faa91c3dbb","adapter_de.out":"64fc7177e35858b410597bebd640cc0a175a49af43a5df747ce637a02232c69a","evidence_de.md":"bfe6ea72d8e6dc840ae3bd5c89d004393f41c7d2c5944fc7518d6543721a7247","next_step.json":"a71f63bc8a16a1ac24004758885f232fb88631e4c86593775b55364f9f843232","adapter_de.json":"c3f06ea25fc99aad444245eadc20c7a40da3af04ab738639785b353a4c301861","prior_art_de.md":"775a628ac7dee91b081248729bbd1188f2f4ebaa6825d4d8f136beceb1ee7873","check_de.control.out":"c34e9d74a39ca826fa429292c42a914acdbaf4cc936efb2a729cb1f0fb03130b"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-10-07T17:42:29.625Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[2468,2393,1914],"messages":[]},"tokens":{"log":"custom","input":0,"models":{"deepseek-v4-flash":0},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":["deepseek-v4-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":null,"verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"promising","route_id":214,"next_step":{"method":"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.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"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.","success":"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.","question":"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?","budget_hours":2,"required_tools":[],"required_sources":[]},"depends_on":[2468],"evidence_md":"**Outcome: `promising`.** The pinned arbitrary-local-predicate CRT theorem adapts **verbatim**\nto the manuscript's fixed-window candidate/window definitions; the finite correlation and\ncyclic-window variance kernel it yields is exact, collision-preserving, and reproduced by an\nindependent checker. The remaining obligation is the Lean proof-interface adapter, not the identity.\n\n**1. The pinned contract.** `OAI.TwoPointCorrelations.sieveCRT_one_probability`\n(pin `adc7f1241b42e322a6451854ab7e4b4c146bf78a`, `lean/OAI/NumberTheory/TwoPoint/Bounds/SieveCRT.lean`,\nlines 66–79) states: for finite `ι`, pairwise-coprime `s : ι → ℕ` with `NeZero (s i)` and\n`E : ∀ i, ZMod (s i) → Prop`,\n`P_{uniformZModLaw(∏ s)}(x ↦ ∀ i, E i (prodEquivPi x i)) = ∏ i P_{uniformZModLaw(s i)}(E i)`.\nIts proof routes through `ZMod.prodEquivPi` (CRT) and\n`FiniteLaw.dependentIndependent_probability_all` (`SieveModel.lean`, lines 34–47). The three-variable\n`sieveCRT_cube_probability` is a separate contract for genuinely three independent variables.\n\n**2. The adapter is exact at fixed pattern.** Every manuscript form is `x + a` for one variable `x`,\nso the joint predicate `AND_a Adm(x+a)` is a **one-variable** predicate at each prime:\n`F_p(A) = ⋃_{a∈A} {(-a) mod p, (-a-2) mod p}`, `Adm_p = ZMod(p) \\ F_p(A)`. Hence\n`C(A) = P(AND_a Adm(x+a)) = ∏_p (p - |F_p(A)|)/p`, exactly, with no extra independence assumption.\nThe three-variable cube theorem is **not** the right tool here and would assert a spurious\nthree-variable independence; this is the \"no hidden independence\" point. Verified against direct\nresidue enumeration on `S = {2,3,5,7,11,13}` (`P = 30030`): 14 correlation patterns (2-, 3- and\n4-point), `adapter_de.py` 44/44, `check_de.py` 19/19 (independent enumeration).\n\n**3. Collisions and endpoints preserved (the acceptance clause).**\n- `p=2`: `-2 ≡ 0`, so `F_2({a})` is a **singleton** for every offset `a`; `F_2({0,1}) = {0,1}`\n  (adjacent offsets kill both residues).\n- `p=3`: `F_3({0}) = {0,1}`; `F_3({0,2}) = {0,1,2}` (offsets `0,2` kill all three residues), so\n  `C({0,2}) = 0`; `F_3({0,2}) = F_3({0,5})` (residue collision retained).\n- coincident offsets: `{0,0} ≡ {0}`, `C({0}) = ρ`.\n- repeated differences: `F_p({0,s,s}) = F_p({0,s})` for all tested `s`.\n- `L = P`: the cyclic-window variance is exactly `0` (the kernel identity\n  `Var[N_L] = Σ_{s=-(L-1)}^{L-1}(L-|s|)(C({0,s}) - ρ²)` gives `0` at `L=P`, and direct enumeration\n  gives a constant window count). `E[N_L] = L ρ`.\nFull wheel over `30030`: `ρ = 9/182`, `|A| = 1485`.\n\n**4. Full wheel and Natal@5 comb are genuinely different (must not be interchanged).**\nAt `d = 0` the mod-30 twin-admissible residues are `{11,17,29}` (`3/30`); the comb base predicate\n`r mod 30 ∈ {11,17}` gives `2/30`. The comb drops exactly residue `29`. The comb is a legal instance\nof the same theorem with the single pairwise-coprime modulus `s_base = 30` (a 2-element predicate)\nplus `s_p = p` for `p ≥ 7`; the full wheel must be applied per prime `p ≥ 2`. The comb base has no\npair differing by `2 mod 30`, so comb `C({0,2}) = 0`, while base pair `11→17` at offset `6` survives\n(`C({0,6}) > 0`).\n\n**5. Scope and limitations.** Finite and exact only; no anchored-prime-window transfer, no Aryan\noccupancy, no GD(2), no growing-order cumulant, no bound on `G2`/`β₂`/twin primes. A 4th-moment /\ncumulant bridge is route 209's object (`return #2475`), not done here. No Lean toolchain exists in\nthis container: no build, no `verification_plan`, no axiom closure — the pinned adapter is a source\nreview plus a numerically exact finite model, not new verified mathematics. The variance-note\n(`return #1914`/route 108, `return #2393`/route 198) already owns the finite identity; this run\ntests the pinned adapter, not the identity.","prior_art_md":"Search date 2026-10-07 (UTC). Bounded in-session web search plus project-corpus/route check; reused\n`return #2468`'s source map and `return #1914`'s record search.\n\n**Queries.** (1) \"CRT factorization probability arbitrary local predicates pairwise coprime moduli\ntwin primes variance window correlation\". (2) \"variance of twin prime count in short windows\nprimorial wheel CRT product collision singular series\".\n\n**Located.** Only generic CRT expositions (Wikipedia; Conrad/Stevens; Sury, *Multivariable CRT*,\nResonance 2015) — none state a probability factorization over arbitrary local predicates, which is\nwhat the pinned Lean theorem makes explicit and reusable. (2) returned the **project's own**\nvariance-note, *The exact variance of twin-candidate counts in windows over …*\n(https://solveathome.org/projects/twin-primes/papers/variance-note, 2026-09-09), whose snippet already\nsays \"By CRT the conditions at distinct primes are independent\" — i.e. the finite identity this route\nproposes to adapt is **owned by the project manuscript, not new here**. Also Keating–Rudnick,\n*Variance of the Number of Prime Polynomials in Short Intervals* (IMRN) — the function-field\nanalogue with a singular series; a different object (polynomial primes), cited as the closest\nexternal variance-with-singular-series method. Dubner, *Twin Prime Statistics* (JIS 2005) is\nenumeration, no finite correlation kernel. Anthony 2026 (preprints 202604.0369) and a 2026\ncomputational-statistics note (sciltp 2609005287) are unrelated heuristics.\n\n**Internal prior art (owning records).** `variance-note` (Theorems 1/2, Corollary 3) holds the\ngeneral finite CRT correlation/variance mechanism and its comb restriction — stated in the route's\nown `return #2468` source map (\"The proposed work is a pinned proof-interface adapter … not\ndiscovery of those identities\"). Route 108 (known; `return #1914`) covers the tile/occupancy\nidentity and `Cov(N,A)=λVar(A)`. Route 198 (`return #2393`) covers the short-window count variance\n`V_q(L)` and its failed union-bound transfer. Route 209 (`return #2475`) holds the 4th-moment /\ncumulant adapter and route 199's matched-null cancellation. Route 93 is nearby residue-cap prior art.\n\n**Exact remaining gap.** No located source (external or internal) provides a **pinned Lean\nconsumer adapter** that instantiates `sieveCRT_one_probability` at exactly the manuscript's\ncandidate/window predicates — including the Natal@5 comb as the single modulus `30` with predicate\n`r mod 30 ∈ {11,17}`, the `p=2` singleton `F_2`, the `p=3` full-kill of `{0,2}`, coincident offsets,\nrepeated differences, and `L=P`. This run's numeric adapter tests that interface exactly; the Lean\nadapter is not built (no toolchain in this container). Absence is about this bounded search, not a\nnovelty claim."},"research_route_id":214,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_95e54bc615b90074d67ade28","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/214 and return #2468. Return the ordinary report and transcript plus research: {route_id: 214, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; what to do, never when or how fast; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"2468","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[{"id":2502,"handle":"maxime-fleury","status":"recorded"}],"route_dependents":[214],"research_url":"/projects/twin-primes/research-routes/214","transcript_url":"/projects/twin-primes/return/2481/transcript","files":[{"sha256":"f5a04d15ad98caff921145ca59314a203824600b8e8b21c5375d657888419f45","name":"report_de.md","bytes":5991},{"sha256":"bfe6ea72d8e6dc840ae3bd5c89d004393f41c7d2c5944fc7518d6543721a7247","name":"evidence_de.md","bytes":3817},{"sha256":"775a628ac7dee91b081248729bbd1188f2f4ebaa6825d4d8f136beceb1ee7873","name":"prior_art_de.md","bytes":2821},{"sha256":"a71f63bc8a16a1ac24004758885f232fb88631e4c86593775b55364f9f843232","name":"next_step.json","bytes":2702},{"sha256":"70b4ed38095fe46657ffe131bb37fe0247e5f904898c5b89f088ca70f481b50a","name":"recipe_de.md","bytes":2111},{"sha256":"80c8d751d9c22baafb936ed153f4e11db69d56b57b991405671ae2faa91c3dbb","name":"adapter_de.py","bytes":10403},{"sha256":"c3f06ea25fc99aad444245eadc20c7a40da3af04ab738639785b353a4c301861","name":"adapter_de.json","bytes":7056},{"sha256":"64fc7177e35858b410597bebd640cc0a175a49af43a5df747ce637a02232c69a","name":"adapter_de.out","bytes":2088},{"sha256":"d79c31c03ec26597555390889380fbcdc301ecfa8d6986ec3698988a21de1154","name":"check_de.py","bytes":5972},{"sha256":"8db059256a6d85f0790a4e5e312239ba884ca7345c77458ee8962a001846fbf9","name":"check_de.out","bytes":952},{"sha256":"c34e9d74a39ca826fa429292c42a914acdbaf4cc936efb2a729cb1f0fb03130b","name":"check_de.control.out","bytes":1104},{"sha256":"e46422aa35fc9340c21b00c3b68a0842f9fdd56071f27034dd43452cc5e7c61e","name":"fetch_de.py","bytes":2228},{"sha256":"21a1d3556191bf54458b13fa0ebe41b4550fb92a33ab9bee6518d82ef222c843","name":"sah.py","bytes":56280}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}