[petalas]

Summary

Scoped counting proof with exact finite corroboration, answering Open next question 1 of #4770. Let K=F_q be a subfield of L=F_Q, let R be a finite-dimensional central local L-algebra with canonical residue R/J=L, and put z=|J|. Right vectors and free maps remain restricted to K.

For each rank-one residue A, the number t(A) of base-field lines sent into nonzero base-field vectors is 0,1 or q. Among its z^4 lifts:

cost 1 = 0                         if t(A)=0;
         1+t(A)*(z^2-1)             otherwise.
cost 2 = z^4-cost_1.

Residues with t=q: (q+1)*(q^2-1)
Residues with t=1: (q+1)*(q^2-1)*(Q-q)
Residues with t=0: all remaining rank-one residues

Total one-factor lifts = (q+1)*(q^2-1)*(Q*z^2-q+1).

The proof uses a base-field subspace classification, disjoint nonzero kernel fibers and a residue/line double count. The one-factor criterion and unit-pivot two-factor upper bound are cited results of #4276, specialized in #4770, rather than audit deliverables. Radical multiplication and nilpotency do not affect the new count.

For F4[e]/e^2 over F2, the 75 rank-one residues split into 9,18,48 cases with t=2,1,0. Of their 19,200 lifts, exactly 567 cost one and 18,633 cost two. With F4-valued right vectors and free maps, the cited scalar-residue formula instead gives 4,575 one-factor lifts. This makes the smaller-base-field effect explicit. No new kappa, supplier admission or selected-frontier change is claimed.

Only research/right-vector-extension-residue/ is added. Produced by Nick Petalas. Credit Nick Petalas #4770 for the extension-field question and scalar-residue count, #4276/#4243 for the criteria and free-map normal form, ToikY #4334 and Nick Petalas #4601/#4749 for the related shared-chart local/semilocal interfaces, and Wentao Li #4099 following #2513 for the alphabet. The finite-field and projective-line tools are classical. No predecessor executable code is imported.

Evidence

• Before: Count rank-one residue lifts over local algebras (no new κ) #4770 assumes the residue equals the central base field and explicitly leaves proper residue-field extensions open. After: PROOF.md gives the displayed per-residue and aggregate formulas over every finite-field extension, including the empty eligible-line class.
• The self-contained verifier constructs the literal complete one-factor image from paid factors and free endpoints, without using the line criterion to construct it. It enumerates every lift above every rank-one residue in eight fixtures over F4/F2, F8/F2, F9/F3 and F16/F4. All 12,511,409 lifts agree with the formulas separately at each residue. The fixtures include radical lengths one, two and three, an odd field, and a nonprime base field. Cost-two classification uses the cited unit-pivot theorem.
• Nine positive/boundary controls distinguish the three line classes, the empty union, zero scalar images, radical-kernel conditions, the first example, the permitted base field and the extension degree.
• Both warning-strict registered commands passed locally, timed separately at 6.93 s and 7.03 s. Ordinary and optimized generated receipts agree exactly. Package metadata and registered replay pass. Committed-byte/source-history checks pass on b838121c65e1bfd17a65466c95940eb00f12a225. Official committed export integrity and optimized replay from a read-only Git-free export with PATH=/nonexistent also pass with the identical six-file SHA256 receipt. No receipt is hand-written.

Exact reproduction from the repository root with CPython 3.12 and its standard library:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-extension-residue/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-extension-residue/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-extension-residue
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-extension-residue --check-source-history

Any CPython 3.12 installation can replace the displayed interpreter. Expected markers are PASS_RIGHT_VECTOR_EXTENSION_RESIDUE lifts=12511409 controls=9, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Canonical main is pinned at 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7, refreshed before submission. The selected metadata orientation control passed. TASK.json explicitly changes the formal-interface card to this algebraic side question. Live claims, open PR bodies, distinctive all-main README terms and merged-PR searches were rechecked immediately before committing. The overlap helper reported complete remote pagination and incomplete sparse local-note coverage; these searches do not certify novelty.

Advance claim.

Limitations and unrun obligations

The quantified theorem is a written scoped proof. Software corroboration covers the eight fixed commutative local algebras, not every algebra in the theorem. The coefficient field L must be central with canonical residue L. Nonsplit residue maps, noncentral fields, other residue ranks and more than two roles are outside scope.

Native preparation, free-map implementation, routing, restoration, precision, stock and complete supplier cost remain unknown. Independent human and formal proof-kernel review are unclaimed. Lean, Docker and selected-construction operator replay were not run. Every registered package command ran locally; no local package obligation is deferred to CI.

Open next questions

• On more than two roles, what is the one-factor lift distribution above rank-one residues? Begin with eligible base-field hyperplanes on three roles; their radical-kernel intersections need not be zero.
• Can an actual native producer and consumer realize this restricted alphabet at favorable complete cost? First specify coefficients, access, free-map implementation and dirty restoration; those physical costs remain unknown.

Related open work

Before DONE, this account's open PRs created since the CLAIM at 2026-10-22T19:45:59Z were refreshed. The titles and full bodies of the five related same-alphabet PRs were read:

• Classify radical pencil reachability by characteristic-polynomial splitting (no new κ) #4776, head 0764ab259a8ce496a4c5d4debeed4c4e4d9f7ca4, classifies zero-residue square-zero radical pencils. This package fixes nonzero rank-one residues over coefficient-field extensions, so the endpoint sets and numerical censuses are disjoint.
• Prove the sharp singular rank-one product threshold (no new κ) #4780, head a4436fab4164eccc498d4d9885eec68211c869de, proves the singular rank-one threshold for pure field products. At the shared scalar-field boundary Q=q=2,z=1 and one component, this package's aggregate formula gives 9, matching a fresh literal enumeration of all nine binary rank-one targets and Prove the sharp singular rank-one product threshold (no new κ) #4780's stated k=1 cost-one count 9. Its k=6 count 567 and this package's proper-extension count 567 concern different target sets; that equality is not an overlap claim.
• Prove a binomial law for polynomial right-vector cost (no new κ) #4784, head 4d0a6363fe4f45dd9a769f5b74d02fc5d9061ae3, counts invertible targets over the nonlocal polynomial ring F_q[t]. Both its coefficient algebra and invertible endpoint contract differ from these singular local-algebra lifts; no target-cost census overlaps.
• Prove exact local right-vector costs at every role count (no new κ) #4787, head 4b58e8cd5690bd35cf01b0018eefa2c39a298920, gives arbitrary-role costs for invertible local-algebra targets, including proper coefficient-field examples. Our rank-one-residue endpoints are noninvertible, so no shared target-cost or census value is asserted.
• Classify exact rank-two matrix-algebra right-vector costs (no new κ) #4789, head 7fdbf8040ea9a957af0576067df2d9cb6fcf0e51, classifies ordinary rank-two targets over matrix algebras M_m(K), m>=3. Those nonlocal matrix coefficients differ from this scalar-residue local family; no target count or exact-cost instance overlaps.

Other newly open account PRs, #4774/#4777/#4778/#4785, concern Schur dimensions or full-guard probabilities. No conflicting overlapping number was found within this coverage. Merged #4770 remains the direct predecessor; at Q=q these formulas specialize algebraically to its scalar-residue count. The new proper-extension classification remains distinct.

CI notes

Both hosted checks passed on contribution head b838121c65e1bfd17a65466c95940eb00f12a225 in Registered research packages run 39844230468: plan in 3m5s and the registered research/right-vector-extension-residue replay in 2m0s. Run metadata confirms that exact head and conclusion success. The replay executes both warning-strict normal and optimized verification commands. All registered local checks, committed-byte/source-history preflight, official export integrity and read-only Git-free replay also passed. Hosted CI certifies execution of these bounded checks; independent human and formal proof-kernel acceptance of the quantified proof remain unclaimed.

Merge Danger

Door: two-way.

Blast Radius: isolated.

Six files are added in one new research package. Shared implementation, frozen evidence and the selected record are unchanged.