Count rank-one residue lifts over local algebras (no new κ)

research/right-vector-rankone-residue/PROOF.md

@@ -0,0 +1,133 @@
+# Rank-one residue lift counts
+
+Let K be a finite field of order q. Let R be a finite-dimensional associative
+unital K-algebra with K central, with Jacobson radical J, and suppose the
+canonical map K -> R/J is an isomorphism. In particular, R is local and
+R = K direct-sum J as a K-vector space. Put d = dim_K J and z = q^d.
+Commutativity and J^2 = 0 are not assumed.
+
+Use the two-role alphabet of #4099/#4243/#4276. A paid factor is
+P(u,y) = I + u y^T, where u belongs to R^2 and y belongs to K^2. Any map in
+GL_2(K) is free anywhere in a word. The cost is the minimum number of paid
+factors. All multiplication orders below are algebraic product orders;
+column-vector execution applies the rightmost factor first.
+
+Fix A in M_2(K) of rank one. The target family is
+
+```text
+L_A = { A + N : N in M_2(J) }.
+```
+
+There are z^4 targets in this family.
+
+## Theorem
+
+For every such R and A, exactly
+
+```text
+q*z^2 - q + 1                 targets have cost 1,
+z^4 - q*z^2 + q - 1           targets have cost 2.
+```
+
+No target in L_A has cost zero or needs a third factor. Consequently the
+counts depend only on q and d, independently of radical multiplication and
+independently of the chosen rank-one residue A.
+
+The new contribution is this uniform counting law. The two-factor upper
+bound and the one-factor column criterion are predecessor results of
+Nick Petalas's #4276, Theorems A and D, following #4243 and Wentao Li's #4099.
+We spell out their specializations to identify precisely what is counted.
+
+## One-factor specialization
+
+For any K-algebra R and any target M, cost(M) <= 1 holds if and only if there
+are nonzero v,w in K^2 with Mv = w.
+
+For the forward implication, conjugating by a free map preserves the paid
+alphabet, so put a word of cost at most one in the form M = P(u,y) S, with
+S in GL_2(K). Choose nonzero w in ker(y^T), or any nonzero w if y = 0.
+Then v = S^-1 w is nonzero and Mv = w.
+
+Conversely, suppose Mv = w with v,w nonzero and scalar. Choose
+S in GL_2(K) such that Sv = w. The K-linear map
+M S^-1 - I : K^2 -> R^2 kills w. Its image therefore has K-dimension at
+most one, so it is u y^T for some u in R^2 and y in K^2. Thus
+M = P(u,y) S. This is also the two-dimensional form of #4276 Theorem A.
+
+For M = A + N in L_A, reduction modulo J now gives
+
+```text
+cost(M) <= 1  iff  some v in K^2 has N v = 0 and A v != 0.
+```
+
+The condition A v != 0 is necessary. For example over K[e]/e^2,
+M = diag(1+e,0) has a common scalar kernel line, but that line is ker(A).
+This target costs two, not one. The verifier checks this distinction against
+the complete literal one-factor image, without using the criterion to build it.
+
+## Counting the eligible kernel lines
+
+There are q+1 lines in K^2, and ker(A) is exactly one of them. Thus there
+are q eligible lines L, namely those not equal to ker(A).
+
+Choose a K-basis j_1,...,j_d of J and write
+
+```text
+N = sum_i j_i B_i,   B_i in M_2(K).
+```
+
+For an eligible line L define E_L to be the set of tuples (B_1,...,B_d)
+with every B_i killing L. A 2-by-2 matrix killing a fixed line is an
+arbitrary linear map K^2/L -> K^2, so there are q^2 choices for each B_i.
+Hence |E_L| = q^(2d) = z^2.
+
+If L and L' are distinct, any B_i killing both is zero, since the two lines
+span K^2. Therefore E_L intersects E_L' in the single tuple N = 0. The
+nonzero parts E_L minus {0} are disjoint, while the zero tuple belongs to
+every event. Their union has cardinality
+
+```text
+1 + q*(z^2 - 1) = q*z^2 - q + 1.
+```
+
+This argument also covers d = 0, when the zero tuple is the only tuple.
+No product of radical elements occurs in the count.
+
+## Exactness of the two costs
+
+A zero-cost target is a scalar invertible matrix. Every target in L_A has
+singular residue A, so none has cost zero. The counted union therefore
+consists of targets of exact cost one.
+
+Every target in L_A has a unit entry, since some entry has nonzero scalar
+residue. Permutation maps move that entry to (1,1). Write the resulting
+matrix as [[a,b],[c,d0]], with a a unit. The word used in #4276 is
+
+```text
+F1 = [[a,0],[c,1]] = P((a-1,c), e1),
+F2 = [[1,a^-1 b],[0,d0-c a^-1 b]]
+   = P((a^-1 b,d0-c a^-1 b-1), e2),
+F1 F2 = [[a,b],[c,d0]].
+```
+
+These identities hold in a noncommutative algebra with exactly the displayed
+orders. The surrounding permutations are free. Thus every target in L_A
+costs at most two, and all z^4 minus the counted union have exact cost two.
+This completes the counting proof, using the credited predecessor upper bound.
+
+There are (q^2-1)^2/(q-1) = (q-1)(q+1)^2 possible rank-one residues A.
+Indeed A = u v^T with u,v nonzero, and exactly q-1 such pairs give the same A.
+Multiplying the two per-residue counts by this number gives the complete
+rank-one-residue census. The verifier enumerates every one of these residues
+in its finite examples, rather than assuming their counts agree.
+
+## Scope
+
+This is a scoped algebraic counting proof. It does not classify zero-residue
+targets, residue-field extensions, matrix-block residues, products of local
+algebras, or more than two roles. It supplies no native producer, routing,
+restoration, precision, stock, recursive invoice, supplier admission or
+complete multiplication theorem. Independent human and formal proof-kernel
+review are unclaimed.
+
+Produced by Nick Petalas. Predecessor credit is detailed in README.md.

research/right-vector-rankone-residue/README.md

@@ -0,0 +1,134 @@
+# Exact costs above a rank-one residue
+
+Scoped counting proof with finite corroboration. No new kappa.
+
+Let R be a finite-dimensional local algebra over K = F_q, with K central
+and canonical residue field R/J = K. Put z = |J| = q^dim_K(J). For any fixed
+rank-one residue A in M_2(K), the z^4 lifts M = A + N, N in M_2(J), have
+the exact paid right-vector cost distribution
+
+```text
+cost 1:  q*z^2 - q + 1
+cost 2:  z^4 - q*z^2 + q - 1
+```
+
+This formula is independent of A and of radical multiplication, including
+noncommutative radicals and higher nilpotency. The new result is the uniform
+count, not the previously proved two-factor upper bound. It answers the
+nonzero rank-one part of the singular-target direction in #4601. The
+[proof](PROOF.md) counts q eligible scalar kernel lines with disjoint nonzero
+parts. The hypothesis that the scalar image is nonzero is essential.
+
+Paid factors are I + u y^T with u in R^2 and y in K^2. Common GL_2(K) maps
+are free anywhere. This is the formal alphabet of Wentao Li's #4099 and
+Nick Petalas's #4243/#4276. Theorem D of #4276 supplies the unit-pivot
+two-factor upper bound; its Theorem A supplies the one-factor column
+criterion. Those results are cited and specialized, not re-audited here.
+
+## Exact finite evidence
+
+The standard-library verifier independently constructs the complete literal
+one-factor image from all paid left vectors, projective right vectors and
+free endpoints. It then enumerates every rank-one-residue lift. For each
+target it checks the new line condition against literal membership,
+constructs a two-factor word and evaluates that word on every basis input
+of the underlying K-vector space. No predecessor code is imported.
+
+| Algebra | Rank-one residues | Lifts | Exact cost 1 | Exact cost 2 |
+|---|---:|---:|---:|---:|
+| F2 | 9 | 9 | 9 | 0 |
+| F2[e]/e^2 | 9 | 144 | 63 | 81 |
+| F3[e]/e^2 | 32 | 2,592 | 800 | 1,792 |
+| F4[e]/e^2 | 75 | 19,200 | 4,575 | 14,625 |
+| F2[x]/x^3 | 9 | 2,304 | 279 | 2,025 |
+| F2[x,y]/(x,y)^2 | 9 | 2,304 | 279 | 2,025 |
+| F2<x,y>/(x^2,y^2,yx, all degree-three words) | 9 | 36,864 | 1,143 | 35,721 |
+
+The total is 63,417 lifts over 152 residues. F4 is implemented as
+F2[t]/(t^2+t+1), so the checks include a nonprime field. The final algebra
+has basis 1,x,y,xy with xy nonzero and yx zero. Exhaustive ring-table checks
+establish associativity, distributivity, a central base field and units
+exactly at the nonzero residue elements in every fixture.
+
+Controls discriminate allowing a zero scalar image, reversing the two
+factors, omitting a factor, changing the odd-field Schur sign and reversing
+the noncommutative inverse order. Invalid field orders 1 and 6 are rejected.
+The zero-image control is applicable to the six nontrivial-radical fixtures;
+over the field itself that erroneous condition does not change the answer.
+A separate binary dual-number compatibility count is [6,54,36] for the
+invertible cost-0/1/2 classes, agreeing numerically with #4601/#4613/#4749.
+That small compatibility check is not the contribution's deliverable.
+
+Every run prints a generated JSON receipt binding all six package files by
+SHA256. No receipt or replay output is hand-written or saved in the checkout.
+All checks use explicit exceptions and remain enabled under optimized Python.
+
+## Reproduction
+
+From the repository root, using the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-rankone-residue/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-rankone-residue/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-rankone-residue
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-rankone-residue --check-source-history
+```
+
+Any CPython 3.12 installation can replace the displayed local interpreter.
+Expected verifier marker is
+`PASS_RIGHT_VECTOR_RANKONE_RESIDUE targets=63417 residues=152`.
+The runner executes both normal and optimized commands, each with a 120-second
+limit. SOURCES.json pins the prior criteria as historical provenance at base
+b58ad9ef4d4e861b0eaa5dba41742bdc072dca51. There are no live external inputs.
+
+## Limits and verification design
+
+The quantified proof covers every finite field and every radical dimension;
+the finite software checks cover only the table above. The residue field must
+equal the central base field. Zero-residue targets and products of local
+algebras are excluded. Native coefficient preparation, conversion, routing,
+control, precision, restoration, stock and complete supplier cost are unknown.
+No selected operator replay, Lean or Docker build is part of this package.
+Independent human and formal proof-kernel review are unclaimed.
+
+The verifier uses no recursion, child process, network, solver or CLI input.
+Its fixed cases enforce q in {2,3,4}, algebra dimension at most 4 and size at
+most 16. Ring-table validation uses at most 16^3 triples. Literal one-factor
+generation uses at most 16^2*5*180 = 230,400 triples. Any image set has at
+most 16^4 entries. Each lift enumeration has at most 36,864 targets and each
+target uses at most eight basis inputs. Receipt inputs are six fixed files,
+each limited to 1 MiB. The program writes only to stdout.
+
+Power of Ten rule 3 has a managed-runtime deviation in verify.py. Python
+allocates tuples, integers and set entries during the finite enumeration;
+prohibiting allocation would require a different implementation language.
+The preceding enforced domain bounds limit live collections to at most one
+65,536-element image set plus fixed arithmetic tables and one current target.
+Warning-strict normal and optimized replays verify the same bounded path.
+Follow-up is a fixed-buffer implementation if these domain bounds are ever
+expanded. No such expansion is part of this result. Other functions remain
+below the 60-line review ceiling. Warning-strict execution is registered in CI;
+no separate Python type checker or linter is a package dependency.
+
+## Open next questions
+
+1. What is the lift distribution when the local residue field is a proper
+   extension L/K? The shared right vectors remain K-valued, so the eligible
+   line count can depend on the residue matrix. Start with F4[e]/e^2 viewed
+   over F2 and one rank-one residue. The present scalar-residue assumption
+   blocks applying this formula there.
+2. Can a literal native producer and consumer realize this alphabet at a
+   favorable complete cost? Specify one pair, its coefficients, access,
+   restoration and precision contracts before constructing more words.
+   Those physical costs remain unknown.
+
+These questions and their causal relevance are also recorded in TASK.json.
+
+## Credit
+
+This package was produced by Nick Petalas. Nick Petalas's #4276 supplies the
+one-factor and local unit-pivot results, following #4265/#4243. #4601 supplies
+the singular-target question, following ToikY's #4334 local-product direction.
+Wentao Li's #4099 supplies the alphabet and column bound, building on #2513.
+The projective-line and finite-field tools are classical. The new claim is
+their stated rank-one-residue counting application. Apache-2.0.

research/right-vector-rankone-residue/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/README.md",
+      "usage": "provenance",
+      "git_blob": "8952fc9ae8a6e1144e5a0008141121aee66aec69",
+      "sha256": "e00d4352a98b02c5046d8796ba4ef2afd3c6a78d66b4398d23794ebd8147580d"
+    }
+  ]
+}

research/right-vector-rankone-residue/TASK.json

@@ -0,0 +1,85 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact one-call/two-call lift counts above each fixed rank-one residue over every finite-dimensional central local F_q-algebra with canonical residue F_q.",
+  "scope_change_reason": "The alphabet is retained and no new physical operation is claimed. This is a counting side result in the singular-target direction of #4601, complementary to the separately claimed zero-residue and invertible regimes.",
+  "bottleneck_link": "An exact formal-alphabet census separates one-call lifts from lifts that necessarily pay a second call. Physical preparation, access, restoration, precision and complete supplier charges are unknown; this is not a mechanism breakthrough.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified uniform counting law and package it without extending to other residue domains.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves q*z^2-q+1 exact cost-one lifts and z^4-q*z^2+q-1 exact cost-two lifts per fixed rank-one residue, z=q^dim(J). verify.py enumerates 63417 lifts over 152 residues in seven local algebras and checks literal one-factor images and attaining two-factor words.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the rank-one-residue lift distribution over a proper local residue-field extension L/K?",
+      "why_it_matters": "A common K-valued right vector sees a different collection of eligible lines, so counts can depend on the residue matrix rather than only q and dim(J).",
+      "first_step": "Fix one rank-one residue over F4 and enumerate its lifts to F4[e]/e^2 with free maps over F2.",
+      "blocked_by": "The present theorem requires the canonical residue field to equal the central base field."
+    },
+    {
+      "question": "Can one native producer/consumer realize these formal algebra-valued left coefficients with a favorable complete bill?",
+      "why_it_matters": "The counted cost distinguishes one versus two formal calls but does not price their implementation in a recursive supplier.",
+      "first_step": "Specify one literal pair and its coefficient, access, restoration and precision contracts before searching new words.",
+      "blocked_by": "Preparation, conversion, routing, control, precision, restoration and stock costs are unknown."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131158",
+  "upstream_refresh": {
+    "commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+    "checked_at": "2026-10-22T19:26:36.366547+00:00",
+    "guidance_changed": false,
+    "predecessor_inputs_changed": false,
+    "scientific_base_retained": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51"
+  },
+  "overlap_coverage": {
+    "open_pr_snapshot": "2026-10-22T19:19:28.259522+00:00",
+    "open_pr_records": 426,
+    "discussion_snapshot": "2026-10-22T19:20:16.526745+00:00",
+    "discussion_records": 3682,
+    "complete_remote_pagination": true,
+    "local_notes_complete": false,
+    "additional_checks": "Live open PRs, current handoff comments, account PRs since CLAIM, and distinctive main/merged searches were rechecked before commit. PR4745/4749/4763/4764/4766 have different target domains. The reported binary dual-number invertible histogram [6,54,36] agrees with the compatibility enumeration here. No exhaustive novelty claim."
+  }
+}