Prove four independent full guards beat their product over every field

research/independent-four-guard-positive/PROOF.md

@@ -0,0 +1,201 @@
+# Four independent full guards are strictly above their product
+
+Let K be a finite field of order q, let m >= 4, and put d = m-1. Fix a
+nonzero column u and four linearly independent rows v_i with v_i u = 1.
+For a uniform G in GL_m(K), let E_i mean that every leading principal minor
+of orders 1 through m-1 of G(I-u v_i)G^-1 is nonzero.
+
+**Theorem.** If p = Pr(E_i), then
+
+```text
+Pr(E_1 and E_2 and E_3 and E_4) > p^4
+```
+
+for every q and m in this domain. This is a four-event statement. It does
+not assert association of every subfamily of an arbitrary dependent tuple.
+
+The new steps below are the explicit four-dimensional subspace
+classification, its closed formula, and the all-field four-event sign.
+SHIN09-git's #6710 supplies the general subspace counting law and the
+enlarged-space method used for triples. Those are cited premises, not new
+results or executable dependencies.
+
+## An explicit formula
+
+Define
+
+```text
+A = q + (q-1)^2
+W = q^4 + (q-1)^5
+D = (q^(d+1)-1) q^d (q^d-1)(q^d-q)(q^d-q^2)
+B_s = q^2 + (q-1)^2 (q+1-s),                  s = 2,3,4
+H_s = (q-1)^(4-s) [(q-1)^s + (-1)^s(q-1)] / q
+C_s = q^3 + (q-1) H_s
+
+(a_2,a_3,a_4) = (7, 6(q-2), (q-2)(q-3))
+(b_2,b_3,b_4) = (6, 4(q-2), q^2-3q+3).
+```
+
+Then the exact joint law is
+
+```text
+J_4 = (q-1) [W^d - sum_s b_s C_s^d
+                    + q sum_s a_s B_s^d - q^3 A^d] / D.
+```
+
+To derive it, apply #6710's law to S = K^4 and t = (1,1,1,1).
+For a subspace L containing t, that law uses
+
+```text
+h(L) = #{x in L : every coordinate of x is nonzero}
+lambda(L) = q^dim(L) + (q-1) h(L)
+mu(L,K^4) = (-1)^c q^(c(c-1)/2), c = 4-dim(L).
+```
+
+In dimension one, L = <t>, h = q-1, and mu = -q^3. In dimension four,
+h = (q-1)^4 and mu = 1.
+
+A two-dimensional L is spanned by t and a nonconstant vector x. Let s
+be the number of distinct coordinates of x. Replacing x by ax+bt, with
+a nonzero, preserves s and gives exactly q(q-1) representatives of the
+same L. The number of ordered four-tuples using exactly s distinct field
+values is S(4,s) q(q-1)...(q-s+1). Since the three relevant Stirling numbers
+are 7, 6, 1, division gives a_s as above. Counting x_0+t_0 x with all
+coordinates nonzero gives h = (q-1)(q+1-s). Thus lambda = B_s and mu = q.
+When s > q the corresponding a_s is zero, so no nonexistent class enters.
+
+A three-dimensional L is a hyperplane a dot x = 0, where a dot t = 0.
+Its normal is unique up to nonzero scale. If its support has size s, the
+number of full-support vectors in L is H_s. Indeed, after scaling the
+s constrained coordinates, the number of nonzero s-tuples summing to zero
+is
+
+```text
+Z_s = [(q-1)^s + (-1)^s(q-1)] / q.
+```
+
+This follows from Z_1 = 0 and Z_(s+1) = (q-1)^s - Z_s: choose the first
+s entries, and the last nonzero entry is forced precisely when their sum
+is nonzero. There are binom(4,s) Z_s/(q-1) normal lines of support s.
+For s = 2,3,4 these are exactly b_s. Thus lambda = C_s and mu = -1.
+These classes exhaust both projective planes of size q^2+q+1 in the
+subspace interval. Substitution proves the formula over every finite field.
+
+## A sufficient tail inequality
+
+Write Q = q^d, t_1 = 1-1/q+1/q^2, and
+
+```text
+c = (1-1/q)/(1-q^(-m)),     p = c t_1^d.
+```
+
+Sample u' uniformly among the nonzero columns. Conditional on u', sample
+four normalized rows independently and uniformly from v u' = 1. This
+affine hyperplane has Q points. Let I be the event that the four rows
+are independent. Normalization makes linear independence equivalent to
+affine independence, so
+
+```text
+P_I = (1-1/Q)(1-q/Q)(1-q^2/Q),
+1-P_I <= (1+q+q^2)/Q.
+```
+
+Conditioning on I gives the uniform independent-four tuple orbit by
+#6710's equal-fiber argument.
+
+Let z(u') be the conditional single-guard pass probability. Its mean is p.
+It vanishes unless the last coordinate u'_m is nonzero. To see this,
+the rank-one determinant identity gives the order-j minor as
+1-sum_(a<=j) u'_a v_a. If u'_m = 0, the order-d minor is zero by
+v u' = 1. The last-coordinate event has probability c.
+Conditional Jensen therefore gives
+
+```text
+T = E[z^4] >= p^4/c^3.
+```
+
+Since the joint event outside I has probability at most 1-P_I,
+P_I J_4 >= T-(1-P_I). It is sufficient for J_4 > p^4 that
+
+```text
+p^4 (c^-3 - 1) > 1-P_I.
+```
+
+Now c^-1 = 1+q^-1+...+q^-d, so c^-3-1 >= 3/q.
+Also c > 1-1/q. Hence the following exact rational inequality suffices:
+
+```text
+L(q,d) = (3/q)(1-1/q)^4 (q t_1^4)^d > q^2+q+1.          (1)
+```
+
+For q >= 4, t_1 >= 3/4 and q(3/4)^4 > 1. For q = 3,
+q t_1^4 = 2401/2187 > 1. Thus a successful tail threshold persists
+as d increases for every q >= 3.
+
+## Uniform large-field coverage and the finite remainder
+
+For q >= 25, at d = 3,
+
+```text
+L(q,3) = 3q^2(1-1/q)^4 t_1^12
+       > 3q^2(1-1/q)^16
+       >= 3q^2 - 48q
+       > q^2 + q + 1.
+```
+
+The middle step is Bernoulli's inequality. The last difference is
+2q^2-49q-1, positive at q=25 and strictly increasing thereafter.
+This covers every d >= 3 at every field order q >= 25.
+
+For q=2, the event u' supported on the last coordinate passes all four
+guards and has probability b = c 2^-d. Since c < 1 and
+(3/4)^4 < 1/2, we have p^4 = c^4(3/4)^(4d) < b.
+
+The remaining finite field orders and exact thresholds in (1) are:
+
+| q | first d_0 >= 3 satisfying (1) | dimensions 3 <= d < d_0 |
+| ---: | ---: | ---: |
+| 3 | 45 | 42 |
+| 4 | 9 | 6 |
+| 5 | 6 | 3 |
+| 7 | 4 | 1 |
+| 8 | 4 | 1 |
+| 9 | 4 | 1 |
+| 11 | 4 | 1 |
+| 13 | 4 | 1 |
+| 16 | 3 | 0 |
+| 17 | 3 | 0 |
+| 19 | 3 | 0 |
+| 23 | 3 | 0 |
+
+The verifier checks (1) at each d_0 and evaluates the closed formula
+against p^4 with exact rational arithmetic in each of the 56 remaining
+cases. It prints every exact ratio, which is strictly greater than one.
+Together with the analytic bounds, these finite comparisons prove the sign
+in all dimensions and over every finite field. No numerical approximation
+or assumption about unenumerated exceptions enters the argument.
+
+## Separate finite corroboration of the formula
+
+The verifier explicitly enumerates all two- and three-dimensional
+subspaces in the above interval over F_2, F_3, F_4, F_5 and F_7 and checks
+both class multiplicities and every h(L). F_4 uses x^2+x+1, rather than
+arithmetic modulo four.
+
+A second computation treats the first new ambient dimension m=4 over
+F_2, F_3, F_4 and F_5. Conditional on u'_m != 0 and exactly j zero
+coordinates among its first three entries, an invertible triangular
+coordinate change makes the allowed rows the box
+K^j times (K without zero)^(3-j). The coordinate change preserves
+affine independence. The number of such u' is
+(q-1) binom(3,j)(q-1)^(3-j).
+
+To count ordered affine bases of a box, enumerate every unordered triple
+of points. A noncollinear triple defines one affine plane. Each point
+outside that plane is a valid fourth point, and each unordered triple
+has six orderings. This counts exactly the ordered affinely independent
+quadruples, without using the subspace formula. Weight the four box counts
+by the image-column multiplicities and divide by
+(q^4-1) q^3(q^3-1)(q^3-q)(q^3-q^2). The resulting fractions agree with
+the formula. These are new bounded checks, not replays of a predecessor's
+scientific suite.

research/independent-four-guard-positive/README.md

@@ -0,0 +1,91 @@
+# Four independent full guards beat their product over every finite field
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written counting proof with exact finite corroboration.
+For every finite field K, every m >= 4, every nonzero column u and four
+independent rows v_i normalized by v_i u = 1, a uniform complete GL_m(K)
+header passes all proper leading-minor guards of I-u v_i with probability
+strictly greater than the product of the four individual probabilities.
+
+[PROOF.md](PROOF.md) gives an explicit eight-term exponential formula for
+the joint law and proves the sign. A uniform analytic bound covers all
+field orders at least 25. Exact tail thresholds cover the remaining field
+orders after 56 rational comparisons. The binary case follows directly
+from the last-coordinate event.
+
+This resolves the four-covector case of Open next question 1 in
+[SHIN09-git's #6710](https://github.com/CrocSwap/integer-mult-bounds/pull/6710).
+That package's general subspace law and independent-triple sampling method
+are credited premises. The new four-dimensional classification, closed
+formula and all-field four-event sign are the contribution here. ToikY's
+#6701 and #6703 supply the binary-family and pair-correlation precedents.
+Nick Petalas's #4227 and #4807 supply earlier marginal and pair laws.
+The retained Ryanson Jonathan, Cinna Davis, source527, commdata2338 and
+Jose Manuel BIT/normalizer/compiler lineage keeps its predecessor credit.
+The binary and ternary signs are already covered by #6710. The uniform
+four-row theorem extends that coverage to every field. No predecessor
+executable is imported or replayed.
+
+## Reproduce
+
+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/independent-four-guard-positive/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/independent-four-guard-positive/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/independent-four-guard-positive
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/independent-four-guard-positive --check-source-history
+```
+
+Other machines can substitute their CPython 3.12 interpreter path. The
+standalone verifier needs no Git, network or predecessor package. It writes
+no artifacts and prints a generated receipt with the SHA256 of all six
+package files, followed by `PASS_INDEPENDENT_FOUR_GUARD_POSITIVE`.
+
+The finite check includes all 56 exceptional sign comparisons, all 258
+two- and three-dimensional subspaces in the declared interval over fields
+of orders 2, 3, 4, 5 and 7, and a separate affine-plane count of ordered
+four-point bases in 16 boxes over fields of orders 2, 3, 4 and 5 at m=4.
+It checks four altered Mobius terms, distinguishes the independence guess,
+and rejects four out-of-domain formula inputs. Every reported comparison
+and box count is computed. The written proof supplies the universal scope.
+
+The verifier uses bounded loops, no recursion and functions below 60 lines.
+Its largest box has 125 points and 317,750 unordered triples; its largest
+stratum check has 57 normal lines and at most 1,296 full-support vectors
+per line. CPython dynamic allocation and integer arithmetic are explicit
+managed-runtime deviations from fixed allocation. Live collections are
+bounded by these fixed domains. Both registered modes treat warnings as
+errors and keep explicit checks enabled under optimization.
+
+## Scope and remaining obligations
+
+Only independent normalized covectors and uniform complete general-linear
+headers are covered. Dependent families can have a different sign. This
+does not price or construct a physical header producer, caller, selection,
+dispatch, dirty restoration, stock or precision. The complete recursive
+invoice and all selected framework assumptions remain open. No new kappa,
+supplier admission, selected-frontier change or complete multiplication
+theorem is claimed. Independent human and formal proof-kernel review are
+unclaimed. Selected cold replay, Lean and Docker were not run.
+
+The formal-interface-lemma card's scope is changed to this explicitly open
+local counting problem. The source pin identifies the question and cited
+theorems. Those files are historical provenance, not runtime inputs.
+The broader overlap helper reported incomplete sparse local-note coverage;
+the target was separately searched in canonical main and live PR bodies.
+Its closed-PR API scan timed out. A direct author/date/reference query
+found #6793, which cites #6710 as background but studies paid monomial
+header costs, rather than the full-GL four-event question here.
+
+## Open next questions
+
+1. Do five or more independent normalized covectors beat their product in
+   every dimension? Start with five rows and classify the intermediate
+   subspaces through the all-ones vector. Their full-support counts need
+   more data than the two four-dimensional classifications used here.
+2. Can an actual BIT caller use the four-event count with a fully paid
+   uniform complete-header producer? First pin its request tuple and
+   header distribution. Selection, emission, dispatch, restoration,
+   precision, storage and the full signed bill are unresolved.

research/independent-four-guard-positive/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/common-image-guard-pencils/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e67bc62fc5efa61b2a184ea176c64861906b71a1",
+      "sha256": "befa92a531d4fc42bb235d78294d92bcea6feb1bb9f5f7c71daf0d6fef21e36d"
+    },
+    {
+      "path": "research/common-image-guard-pencils/README.md",
+      "usage": "provenance",
+      "git_blob": "0a040368a1b6674d491321e22154c69abc5a3b40",
+      "sha256": "79a4c4476cd5da844b1c1604474a4e09dcf6470b42ee1d81f466998c45d1af97"
+    },
+    {
+      "path": "research/common-image-guard-pencils/TRIPLES.md",
+      "usage": "provenance",
+      "git_blob": "d84835704ea510b6693d654277943a94e5d87a56",
+      "sha256": "770723e2dc12bfc87e161ca2f7d1541ec4fce0c6b4cf97b0291e0aae6cb577ce"
+    }
+  ]
+}