Prove positive binary correlation for a common-covector guard pair (no κ)

research/common-covector-header-law/PROOF.md

@@ -0,0 +1,139 @@
+# A common-covector pair has a different dependence law
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let K=F_q be any finite field, m>=2, and let a,c be independent columns
+in K^m. Let b be a row with ba=bc=1. Put U=ab, V=cb, P=I-U, Q=I-V.
+Thus U,V are distinct rank-one idempotents with UV=U and VU=V. Both
+products are nonzero. Their complementary projectors P,Q have a common
+image ker(b). This is outside the orthogonal and one-way coupling hypotheses.
+
+For a complete header G chosen uniformly from GL_m(K), let E_P mean that
+every leading principal minor of GPG^-1 of orders 1 through m-1 is
+nonzero. Define E_Q in the same way. Write n=m-1 and
+
+```text
+alpha = q^2-q+1,
+delta = q^2+(q-1)^3.
+```
+
+Then the exact joint passing probability is
+
+```text
+                 (q-1)(delta^n-alpha^n)
+J(q,m) = ----------------------------------------- .             (1)
+         (q^m-1)(q^m-q) q^(m-2)
+```
+
+In particular, over F_2 the events are strictly positively correlated for
+every m>=2. At m=2 the joint probability is 1/3 and each marginal is 1/2.
+This refutes extension of the known negative-correlation statements to
+arbitrary two-way coupled rank-one kernels. It does not contradict their
+stated hypotheses.
+
+Claim type: scoped counting proof with finite corroboration.
+
+## Header orbit and the guard
+
+Conjugation takes the triple to (Ga,Gc,bG^-1). GL_m(K) acts transitively
+on all triples (a,c,b) satisfying independence and ba=bc=1. To see this,
+take a,c-a as the first two basis vectors. The second lies in ker(b).
+Extend it to a basis of ker(b), and b has coordinates (1,0,...,0).
+The same construction for any other triple gives the required change of
+basis. Every triple therefore has the same number of complete-header
+preimages, by the stabilizer coset bijection.
+
+There are (q^m-1)(q^m-q) ordered independent pairs a,c. For each pair,
+the two independent linear equations ba=bc=1 have q^(m-2) solutions b.
+Consequently the denominator in (1) is the number of triples in this orbit.
+
+The rank-one determinant identity gives
+
+```text
+det(P[1:k,1:k]) = 1 - sum_(i=1)^k b_i a_i,
+det(Q[1:k,1:k]) = 1 - sum_(i=1)^k b_i c_i.
+```
+
+This is the marginal guard identity of Nick Petalas #4227. We use its
+partial-sum method, also used in #4261, and count the new common-covector
+orbit directly. For every proper prefix, both partial sums must avoid 1;
+at the final coordinate both sums equal 1.
+
+## Count first, subtract dependent pairs
+
+Temporarily allow all a,c, retaining ba=bc=1. At one coordinate the
+increment is (b_i a_i,b_i c_i). A zero increment has q^2+q-1 preimages:
+q^2 choices with b_i=0, and q-1 with b_i nonzero and a_i=c_i=0.
+Every nonzero increment has q-1 preimages, one for each nonzero b_i.
+Thus the increment weight is q^2 times the zero indicator plus the
+constant q-1 on K^2.
+
+The safe state set S=(K minus {1})^2 has N=(q-1)^2 elements. Its weighted
+transition matrix is q^2 I+(q-1)11^T. Every row sum is
+q^2+(q-1)N=delta. Start at (0,0) in S. After n safe transitions the
+total path weight is delta^n. The terminal state (1,1) is outside S,
+so the last increment is nonzero from every safe state and has weight
+q-1. The number of all passing triples before enforcing independence is
+(q-1)delta^n.
+
+If a,c are dependent, the endpoint conditions force c=a. Indeed a is
+nonzero, write c=t a, and 1=bc=t ba=t. Conversely every diagonal pair
+c=a with ba=1 is a dependent triple. There are no other dependent cases.
+
+For these diagonal triples the scalar increment b_i a_i has 2q-1
+preimages at zero and q-1 at every nonzero element. On K minus {1},
+the safe transition matrix is q I+(q-1)11^T, with row sum
+q+(q-1)^2=alpha. The last step again has weight q-1. Therefore exactly
+(q-1)alpha^n of the passing triples have dependent columns. Subtracting
+them gives the numerator of (1). Dividing by the independent-triple orbit
+count proves (1), in every characteristic and every finite field.
+
+## Binary positive correlation in every dimension
+
+The cited single-request law #4227 gives
+
+```text
+p(q,m) = (q-1)alpha^n / ((q^m-1)q^(m-1)).
+```
+
+At q=2, alpha=3 and delta=5, and direct cancellation yields
+
+```text
+J(2,m) / p(2,m)^2
+ = [2^(n+1)(2^(n+1)-1)/(2^(n+1)-2)] (5^n-3^n)/9^n.       (2)
+```
+
+Since 5>9/2, replacing 5^n by (9/2)^n strictly decreases (2). The
+resulting lower bound is
+
+```text
+2(2^(n+1)-1)/(2^(n+1)-2) * (1-(2/3)^n).
+```
+
+This is at least 1 exactly when 3^n>=2^(n+1)-1. The latter inequality
+holds for every n>=1. It is equality at n=1; if it holds at n then
+3^(n+1)>=3*2^(n+1)-3>=2^(n+2)-1, since 2^(n+1)>=2.
+The replacement of 5^n was strict even at n=1, so J(2,m)>p(2,m)^2
+for every m>=2. This is a written dimension-uniform proof, rather than
+an inference from a finite census.
+
+## Credit and limits
+
+The two-way-coupling question is Open next question 1 of Nick Petalas
+[#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778), following
+#4769/#4274's one-way law. The marginal identity and probability are from
+#4227; #4261 supplies the predecessor partial-sum/header counting method.
+The common-covector orbit, its dependent-pair subtraction, formula (1),
+and the binary positive-correlation proof are the new contribution here.
+Cinna Davis supplied the BIT request context. source527, commdata2338 and
+Jose Manuel retain the normalizer and recursive-closure lineage credit.
+
+Only this common-covector pair and complete uniformly weighted headers are
+covered. The proof does not classify arbitrary two-way pairs, larger
+families, restricted header catalogues, or odd-field correlation signs.
+Selection, emission, dispatch, dirty restoration, stock, precision and the
+physical caller bill remain unknown. No supplier admission, new kappa,
+selected-frontier change or complete multiplication theorem follows.
+Independent human and formal proof-kernel review are unclaimed.

research/common-covector-header-law/README.md

@@ -0,0 +1,104 @@
+# Positive correlation for a common-covector full-guard pair
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped counting proof with finite corroboration. Over any finite
+field F_q, let a,c be independent columns, b a row with ba=bc=1, and
+P=I-ab, Q=I-cb on F_q^m, m>=2. For complete uniformly weighted GL_m(F_q)
+headers, the joint full-guard passing fraction is exactly
+
+```text
+           (q-1)[(q^2+(q-1)^3)^(m-1) - (q^2-q+1)^(m-1)]
+J(q,m) = ------------------------------------------------- .
+                    (q^m-1)(q^m-q)q^(m-2)
+```
+
+Over F_2 these two guard events are strictly positively correlated in every
+dimension m>=2. At m=2, J=1/3 exceeds the marginal product 1/4; at m=3,
+J=4/21 and each marginal is 9/28. Thus negative correlation for the known
+orthogonal and one-way cases does not extend to every two-way pair.
+
+[PROOF.md](PROOF.md) counts the common-covector header orbit by two partial
+sums, subtracts exactly the equal-column paths, and proves the binary
+comparison for all dimensions. This answers one case of Open next question 1
+in [#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778). That
+question and #4769/#4274's contrasting one-way law retain Nick Petalas's
+credit, as do #4227's marginal law and #4261's partial-sum/header method.
+Cinna Davis supplied the BIT request context; source527, commdata2338 and
+Jose Manuel retain the normalizer and recursive-closure lineage credit.
+No predecessor implementation is imported or replayed.
+
+## Reproduction and evidence
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/common-covector-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/common-covector-header-law/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/common-covector-header-law
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/common-covector-header-law --check-source-history
+```
+
+Another CPython 3.12 installation may replace the local interpreter path.
+The direct marker is `PASS_COMMON_COVECTOR_HEADER_LAW`. The verifier writes
+no files. It prints a generated receipt with every domain's counts and
+SHA256 hashes of all six package files. Both registered modes keep explicit
+checks active, including optimized Python.
+
+The verifier enumerates all 34,290 complete headers in eight domains:
+GL_2 over F_2,F_3,F_4,F_5,F_7, GL_3 over F_2,F_3, and GL_4 over F_2.
+It inverts each header, conjugates both literal projectors and tests every
+leading minor through rank m-1. Both marginals and the joint count agree.
+F_4 is F_2[x]/(x^2+x+1), rather than integers modulo four.
+
+A separate vector enumeration counts all 26,070 independent orbit triples
+in nine domains: q=2,m=2..5; q=3 or 4,m=2..3; q=5,m=2. Ten coordinate
+transfers enumerate the actual increment factorizations for widths one and
+two over F_2,F_3,F_4,F_5,F_7, at path lengths zero through eight. Their
+difference agrees with the joint formula at m=2..9. Exact rational checks
+corroborate binary positive correlation in all 255 dimensions m=2..256.
+Fourteen fixture, mutation and invalid-input controls distinguish the
+field arithmetic, independence, orthogonal substitution, omitted diagonal
+subtraction, omitted row fiber and invalid finite-check parameters.
+
+## Scope and implementation limits
+
+The all-field and all-dimension claims rest on the written proof. Finite
+execution corroborates the explicitly enumerated domains. Only two distinct
+rank-one kernels with a common right covector and complete equally weighted
+headers are covered. Other two-way pairs, larger families, restricted
+headers and odd-field correlation signs are outside the proved claims.
+
+Header selection, emission, dispatch, dirty restoration, stock, precision,
+producer compatibility and the complete paid physical caller remain unknown.
+No new kappa, 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 operator replay are unrun.
+
+[TASK.json](TASK.json) records the change from the formal-interface card to
+this algebraic side question. [SOURCES.json](SOURCES.json) binds predecessor
+text, the catalogue and selected record as historical provenance on canonical
+main. There are no runtime dependencies outside this package and no pending
+Git-object dependency. Provenance/history checks require full Git history;
+the direct verifier also runs from a standalone exported package.
+
+Power of Ten inspection finds no recursion or subprocesses in the verifier.
+Every loop is bounded by fixed domains: at most 65,536 candidate matrices
+of size four, 64 vectors per triple coordinate, 49 transfer states, nine
+transfer rounds and 255 correlation dimensions. Functions fit within 60
+lines. Explicit require checks enforce input and mathematical contracts.
+CPython allocates dynamically, a managed-runtime deviation from fixed
+allocation; the stated domains bound live collections. Diagnostics use
+warnings as errors. No shared implementation is changed.
+
+## Open next questions
+
+1. Determine the law for two-way pairs with independent covectors. Start
+   with one normalized pair whose two cross products are nonzero; its
+   partial-Gram orbit differs from the shared-covector model here.
+2. Determine the correlation signs for this common-covector family over
+   odd fields. Compare the new joint formula with #4227's marginal squared,
+   starting with q*delta-alpha^2=q-1; a quantified sign proof is unclaimed.
+3. Find a named physical producer and fully charged shared-header caller.
+   Pin its header domain before charging selection, emission, dispatch,
+   dirty restoration, precision and stock. Those costs are unknown.

research/common-covector-header-law/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "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/projector-header-density/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d",
+      "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262"
+    },
+    {
+      "path": "research/corankone-all-field-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ac0152e05a5c050bbd740ddbe6d0cbaaecbb6cd8",
+      "sha256": "ca7762bea269445f7b30c59c7b6161282483da5fd191faa668145f1ad6d8ade4"
+    },
+    {
+      "path": "research/corankone-pair-header-law/README.md",
+      "usage": "provenance",
+      "git_blob": "743cf79ee8403d66cb651ac1111065cc650ad638",
+      "sha256": "ca362324cd8a041a25d6494f857e0f8bf7b2ef0d6f8c83ec5e8c08b0f92ca515"
+    },
+    {
+      "path": "research/corankone-all-field-law/README.md",
+      "usage": "provenance",
+      "git_blob": "83a3e9e3de457d97743e6364a71cc493d0158fc1",
+      "sha256": "05422e3227c67f6a973282e01ac77031df58464184caf0f138d7b0c1af935c98"
+    }
+  ]
+}