[petalas]

Summary

Scoped written algebraic proof with exact finite corroboration. Extend Josie Elliston's PR6044 one-relation obstruction from fields to every nonzero commutative coefficient ring with normalized rank-one scalar projectors. This answers its Open next question 2 for that class, including Z/2^e and rings with nilpotents or zero divisors.

formal endpoint over R[H]
  -> quotient to one residue field, keeping every address label
  -> discard zero projectors
  -> apply the cited PR6044 field theorem
  -> disjoint target assignments; total target rank <= surviving factors

The stronger statement needs only one residue field where projectors have rank zero or one and surviving frames have at most one rational relation. A Z/6 example attains the sharper active-factor floor. The ordinary floor is sharp over every nonzero commutative ring. See PROOF.md.

The extension was produced by Nick Petalas. Credit Josie Elliston for the field theorem and question, Hanson Sun / PR1454, woklerx / PR1456, theon199 and the retained Ali Romman / PR468, eumemic / PR288 and huxint / PR203 lineage. Residue-field specialization and the other elementary algebraic methods are classical. No general literature-priority claim is made.

Evidence

• Before: PR6044 explicitly leaves nonfield coefficient rings outside its theorem. Its field theorem is a cited premise, not an audit or replay deliverable here.
• After: the written extension and sharp examples, plus a standalone composite-ring verifier. It enumerates 42,945 matrices, retains 864 qualifying projectors, checks all 45,821 declared formal words and their 85 diagonal monomial endpoints, and passes nine rejection controls.
• Warning-strict normal and optimized CPython 3.12.15 checks passed locally in 0.684 and 0.680 seconds. The registered pair passed in 1.708 seconds. Each registered command is well below its 120-second timeout.
• Committed-byte/source-history preflight, generated hash-bound receipt checks, four receipt rejection checks, official export integrity and read-only Git-free normal/optimized replay passed. All seven exported files remained unchanged. No predecessor scientific executable was run.

Exact reproduction from the repository root:

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

A reviewer may substitute another CPython 3.12 executable. Expected markers are PASS_NONFIELD_ONE_RELATION, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES.

Limitations

The field theorem remains an explicit mathematical dependency. The finite checks corroborate the extension; independent human and formal proof-kernel review are unclaimed. Noncommutative coefficient rings, rank-two residue projectors and surviving lists with two independent relations are outside the argument. Native implementation, physical hosting, compiler, rounding and complete paid supplier costs are not supplied. No new kappa, selected-frontier change or discharge of the five framework assumptions is claimed. Lean, Docker and the selected cold replay were outside scope and were not run.

Open next questions

• Find a shorter exact field word with two surviving frame relations before attempting a commutative-ring lift. A completed endpoint and native tariff are missing.
• Specify one noncommutative coefficient ring and its legal paid alphabet to test whether the residue-field argument can be replaced. Failure of specialization alone establishes no saving.

Related open work

No open PR studying this coefficient-ring extension or surviving-factor bound was found in the refreshed open-PR inventory and live one-relation/nonfield searches. PR6044 is the merged predecessor. PR4099's merged arbitrary-algebra result counts nonidentity diagonal entries under a fixed binary right-vector hypothesis, a different quantity and alphabet.

Completion refresh inspected the 12 other account open PRs created since the advance CLAIM, through PR6602. None studies this coefficient-ring extension or reports a competing value for its rank bound. No additional computations audited other contributions.

• PR6596 removes an ownership cap for independent-stage linear BIT support obstructions. This PR instead changes the coefficient ring of a formal abelian one-relation word; it does not study PR6596's native-chain endpoint.

CI notes

Both hosted checks, plan and replay (research/nonfield-one-relation), passed at exact head 75ef2f7cc2b035748cf4c7b9d01b34946f5c08f9 in run 41626060904. The completed checks were read once; run metadata confirms completed success and the matching head. The plan took 4m29s and the replay job took 1m37s.

Hosted replay certifies execution of the registered normal/optimized finite checks and source metadata at this commit. It does not independently establish the universal written proof or revalidate PR6044's cited field theorem. Local registered checks, source-history preflight, generated-receipt controls and read-only Git-free export checks also passed. Independent human and formal proof-kernel review remain unclaimed.

Merge Danger

Door: Two-way.

Blast Radius: Isolated. Adds six files under research/nonfield-one-relation/; no shared source or selected certificate changes.