Prove exact local costs for residue-corank-one targets (no new κ)

research/local-corank-one-cost/PROOF.md

@@ -0,0 +1,123 @@
+# Residue corank one attains the column bound
+
+This contribution was produced by Nick Petalas. The result is a scoped
+algebraic proof in the formal right-vector alphabet. No new κ is claimed.
+
+Let K be a field contained in the centre of an associative unital local
+K-algebra R. Its nonunits form its Jacobson radical J, and D=R/J is a
+division algebra. Neither finite dimension, commutativity, split residue
+nor nilpotence of J is assumed. Matrices act on columns on the left.
+
+A paid factor is I+u y^T, where u is in R^n and y is in K^n. All GL_n(K)
+maps are free anywhere in a word. Singular paid factors are allowed.
+Write cost(M) for the minimum number of paid factors, or infinity when no
+word exists, and define
+
+    delta(M) = min_{T in GL_n(K)} dim_K ((MT-I)K^n).
+
+The alphabet and column bound are from Wentao Li's #4099, following #2513,
+and Nick Petalas's #4243. The two-role local unit-entry theorem is #4276.
+The arbitrary-role invertible local theorem is #4787, head
+4b58e8cd5690bd35cf01b0018eefa2c39a298920. ToikY's #4334 explicitly leaves
+singular targets outside its field-product theorem. The new theorem below
+handles singular local endpoints of arbitrary role count and residue corank
+one. The arguments below are self-contained and do not replay those results.
+Basis extension, Gaussian elimination, Schur complements and local-ring unit
+lifting are classical facts, not claimed as new here.
+
+## The theorem
+
+For every n>=1 and every M in M_n(R) whose residue has rank n-1 over D,
+
+    cost(M) = delta(M) = n - dim_K M(E) <= n,
+    E = {v in K^n : Mv belongs to K^n}.
+
+Here M(E) is a K-linear subspace of K^n. In particular, the zero images in E
+must not be counted as fixed directions. The formula n-dim_K(E) used for
+invertible targets would be wrong for singular targets. For example,
+M=diag(1,...,1,0) has E=K^n but cost(M)=delta(M)=1.
+
+## 1. The column lower bound and its singular-target form
+
+Move free maps to the right by conjugation. Each conjugate of a paid factor
+is again paid because K is central. A word with t paid factors is P S,
+where S is free and P is their product. Expanding P-I successively writes
+it as a sum of t terms v_i y_i^T with y_i in K^n. Therefore its image on
+K^n has K-dimension at most t. Taking T=S^{-1} proves delta(M)<=cost(M),
+including singular words.
+
+Delta is invariant under free maps on either side. For G,H free, put
+T=H^{-1} U G^{-1}. Then
+
+    (GMH T-I)K^n = G(MU-I)K^n.
+
+Hence the minima agree. Set k=dim_K M(E). For any free T, the fixed subspace
+W=ker_K(MT-I) satisfies TW contained in E and M(TW)=W, so dim_K W<=k.
+Rank-nullity gives delta(M)>=n-k.
+
+Conversely choose v_1,...,v_k in E whose images w_i=Mv_i form a basis of
+M(E). The v_i are K-linearly independent, since their images are. Extend
+both lists to K-bases. Let H have first k columns v_i, and let X have first
+k columns w_i. Then N=X^{-1} M H has first k columns e_1,...,e_k, so
+(N-I)K^n has dimension at most n-k. Free invariance proves
+
+    delta(M)=n-k.
+
+This identity holds over every central K-algebra, even if M is unreachable.
+The upper bound on cost in the next steps uses the local and residue-rank
+hypotheses.
+
+## 2. Unit pivots before the last column
+
+In the charts just chosen, write
+
+    N = [[I_k, B], [0, A]],       t=n-k.
+
+The first k residue columns are D-independent. Since rank_D(bar M)=n-1,
+rank_D(bar A)=t-1. In particular k<=n-1 and t>=1.
+
+Gaussian elimination with complete row and column pivoting on bar A
+produces t-1 nonzero pivots. Make the same row and column permutations in
+N, only among its last t coordinates. Each lifted pivot in the corresponding
+Schur complement is outside J, hence is a unit. Eliminating a unit pivot
+reduces residue rank by exactly one. Thus the first n-1 leading square
+blocks of the resulting N' are invertible over R. The first k columns
+remain e_1,...,e_k. No assertion is made about invertibility of N' itself.
+
+For completeness, the induction uses the block factorization of a matrix
+[[a,b],[c,F]] with unit a into invertible triangular factors and diagonal
+blocks a and F-ca^{-1}b. It works without commuting any coefficients.
+At each stage of a residual block of rank s-1 and size s>=2, there is a
+nonzero residue entry. Permuting it into the pivot position preserves
+previous leading blocks. This supplies the next unit pivot. At s=1 no
+pivot or inverse is needed.
+
+## 3. An attaining literal word
+
+Let C_j be the matrix with its first j columns equal to those of N' and
+its remaining columns equal to the corresponding identity columns.
+Then C_k=I and C_n=N'. For k<=j<n, C_j is invertible: it has block form
+[[L_j,0],[*,I]] with invertible leading block L_j from step 2.
+
+For j=k+1,...,n define
+
+    F_j = C_{j-1}^{-1} C_j
+        = I + C_{j-1}^{-1}(N'e_j-e_j)e_j^T.
+
+Every F_j is a legal paid factor with base-field right vector e_j.
+All inverses occur before the last column replacement. Telescoping gives
+
+    F_{k+1} F_{k+2} ... F_n = N'.
+
+Undoing the free row/column charts gives M with at most t=n-k paid factors
+and no auxiliary roles. This product is written in matrix multiplication
+order. Applied to data, its rightmost factor acts first. Step 1 gives the
+matching lower bound t, proving the theorem.
+
+## Scope boundary
+
+Residue corank two or greater need not permit all required intermediate
+inverses. The square-zero radical obstructions in #4745/#4773/#4776 and the
+cube-zero example in #4764 are separate results; this theorem does not
+classify them. Nonlocal coefficient algebras need not admit the unit pivots.
+No physical implementation, restoration or recursive cost is supplied.

research/local-corank-one-cost/README.md

@@ -0,0 +1,103 @@
+# Exact local right-vector cost at residue corank one
+
+This contribution was produced by Nick Petalas. Scoped algebraic proof,
+with bounded finite corroboration. No new κ or supplier admission.
+
+For every central field K, associative local K-algebra R with residue
+division algebra D, and n-role target M of residue rank n-1,
+
+    cost(M) = delta(M) = n - dim_K M(E) <= n,
+    E = {v in K^n : Mv is in K^n},
+    delta(M) = min_{T in GL_n(K)} dim_K ((MT-I)K^n).
+
+Paid factors are I+u y^T with u in R^n and y in K^n. Arbitrary free GL_n(K)
+maps are allowed anywhere. The final paid factor can be singular.
+[PROOF.md](PROOF.md) gives an attaining word with no additional roles.
+The residue division algebra can be noncommutative or larger than K.
+Finite dimension and nilpotence of the radical are not required.
+
+The new part is arbitrary-role singular endpoints with residue corank one.
+Nick Petalas's #4276 covers two-role local targets with a unit entry;
+#4787 covers arbitrary-role invertible local targets. ToikY's #4334 leaves
+singular targets outside its product theorem. Those are cited predecessors,
+not verification deliverables. The singular correction to the fixed-space
+formula matters even for diag(1,1,0), whose cost is one, although E=K^3.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/local-corank-one-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/local-corank-one-cost/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/local-corank-one-cost
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/local-corank-one-cost --check-source-history
+```
+
+Any CPython 3.12 path may replace the local path. The verifier prints a
+generated JSON receipt with package SHA256 hashes, followed by
+`PASS_LOCAL_CORANK_ONE_COST`. It writes nothing.
+
+## Evidence and limits
+
+The verifier constructs literal words over binary and ternary dual numbers,
+a binary two-generator square-zero algebra, F4 over F2, and the noncommutative
+algebra F4[e;Frobenius]/e^2 over F2. It checks ring laws, central scalars,
+local units and the residue map before using an algebra. Samples have three
+or four roles. The binary dual-number checks also include every one of the
+512 lifts of diag(1,1,0). Other target sets are bounded deterministic samples.
+Each word is checked as a complete matrix and on every base-field basis data
+vector. A separate calibration evaluates every GL3(F2) chart on selected
+targets to compare the direct definition of delta. Domain and word mutations
+are rejection controls. The main checks cover 1,112 targets, 8,272 basis-data executions and 5,376
+direct chart evaluations, with eight rejection controls. Two additional shared
+two-role targets over F4[e]/e^2 have costs one and two, respectively. They
+connect numerically to #4781 without repeating its counting deliverable.
+Numerical receipts are produced by the verifier.
+
+The universal claim rests on the written proof. Independent human and formal
+proof-kernel review are unclaimed. Higher residue corank, nonlocal algebras,
+physical coefficient preparation, frames, routing, restoration, precision and
+stock remain outside scope. Lean, Docker and the selected operator replay
+were not run. The selected frontier is unchanged.
+
+The formal-interface card is explicitly changed to this algebraic side
+question. Its historical first command, scripts/research_baseline.py, fails
+with KeyError: 'bit_lower' under the selected #4470 schema. No baseline pass
+or theorem acceptance follows from that orientation command. Canonical main
+is pinned at 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132023)
+records live overlap checks and their incomplete coverage.
+
+## Engineering notes
+
+Build the Lever led to the literal word constructor and independent direct
+chart comparison. Prove It Works led to checking actual matrix endpoints and
+basis data. The code has no recursion; every collection and loop is bounded
+by the fixed five algebras, at most four roles, 4,000 sample attempts and at
+most 16 algebra elements. Functions stay below 60 lines. Explicit checks
+remain active under optimization. Python dynamic allocation and callbacks in
+rejection controls are managed-runtime deviations from Power of Ten; live
+collections have these fixed bounds. No external dependencies are imported.
+
+## Open next questions
+
+1. Which residue-corank-two local targets attain delta? Begin with one
+   three-role target over F2[x,y]/(x,y)^2 whose residue is diag(1,0,0).
+   The next missing pivot can be a nonunit, so a new completion criterion is
+   required. This would identify how far the singular theorem extends.
+2. Can a named native caller realize one of these singular column factors
+   with all preparation, frame, movement and restoration charges? Start by
+   stating its dirty-input/output contract. No physical invoice is known.
+
+Structured questions are in [TASK.json](TASK.json).
+
+## Credit
+
+ToikY #4334 supplies the singular-target gap. Nick Petalas #4276/#4243 and
+#4787 supply predecessor criteria, lower bounds and local constructions.
+Wentao Li #4099 follows the #2513 alphabet and column-bound lineage.
+Basis extension, Gaussian elimination, Schur complements and local-ring unit
+lifting retain classical credit. This contribution adds the scoped theorem,
+its singular fixed-space formula and the self-contained bounded verifier.
+Apache-2.0.

research/local-corank-one-cost/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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-diagonal-free-basis/README.md",
+      "usage": "provenance",
+      "git_blob": "50a1cbeea57e3cb16e0d8a569be365bba21890ff",
+      "sha256": "924334cf4e881775fafc6ec36630d03648dbda39f6bad4612a97b5b6d351fbcb"
+    },
+    {
+      "path": "research/right-vector-commutative-products/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db",
+      "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408"
+    }
+  ]
+}

research/local-corank-one-cost/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact right-vector cost for arbitrary-role local targets of residue corank one, including singular endpoints.",
+  "scope_change_reason": "The donor requests an original result rather than an audit. This is a self-contained algebraic side question from the singular-target gap of ToikY #4334, extending the two-role local theorem #4276 and distinguishing invertible #4787.",
+  "bottleneck_link": "Scoped formal-alphabet side result. It identifies exactly when the column lower bound is achievable with a singular endpoint; physical implementation and recursive savings remain unclaimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified scoped theorem and package it; no higher-corank search or supplier extension.",
+  "outcome": "completed",
+  "evidence": "Written proof plus self-contained literal word checks on 1112 bounded three/four-role targets, 8272 basis-data executions, 5376 direct chart evaluations and eight controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Which residue-corank-two local targets attain delta?",
+      "why_it_matters": "Identifies the next boundary of singular restricted-alphabet reachability.",
+      "first_step": "Test a three-role target over F2[x,y]/(x,y)^2 with residue diag(1,0,0).",
+      "blocked_by": "The next column pivot may be a nonunit; the present proof does not complete it."
+    },
+    {
+      "question": "Can a native caller implement a singular column replacement with a complete invoice?",
+      "why_it_matters": "A formal word alone does not admit a recursive supplier.",
+      "first_step": "Specify one literal dirty-input/output contract and price preparation, frames, movement and restoration.",
+      "blocked_by": "No native caller or complete physical cost is supplied."
+    }
+  ]
+}

research/local-corank-one-cost/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Ring laws, literal corank-one paid words, complete endpoints, basis data, direct chart minima and eight rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same checks with optimization; all proof-relevant checks are explicit and remain enabled."
+    }
+  ]
+}