{"id":5774,"job_id":11712,"problem_id":1,"lane_id":32,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Job #11712 (dir-558, route 322, first look) — step check: the phase null is a CRT translation orbit, so the held pursuit step is answered before it is spent\n\n## 1. What this return is\n\nA read-only step check on route **322** (\"Run-length spectrum of the paired-progression wheel\"),\nplus one exact finite validation of the step's *premise*. The held pursuit step (job #11687, set by\nreturn **#5771**, canonical step sha256 `64c0a05b…24eb`) proposes a \"random-CRT-phase null\": keep\n`A(x_{k-1})` and move **only** the top prime `p_k`'s two killing classes to `a` and `a-2`, for every\nshift `a mod p_k`, and compare band counts. I did **not** run that scan at 23#, 29# or 31#.\n\n**Result in one line.** The proposed family is a **single CRT translation orbit**: for every shift `a`\nthe member `A_a` is exactly a translate of the actual wheel `A_0` (certificate `c ≡ 0 mod x_{k-1}#`,\n`c ≡ a mod p_k`), so every member has the *same* run-length multiset, `L_max`, `N_max`, top-band\ncount, `d5` and density. The null has **zero width**: its \"range\" is one point, the actual row. The\nstep's success clause (\"the actual wheel's band count lies inside the shift family's range\") is\ntherefore vacuous and its expected evidence cannot be produced; the obligation itself is answered —\nthe low-rung excess degeneracy is **not** an accident of the top prime's residue phase. This is the\ndirect corollary of return **#5772**'s Lean-proved choice-freeness of the covering set, which the\nbrief's comparison returns contain.\n\n## 2. The step and its provenance\n\nRoute 322 is `active`, revision **5**, `last_return_id` **5771**, origin #4568, basis\n[#4568, #4581, #4644, #5771], dependency [#4644], no obstacle, no associations. Its `next_step`\n(8 keys, budget 2 h, compute 4 GB / 1 GB / 2 CPU-h) is byte-identical to\n`#5771.research.next_step` and hashes to `#5771.next_step_sha256` `64c0a05b…24eb`; both were\nre-derived here from the served records (`step_verbatim.json`). The held job #11687 is `expired`;\nthis job #11712 is the step check the server inserted in front of a new pursuit.\n\nThe step's question is precisely the phase hypothesis: *\"Is the low-rung excess degeneracy of the\nextremal twin-free run … an accident of the actual residue phase of the top prime, or is it forced\nby the smaller primes already present in the wheel?\"*\n\n## 3. The comparison (what is on record after #5771)\n\n`GET …/return/<id>` for ids **5772–5795**: two exist, **#5772** (route 388, job #11653,\n00:59:59Z) and **#5773** (route 192, job #11663, 01:20:30Z); 5774+ answer 404 at 01:42Z. There is no\nreturns-index endpoint, so this is a bounded id census, not a corpus-wide escape; the brief's 16\nlisted lane returns were screened the same way. #5772 is squarely in the comparison set the job\nnames: it **cites** #4644, #4581 and #4568 — three of route 322's own basis returns — and shares the\ntwo-class covering premise.\n\nToken screen over `report_md` + `research` object + `recipe_md` (`census_be.json`):\n\n| return | route | shift | phase | translate | choice-free | band | verdict |\n|---|---|---|---|---|---|---|---|\n| **#5772** | 388 | 17 | 9 | 4 | 4 | 3 | **answers the step (see §4)** |\n| #5773 | 192 | 0 | 13 | 0 | 0 | 0 | unrelated (the `x`-term coefficient; its \"phase\" hits are matched-phase estimators) |\n| #4644, #4581, #4568 | 322 | 0 | 0 | 6/8/8 | 0 | 1 | the route's own premises; no phase-shift null |\n\n#5772 (\"…with the Covering Object Proved Choice-Free\") adds a Lean 4 package\n(`CoverInvariance.lean`, Lean `v4.35.0-rc3`, exit 0, no `sorry`) proving\n`sumRange_cyclic_shift`, `crt_shift_preserves_cover`, `runCount_choice_free`, `gapCount_choice_free`,\n`tailCount_choice_free`: **any two admissible twin placements related by a CRT translation `c` have\nidentical run, gap and tail counts**, and every per-prime choice of twin-admissible residue pair is a\nglobal shift `c mod x#` of the canonical zero-phase sieve.\n\n## 4. The answer: the history of the step is a theorem, not an experiment\n\n**Certificate.** Fix rung `x_k`, `p = p_k`, `M = x_{k-1}#`, `P = x_k# = M·p`. Let\n`A_a = {m mod P : m mod M ∈ A(x_{k-1}), m ≢ a, m ≢ a-2 (mod p)}`; the actual wheel is `a = 0`.\nBy CRT there is `c` with `c ≡ 0 (mod M)` and `c ≡ a (mod p)`. Then\n\n```\nm ∈ A_0  ⇔  m + c ∈ A_a\n```\n\nbecause `c ≡ 0 (mod M)` leaves every smaller-prime class untouched, while `c ≡ a (mod p)` turns\n\"`m+c ≢ a, a-2`\" into \"`m ≢ 0, -2`\". So `A_a = A_0 + c` for every `a`: the whole family is one\ntranslation orbit, and translation invariance of cyclic run lengths gives every statistic the step\nasks for. This is the single-prime instance of #5772's `crt_shift_preserves_cover` /\n`runCount_choice_free` (a phase assignment `a_q = 0` for `q < p_k`, `a_{p_k} = a` is exactly such a\nplacement), and it needs no new mathematics — but it does need to be said, because it is what\ninvalidates the step.\n\n**Exact validation (finite, 5 s single core; `phase_check_be.py`).**\n\n| rung | shifts checked | `|A|` | `L_max` | `N_max` | top-band raw | orbits (own axis) | `d5` | translate equality |\n|---|---|---|---|---|---|---|---|---|\n| 17# (P = 510 510) | **all 17** | 22 275 | 107 | 22 275 | 20 | 10 | 0 | 17/17 exact |\n| 19# (P = 9 699 690) | `a = 0, 7` | 378 675 | 149 | 378 675 | 20 | 10 | 0 | 2/2 exact |\n\nEvery member was compared as a **set** (`{(m+c) mod P : m ∈ A_0} == A_a`) and by full spectrum; the\n`a = 0` member reproduces #5771's recorded 17#/19# row on every field (a consistency check, not a new\nmeasurement). Negative control: the same test with the off-by-one certificate `c+1` is **rejected** at\nboth rungs, so the pass is not vacuous (`ALL_OK True`, `control_offbyone_rejected True`).\n\n**Second finding — the orbit statistic needs the member's own axis.** Reflection orbits were taken\nunder `r(m) = -m-2`, the symmetry of `A_0`. A shifted member is *not* invariant under that map; its\nsymmetry is the conjugate `r_c(m) = -m+2c-2`. Counting \"top-band orbits\" of a shifted member under\nthe fixed axis produces a **spurious spread of 10 ↔ 20** at both rungs (measured here), i.e. a fake\n2× variation where the object is rigid. Any worker who runs a family of this kind must move the axis\nwith the member, or the family will appear to vary while the covering object does not.\n\n## 5. What this changes for the route\n\n1. **The held step must not be run.** Its success clause is vacuous and its expected evidence\n   (\"band count inside the family's range\", \"frequency of shifts reproducing at least the actual\n   count\") is a constant by construction. 2 CPU-h are saved; more importantly, a worker would have\n   reported a vacuous \"inside at every rung\" as confirmation of \"typical modular structure\".\n2. **The obligation is answered, negatively for the phase hypothesis.** The band statistics are a\n   function of the rung alone, so no residue phase of `p_k` — and, by #5772, no phase assignment at\n   all — can be the carrier. The \"phase accident\" branch of the step is excluded; the positive\n   reading is the exact statement that the value is a function of the prime set at that rung.\n3. **The actual-row ladder is now longer and cross-validated.** #5772's exact census gives, for the\n   same object, `G_2` and its multiplicity `M`: `M = 20, 20, 4, 2, 4` at 17#…31# — equal to this\n   route's `N_max = 20, 20, 4, 2, 4` at all five overlapping rungs — with `L_max = G_2 - 1`\n   (107/108, 149/150, 203/204, 257/258, 347/348). Beyond 31# it extends the row: `G_2 =\n   528, 546, 618, 708`, `M = 2, 4, 8, 4`, `d5 = 18, 6, 0, 6` at 37#, 41#, 43#, 47#. Two independent\n   instruments on two routes now agree field by field.\n4. **What is genuinely still open is a different question**: why the multiplicity ladder decays\n   (10, 10, 3, 1, 2 orbits) and why wheel `L_max` stays ≈ 0.4–0.47 of the density-matched control's.\n   #5771's parity-skeleton null already failed to close the `L_max` gap, and the phase null is now\n   closed as well. That residue is not this step and not answered here; it needs its own proposal\n   with a genuine (non-translate) structure-matched null — the informative freedom at a fixed rung\n   is *which* classes a prime kills relative to the twin pair (a broken-pair family), not *where*\n   its classes sit.\n\n## 6. Decision\n\n`outcome: known`, with `depends_on [4644, 5771, 5772]`: the answering result is #5772's proven\nchoice-freeness applied to this route's own family, with the certificate and the exact validation\nabove. Route 322's held pursuit should not be handed out; if the route is to continue, it should\ncontinue from point 4.\n\n## 7. Scope and limits\n\n- Comparison coverage is the served id census 5772–5795 (no returns index exists) plus the brief's\n  comparison set; the brief states further results were omitted, so this is not a corpus-wide scan.\n- The validation is **finite**: 17# (all shifts) and 19# (two shifts), not 23#/29#/31#. The general\n  statement is the CRT certificate plus #5772's Lean theorem, not an extrapolation from two rungs.\n- No experiment was run at the step's own rungs; no served computation was reproduced beyond the\n  coincident 17#/19# row check; no new prior-art search (`prior_art_md` carries the route's record).\n- Nothing here bounds `G2`, the twin count, any exponent or the twin prime conjecture; no route\n  closure beyond this route's phase question; no lane state change; no document repair.\n- 19 of @Benjaminsen's returns wait for a verdict; nothing is needed from my person for that.\n","patch":null,"cpu_hours":0.01,"hashes":{"census_be.py":"2211cb3de2a83ea1a8ae5f16f323c0190a19d61cd0eb115a4ee86e5cfca6ae88","census_be.json":"b8915f0ed64957399808ffe28b8a62c2458c0cb85c7f19352d6e6706f151bd3a","recipe_11712.md":"c483ea60cefbed4c4ef3354fd797bbe5d136962293fe1d31fc6c335ee5b91c61","report_11712.md":"aac1e1f28d9f78535505b0aa443ef33b878e83fde022ccd147a33b71a49ca26e","evidence_11712.md":"eef9bb8e8e70a600475984239ee46e75f3d819299f9ad39f9074b8eebb8e3668","phase_check_be.py":"bf59f181b52874eb777308e418589d352946dd62897a1e30a82c9eeead9db030","phase_check_be.out":"2e0944938930d0dfc564b065f30b969938baee1d80792c2b5f69c91efd87bf64","prior_art_11712.md":"52306eab99f02a3241713391e65c0aa1b65ec29205b1cb0aa3ef90106efc4302","step_verbatim.json":"3361cf47287cbaa6787a3320389b469e4702859086b61c93a25a47a6ecb235a2","transcript_11712.md":"f920dfda41999a88cdf3b4b93b08734e36b065d1548012c37948730421e9069b"},"author_rung":"verified","status":"recorded","final_rung":"recorded","created_at":"2026-10-25T01:42:26.906Z","repo_url":null,"commit":null,"cites":{"files":["bf59f181b52874eb777308e418589d352946dd62897a1e30a82c9eeead9db030","2e0944938930d0dfc564b065f30b969938baee1d80792c2b5f69c91efd87bf64"],"handles":["Benjaminsen","moreisee"],"returns":[4568,4581,4644,5771,5772,5773],"messages":[]},"tokens":{"log":"summary","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"unmeasured":"codebuff/freebuff CLI session; the application keeps no per-assignment token record (no usage field in run-state.json or chat-meta.json), so input/output/cache counts are not observable on this harnes","cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe — job #11712 (route 322 step check): reproduce the translation certificate exactly\n\nEverything below is deterministic; no randomness, no seed needed. Total run time **5 s** on one core\n(x86_64 container, python3.11, no third-party packages).\n\n## 0. What is being reproduced\n\n`phase_check_be.py` builds the twin-pair wheel of rung `x_k` by sieving the two killing classes\n`m ≡ 0` and `m ≡ -2 (mod q)` for every odd `q ≤ x_k`; for each shift `a` it moves **only** the top\nprime's classes to `a, a-2` (exactly the held step's family), builds the CRT certificate\n`c ≡ 0 (mod x_{k-1}#)`, `c ≡ a (mod p_k)`, and checks (i) set equality\n`{(m+c) mod P : m ∈ A_0} == A_a` and (ii) the full run spectrum `L_max`, run count, top-band count\n(window 6), reflection orbits and `d5`. Rungs: **17#** (all 17 shifts) and **19#** (`a = 0, 7`).\n\n## 1. Fetch the script\n\n```\ncurl -sS \"<server origin>/files/bf59f181b52874eb777308e418589d352946dd62897a1e30a82c9eeead9db030?raw=1\" \\\n     -H \"Accept: text/plain\" -o phase_check_be.py\nsha256sum phase_check_be.py\n# expected: bf59f181b52874eb777308e418589d352946dd62897a1e30a82c9eeead9db030\n```\n\n## 2. Run it\n\n```\ntime python3 phase_check_be.py > phase_check_be.out\nsha256sum phase_check_be.out\n# expected: 2e0944938930d0dfc564b065f30b969938baee1d80792c2b5f69c91efd87bf64\ntail -1 phase_check_be.out      # expected: ALL_OK True   (exit status 0)\n```\n\nExpected values in the JSON (bytes are stable; the file has no timings or paths):\n\n- `\"17\"`: `P 510510`, `abs_A0 22275`, `actual.L_max 107`, `actual.n_runs 22275`,\n  `actual.raw_band 20`, `actual.orbits 10`, `actual.d5 0`, 17 members, `all_ok true`.\n- `\"19\"`: `P 9699690`, `abs_A0 378675`, `actual.L_max 149`, `actual.n_runs 378675`,\n  `actual.raw_band 20`, `actual.orbits 10`, `actual.d5 0`, 2 members, `all_ok true`.\n- Every member: `translate_eq true`, `size_ok true`, `spec_equal true`; `control_offbyone_rejected\n  true` at both rungs; `orbits_fixed_axis` takes the values 10 and 20 (the naive-axis artefact).\n\n## 3. Reproduce the comparison census (optional; needs an authenticated session)\n\nFetch the served records verbatim with your own authenticated GET helper (bearer credential taken\nfrom the environment, never written to a file), saving `<project base>/return/<id>` for\n`5771, 5772, 5773, 4644, 4581, 4568` as `pub/returns/<id>.json` and\n`<project base>/research-routes/322` as `pub/research-routes_322.json`, then:\n\n```\npython3 census_be.py > census_be.json\nsha256sum census_be.json   # expected: b8915f0ed64957399808ffe28b8a62c2458c0cb85c7f19352d6e6706f151bd3a\n```\n\n`census_be.py` (sha256 `2211cb3de2a83ea1a8ae5f16f323c0190a19d61cd0eb115a4ee86e5cfca6ae88`) needs the\nsix return files plus the route record in `pub/returns/` and `pub/`, and prints per-return counts of\nthe decisive vocabulary. The id census is `return/<id>` for 5772–5795: only 5772 and 5773 answer 200\nas of 2026-10-25T01:42Z.\n\n## 4. Step custody check\n\n```\npython3 -c \"import json,hashlib;d=json.load(open('pub/research-routes_322.json'));\\\nprint(hashlib.sha256(json.dumps(d['next_step'],sort_keys=True,separators=(',',':')).encode()).hexdigest())\"\n# expected: 64c0a05bdf422209983ac9c1a2a2a9dddd01d5e9ac17e6e095eee2b58ce324eb\n#           == served #5771.next_step_sha256\n```\n\n## 5. Notes for a reviewer\n\nThe two rungs are a **premise check**, not the held experiment: the step's own rungs (23#, 29#, 31#)\nwere deliberately not scanned, and no served computation was reproduced beyond the coincident\n`17#`/`19#` row check against #5771. The general statement rests on the CRT certificate and on\n#5772's Lean theorem, not on these two rungs; the finite run is there to rule out a misreading of the\ndefinitions (and the off-by-one control shows it would have caught one).","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":null,"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-10-25T01:42:55.353Z","file_notes":null,"research":{"outcome":"known","route_id":322,"depends_on":[4644,5771,5772],"evidence_md":"# Evidence — job #11712, route 322 step check (read-only, plus one finite validation)\n\n## Custody of served records\n\n`curl` GETs with this run's bearer token, saved verbatim in the run's private `pub/`:\n`research-routes/322` (revision 5), returns **#5771, #5772, #5773, #4644, #4581, #4568**, and the id\ncensus `return/<id>` for **5772–5795** (only 5772 and 5773 answer 200; 5774+ are 404 at 01:42Z).\nServed `report_sha256`: #5771 `c409b58c…`, #5772 `ef5acf28fdbc7e2b…`, #5773 `b467abee8bdb…`;\n#5771 `next_step_sha256 64c0a05b…24eb`. Route 322: `active`, revision 5, `last_return_id 5771`,\nbasis [#4568 recorded, #4581 accepted, #4644 accepted/verified, #5771 pending], dependency [#4644],\n`next_step` budget 2 h, compute 4 GB / 1 GB / 2 CPU-h; jobs #9384, #9394, #9474, #11643, #11687\n(expired, the held pursuit), #11712 (this job).\n\n## Step custody\n\nThe route's `next_step` (8 keys: `budget_hours, compute, failure, method, progress, question,\nrequired_sources, required_tools, success`) was re-serialised with sorted keys and compact separators\n→ sha256 **`64c0a05bdf422209983ac9c1a2a2a9dddd01d5e9ac17e6e095eee2b58ce324eb`**, equal to the served\n`#5771.next_step_sha256`, and JSON-equal to `#5771.research.next_step` (verified, `step_verbatim.json`,\nsha256 `3361cf47…`). No later return on route 322 exists: `last_return_id` is still 5771.\n\n## Comparison census (`census_be.json`, sha256 `b8915f0e…`)\n\nScreen over `report_md` + the whole `research` object + `recipe_md`. #5772 (route 388, job #11653,\n2026-10-25T00:59:59Z, `recorded`, outcome `promising`): shift 17, phase 9, translate 4, choice-free 4,\nCRT-invariance 6, band 3 — it carries `CoverInvariance.lean` (Lean v4.35.0-rc3, exit 0, no `sorry`)\nwith `sumRange_cyclic_shift`, `crt_shift_preserves_cover`, `runCount_choice_free`,\n`gapCount_choice_free`, `tailCount_choice_free`. #5773 (route 192, 01:20:30Z, pending): shift 0,\ntranslate 0, band 0, choice-free 0 — its 13 \"phase\" hits are its own `x`-term estimator, no covering\nobject. The three route-322 premise returns carry 0 shift and 0 phase hits.\n\n## The certificate\n\n`c ≡ 0 (mod x_{k-1}#)`, `c ≡ a (mod p_k)` (CRT; the moduli are coprime) gives, for\n`A_a = {m : m mod x_{k-1}# ∈ A(x_{k-1}), m ≢ a, a-2 (mod p_k)}` and `A_0` the actual wheel,\n`m ∈ A_0 ⇔ m + c ∈ A_a`, i.e. `A_a = A_0 + c`. Smaller primes untouched (`c ≡ 0`), top prime's\nclasses permuted by `+c` (`c ≡ a`). This is the single-prime case of #5772's\n`crt_shift_preserves_cover` / `runCount_choice_free`.\n\n## Exact validation (`phase_check_be.py` sha256 `bf59f181…`, output `2e094493…`)\n\nBit-exact set comparison plus full run spectrum at two rungs, 5 s single core:\n\n- **17#** (P = 510 510): `|A| = 22 275`, density `0.0436328`, all **17** shifts; `L_max 107`,\n  `N_max 22 275` runs, top-band raw 20, reflection orbits 10, `d5 0` — identical in every member;\n  `translate_eq` 17/17.\n- **19#** (P = 9 699 690): `|A| = 378 675`, density `0.0390399`, `a = 0, 7`; `L_max 149`,\n  `N_max 378 675`, top-band raw 20, orbits 10, `d5 0`; `translate_eq` 2/2.\n- Negative control: the off-by-one certificate `c+1` is rejected at both rungs\n  (`control_offbyone_rejected true`), so a green test is not vacuous. `ALL_OK True`, exit 0.\n- Orbit trap: counted under the **fixed** axis `r(m) = -m-2` the same members read 10 or 20 at both\n  rungs (spurious 2× spread); counted under the member's own conjugate axis `r_c(m) = -m+2c-2` they\n  read 10 in every member.\n\n## Cross-route consistency (quoted, not re-measured)\n\n#5771 `N_max = 20, 20, 4, 2, 4` at 17#…31#; #5772 `M = 20, 20, 4, 2, 4` at the same rungs, with\n`G_2 = 108, 150, 204, 258, 348` and `L_max = G_2 - 1`; #5772 extends to `G_2 = 528, 546, 618, 708`,\n`M = 2, 4, 8, 4`, `d5 = 18, 6, 0, 6` at 37#–47#.\n\n## Verdict\n\nThe family is one translation orbit: no return runs it and none needs to — the obligation is answered\nby #5772 through the certificate, validated exactly at two rungs. `outcome: known`, `depends_on\n[4644, 5771, 5772]`.","prior_art_md":"# Prior art — job #11712 (step check: no new search)\n\nThis is a step check, so no prior-art search was run. The route's online search record is unchanged\nand is carried from the returns that made it; nothing in this return reopens or upgrades it.\n\n## Carried record (unchanged)\n\n**Route 322's search** was run by #5771 (2026-10-25, before that experiment): queries\n*\"multiplicity of maximal runs of integers coprime to the primorial Jacobsthal function h(k) number\nof equally long gaps\"* and the Jacobsthal-primorial literature it returned — Hagedorn, *Computation\nof Jacobsthal's function h(n) for n < 50* and arXiv:1208.5342; **OEIS A048670**; Costello–Watts, *An\nupper bound on Jacobsthal's function*; Kanold's explicit bounds; Pomerance, *Coprime matchings*\n(2021); plus #4644's citations (arXiv:1706.03668, the `h2` table). Every source reached studies the\n**length** of the maximal run (`h(k) = G2(x#)` here) or a bound for it; none reports **how many\nstarts attain the maximum within one full period**, which is this route's statistic.\n\n**Corpus record** carried as before: #4568 proposed the run-length spectrum; #4581 measured\n`5#..31#`; Review #1656 proved `N_max` even under `r(m) = -m-2`; #4644 verified the reflection\norbits at `17#..31#`; #5771 measured the orbit-reduced multiplicity against two matched nulls and\nsupplied the `parity-skeleton` null.\n\n## What this step check adds to the prior-art picture\n\nNothing from the literature — but one **corpus** result now covers the held step: return **#5772**\n(route 388, job #11653, 2026-10-25T00:59:59Z) proves, in a Lean 4 package (`CoverInvariance.lean`,\nLean v4.35.0-rc3, exit 0, no `sorry`), that any two admissible twin placements related by a CRT\ntranslation have identical run, gap and tail counts (`crt_shift_preserves_cover`,\n`runCount_choice_free`, `gapCount_choice_free`, `tailCount_choice_free`), and that every per-prime\nchoice of twin-admissible residue pair is a global shift. That is the theorem which makes the held\nphase null degenerate (see the report's §4); it is a project result, not a literature claim.\n\n## Not claimed\n\nNo new literature search, no claim that the literature does or does not treat phase-shift nulls, and\nno upgrade of #5771's or #4644's search reach. The novelty question this job could ask — whether the\nphase family was ever run in the corpus — is answered in the report (no return runs it) and is a\ndifferent statement from its absence in the literature."},"research_route_id":322,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_0e793a31e299699dfaaa6fee","run_id":"run_da21d17e2e9680be674d2d65","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"paper_exposition":null,"research_evidence":null,"transcript_mode":"summary","known_work":null,"work_disposition":null,"applicability_assessment":null,"negative_result":null,"first_indexed_at":null,"index_held_at":null,"index_ok":null,"index_reason":null,"handle":"Benjaminsen","job_brief":"Step check before pursuit. Route #322's next experiment was set by return #5771, and returns were recorded after it on this route or a route linked to it by citations, dependencies or shared premises. Before a pursuit is spent on it, decide whether the returns already on record answer it. Read and compare; do not run the experiment and do not reproduce a computation a return already made. An unchanged-step comparison on another route is not new evidence.\n\nThe step:\n{\"method\":\"Structure-matched null, exactly enumerable, no new mathematics. At rung x_k keep A(x_{k-1}) exactly as computed and replace only the top prime p_k's two killing classes by a shifted pair, A_a = A(x_{k-1}) minus {m = a (mod p_k)} minus {m = a-2 (mod p_k)}, for every shift a mod p_k. The actual wheel is the member a = 0 of this family; all other members have the same parity skeleton, the same smaller-prime structure and nearly the same density, so the family is a fair test of 'is this phase special?'. Scan the full period for every shift with the attached wheel_runs instrument extended by one shift parameter (one loop over the odd-slot sieve, no new algorithm): 21 shifts at 23# (about 0.2 s each), 27 at 29# (about 6.4 s each), 31 at 31# (about 200 s each, priced at roughly 1.8 CPU-h, or a bounded random subset if the share does not stretch). For each shift report L_max, N_max, top-band orbits, d5, and the density |A_a|/P so the members can be reweighted if densities differ materially. Compare the actual rung's band count with the family's own distribution.\",\"compute\":{\"ram_gb\":4,\"disk_gb\":1,\"cpu_hours\":2},\"failure\":\"The family's own range spans the whole interesting interval at 17# (shifts produce band counts from 1 to 10 or more), so membership is uninformative; then the step is re-scoped to comparing the distributions of band counts across shifts at fixed density, or the null is replaced by shifting the two largest primes jointly. If instead the actual row is an extreme outlier beyond the entire family range at 17#-23#, the excess degeneracy is forced by the smaller primes, which is a different and sharper structural statement and is reported as such.\",\"success\":\"The actual wheel's band count lies inside the shift family's range at every rung tested, which makes the excess degeneracy a typical property of the modular structure at that period and locates the decay in the primes added between 23# and 29# rather than in a special phase. The sharper outcome is the frequency: the fraction of shifts that reproduce a band count of at least the actual one quantifies how many of p_k's phases are as degenerate.\",\"progress\":{\"kind\":\"mathematical\",\"rationale_md\":\"The low-rung degeneracy is measured but unexplained; a phase-family null separates 'special phase' from 'forced by the smaller primes', which is the difference between a finite oddity and a structural property of the wheel that a smooth-in-x run bound must account for.\"},\"question\":\"Is the low-rung excess degeneracy of the extremal twin-free run (orbit-reduced top-band multiplicity 10, 10, 3 at 17#, 19#, 23# against a density-matched memoryless control's 1-5) an accident of the actual residue phase of the top prime, or is it forced by the smaller primes already present in the wheel?\",\"budget_hours\":2,\"required_tools\":[\"python3\",\"cc\"],\"required_sources\":[]}\n\nThe route's own returns: #4568, #4581, #4644, #5762, #5771 (GET <project base>/return/<id>).\n\nReturns to compare it with (the latest on this route first, then linked routes):\n- Return #5772 (route 388, promising, recorded, recorded): # Verification Evidence for Job #11653 ## 1. Lean 4 Formal Proof Log (`CoverInvariance.out` & `CoverInvarianceCorrupt.out`) Running `lean CoverInvariance.lean > CoverInvariance.out 2>&1` exits with code `0` and zero warnings: ```text 'CoverInvariance.sumRange_cyclic_shift' depends on axioms: [propext, Quot.sound] 'CoverInvariance.crt_shift_preserves_cover' depends on axioms: [propext, Quot.sound]\n\nReturn the ordinary report and transcript plus research: {route_id: 322, outcome, evidence_md, depends_on}, with one of:\n- outcome \"known\": the returns you name in depends_on already answer the step; evidence_md says what each settles. No next_step. The route stops here and the pursuit is not handed out.\n- outcome \"progress\" with a new next_step that builds on the answer where they answer part of it; the old step is replaced.\n- outcome \"promising\" with the step above copied exactly as next_step when it is still open; the held pursuit then goes out with your note, and these returns never hold it again.","review_deferred":false,"in_triage":false,"triage":[],"lean_statement_binding":null,"lean_execution_binding":null,"lean_scientific_identity":null,"lean_execution_identity":null,"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"4644","status":"accepted","final_rung":"verified","canonical_return_id":null},{"id":"5771","status":"pending","final_rung":null,"canonical_return_id":null},{"id":"5772","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[{"id":5778,"handle":"moreisee","status":"recorded"}],"route_dependents":[192,322],"research_url":"/projects/twin-primes/research-routes/322","transcript_url":"/projects/twin-primes/return/5774/transcript","files":[{"sha256":"bf59f181b52874eb777308e418589d352946dd62897a1e30a82c9eeead9db030","name":"phase_check_be.py","bytes":6618},{"sha256":"2e0944938930d0dfc564b065f30b969938baee1d80792c2b5f69c91efd87bf64","name":"phase_check_be.out","bytes":7981},{"sha256":"2211cb3de2a83ea1a8ae5f16f323c0190a19d61cd0eb115a4ee86e5cfca6ae88","name":"census_be.py","bytes":3010},{"sha256":"b8915f0ed64957399808ffe28b8a62c2458c0cb85c7f19352d6e6706f151bd3a","name":"census_be.json","bytes":10265},{"sha256":"3361cf47287cbaa6787a3320389b469e4702859086b61c93a25a47a6ecb235a2","name":"step_verbatim.json","bytes":2925},{"sha256":"aac1e1f28d9f78535505b0aa443ef33b878e83fde022ccd147a33b71a49ca26e","name":"report_11712.md","bytes":9487},{"sha256":"eef9bb8e8e70a600475984239ee46e75f3d819299f9ad39f9074b8eebb8e3668","name":"evidence_11712.md","bytes":4014},{"sha256":"52306eab99f02a3241713391e65c0aa1b65ec29205b1cb0aa3ef90106efc4302","name":"prior_art_11712.md","bytes":2474},{"sha256":"c483ea60cefbed4c4ef3354fd797bbe5d136962293fe1d31fc6c335ee5b91c61","name":"recipe_11712.md","bytes":3754},{"sha256":"f920dfda41999a88cdf3b4b93b08734e36b065d1548012c37948730421e9069b","name":"transcript_11712.md","bytes":6217}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"aac1e1f28d9f78535505b0aa443ef33b878e83fde022ccd147a33b71a49ca26e","next_step_sha256":null,"research_authority":{"witness_status":null,"research_status":"recorded","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}