[petalas]

Summary

Scoped written proof with exact finite corroboration, produced by Nick Petalas. This answers the polynomial-entry question in unpaidmoon's #7103. In its two literal stage-0 gaps, every pair R,S over K[x] of entry degree at most d satisfying the required coefficient endpoint has an explicit affine parametrization:

R B + B S = B,  B = diag(1,1+x,1,1,1,1,1,1)
solution space = K[x]_(<=d)^50 × K[x]_(<=d-1)^14
               dimension 64d+50 over every field K
new degree-one crossing: R=I-(1+x)E10, S=E10

The degree-one dimension is 114. Over F_q the bijection gives q^(64d+50) pairs. The finite verifier enumerates entrywise factors of this count; it does not enumerate every full matrix pair. This changes the constant-entry hypothesis and opens couplings through coordinate 1. No new κ, paid-rank gain, native caller or supplier admission is claimed.

Credit unpaidmoon for #7103 at f3af1384aeda8c75be58f09cb07da3941ba7aba3, the literal word of #7027 at 1ba2ac5adfe58fbe9dba34d50d4e5d30633ce3d0, and #7039's coefficient-target distinction. Credit Ali Romman for #5747 and its retained #5673/#5631/#5617 lineage. Those results are cited inputs, not audit targets.

Evidence

• Before: Classify two constant insertions after the stage-0 paired-star gates (no κ) #7103 leaves polynomial entries outside its constant classification.
• After: the written entrywise proof classifies all degrees and all fields; the standalone verifier checks the new polynomial domain directly from the eleven-factor operator.
• Local CPython 3.12.15 checks pass: 56,960 exhaustive entry pairs; coefficient ranks for degrees 1–4 over F2/F3/F5/F7; 56 integer polynomial crossing witnesses; four rejected false witnesses.
• Both warning-strict registered commands pass, including isolated optimized mode. Each was timed locally at about 0.35 seconds; the complete registered run took about one second. These are timeout checks, not performance claims.
• Metadata/pins, committed bytes, source history, executable modes and static compilation pass. Every verifier run emits a generated SHA256-bound receipt to stdout. No predecessor scientific suite was replayed.

From the repository root, use the exact local interpreter path below. On another machine, use CPython 3.12 at its corresponding path.

~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/polynomial-two-gap-insertions/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/polynomial-two-gap-insertions/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/polynomial-two-gap-insertions
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/polynomial-two-gap-insertions --check-source-history --check-modes

Limitations

The universal quantifiers come from the written proof, with finite computation as corroboration. Independent human and formal proof-kernel review are unclaimed. The insertion entries now depend on x; native legality, implementation, restoration, precision, hosting and a complete signed invoice are unproved. The explicit witness has no established cost advantage over (I,0). No Lean, Docker, selected-frontier replay or complete multiplication implementation was run. The selected frontier is unchanged.

Open next questions

Can the explicit polynomial crossing pair save work once every x-dependent entry is legally implemented and all restoration is charged? First realize R=I-(1+x)E10, S=E10 in the actual interface, then compare its complete bill with (I,0). A legal priced realization is the missing step.

Related open work

• Prove rank factor 1 for every-stage paired-star gaps and raise the thin-rank bound to 2q⌈g/3⌉ (no κ) #7126 studies the same paired-star gate family and proves a rank bound for constant internal thin maps under its square condition; this contribution classifies polynomial entries in two fixed gaps and does not compute that rank budget.

• Classify two constant insertions after the stage-0 paired-star gates (no κ) #7103 fixes these two gaps and classifies constants; this contribution answers its polynomial-entry question.

• Record a valuation-1 factor outside the paired-star T-commutant #7027 supplies the diagonal nine-gate word; its valuation and factorization results are cited without replay.

• Prove no constant insertion makes the valuation-1 e coefficient I #7039 treats one-gap insertions and distinguishes coefficient I from coefficient P; this contribution requires P and uses two gaps.

• Record the idempotent triples after rows (1, 1, 0, 0) #7040 classifies other idempotent stage factorizations; those gates are not substituted into this word.

• Record that one unsplit call per stage still needs thin rank 8 #7086 studies two thin maps in the different unsplit three-call word and asks about polynomial entries there; that rank problem is outside this classification.

CI notes

CI did not certify this package. At head 4268eab9d5bc1293a006d27abf9164d125ff094d, run 43000676071 failed in plan, at job 130455727586. The package replay job was skipped because plan failed.

I read the checks once and inspected the job log. The failing step is Onboarding helper tests: 760 tests ran, exactly one failed, and 24 were skipped. The failure is:

test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record
AssertionError: '`make frontier7000-verify`' not found in the CI verification document

The cause is already in base main e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md opens with Current selected-family replay: #6030 and names make frontier6030-verify. Both files and the failing test are unchanged by this PR, which adds only research/polynomial-two-gap-insertions/.

I also read the failed-step logs of 42905094314, 42903313790, 43000211746 (#7189), and 43000790178 (#7192). Each reports the same sole failing test and assertion, with 760 tests and 24 skips.

No fix, retrigger commit, push or job rerun was made for this repository-level failure. Evidence for this package remains local: both registered commands and all required package checks passed as recorded above.

Merge Danger

Door: two-way. Blast Radius: isolated research package. Five new files; no shared implementation, pinned predecessor, selected record or frontier change.