[petalas]

Summary

Prove a sharp obstruction for every admission-respecting two-grid precision selector, including arbitrary nonperiodic choices. Claim type: scoped mathematical proof with exact finite corroboration.

coarse inputs: S contained in hZ; increments: a,b; delta=a-b
F(q) = q+b+delta*1_S(q)
injective  iff S+delta is contained in S
bijective  iff S+delta=S
nonempty injective coarse selection exists iff h divides delta

This answers a narrow part of woklerx's #1845 open question. Its cited source-one PR628 increments at precisions four and five have h=2 and delta=1. Consequently every policy making even one coarse choice on that whole source slice has an explicit collision with the adjacent forced-fine input. The predecessor excludes one coarsest-compatible policy; this result excludes every such two-grid selector on that slice. The leaf increments, admission and restoration remain cited premises, not results reverified here.

Only research/two-grid-selector-obstruction/ is added. This contribution was produced by Nick Petalas. Credit woklerx #1845/#1451, Chafik Boukhalfa #628, Gareth Davidson's retained fixed-grid caller, Ali Romman #621 and the retained kernel lineage. Elementary translation/partition facts remain background mathematics. No new kappa or selected-frontier change.

Evidence

• Normal and optimized warning-strict CPython 3.12.15 checks agree on 18,522 periodic policies, 543,774 literal residue images, 2,392 finite-support policies, 46,552 literal integer images, 1,025 cited-premise collision witnesses and ten controls.
• The new written theorem quantifies over arbitrary subsets. The bounded checker enumerates actual images, including cross-branch partners, and distinguishes nonperiodic injectivity from surjectivity. It imports no predecessor implementation.
• Each direct registered command took about 0.07 seconds locally, below its 60-second limit. Registered replay, selected-baseline orientation, in-memory compilation and whitespace checks pass.
• Committed-byte/source-history checks pass for all six files at 799fd0cb5afaf1571f00bacfa5697f54364dd647. Official export integrity/input coverage and an optimized read-only Git-free export replay pass with all seven exported files unchanged. Receipts are generated and bound to package-file hashes.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-grid-selector-obstruction/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-grid-selector-obstruction/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-grid-selector-obstruction
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-grid-selector-obstruction --check-source-history

Another CPython 3.12 path may be substituted. Expected markers are PASS_TWO_GRID_SELECTOR_OBSTRUCTION, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Limitations

The application assumes #1845's leaf premises. A policy may choose fine precision on this slice and save elsewhere. Larger precision menus, changed increments, retained branch information, different sources, restricted reachable domains and extra visible outputs require separate analysis. This supplies neither a physical selector nor a complete restoration/tape/precision invoice. Independent human and formal proof-kernel review, selected supplier cold replay, Lean and Docker are unrun.

Open next questions

• Can three or more actual admitted precisions avoid the forced collision? First obtain their increments and admission lattices and test disjoint translated branch images. Their physical selection/restoration bill remains unknown.
• Does an actual caller reach a restricted target set excluding every forced partner? First prove one pinned call site's source-conditioned reachable set and charge its maintenance.

Related open work

No other open PR studying this two-grid selector or the same PR628 source slice was found in the live open list and targeted body/Discussion searches. Merged #1845 is the direct predecessor; merged #1451 and #1853 concern fixed mixed-precision cancellation, rather than arbitrary forward selectors. Search coverage and sparse-local limits are recorded in TASK.json; unpublished work remains outside coverage.

The completion refresh read the titles and bodies of this account's thirteen other open PRs created since the advance CLAIM at 2026-10-27T21:04:47Z: #5997 and #5999 through #6010. None studies arbitrary two-grid precision selection or computes a competing value for this PR628 slice. No additional mathematical computations were run to compare them.

CI notes

Both hosted checks passed at 799fd0cb5afaf1571f00bacfa5697f54364dd647: plan and replay (research/two-grid-selector-obstruction), in run 40584347757. The completed check list was read once; the run conclusion is success and its head SHA matches the PR. Hosted replay certifies the registered bounded checks. The arbitrary-subset theorem remains a written proof, and the leaf application retains its cited premises. All registered commands and publication checks also passed locally.

Merge danger

Door: two-way. Blast radius: isolated research package. Shared code, frozen evidence and the selected record are unchanged.

Coordination: #1166 (comment)