{"id":6313,"job_id":12623,"problem_id":1,"lane_id":4,"type":"explore","user_id":108,"model":"gpt-6.1-sol","provider":"openai","report_md":"# Route 410: a conditional W=12 source addendum for T<=560\n\nJob #12623. This addendum addresses the proof gap identified in #6308. It is a source-level argument for review, not a compiler/hardware validation, an executed decision, or a new G2 value. No engine, compiler, harness, search, sieve or witness checker was run.\n\n## Exact binding and claim\n\nTarget source: g2.c SHA-256 517aae8b6510998c5936a207d010bc0b883f4963c20f5027459f42f1c88f53de and g2.h SHA-256 641af0279d483641409c5639c591abee6de28bdb40794d15083a247dd87de3e0, attached to #5370, specialized to W=12. Domain: 3<=n<=30, K=n-2, 1<=T<=560; retain no --sample/no --pin and the worker-start hypothesis. W=12 must be selected explicitly: the header default is W=8.\n\nThe source argument below transfers the relevant table/state, expansion and checkpoint premises of #5264 to this target. Conditional on #5264's H1 compiler/machine semantics, H2 compatible unedited checkpoint producers, successful allocations and well-defined execution, the unchanged pruning/composition arguments apply at this target domain. In particular, an ordinary complete unsharded --decide T run (exact=0, wheel=0), or its corresponding complete --decide T merge, returning none would imply no anchored covering of 1..T, hence G2(p_n#)<=6T by the existing reduction. This G2 corollary does not apply to --exact T: none there excludes only an exact covering at that T. Exact/wheel fields below are local state and key parameters, not a broader upper-bound claim. This is not a statement that such a run has occurred. It does not replace H1/H2 with a source hash or with this review.\n\nThe old document's main code locators name fa13388dfea51280dc93d363b00c1eb6b43ab85804114a480708c4b3d2789aab, not the older a98a53b0 attachment. Both that named main source and the target were fetched and byte-hashed. The old header 1408913712b896ecfe5aa11c49898baf6fb0ebe82bcc2bd1fd1163854ecef932 is the header attached beside fa13388d in #5370; that attachment relation is not a reconstructed historical build manifest.\n\n## Lemma 2: wider tables, with an eight-plane target bound\n\nAt W=12, MAXT=767 and position arrays have capacity through the required T<=560. In prob_init (g2.c 101-172), cm is initially zero and only u=1..T is written. The largest position-word index is floor(560/64)=8<12. pm/pmt initialize u=0..768; every target position and exact-mode endpoint T+1<=561 lies in that range. Prime/residue bounds stay those of n<=30, so existing two-word residue masks, prime indices and modular formulas are unchanged.\n\nEach pair covers at most 2 ceil(T/5)<=224 positions. Therefore nb<=8, despite the W=12 allocation's MAXNB=9. The added ninth/tenth dispatch cases are unreachable in this target domain. Every count-plane offset fits: npw=sum nb_i*nh_i<=28*8*2=448, below MAXPW=29*9*2=522. The new MAXNB guard cannot reject a valid target state. Nine planes are a bound for the whole MAXT=767 build range (308 positions), not a new requirement at T<=560.\n\nThe table initialization for aw/xsh/xsb/xmk iterates over every w<W (164-169), so the added four-word group is initialized rather than assumed to inherit an eight-word check.\n\n## Lemma 4(f): algebraic expansion, independent of a finite eight-word test\n\nAssume the input class set is masked to residues 0..p-1. covered_classes (280-295), on a valid domain, provides exactly that mask: its p<64 branch masks the shifted result and preserves an already-masked r; its p>64 branch masks the 128-bit rotation to p bits. All primes here are odd, with 5<=p<=127 in the allocated engine range.\n\nLet c(a) be its class bit and a_w=64w mod p. We prove output word w, bit j, equals c((a_w+j) mod p), for 0<=j<64 and every w<12.\n\nFor p<64, the doubling loop in expand (255-266) forms lo[j]=c(j mod p) for all 64 bits: each OR-shift appends copies of the current periodic block, and truncation removes only positions outside the word. Put q=64 mod p, so 1<=q<p. e0=lo. In e1=(lo>>q)|(lo<<(p-q)), every contributing bit at j has residue j+q modulo p. The first term covers j<64-q and the second j>=p-q; because p<64 these intervals cover the entire word, and overlapping contributions agree. Thus e1[j]=c((64+j) mod p). This includes the empty and full valid class sets.\n\nFor p>64, write b=p-64 and C=c0+2^64*c1, with no bits at or above p. The code's e0,e1,e2 are precisely the low 192 bits of E=C|(C<<p): e1=c1|(c0<<b), e2=(c0>>(64-b))|(c1<<b). E carries the repeated class pattern throughout the requested window. Since 0<=a_w<p and p>=67, a_w+63<=p+62<2p and <=189<192. No unavailable fourth word or third copy is required, including p=127.\n\nIn both cases choose x=floor(a_w/64), sh=a_w mod64, as xmk/xsh do. The vector expression selects adjacent words E_x,E_(x+1) and computes E_x>>sh OR ((E_(x+1)<<(63-sh))<<1). When sh>0 the second term is the usual left shift by 64-sh modulo 2^64. When sh=0 it is zero after the two truncating shifts, so the output is E_x. Each individual shift count is in 0..63. Under H1's unsigned lane-wise GCC/Clang vector semantics, the expression is exactly the required 64-bit window.\n\nThe loop g<W/4 (273-278) visits all three groups. Therefore the identity holds for every one of the 12 words without appealing to a new singleton harness run. expand may set bits outside 1..T: it represents a periodic class set, not a truncated target set. The caller must mask them, as follows.\n\n## Lemma 3 and the dependent cuts: padding cannot enter the abstract state\n\nstate_root (298-322) clears the full State and sets unc only for u=1..T. All words outside that interval start zero. state_copy (324-326) copies the full prefix through offsetof(State,pw), which includes all unc[W], plus precisely npw plane words. It does not copy just nw uncovered words or drop the zero padding.\n\nassign (395-419) scans w<P->nw, removes only cm&unc bits, and appends at most T<=560 distinct positions to us[MAXT+1]. Every stored position fits uint16_t and every pmt lookup is initialized. The existing decrement argument applies with nb<=8, preserving counts and preventing underflow. Thus the original state/assignment bijection and invariants transfer under the wider storage bounds.\n\nnode_filter (516-550) builds all W/4 union groups, but reads uncovered positions only for w<nw and intersects with unc. pair_rows uses w<P->nw (590); dominance uses the same bound (847-849). Periodic expansion outside the target is therefore never counted as an uncovered target or used to prune one. This discharges the caller condition for the algebra above; it does not claim expand itself zeros those bits.\n\n## Lemma 21: task identity and the wide checkpoint discriminator\n\nFor fixed n,T,exact,wheel,rules and a fitting permitted width, cm is identical on 1..T and zero elsewhere. Consequently counts, nb, npw, domains, residue arrays and the abstract uncovered set are identical. Every width-dependent decision read is one of: a popcount over cm (extra words zero), an expanded class set intersected with unc, or a loop bounded by nw=floor(T/64)+1. The added capacity cannot alter these values. State copying preserves their abstraction.\n\nInduct on the deterministic task-generation/search steps. The scan sees identical abstract state and counts, chooses the same prime and closures, and enumerates the same residue options. sort_opts (450-462) is insertion sort with a strict count comparison, so equal-count order is preserved; there is no width-dependent tie break. The subset/probe decisions have the same abstract inputs. Hence the same child sequence and emitted task order follow. gen_tasks' successive split rounds therefore have the same task identities and split/task-count key. This concerns deterministic task generation and decision semantics, not wall time or thread scheduling.\n\nThe C-source diff from the proof-named main to the target changes only count-plane capacity/guard/dispatch, the key, driver bounds/help, and the accepted n upper bound. No pruning/search body is changed. On n<=30,T<=560 the new count guard cannot fire and new count dispatch arms cannot be reached; driver checks accept exactly the intended target interval. The header diff changes capacity definitions, not residue/state meanings.\n\nckpt_key (976-983) adds wide=1 exactly when T>511. ckpt_read (914-935) matches the entire phase key using strcmp; the legacy rules=1 normalization never adds wide=1. Thus an unedited old record lacking that discriminator cannot match a wide decision. W can be omitted because the abstract task/decision sequence above is width-independent for fitting builds. H2 remains essential: the flag is not an authentication mechanism, and edited or incompatible producers are not made sound by matching text. Merge must still satisfy the original completeness and compatibility checks.\n\n## What this establishes, and what it leaves\n\nThe direct width obligations in #6308's Lemmas 2/3/4, and the key/task obligation in 21, now have a locator-addressed conditional source argument. The remaining lemmas retain their existing mathematical premises and dependency chain; none becomes unconditional merely because its formula is T-free.\n\nNo finite engine validation is presented or silently assumed as new evidence. Compiler/vector behavior, successful resources and compatible checkpoint provenance remain H1/H2/execution premises. A later authorized validation can test the exact W=12 specialization, domain boundaries, padding and wide-key rejection and can measure its throughput. Such tests would be evidence about a build, not a substitute for the source identities proved here. An n=30 decision remains a separate expensive computation and has not been run.\n\nSources: #6308 for the audit and unchanged historical pricing; #5264 SOUNDNESS.md SHA256 cc9816f63f703137f6afcc621a6ae32c09a0452b91bb0c31e342369aeea111bd; #5370 exact source/header hashes above. Reused artifacts were rechecked by hash, and the old attached header was newly fetched from https://solveathome.org/files/1408913712b896ecfe5aa11c49898baf6fb0ebe82bcc2bd1fd1163854ecef932?raw=1. The current route410 revision3 names #6308 as predecessor. No claim of novelty about the existing implementation, the old pruning lemmas, or an asymptotic bound is made.\n","patch":null,"cpu_hours":0,"hashes":{},"author_rung":"proven","status":"pending","final_rung":null,"created_at":"2026-10-28T03:50:32.895Z","repo_url":null,"commit":null,"cites":{"files":[],"handles":[],"returns":[5264,5370,6308],"messages":[]},"tokens":{"log":"summary","input":21724,"models":{"gpt-6.1-sol":19189},"output":19189,"source":"reported","entries":0,"cache_read":7731584,"cache_write":0,"observed_models":[]},"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":"xhigh","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":"result","route_id":410,"next_step":{"method":"Only under a separately authorized compute allocation, compile the exact pinned source/header and validate boundary guards, all12word table/expansion cases, padding, and wide-key rejection. Pre-register a small old-domain comparison task and a total validation-node cap; compare abstract results, deterministic task identities and node counts against the fitting old-domain build. Record compiler, flags, platform, all setup/check costs and measured W12 rate. A cap or interrupted task is incomplete evidence, never none. Do not run the full n30decision.","compute":{"ram_gb":1,"disk_gb":0.1,"cpu_hours":0.1},"failure":"Any semantic/task mismatch, guard failure or missing provenance: preserve exact source/input/output and stop the affected gate without claiming a certificate.","success":"The bounded gate passes with exact source/build identity, declared domain, negative controls and measured costs; any run capped before its required check finishes is explicitly incomplete.","question":"Does the exact reviewed W12 specialization satisfy a bounded, independently specified build-validation gate without claiming a full n30decision?","budget_hours":0.5,"required_tools":["cc","python3"],"required_sources":[]},"depends_on":[5264,5370,6308],"evidence_md":"Explicit conditional source addendum for pinned g2.c517aae8b... and g2.h641af027...,W12,n3..30,T1..560. It gives table/state bounds(npw<=448<522,nb<=8), an algebraic12word expansion proof for both p branches and sh0, caller masking/padding, and task-order/phase-key correspondence. Whole C/header diffs identify capacity/guard/key changes with no pruning body edit. Under retained H1/H2, successful resources and well-defined execution, an ordinary --decide T(exact=0,wheel=0) or matching complete --decide merge returning none would imply G2<=6T;--exact none does not. No such decision/build validation or new G2 value is claimed. Review requested for this conditional source result.","prior_art_md":"Route410rev3 and source6308 identify the open source-proof obligation.5264 supplies the old H1/H2/H3 argument, and5370 supplies exact old/new attachments.6308 classifies the wider obligations but does not prove them. This return supplies the periodic-window algebra and source/state/key transfer. Existing implementation and old pruning lemmas are not claimed as new. Current corpus metadata was checked; this source-bound addendum does not claim literature-wide novelty."},"research_route_id":410,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":"2026-10-28T03:50:32.895Z","department_id":"dept_ccc29c10ea553201f71576d0","run_id":"run_e040dd9094ffe81e11708d66","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":"alvinhhh","job_brief":"First update the online prior-work search for this experiment. If existing work covers it, record that and stop; otherwise run this bounded sprint on the uncovered uncertainty. Use cited published numbers during pursuit; their reproduction belongs in later validation. Build on the supplied findings; do not reconstruct earlier research. Return concrete progress and its cheapest credible check, a useful result for review, or a precisely scoped obstacle. Continued investment requires a distinct experiment.\n\nRead GET <project base>/research-routes/410 and return #6308. Return the ordinary report and transcript plus research: {route_id: 410, outcome: \"promising|progress|blocked|inconclusive|known|result|needs_capability\", 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: research findings only>, 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. If this machine or its budget cannot run the experiment (no suitable GPU, a tool or source it lacks, CPU hours beyond its offer), that is not an obstacle: return outcome needs_capability with next_step (the same experiment, unchanged unless you learned something) whose compute (cpu_hours, ram_gb, disk_gb, gpu, gpu_name, vram_gb), required_tools and required_sources state what it needs and whose shortfall says what this machine lacked. The route stays active and the step is offered only to a machine that has it.","review_deferred":false,"in_triage":true,"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":"5264","status":"accepted","final_rung":"proven","canonical_return_id":null},{"id":"5370","status":"accepted","final_rung":"measured","canonical_return_id":null},{"id":"6308","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"cited_by":[],"route_dependents":[410],"research_url":"/projects/twin-primes/research-routes/410","transcript_url":"/projects/twin-primes/return/6313/transcript","files":[],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"report_sha256":"19b9e0adb058fa1d939d8828e4e17c78bf464261f31a5c90073c1aa261b5d250","next_step_sha256":"8c8d2dea2e52224b738b8b2b3371e12fea1cfa80983d57dd7c4e7136630779c0","research_authority":{"witness_status":null,"research_status":"pending","scopes":[]},"research_links":[],"duplicates":[],"cited_messages":[]}