Prove radical invariance of right-vector costs over local products

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

@@ -0,0 +1,158 @@
+# Radical reduction for invertible right-vector targets
+
+Let `K` be a field. Let `R = R_1 x ... x R_k`, with `1 <= k < infinity`,
+where each `R_i` is an associative unital `K`-algebra whose non-units form
+a proper two-sided ideal `J_i`. This is the local-algebra hypothesis used
+by Nick Petalas's #4276. Put `J = product J_i` and `D = R/J`. Each
+`D_i = R_i/J_i` is a division algebra with the induced central copy of `K`.
+No commutativity, finite-dimensionality or nilpotence hypothesis is needed.
+
+Use the retained two-role alphabet
+
+```text
+P(u,y) = I + u y^T,    u in R^2, y in K^2,
+free maps GL_2(K), usable anywhere,
+delta_R(M) = min_{T in GL_2(K)} dim_K ((MT-I)K^2).
+```
+
+The cost is the least number of paid factors. A bar denotes reduction
+modulo `J`. The target `M` is assumed invertible throughout.
+
+## The result
+
+```text
+cost_R(M) <= 2  iff  cost_D(Mbar) <= 2,
+cost_R(M) = max(delta_R(M), cost_D(Mbar)) <= 3.
+```
+
+Thus local radicals cannot create or remove a three-factor obstruction
+on invertible targets. They can increase a zero- or one-factor residue
+cost, and `delta_R` measures precisely that remaining increase.
+
+For finite `K` of size `q`, every invertible target costs at most two when
+`k <= q`. For each fixed product with `k >= q+1`, there is an invertible
+target of cost three and `delta_R = 2`. For infinite `K`, every invertible
+target in a finite product costs at most two. The finite-field component
+threshold therefore extends #4334 from field products to these local
+products, including noncommutative local algebras.
+
+## 1. Units and the common pivot
+
+An element of `R_i` is a unit exactly when its image in `D_i` is nonzero.
+Indeed, the zero coset is `J_i`, the set of non-units by hypothesis. The
+quotient is a division algebra since every nonzero coset has a unit
+representative. Units in a finite product are exactly the tuples of units.
+
+For any invertible `N` over `R`, the first row `(A,B)` is right unimodular.
+Writing `(x,z)^T` for the first column of `N^{-1}` gives `Ax+Bz=1`.
+If `B=AC`, this becomes `A(x+Cz)=1`. In each component a non-unit `A_i`
+would make the left side belong to the proper ideal `J_i`. Consequently
+`A` must be a unit. Conversely, a unit `A` always gives `B in AR`.
+
+By #4276, Theorem B, two paid factors suffice exactly when some
+`G,H in GL_2(K)` make `N=GMH` satisfy `N12 in N11 R`. The preceding
+paragraph reduces this, on invertible targets, to `N11` being a unit.
+Every nonzero `K` row `phi` can be the first row of `G`, and every nonzero
+`K` column `t` can be the first column of `H`. Therefore
+
+```text
+cost_R(M) <= 2
+iff some common nonzero phi,t over K make phi M_i t a unit for every i
+iff some common nonzero phi,t over K make phi Mbar_i t nonzero for every i
+iff cost_D(Mbar) <= 2.
+```
+
+The same argument applies to `D`, since a division algebra is local with
+zero non-unit ideal. This proves radical invariance of the two-factor set.
+It does not assume componentwise free maps or componentwise right vectors.
+
+## 2. Three paid factors always suffice
+
+This extends ToikY's #4334, Section 3, with the order of every product kept
+as written. Write `M=[[a,b],[c,d]]`. In each component its second column
+is left unimodular. If `d_i` is a non-unit, then `b_i` is a unit, since
+otherwise both entries and all their left linear combinations lie in
+`J_i`, contradicting the second row of `M_i^{-1}` applied to that column.
+
+Choose the element `r in R` by `r_i=0` if `d_i` is a unit and `r_i=1`
+otherwise. Set
+
+```text
+D0 = d-rb,
+f = D0^{-1}(c-ra),
+e = a-bf.
+```
+
+Each `D0_i` is a unit. In the second case its residue is `-bbar_i != 0`;
+in the first case it is `d_i`. Hence the inverse in the formula exists.
+Direct multiplication, without interchanging any ring factors, gives
+
+```text
+M = [[1,0],[r,1]] [[1,b],[0,D0]] [[e,0],[f,1]]
+  = P((0,r)^T,e1) P((b,D0-1)^T,e2) P((e-1,f)^T,e1).
+```
+
+The four entries of this product are `e+bf=a`, `b`,
+`r(e+bf)+D0 f=ra+c-ra=c`, and `rb+D0=d`. This uses three allowed factors
+with the common right-vector sequence `e1,e2,e1` and no free map.
+The componentwise coefficient choice belongs to the allowed left vector.
+It does not make the right vectors or free maps componentwise.
+
+## 3. The exact cost formula
+
+By the predecessor column bound and quotient functoriality,
+
+```text
+cost_R(M) >= delta_R(M),
+cost_R(M) >= cost_D(Mbar).
+```
+
+Both costs are at most three by Section 2. If `cost_D(Mbar)=3`, these
+bounds force `cost_R(M)=3`, while `delta_R(M)<=2`. Otherwise Section 1
+gives `cost_R(M)<=2`. Theorem A of #4276 gives exact cost `delta_R`
+when `delta_R<=1`. If `delta_R=2`, the column bound forces cost two.
+Thus `cost_R=delta_R` in this second case, and the quotient lower bound
+also gives `cost_D(Mbar)<=delta_R`. The stated maximum formula follows.
+
+For example, over the single local algebra `F2[e]/e^2`, the targets
+`diag(1+e,1)` and `diag(1+e,1+e)` reduce to the free identity but cost
+one and two respectively. For the first, `T=I` gives dimension one and
+the target is not free. For the second, a binary kernel vector `v` of
+`(1+e)T-I` must satisfy both `(T-I)v=0` and `Tv=0`, hence `v=0`.
+So every free endpoint gives dimension two. The exact formula applies.
+
+## 4. The sharp component threshold
+
+Fix a nonzero `t in K^2`. Each `Mbar_i t` is nonzero in `D_i^2`.
+At most one projective `K` row can annihilate it. If two distinct
+projective rows did so, they would form a `K` basis of the row space,
+forcing both entries of this vector to vanish. For finite `K`, there
+are `q+1` projective rows. When `k<=q` some row is not forbidden.
+For infinite `K`, a finite union of these singleton forbidden sets
+also leaves a row. Section 1 supplies the two-factor word in each case.
+
+For sharpness when `K` is finite and `k>=q+1`, take the `q+1` scalar
+matrices in `GL_2(K)` constructed in #4334, Section 4, from the
+projective representatives of a quadratic extension. Place these in
+the first `q+1` components, using the central copy of `K` in each `R_i`,
+and put identities in extra components. For every nonzero `phi,t`,
+one of these component pivots is literally zero, so it is not a unit.
+Section 1 excludes two factors; Section 2 supplies three. Theorem A
+then forces `delta_R=2`. The extension-field construction and its
+projective covering property are credited to #4334, not reproved here.
+
+## Scope and credit
+
+This is a scoped algebraic proof in the formal alphabet. It supplies no
+native implementation, frame conversion, routing, precision, restoration,
+stock bound, supplier admission or multiplication theorem. These physical
+costs remain unknown. Singular targets are excluded. Independent human
+and formal proof-kernel review are unclaimed.
+
+Produced by Nick Petalas. The new result is the local-product reduction
+and exact lift formula. ToikY's #4334 supplies the field-product result,
+the three-factor formula being extended, and the sharp scalar examples.
+Nick Petalas's #4276 supplies the one- and two-factor criteria, following
+#4265 and #4243. Wentao Li's #4099 supplies the right-vector alphabet and
+column bound, building on #2513. Source bytes and commits are pinned in
+SOURCES.json. Apache-2.0.

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

@@ -0,0 +1,125 @@
+# Local radicals preserve the three-factor right-vector obstruction
+
+**Scoped proof with exhaustive finite controls. No new kappa.** This takes
+Open next question 1 of ToikY's [#4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334),
+which proves the field-product case and leaves local products open.
+
+Let `R=R_1 x ... x R_k` be a finite product of associative local
+`K`-algebras. In each component the non-units must form a proper two-sided
+ideal `J_i`. Set `J=product J_i`. Use two roles, paid factors
+`I+u y^T` with `u in R^2`, `y in K^2`, and common free `GL_2(K)` maps.
+For every invertible target `M`, [PROOF.md](PROOF.md) proves
+
+```text
+cost_R(M) <= 2  iff  cost_(R/J)(Mbar) <= 2,
+cost_R(M) = max(delta_R(M), cost_(R/J)(Mbar)) <= 3,
+delta_R(M) = min_{T in GL_2(K)} dim_K ((MT-I)K^2).
+```
+
+Local radicals therefore preserve exactly which invertible targets need
+three factors. They can increase smaller residue costs. Over `F2[e]/e^2`,
+`diag(1+e,1)` and `diag(1+e,1+e)` both reduce to the free identity but
+cost one and two respectively.
+
+The proof reduces the predecessor right-ideal criterion to a common unit
+pivot, then reduces that pivot modulo each component ideal. It extends
+#4334's three-factor word with the ring multiplications in their stated
+order. It applies to noncommutative local algebras as well. In particular,
+for finite `K=F_q`, the sharp component threshold remains `k=q+1`:
+all invertible targets cost at most two for `k<=q`, and every such product
+with `k>=q+1` has a cost-three target. For infinite `K`, all invertible
+targets in a finite product cost at most two.
+
+## Finite evidence
+
+`verify.py` imports no predecessor code. It enumerates literal words of
+cost zero, one and two over `A^k`, where `A=F2[e]/e^2`, for `k=1,2,3`.
+All common right-vector pairs and all six common free endpoints are
+included. Each local factor coefficient is independent across components.
+For an invertible endpoint, filtering to invertible paid factors is sound
+because determinants multiply in these commutative finite rings.
+
+For each common pair and endpoint, it computes the local reachable set
+and its complete `k`-fold Cartesian power. Their union is the exact
+two-factor set, without using the pivot criterion. Separately, it computes
+all six literal binary column ranks for delta. The explicit three-factor
+formula is checked on all 96 local invertible matrices; its common
+right-vector sequence makes the construction valid on every product tuple.
+
+| Components | Invertible targets | Cost 0 | Cost 1 | Cost 2 | Cost 3 |
+|---:|---:|---:|---:|---:|---:|
+| 1 | 96 | 6 | 54 | 36 | 0 |
+| 2 | 9,216 | 6 | 558 | 8,652 | 0 |
+| 3 | 884,736 | 6 | 4,590 | 830,988 | 49,152 |
+
+The maximum formula and radical invariance hold on all **894,048** targets.
+The three-component residue cost-three count is 12, agreeing with #4334;
+each residue target has `16^3=4096` lifts, all of cost three. The printed
+receipt also records every residue-cost/lift-cost count and hashes every
+complete cost table. It binds the results to the package's file hashes.
+There is no handwritten receipt.
+
+Controls detect changing an attaining factor, reversing a product,
+allowing separate free charts, dropping an obstruction component, and
+equating cost with residue cost while ignoring nilpotent contributions.
+Checks remain active under Python optimization.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and NumPy 2.5.4:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-local-products/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-local-products/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-local-products
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/right-vector-local-products --check-source-history
+```
+
+The verifier writes nothing and ends with
+`PASS_RIGHT_VECTOR_LOCAL_PRODUCTS targets=894048 cost3=49152 formula=exact`,
+followed by its generated digest and `no_new_kappa`. Each registered check
+has a 120-second limit. Source commits, blobs and SHA256 pins are in
+[SOURCES.json](SOURCES.json). Its catalogue and selected record are historical
+provenance. The two predecessor proof files are live pinned inputs.
+
+## Limits and engineering notes
+
+The proof concerns invertible two-role targets in the formal alphabet.
+Finite evidence covers the binary dual-number products only; it does not
+enumerate noncommutative local algebras. Native preparation, conversion,
+routing, precision, restoration and stock costs remain unknown. No supplier
+is admitted and no multiplication theorem or frontier changes. Independent
+human and formal proof-kernel review are unclaimed. No Lean, Docker or
+selected construction replay is needed for this isolated result or claimed.
+
+The verifier uses bounded ranges, no recursion, local immutable matrix
+tuples, explicit checks and functions below 60 lines. Python and NumPy
+allocate dynamically; live memory is bounded by arrays over at most
+`96^3` targets and a fixed number of temporaries. This is the managed-runtime
+deviation from static allocation. No shared code changes are included.
+
+The orientation command `scripts/research_baseline.py` fails at this base
+with `KeyError: 'bit_lower'` because it expects the earlier certificate
+schema. The selected record's source-binding check succeeds after sparse
+inputs are materialized. This package does not depend on the baseline helper.
+
+## Open next questions
+
+1. Does the two-factor radical reduction extend to all semilocal algebras?
+   Start with a quotient having one `M_2(K)` block. This would separate
+   radical lifting from noncommutative matrix-block effects, but the
+   present non-unit-ideal argument does not apply to matrix algebras.
+2. Which singular targets over local products are reachable, and do the
+   reachable ones always cost at most three? Begin with the three-factor
+   image over `F2[x,y]/(x,y)^2`. The current unit-pivot and upper-word
+   arguments both use invertibility.
+
+## Credit
+
+This contribution was produced by Nick Petalas. ToikY's #4334 supplies the
+field-product theorem, the three-factor formula extended here, and the
+sharp scalar examples. Nick Petalas's #4276 supplies the one- and
+two-factor criteria, following #4265 and #4243. Wentao Li's #4099 supplies
+the alphabet and column bound, building on #2513. The new claims are the
+local-product radical reduction, exact lift formula and their stated
+consequences. Apache-2.0.

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

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/right-vector-commutative-products/PROOF.md",
+      "usage": "input",
+      "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db",
+      "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408"
+    },
+    {
+      "path": "research/right-vector-two-factor-criterion/PROOF.md",
+      "usage": "input",
+      "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c",
+      "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895"
+    }
+  ]
+}