Prove exact all-role right-vector costs for small local products

research/right-vector-small-local-products/PROOF.md

@@ -0,0 +1,151 @@
+# Common scalar pivot flags in small local products
+
+Let K be a finite field of cardinality q. Let
+
+    R = R_1 x ... x R_k,     1 <= k <= q,
+
+where each R_i is an associative unital central K-algebra whose nonunits
+form a proper two-sided ideal J_i. Thus D_i=R_i/J_i is a division algebra.
+No commutativity, finite dimension, nilpotence, or equality D_i=K is assumed.
+Fix n>=1 and an invertible M in M_n(R).
+
+A paid factor is I+u y^T, with u in R^n and y in K^n. Arbitrary common
+GL_n(K) maps are free anywhere in a word. In particular the free maps and
+right vectors cannot be chosen separately in the product components.
+Let pi:R^n -> (R/K)^n use the diagonal central copy of K. The theorem is
+
+    cost_R(M) = delta_R(M) = rank_K(pi M|_{K^n}) <= n,
+    delta_R(M) = min_{T in GL_n(K)} dim_K((MT-I)K^n).
+
+The column lower bound cost>=delta is cited from #4243/#4099. The new
+step extends #4787's local arbitrary-role upper bound to these products.
+#4601 and ToikY #4334 already give the two-role small-product case.
+
+## Avoiding the component kernels
+
+A union of k<=q proper K-linear subspaces of K^d cannot equal K^d, for
+every d>=1. Each subspace has at most q^(d-1) elements and contains zero.
+Their union therefore has size at most
+
+    1 + k(q^(d-1)-1) <= q^d-q+1 < q^d.
+
+We use only this elementary finite-vector-space count.
+
+For any invertible A in M_d(R), its reduction Abar_i is invertible over
+D_i. The K-linear map
+
+    L_i : K^d -> D_i,     phi -> phi Abar_i e_1
+
+is nonzero, since otherwise every entry in the first column of Abar_i
+would vanish. Thus ker L_i is a proper scalar subspace. Choose one phi
+outside their union. Then every phi A_i e_1 is a unit in R_i, since its
+residue is nonzero. Hence a=phi A e_1 is a unit in R. This argument uses
+one common scalar row phi, including when the division residues differ.
+
+## A common full pivot flag
+
+We prove by induction on d that some Q in GL_d(K) makes every leading
+square corner of QA invertible over R. The d=0 statement is vacuous.
+For d>=1 choose phi as above, and extend it to the first row of a scalar
+basis matrix Q_0. Write
+
+    Q_0 A = [[a,b],[c,F]],     S=F-c a^(-1)b.
+
+Here a is a unit in R. Block triangular elimination makes diag(a,S),
+so S is invertible. Apply the induction hypothesis to S, obtaining
+P in GL_(d-1)(K), and set Q=diag(1,P)Q_0. Each leading corner of size
+j>=2 in QA has pivot a and Schur complement the leading corner of PS
+of size j-1. Both are invertible, so that corner is invertible. The
+size-one corner is a. All ring products retain the displayed order;
+no commutativity of R_i or D_i has been used.
+
+This proves existence of one common scalar pivot flag. The finite
+constructor in verify.py searches scalar rows at each step and performs
+this induction iteratively on its fixed bounded examples.
+
+## The exact number of active columns
+
+The following chart reduction is the cited #4787 argument, included to
+connect the new flag to the precise cost. Put
+
+    E={v in K^n : Mv belongs to K^n},
+    s=dim_K E,     d=n-s=rank_K(pi M|_{K^n}).
+
+Invertibility makes M:E -> M(E) injective. Choose a scalar basis of E,
+extend it to a basis H of K^n, and extend its images to a basis B of K^n.
+Then N=B^(-1)MH has its first s columns equal to those of I, so
+
+    N=[[I_s,C],[0,A]],
+
+with A invertible. For any scalar T, pi(MT-I)=pi MT has rank d, giving
+delta>=d. Conversely T=HB^(-1) gives
+
+    MT-I=B(N-I)B^(-1),
+
+whose scalar column rank is at most d. Therefore delta=d. This reduction
+needs invertibility but does not need the local-product hypothesis.
+
+Apply the common-flag lemma to A and left-multiply N by diag(I_s,Q).
+This is free and preserves the first s fixed columns. Call the resulting
+matrix N again. Its active leading corners are all invertible.
+
+For j=0,...,d let A_j consist of the first s+j columns of N and the
+remaining columns of I. All A_j are invertible by the corner property.
+A_0=I and A_d=N. Set h=s+j for j=1,...,d and
+
+    u_j=A_(j-1)^(-1)(N e_h-e_h),     F_j=I+u_j e_h^T.
+
+The h-th column of A_(j-1) is still e_h. Right multiplication by F_j
+therefore replaces exactly that column, giving A_(j-1)F_j=A_j. Hence
+
+    N=F_1 ... F_d.
+
+Every right vector e_h is scalar and common to all components. Undoing
+the free charts gives a legal word for M with at most d paid factors.
+Together with the cited lower bound, its cost is exactly d. If d=0,
+M itself is a common free map and no paid factor is needed. There is no
+auxiliary role or componentwise free operation in this construction.
+
+## Coverage of the separate binary metric
+
+The finite oracle treats invertible pairs (A,B) over F_2. A free common
+left map sends this pair to (I,C), where C=A^(-1)B. Common free right
+multiplication by T sends C to T^(-1)CT. A paid factor has components
+P_0=I+u_0 y^T and P_1=I+u_1 y^T. Applied at the normalized representative,
+it sends C to P_0^(-1)P_1 C. At an arbitrary representative, conjugating
+the paid factor by A gives the same alphabet with a changed scalar y.
+Thus all normalized paid transitions are exactly the generators enumerated
+by the bit-matrix oracle. Both P_i must be invertible on any path to an
+invertible endpoint, since singular matrices cannot regain rank over a field.
+
+BFS gives attaining paid paths. The verifier also checks every paid edge
+against the distance labels and checks that every free conjugation leaves
+its label unchanged. These inequalities prove the lower bound for every
+word with arbitrary interleaved free maps. Hence the independent finite
+metric is exact, without using the common-pivot theorem to prune its words.
+
+## What is new and what remains open
+
+The new statement is the arbitrary-role small-product theorem, in particular
+all invertible targets over two local F_2-algebras at every role count.
+The finite-subspace avoidance argument and Gaussian elimination are
+classical. Their use to choose a complete common scalar pivot flag closes
+the product gap left in #4787 while preserving the exact column bound.
+The k<=q condition is necessary for a theorem covering every role count:
+ToikY #4334 and #4601 already give two-role cost-three examples with
+k=q+1 and delta=2. Their examples are cited, not replayed as this result.
+No claim is made that k<=q is necessary for an individual target.
+
+Singular endpoints, products with more than q components at n>=3, matrix
+blocks in a semilocal quotient, and a complete physical supplier are not
+classified. Native coefficient preparation, routing, frames, restoration,
+precision, stock and the full recursive bill remain unknown. This is a
+scoped algebraic proof, not a complete multiplication theorem or new kappa.
+Independent human and formal proof-kernel review are unclaimed.
+
+This contribution was produced by Nick Petalas. Credit Nick Petalas #4787
+for the local arbitrary-role theorem, active-column chart and open product
+question; #4601 for the local-product two-role theorem; ToikY #4334 for
+the field-product threshold; and Nick Petalas #4243 and Wentao Li #4099,
+following #2513, for the alphabet, normal form and column lower bound.
+Predecessor files and attribution are unchanged. Apache-2.0.

research/right-vector-small-local-products/README.md

@@ -0,0 +1,139 @@
+# Exact all-role right-vector cost for small local products
+
+Scoped algebraic proof with finite corroboration. No new kappa.
+
+Let K=F_q and R=R_1 x ... x R_k, where 1<=k<=q and each R_i is an
+associative central local K-algebra. Its nonunits must form a proper
+two-sided ideal. For every n>=1 and every invertible M in M_n(R),
+
+```text
+cost_R(M) = delta_R(M) = rank_K(pi M|_{K^n}) <= n,
+delta_R(M) = min_{T in GL_n(K)} dim_K((MT-I)K^n),
+pi : R^n -> (R/K)^n.
+```
+
+K embeds diagonally in R. A paid factor is I+u y^T with u in R^n and
+y in K^n. Arbitrary common GL_n(K) maps are free anywhere. No extra role
+is used. The residue division algebras may differ from K and may be
+noncommutative. No finite-dimensionality or nilpotence assumption is needed.
+
+[PROOF.md](PROOF.md) gives the universal statement and attaining words.
+It answers the arbitrary-role product question explicitly left open by
+Nick Petalas #4787. ToikY #4334 and Nick Petalas #4601 already prove the
+two-role small-product case. The new step chooses a common scalar pivot
+at every Schur complement. Each component forbids a proper scalar
+subspace; at most q such subspaces cannot cover the scalar row space.
+This gives one common full pivot flag, followed by exactly delta column
+replacements. Classical finite-vector-space counting and elimination
+retain their ordinary mathematical credit.
+
+The component hypothesis cannot be removed from an all-role theorem:
+the cited two-role predecessors already give k=q+1 examples with cost
+three and delta two. That is predecessor credit, not a new certificate
+in this package. Necessity for individual higher-role targets is open.
+
+## Finite evidence
+
+The standard-library verifier imports no predecessor code. It constructs
+literal common-chart words and checks their full matrix products on all
+28,224 invertible three-role targets over F2 x F2. Its exact paid-cost
+histogram, in cost order zero through three, is
+
+```text
+[168, 3528, 16464, 8064].
+```
+
+A separate bit-matrix implementation enumerates GL3(F2). It normalizes a
+pair (A,B) by its free left map to (I,A^(-1)B). Literal paid pairs with a
+common right vector give 22 distinct normalized generators, including the
+identity. BFS covers all 168 normalized states. Its labels satisfy all
+3,696 paid edges and 28,224 free-conjugation edges, so they certify the
+actual normalized alphabet metric. Every constructor length agrees.
+Left normalization transports its witnesses to all 28,224 ordered pairs.
+All 1,008 base-field basis-data actions on the 168 normalized words pass.
+
+The verifier also checks 431 distinct bounded examples on three and four
+roles over (F2[e]/e^2)^2, F3^3 and (F3[e]/e^2)^3. These are samples, not
+complete target censuses. They exercise every active dimension from zero
+through the role count. All 6,644 basis-data actions and 18,200 literal
+scalar-subspace input checks pass. The latter independently enumerate E
+and check |E|=p^(n-d), rather than using the constructor's row reduction.
+
+Eight rejection controls cover missing factors, reversal, changed
+coefficients, componentwise free maps, singular targets, too many
+components, nonunit inversion and an illegal paid right-vector shape.
+Two additional boundary fixtures require a non-coordinate common pivot
+and demonstrate the covering failure at q+1 scalar hyperplanes. Checks
+use explicit exceptions and remain active under optimized Python.
+The verifier writes nothing and emits a generated receipt bound to all
+six package files. No receipt is handwritten or committed.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-small-local-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-small-local-products/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-small-local-products
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-small-local-products --check-source-history
+```
+
+Any CPython 3.12 installation may replace the local path. Expected marker:
+
+```text
+PASS_RIGHT_VECTOR_SMALL_LOCAL_PRODUCTS binary_pairs=28224 sampled_targets=431 controls=8 no_new_kappa
+```
+
+Both registered commands have 120-second limits and run the same complete
+checks. SOURCES.json pins predecessor documents to canonical base
+`de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are cited dependencies,
+not audited deliverables. The original card is explicitly changed to this
+algebraic side result in TASK.json. Its selected-baseline first command
+passed after sparse inputs were materialized; it is source-binding
+orientation only. No selected operator replay was run.
+
+## Limits and implementation discipline
+
+The all-q, all-n result is the written proof. Software corroboration uses
+base fields F2 and F3, the complete binary pair domain, and the stated
+three-/four-role samples. It does not enumerate extension base fields or
+noncommutative local products. Singular targets, more than q components
+at n>=3 and matrix blocks in a semilocal quotient are not classified.
+Native coefficient preparation, frames, routing, restoration, precision,
+stock and a full supplier bill remain unknown. No supplier admission,
+selected-frontier change or complete multiplication theorem is claimed.
+Independent human and formal proof-kernel review are unclaimed. Lean,
+Docker and the selected construction's cold replay are outside scope.
+
+The verifier has no recursion or subprocesses. Matrices have at most four
+roles; local coefficient tables have at most nine elements; products have
+at most three components. Scalar row searches and literal scalar inputs
+have at most 3^4=81 candidates. The binary group has 168 states, its BFS
+has exactly 168 iterations, and the complete pair loop has 168^2 cases.
+Each sampler generates at most 80 candidates and stores at most 80 target
+matrices. All functions fit within 60 lines. Python requires dynamic
+allocation, a managed-runtime deviation bounded by these fixed domains.
+Eight fixed negative-control callbacks are bounded local dispatch.
+Warning-strict normal/optimized replay and in-memory source compilation
+supply the available Python diagnostics. No shared configuration changes.
+
+## Open next questions
+
+1. For n>=3 and more than q components, determine which common scalar
+   flags still attain delta. Start with a three-component binary
+   three-role target. The present subspace count ceases to guarantee a
+   row, so an individual flag criterion is needed.
+2. Specify one native producer/consumer for a column replacement and
+   price coefficient preparation, access, frames, restoration, precision
+   and stock before implementing a supplier. Those costs are unknown.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Nick Petalas #4787
+for the local arbitrary-role theorem, chart reduction and open product
+question; #4601 for the two-role local-product extension; ToikY #4334 for
+the field-product threshold; and Nick Petalas #4243 and Wentao Li #4099,
+following #2513, for the alphabet, normal form and column lower bound.
+The exact source documents and predecessor attribution are unchanged.
+Apache-2.0.

research/right-vector-small-local-products/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/right-vector-commutative-products/README.md",
+      "usage": "input",
+      "git_blob": "fc9889d41621b596209c707b6057517744b4642f",
+      "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f"
+    },
+    {
+      "path": "research/right-vector-local-all-roles/PROOF.md",
+      "usage": "input",
+      "git_blob": "46d63f385b1036db0019f9dd8b1909eac39bba99",
+      "sha256": "ce08b72a33602f5bd7ecae575711e584fe2ba3fb46deb797fe8109a6a2b98142"
+    },
+    {
+      "path": "research/right-vector-local-products/PROOF.md",
+      "usage": "input",
+      "git_blob": "7230a0e7bb82384758114990a8c8958efd73d6e2",
+      "sha256": "c8ffdb932990533d1b1b5eda1b05ac2430cc6a1b2d7a263ca1f0bf76c414da0f"
+    }
+  ]
+}