Extend the one-relation paid-rank floor to nonfield rings (no κ)

research/nonfield-one-relation/PROOF.md

@@ -0,0 +1,154 @@
+# A residue-field extension of the one-relation obstruction
+
+This scoped proof is produced by Nick Petalas. The every-field theorem of
+Josie Elliston's [PR6044](https://github.com/CrocSwap/integer-mult-bounds/pull/6044),
+head `4ebdea4e95fa4cbf227b4be630f656105d96e5f7`, is a cited mathematical
+premise. Its proof and scientific census are not replayed here. The new step
+is specialization of the coefficient ring, including factors that disappear.
+
+## Setting and cited premise
+
+Let R be a nonzero commutative ring with identity. Let A_1,...,A_k be
+nonzero rank-one rational d-by-d matrices. Write H for their additive
+integer span. In the formal group algebra R[H], distinct matrices h give
+independent basis symbols [h], and [h][g]=[h+g]. The integer exponent
+labels are not reduced modulo the characteristic of R.
+
+For W>=1 let N_j be idempotent W-by-W matrices over R, and suppose the
+following formal identity holds:
+
+    product_(j=1,...,k) (I + ([A_j]-1) N_j)
+        = diag([C_1],...,[C_W]).                              (1)
+
+The C_w belong to H, so are rational d-by-d matrices. Zero C_w are restored dirty registers.
+The identity acts on arbitrary register contents; no zero initialization is
+assumed. A global normalized outer product N_j=x_j y_j^T, y_j^T x_j=1,
+is one important allowed case.
+
+We use the following statement from PR6044. Over any field K, if all paid
+projectors are rank-one idempotents and the rational span of the k paid
+frames has dimension at least k-1, a formal diagonal monomial endpoint
+has pairwise disjoint assignments
+
+    C_w = sum_(j in I_w) A_j.
+
+Consequently sum_w rank_Q(C_w)<=k. This is the exact prerequisite imported
+from that work, including its arbitrary register count and restored roles.
+
+## Theorem: one qualified residue field suffices
+
+Choose a maximal ideal m of R and put K=R/m. Reduce N_j entrywise to
+bar(N_j). Suppose every bar(N_j) has rank zero or one over K. Let
+
+    J_m = { j : bar(N_j) != 0 },  n_m = |J_m|.
+
+If n_m>0, assume
+
+    dim_Q span { A_j : j in J_m } >= n_m-1.                   (2)
+
+Then there are pairwise disjoint subsets I_w of J_m such that
+
+    C_w = sum_(j in I_w) A_j,
+    sum_w rank_Q(C_w) <= n_m.                               (3)
+
+If J_m is empty, every C_w is zero and the same conclusion holds with
+empty assignments. The hypothesis concerns this one residue field; no
+constant rank or global outer-product representation of N_j is needed.
+
+### Proof
+
+The unital quotient map R->K induces a coefficientwise homomorphism
+R[H]->K[H]. It fixes every formal label [h]. In particular its action on
+(1) retains exactly the same C_w on the right. Distinct labels remain
+linearly independent because 1_K is nonzero.
+
+The reduced matrices are still idempotent. A zero reduced projector gives
+an identity factor, which can be removed without changing the order of the
+remaining factors. A nonzero rank-one reduced projector has a normalized
+outer product: choose a nonzero vector x spanning its image. There is a
+linear functional y^T with N(v)=x y^T(v). Idempotence and x!=0 give
+N(x)=x, hence y^T x=1. Thus every surviving factor has precisely PR6044's
+field form.
+
+Let H_m be the additive integer span of the surviving frames. The entire
+reduced left side lies in M_W(K[H_m]). Inclusion K[H_m]->K[H] is injective
+on formal basis elements. Therefore each endpoint C_w belongs to H_m:
+otherwise its coefficient 1 on the right could not occur on the left.
+For n_m>0, apply the cited field theorem to this reduced, ordered word and
+(2). It gives the disjoint subsets in (3). Rank subadditivity and the
+rank-one hypothesis on each A_j give the displayed rank bound.
+
+If n_m=0, the left side is I. Independence of formal labels gives
+[C_w]=[0], hence C_w=0 for every w. This proves the empty case. QED.
+
+## Corollary: nonfield free rank-one projectors do not escape
+
+Suppose every N_j=x_j y_j^T over R with y_j^T x_j=1_R, and
+
+    dim_Q span {A_1,...,A_k} >= k-1.
+
+Then (1) implies disjoint assignment of the C_w to the original paid
+frames and sum_w rank_Q(C_w)<=k, for every nonzero commutative R.
+
+Indeed R has a maximal ideal. At every such ideal the normalized outer
+product remains normalized, so each reduced projector is nonzero and has
+rank one. Thus J_m is the full index set, and the theorem applies. This
+covers Z/2^e for every e>=1, other Z/m with m>=2, nilpotents and zero
+divisors. It uses the cited field theorem, rather than extending its
+individual domain or graph arguments to rings with zero divisors.
+
+The bound is sharp over every such R. Take k=d, A_j=E_jj, and N_j=E_11
+on W>=1 scalar registers. Their product has endpoint
+
+    diag([I_d],[0],...,[0]).
+
+The rational target rank sum is d=k. All other registers are restored on
+arbitrary inputs. There is no physical/native tariff claim in this example.
+
+## Varying rank and the sharper active count
+
+More generally suppose every N_j has rank at most one at every maximal
+ideal, and the full frame list has at most one rational relation. Every
+sublist also has at most one relation: its relation space injects into
+the relation space of the full list by extending coefficients with zeros.
+Thus the theorem applies at every maximal ideal, and
+
+    sum_w rank_Q(C_w) <= min_m |J_m|.                        (4)
+
+The minimum exists because its possible values lie in {0,...,k}. The
+assigned subsets may depend on the chosen ideal. We assert neither one
+assignment simultaneously describing all projectors nor a global
+factorization of every idempotent. Vanishing two-by-two minors over R are
+a sufficient, though unnecessary, way to ensure the required fiber rank.
+
+For a concrete example over Z/6, take W=2 and
+
+    N_1=3 E_11,  N_2=4 E_11,  A_1=A_2=A!=0.
+
+Both matrices are idempotent, their product is zero, and their sum is
+E_11. Multiplication gives
+
+    (I+([A]-1)N_1)(I+([A]-1)N_2)
+        = diag([A],[0]).
+
+Exactly one factor survives modulo 2 and exactly one survives modulo 3.
+Formula (4) gives the sharp bound one, although the written ring word has
+two nonzero factors. Neither N_j admits a normalized global outer product:
+it vanishes in one residue field, contradicting the reduction of y^T x=1.
+
+By itself the first factor has diagonal entry 4+3[A], which is a monomial
+in each residue field with different exponents there. It is not a formal
+monomial over Z/6. This explains why the fixed global endpoint (1) matters;
+component-dependent endpoints cannot be substituted for it.
+
+## Scope
+
+This extends PR6044's explicit nonfield question for commutative rings and
+the stated residue-rank hypothesis. The general theorem can also apply
+when the full frame list has more relations, provided one surviving
+sublist satisfies (2). Noncommutative rings, rank-two residue projectors,
+and surviving lists with two or more independent relations remain outside
+this argument. A ring quotient alone does not supply a native operation,
+legal physical endpoint, hosting, compiler, rounding or complete paid bill.
+There is no new kappa or complete multiplication theorem. Independent human
+and formal proof-kernel review are unclaimed.

research/nonfield-one-relation/README.md

@@ -0,0 +1,106 @@
+# Nonfield coefficients do not escape the one-relation paid-rank floor
+
+This scoped mathematical proof is produced by Nick Petalas. For every nonzero
+commutative coefficient ring R, a formal word with normalized rank-one scalar
+projectors and at most one rational relation among its paid rank-one address
+frames has disjoint target assignments and
+
+    sum_w rank_Q(C_w) <= number of paid factors.
+
+This answers Open next question 2 of Josie Elliston's
+[PR6044](https://github.com/CrocSwap/integer-mult-bounds/pull/6044) for the stated
+commutative-ring class. It includes Z/2^e, arbitrary composite moduli,
+nilpotents, zero divisors and any finite number of restored dirty registers.
+The [proof](PROOF.md) uses PR6044's every-field theorem as a cited premise.
+It does not recheck that theorem or rerun its scientific executable.
+
+The new specialization theorem permits projectors without a global normalized
+outer product. It is enough that one residue field sees only rank-zero and
+rank-one projectors, and that the surviving frames have at most one relation.
+The bound then counts only surviving factors. If every residue qualifies,
+take their minimum. A Z/6 example has two nonzero ring factors but only one
+active factor in each residue and attains that sharper floor. A second
+example attains the ordinary rank-two floor over Z/4. The written construction
+attains the general k-factor bound over every nonzero commutative ring.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/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 their CPython 3.12 path. The direct verifier works
+from a Git-free export. Expected marker: `PASS_NONFIELD_ONE_RELATION`.
+Normal verification writes no files. Optional `--emit-to EXTERNAL_NEW_FILE`
+creates a generated receipt containing all six source hashes and every result;
+`--check-receipt FILE` recomputes and checks its canonical bytes. Creation
+refuses overwrites and paths inside the package. No receipt is hand-written.
+
+The exact finite evidence checks the new composite-ring setting:
+
+- Enumerate every two-by-two matrix over Z/m for m=4,6,8,9,10,12. Retain
+  exactly 864 idempotents with zero determinant among 42,945 matrices. Compare the full
+  residue-rank histogram with the classical prime-power/CRT formula.
+- Multiply every two-factor word on those projectors for m=4,6,8,9, using
+  independent frames A=diag(1,0), B=diag(0,1). Also multiply every three-factor
+  word over Z/4 with frames A,B,A, which have one relation. Compare every
+  coefficient after specialization on 45,821 words, and check disjoint assignment and the
+  sharper active-factor bound at all 85 diagonal monomial endpoints.
+- Check the Z/6 partial-projector example, its glued endpoint, its rejection
+  as a global monomial before gluing, and the sharp rank-two Z/4 example.
+- Nine rejection controls cover the zero ring, a map that is not a residue
+  quotient, failed idempotence, rank-two fibers, excess relations, nonunit
+  coefficients, off-diagonal endpoints, nonmonomial diagonal entries and
+  reduction of rational address labels modulo the characteristic.
+
+These finite checks corroborate the written extension. They do not prove
+PR6044's universal field theorem or replace its review.
+
+## Limits and implementation
+
+Claim type: scoped written algebraic proof using a credited theorem, with
+exact finite corroboration. No new kappa, physical supplier, selected-frontier
+change or discharge of the five selected assumptions is claimed. No predecessor
+scientific replay, Lean, Docker or selected cold replay is required or run.
+Independent human and formal proof-kernel review are unclaimed.
+
+The new verifier has no recursion, network, subprocesses or dynamic code
+loading. The matrix census visits at most 12^4 matrices per modulus; stored
+projector lists have at most 325 entries. Words have at most three factors,
+formal supports at most eight labels and assignment searches at most 27
+possibilities. Functions are below 60 lines. Explicit exceptions keep all
+checks active under optimized Python. Python managed allocation is a deviation
+from fixed allocation, bounded here by these fixed finite domains and one-MiB
+source/receipt limits. A larger or externally parametrized replay would need
+new capacities or a fixed-storage runtime. Warning-strict normal and optimized execution provide
+the available diagnostics. No shared configuration or predecessor code changes.
+
+## Open next questions
+
+1. Can a surviving frame list with exactly two relations beat the rank floor
+   over a commutative ring? First seek such a field word, since the present
+   specialization transfers every qualifying field obstruction. A shorter
+   field endpoint and a complete native tariff remain missing.
+2. Can a noncommutative coefficient ring evade this particular specialization
+   argument? First specify a ring, a paid alphabet and a diagonal endpoint.
+   The residue field and scalar rank-one decomposition used here need not
+   exist. No saving follows merely from that failure.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+Credit Josie Elliston / PR6044 for the every-field one-relation theorem and
+its explicit nonfield question. Credit Hanson Sun / PR1454, woklerx / PR1456,
+theon199, Ali Romman / PR468, eumemic / PR288 and huxint / PR203 for the
+retained register-model and one-relation lineage. Maximal-ideal reduction,
+rank-one idempotent factorization over fields, CRT and prime-power projector
+counts are classical. No general literature-priority claim is made.
+[SOURCES.json](SOURCES.json) pins the predecessor statement and historical
+orientation sources; no predecessor executable is imported. New files are
+under Apache-2.0.

research/nonfield-one-relation/SOURCES.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-one-relation-every-field/README.md",
+      "usage": "provenance",
+      "pin": "head:4ebdea4e95fa4cbf227b4be630f656105d96e5f7:research/bit-one-relation-every-field/README.md",
+      "git_blob": "e454cd51dd1b870fd83a48a829e7484c34044cc1",
+      "sha256": "6b40d96ad12201832626be9fdad2d8941e09a5f082f15e7bbe15709ebe0de654"
+    }
+  ]
+}

research/nonfield-one-relation/TASK.json

@@ -0,0 +1,88 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "A residue-field extension of the one-relation paid-rank obstruction to nonzero commutative coefficient rings, with a sharper surviving-factor bound.",
+  "scope_change_reason": "Answer PR6044 Open next question 2. The changed coefficient ring is a scoped algebraic side result, rather than the card's completed larger/nonabelian native construction.",
+  "bottleneck_link": "Closes the commutative-ring escape from this low-relation register obstruction. It does not supply native conversion or improve the selected BIT budget.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first proved ring extension and sharp finite example; leave multiple-relation or noncommutative models to follow-on work.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the extension using PR6044 as a cited premise. verify.py enumerates composite-ring projectors and checks formal specialization, disjoint assignment, sharp fixtures and nine rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a surviving frame list with exactly two relations beat the rank floor over a commutative ring?",
+      "why_it_matters": "Identifies the first relation dimension outside the transferred obstruction.",
+      "first_step": "Find one fully specified shorter field word before considering a ring lift.",
+      "blocked_by": "No such exact endpoint or complete native tariff is supplied."
+    },
+    {
+      "question": "Can a noncommutative coefficient ring evade this specialization argument?",
+      "why_it_matters": "The residue-field proof depends on commutativity.",
+      "first_step": "Specify a noncommutative ring, its legal paid alphabet and a diagonal formal endpoint.",
+      "blocked_by": "A field quotient and scalar rank-one decomposition may be absent; no saving is established."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372283",
+  "scientific_dependency": {
+    "pr": 6044,
+    "author": "JosieElliston",
+    "head": "4ebdea4e95fa4cbf227b4be630f656105d96e5f7",
+    "used_as": "Cited every-field theorem; no predecessor scientific replay."
+  },
+  "environment": {
+    "python": "Python 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "Python standard library only"
+  },
+  "upstream_checkpoint": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "selected_pr": 6030,
+    "utc": "2026-11-03T11:03:38Z"
+  }
+}