Prove the full-guard law for one-way coupled corank-one requests

research/oneway-corankone-header-law/PROOF.md

@@ -0,0 +1,127 @@
+# One-way coupled corank-one requests
+
+## Contract
+
+Let K be a finite field of order q and m>=2. Let U,V be rank-one
+idempotents on K^m with UV nonzero and VU=0. Put P=I-U and Q=I-V.
+A header G in GL_m(K) passes R when every leading principal minor of
+GRG^-1 of orders 1 through rank(R) is nonzero. Headers have equal weight.
+Both requests have rank m-1 and use the same complete header.
+
+The claim is a scoped counting proof. It extends the partial-Gram method
+of Nick Petalas's #4261 from orthogonal kernels to one-way coupled kernels.
+The noncommuting requests are outside its hypotheses and outside #4259's
+laminar-family theorem. No physical implementation or new kappa follows.
+
+## All-field transfer theorem
+
+Write B=[[1,1],[0,1]]. Define, for 2 by 2 matrices A,
+
+```text
+w(A) = 2q^2-1 if A=0;
+       q-1    if rank(A)=1;
+       0      if rank(A)=2.
+S = {A : A_11 != 1 and A_22 != 1}.
+f_0(A) = 1 if A=0, otherwise 0.
+f_(j+1)(A) = sum_(T in S) f_j(T) w(A-T), for A in S.
+C(q,m) = sum_(A in S) f_(m-1)(A) w(B-A).
+D(q,m) = (q^m-1)(q^m-q) q^(2m-4).
+```
+
+**Theorem.** The joint passing fraction is C(q,m)/D(q,m). There are
+C(q,m)|GL_(m-2)(K)| passing headers, with |GL_0(K)|=1. The transfer has
+q^2(q-1)^2 states and applies to every finite field.
+
+**Proof.** Write U=u a and V=v b with a(u)=b(v)=1. The assumptions give
+b(u)=0 and a(v)!=0. Rescale v and b inversely so that a(v)=1. Then
+X_0=(u,v) and Y_0=(a;b) satisfy Y_0 X_0=B. Both have rank two since B
+is invertible. Choose an ordered basis of ker(Y_0) after u,v. In this
+basis U=e_1(e_1^T+e_2^T), V=e_2 e_2^T and Y_0=[B 0]. This change of
+fixed basis permutes the header domain, preserving the fraction.
+
+For a header G, put X=G X_0 and Y=Y_0 G^-1. Then YX=B and the
+conjugated kernels are the first column of X times the first row of Y,
+and the second column times the second row. Conversely, given X,Y with
+YX=B, choose the remaining columns of G as any ordered basis of ker(Y).
+This gives an invertible G and YG=[B 0]=Y_0. The fiber has exactly
+|GL_(m-2)(K)| elements. There are (q^m-1)(q^m-q) full-rank X, and each
+of the two rows of Y has q^(m-2) solutions to its two equations. Thus
+there are D(q,m) pairs, with equal fibers.
+
+For a column x and row y, multilinearity of the determinant gives
+
+```text
+det((I-xy)[1..j,1..j]) = 1 - sum_(i=1)^j y_i x_i.
+```
+
+Terms choosing the rank-one part from two columns vanish. This is the
+corank-one guard reduction of #4227. If x_i is row i of X and y_i is
+column i of Y, the two diagonal entries of A_j=sum_(i<=j) y_i x_i are
+exactly the two guard prefix sums. Hence A_j must lie in S for 1<=j<m,
+while A_m=B. The guards impose no condition at order m.
+
+Each coordinate increment y_i x_i has w(A) ordered factorizations.
+For A=0, either factor is zero, giving 2q^2-1 choices. Every nonzero
+rank-one A has q-1 factorizations by reciprocal rescaling; rank two has
+none. Summing independent coordinate choices gives the transfer above.
+Invertibility of B already forces X,Y to have rank two, so no further
+rank or independence filter is missing. Equal fibers prove the claim.
+
+## Binary closed form
+
+Put n=m-1. For every m>=2,
+
+```text
+C(2,m) = (9^n - 5^n)/4,
+Pr(P and Q pass) = (9^(m-1)-5^(m-1))
+                  / [4(2^m-1)(2^m-2)2^(2m-4)].
+```
+
+**Proof.** Safe states over F2 have zero diagonal and are indexed by their
+two off-diagonal bits. Safe increments are zero with weight seven, E_12
+with weight one and E_21 with weight one. The final increment B-A has
+both diagonal entries one. Its determinant vanishes exactly when
+(1+A_12)A_21=1, so only A_12=0,A_21=1 contributes, with weight one.
+
+The length-n walk on F2^2 therefore ends at (0,1). The four character
+eigenvalues of its transition operator are 9,7,7,5. Character inversion
+at (0,1) gives (9^n+7^n-7^n-5^n)/4. This proves the formula, including
+integrality. A walk with one E_21 and n-1 zero increments proves positivity
+for every m>=2. For m=2,3,4,5,6 the fractions are respectively
+1/6, 1/12, 151/3360, 371/14880 and 451/32256.
+
+## Comparison and correlation
+
+The orthogonal-kernel count in #4261 is
+C_orth=(9^n-2*7^n+5^n)/4. The new one-way count exceeds it by
+(7^n-5^n)/2>0 for every m>=2, with the same denominator D(2,m).
+Thus one-way coupling creates passing headers even at m=2, where the
+orthogonal pair has none. This is a count improvement, without a priced
+caller or a primitive-saving claim.
+
+The two passing events remain strictly negatively correlated. The marginal
+law from #4227 is s_m=3^n/[(2^m-1)2^n]. Directly, each of the first n
+coordinate products must be zero, with three choices each; the last must
+be one. The normalized rank-one denominator is (2^m-1)2^n. Therefore
+
+```text
+joint / s_m^2 = (2^(n+1)-1)/(2^(n+1)-2) * [1-(5/9)^n] < 1.
+```
+
+The inequality is equivalent to (2^(n+1)-1)5^n>9^n. It holds at n=1;
+the left-to-right ratio increases at each step since
+5(2^(n+2)-1)>9(2^(n+1)-1). The joint density is asymptotic to
+(1/4)(9/16)^n and its ratio to s_m^2 tends to one from below. These
+conclusions use the complete equally weighted header domain.
+
+## Scope
+
+The theorem covers one-way coupled rank-one kernels over finite fields.
+Pairs with both UV and VU nonzero, coincident images or covectors, restricted
+header subsets, and finite local rings are outside scope. The all-field
+result is a recurrence; only F2 has a closed form here. Written mathematics
+is the universal evidence. The executable census covers only its declared
+finite domains. Binary guards extend beyond the retained normalizer's
+odd-prime executable domain. Even for odd fields, a request producer,
+header selection/emission, dispatch, dirty return, stock and full physical
+invoice remain unknown. No multiplication theorem or supplier is admitted.

research/oneway-corankone-header-law/README.md

@@ -0,0 +1,154 @@
+# Exact full-guard law for a one-way coupled pair
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: **scoped counting proof with finite corroboration**. Let U,V
+be rank-one idempotents over F_q^m with UV nonzero and VU=0. Both
+corank-one requests P=I-U and Q=I-V use one equally weighted complete
+GL_m header. A request passes when every leading principal minor through
+its rank is nonzero. These requests do not commute.
+
+[PROOF.md](PROOF.md) proves an exact all-field transfer with
+q^2(q-1)^2 states. Over F2, for every m>=2, its closed form is
+
+```text
+Pr(P and Q pass) = (9^(m-1)-5^(m-1))
+                  / [4(2^m-1)(2^m-2)2^(2m-4)].
+```
+
+The fractions at m=2,3,4 are 1/6, 1/12 and 151/3360. This strictly
+exceeds the orthogonal-kernel density of
+[#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261) in every
+dimension, by (7^(m-1)-5^(m-1))/(2D), with
+D=(2^m-1)(2^m-2)2^(2m-4). Both passing events are still strictly
+negatively correlated. Their joint fraction is asymptotic to
+(1/4)(9/16)^(m-1); its ratio to the product of marginals tends to one.
+
+The changed premise is one-way coupling of the kernel projectors. This
+answers a higher-rank subcase of the nonorthogonal full-guard question in
+[#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240).
+The new step normalizes the partial-Gram endpoint to [[1,1],[0,1]] and
+extracts the changed binary walk endpoint. It is original counting work,
+not an audit of the cited packages. No new kappa or supplier admission.
+
+## Reproduction and evidence
+
+From the repository root, with any CPython 3.12 replacing this local path:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/oneway-corankone-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/oneway-corankone-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/oneway-corankone-header-law
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/oneway-corankone-header-law --check-source-history
+```
+
+The scientific marker is `PASS_ONEWAY_CORANKONE_HEADER_LAW`. Its generated
+stdout JSON records each exact count and SHA256 bindings for every package
+file and both live inputs. No stored or handwritten receipt is used. The
+verifier authenticates inputs before enumeration and writes no files.
+
+The complete bounded replay checks:
+
+- **32,094 complete GL headers** over F2 at m=2,3,4; F3 at m=2,3;
+  and F5 at m=2. Generic matrix conjugation and literal no-pivot
+  elimination test both full guard chains. Every normalized-pair fiber
+  is counted and checked to have the same size.
+- **1,946,574 normalized pairs X,Y with YX=[[1,1],[0,1]]**, separately
+  enumerated over F2 at m=2..6, F3 at m=2..4 and F5 at m=2,3. Every
+  joint fraction matches the transfer and every marginal matches the
+  cited #4227/#4228 corank-one formula.
+- **84 transfer cases**, over F2 at m=2..64 and F3,F5,F7 at m=2..8.
+  All 63 binary counts match the closed form and strict gain/correlation
+  identities. Rank-one factor multiplicities are independently enumerated
+  over all four fields.
+- Five controls distinguish the orthogonal endpoint, wrong binary parity,
+  a lost zero-factor multiplicity, independent marginals and first-pivot-only
+  admission. At q=2,m=3, first-only admission accepts 66 headers while
+  full admission accepts 14, out of 168.
+
+Both normal and optimized Python execute explicit checks, so `-O` does not
+remove them. The finite counts corroborate the written all-parameter proof.
+
+## Scope and remaining obligations
+
+The transfer applies to every finite field. Executed arithmetic uses only
+F2,F3,F5,F7; extension-field execution is unrun. Only F2 has a closed form
+here. The theorem requires fixed one-way coupled kernels and complete,
+equally weighted headers. It says nothing about arbitrary restricted covers,
+local rings, coincident image/kernel types or pairs with both products nonzero.
+
+Binary guards extend beyond the retained normalizer's odd-prime executable
+domain. Even in odd characteristic, no real producer, header selection or
+emission, dispatch, dirty return, stock, precision or complete physical invoice
+is supplied. Those costs are unknown. No selected cold replay, GL64 scan,
+Lean or Docker run was performed. No complete multiplication theorem is
+claimed. Independent human and formal proof-kernel review are unclaimed.
+
+The executable loops have bounded domains, with no recursion. The largest
+transfer has 1,764 states and at most 679,140 candidate transitions; each
+normalized census uses at most 125 vectors, at most 125^2 candidate X
+choices and at most 125 candidate rows per X. Accepted row-fiber pairs
+have at most 16^2 combinations. Direct GL censuses visit at most 65,536
+candidate matrices, of dimension at most four; factor vectors have length
+at most six.
+CPython's dynamic integers and containers are a managed-runtime deviation
+from fixed allocation, constrained here by these explicit finite domains.
+All functions stay below 60 lines. Registered diagnostics use warnings as
+errors in normal and optimized modes. No standalone Ruff executable was
+available; local AST inspection checks syntax and function sizes.
+
+## Related open work and credit
+
+- [#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261), head
+  `4728fc766b3084f3ab2f5c8543a5e74e4a12b126`, supplies the orthogonal-kernel
+  partial-Gram method. The new numerator is strictly larger in all 63 binary
+  replay dimensions. Its m=3 density 1/84 differs from the new 1/12, as the
+  changed premise predicts; no same-type joint number is shared.
+- [#4240](https://github.com/CrocSwap/integer-mult-bounds/pull/4240), head
+  `9f9c89ed75e9fdae6b6762925b080fb308824858`, supplies the one-sided
+  rank-one classification. At m=2 our requests have that type. Its joint
+  fractions for q=2,3,5,7 agree numerically with this transfer, respectively
+  1/6, 1/4, 13/30 and 31/56. This adds the full chain at m>2.
+- [#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227), head
+  `3d793eade8de2ba49ec08f8d004c1b2f566a78e6`, supplies the determinant
+  reduction and marginal law. All ten marginal census fractions agree
+  numerically; the joint one-way law is new.
+- [#4228](https://github.com/CrocSwap/integer-mult-bounds/pull/4228), head
+  `bb25dcedb5bbbacd3c35359eb6b5488b087bcde6`, supplies all-rank marginal
+  densities. Its corank-one specialization agrees on those same ten cases;
+  no intermediate-rank recurrence is imported.
+- [#4239](https://github.com/CrocSwap/integer-mult-bounds/pull/4239), head
+  `5e24dfb5463d540721687d92c369609da5589523`, counts orthogonal rank-one
+  requests. The one-way requests here share no joint type with that theorem,
+  including at m=2, so no overlapping joint number is asserted.
+- [#4246](https://github.com/CrocSwap/integer-mult-bounds/pull/4246), head
+  `a2d99d73bf21b39fbb0a9a88917424ff26c2e63c`, counts orthogonal full chains.
+  Our noncommuting pair is outside that hypothesis; no joint number is shared.
+- [#4259](https://github.com/CrocSwap/integer-mult-bounds/pull/4259), head
+  `2a582d8f66d1900b22ee2cd0062ee5dca94e8f85`, counts laminar full chains.
+  Our pair is neither contained nor orthogonal; no joint number is shared.
+- [#4100](https://github.com/CrocSwap/integer-mult-bounds/pull/4100) supplies
+  the BIT request and complete-header context. Its actual caller costs and
+  multiplication claim are outside this package; no recursive bill is compared.
+
+All the preceding counting packages were produced by Nick Petalas. Source527,
+commdata2338 and Jose Manuel retain the normalizer and recursive-closure
+credit. Cinna Davis supplies BIT.md. Chris R / Clear1nsight's #3950 is earlier
+deterministic counting context. The proof and enumerators are self-contained;
+no unmerged source code or unavailable Git-history object is imported.
+SOURCES.json pins the two retained main-branch contract files, base and card.
+
+## Open next questions
+
+1. What is the full-guard law when both UV and VU are nonzero? Start with
+   endpoint [[1,a],[b,1]], separating invertible endpoints from ab=1.
+   The singular endpoint needs extra image/covector-rank filters to identify
+   the intended simultaneous-conjugacy orbit.
+2. Can an actual odd-field producer use a fully charged one-way shared-header
+   caller? Pin its kernel lines and charge selection, emission, dispatch,
+   dirty restoration and stock. No producer or complete invoice is supplied.
+
+The active ternary orthogonal-pair and three-orthogonal-kernel claims in the
+[handoff thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166)
+change the field or number of orthogonal kernels. They are separate from this
+changed-coupling question. [TASK.json](TASK.json) records scope and provenance.

research/oneway-corankone-header-law/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py",
+      "usage": "input",
+      "git_blob": "3e8a72e7ce705c51ff24e9015ccf6463204ff193",
+      "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77"
+    },
+    {
+      "path": "research/unconditional-batched-crt/BIT.md",
+      "usage": "input",
+      "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa",
+      "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da"
+    }
+  ]
+}