Prove the binary pair-versus-singleton full-guard inequality (no κ)

research/corankone-triple-block-correlation/PROOF.md

@@ -0,0 +1,131 @@
+# A pair of binary full guards is negatively correlated with a third guard
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Let U1,U2,U3 be pairwise orthogonal rank-one idempotents on F2^m,
+where m>=3, and let Ei be the event that every leading principal minor
+through rank m-1 of G(I-Ui)G^-1 is nonzero. All three events use the same
+uniform complete header G in GL_m(F2).
+
+**Theorem.** Pr(E1 E2 E3) < Pr(E1 E2)Pr(E3), for every m>=3.
+
+This is a scoped counting proof with an exact computer-assisted finite
+component. It answers the first bounded step in Open next question 1 of
+Nick Petalas's [#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767).
+The pair and triple counting laws below are cited predecessor theorems,
+not re-proved or independently audited here. The new result compares a
+two-event block with a singleton. Symmetry gives every permutation of
+the split. No statement about arbitrary increasing functions is claimed.
+
+## Cited inputs and the new reduction
+
+Write n=m-1, X=2^m, and define
+
+```text
+A = 9^n - 2*7^n + 5^n,
+B = 3^n A = 27^n - 2*21^n + 15^n,
+T = 27^n - 6*21^n + 6*19^n - 6*17^n + 16*15^n
+    - 18*13^n + 9*11^n - 2*9^n.
+```
+
+Nick Petalas's #4227, #4261 and #4275 respectively supply
+
+```text
+p1 = Pr(E3)       = 3^n / ((X-1)2^n),
+p2 = Pr(E1 E2)    = A / ((X-1)(X-2)2^(2n)),
+p3 = Pr(E1 E2 E3) = T / ((X-1)(X-2)(X-4)2^(3n)).
+```
+
+These are complete-header probabilities. All source proofs are pinned as
+historical provenance in SOURCES.json. No predecessor executable is used.
+The sharp difference from the earlier comparison p3<p1^3 is that the
+denominator of the new ratio contains the nontrivial pair numerator A.
+
+For n>=2, A>0 by strict convexity of t^n at 5,7,9. Equivalently, the
+even terms of (7+2)^n+(7-2)^n-2*7^n are positive. Thus B>0, and
+
+```text
+R = p3/(p2 p1) = (T/B)(X-1)/(X-4).
+R<1  iff  (X-4)B - (X-1)T > 0.                         (1)
+```
+
+The factor (X-1)/(X-4) must be retained. Treating complete headers as
+independent factor coordinates would omit it.
+
+## Uniform tail, n>=42
+
+Put x=(7/9)^n. The terms of T below base 21 have absolute coefficient
+sum 57 and bases at most 19. Exact integer arithmetic gives
+
+```text
+57*19^42 < 21^42.
+```
+
+Since 19/21<1, for every n>=42,
+
+```text
+0 <= T <= 27^n - 6*21^n + 57*19^n < 27^n - 5*21^n.
+```
+
+The lower bound uses the cited interpretation as a count. Since
+27^n-2*21^n < B < 27^n, this yields
+
+```text
+T < B - 3*21^n,
+T/B < 1 - 3*21^n/B < 1 - 3x.
+```
+
+The last upper bound is positive at n=42, as checked by
+3*7^42<9^42, and remains positive for larger n.
+
+For n>=3, X>=16, so X-4>=3X/4. Also
+2<(14/9)^2 and 14/9>1 imply 2/2^n < (7/9)^n for n>=2. Consequently
+
+```text
+(X-1)/(X-4) = 1 + 3/(X-4) <= 1 + 4/X
+            = 1 + 2/2^n < 1 + x.
+```
+
+Every factor needed to multiply these upper bounds is nonnegative.
+Therefore, for n>=42,
+
+```text
+0 <= R < (1-3x)(1+x) = 1-2x-3x^2 < 1.
+```
+
+## Exact finite component, 3<=m<=42
+
+The verifier evaluates all 40 integers in (1), using unrestricted-precision
+integer arithmetic, and requires each to be strictly positive. It also
+computes p1,p2,p3 independently as rational expressions and requires their
+ratio to equal (1)'s ratio. The generated stdout receipt lists every m,
+its integer gap and its exact ratio. There is no floating-point tolerance.
+At m=3 the triple count is zero and the pair count is positive. At m=4,
+
+```text
+p1=9/40, p2=1/80, p3=1/1680, R=40/189.
+```
+
+This finite component and the uniform tail cover every m>=3. The extra
+86 exact comparisons at 43<=m<=128 corroborate the tail bound, without
+being a substitute for its quantified proof. The verifier also rejects
+grouped independence, a reversed leading spectral sign, an omitted
+finite-GL correction and invalid replay dimensions. QED.
+
+## Scope
+
+Only binary arithmetic, orthogonal kernel lines and uniformly weighted
+complete GL headers are covered. The pairwise inequality from #4767 and
+the three-independent-marginal inequality from #4275 do not imply this
+split inequality; those predecessor results retain their credit.
+
+This result alone does not prove negative association of the three-event
+Bernoulli vector. For example, comparison of E1 union E2 with E3 would
+require a second inequality. Larger blocks, odd fields and restricted
+header distributions remain open. A request producer, header selection,
+emission, dispatch, dirty restoration, stock, precision and a full paid
+physical caller are not supplied. No new kappa, supplier admission or
+complete multiplication theorem follows. Independent human and formal
+proof-kernel review are unclaimed.

research/corankone-triple-block-correlation/README.md

@@ -0,0 +1,104 @@
+# A binary corank-one pair is negatively correlated with a third full guard
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped counting proof with an exact computer-assisted finite
+component. For three pairwise orthogonal rank-one idempotents Ui on F2^m,
+m>=3, let Ei mean that every leading principal minor through rank m-1 of
+G(I-Ui)G^-1 is nonzero. With one uniformly weighted complete GL_m(F2) header,
+
+```text
+Pr(E1 E2 E3) < Pr(E1 E2)Pr(E3), every m>=3.
+```
+
+This answers the first bounded step in Open next question 1 of
+[#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767).
+The earlier comparison with three independent marginals does not imply
+this stronger two-block inequality. [PROOF.md](PROOF.md) cites the triple,
+pair and marginal laws, derives the new ratio, and proves its uniform
+tail for m>=43. Forty exact integer comparisons cover 3<=m<=42.
+At m=4, the ratio of the joint probability to the block product is 40/189.
+The result holds for each permutation of the split by symmetry.
+
+## Reproduction and evidence
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-triple-block-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-triple-block-correlation/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-triple-block-correlation
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-triple-block-correlation --check-source-history
+```
+
+Another CPython 3.12 interpreter can replace the local path. The direct
+verifier prints `PASS_CORANKONE_TRIPLE_BLOCK_CORRELATION` in generated JSON.
+It writes no files, uses only the standard library, and hashes all six
+package files. Its receipt enumerates each finite proof case with its
+positive integer gap and exact rational ratio. Nothing is handwritten
+as a verification receipt.
+
+The checks cover all 40 finite proof cases, all 86 additional dimensions
+43<=m<=128, the exact integer constants of the uniform tail, and seven
+controls. The controls detect grouped independence, a reversed leading
+spectral sign, omission of the finite-GL correction, and four invalid
+replay dimensions. Explicit checks remain active under optimized Python.
+The three cited m=4 probabilities are 9/40, 1/80 and 1/1680.
+
+## Scope, credit and limits
+
+The counting laws are cited mathematical inputs, not the subject of an
+independent audit. Nick Petalas's #4275 supplies the binary triple law,
+#4261 the pair law, #4227 the marginal law, and #4767 the open grouped
+question. Their exact retained-main source bytes are pinned as historical
+provenance in SOURCES.json. The verifier imports no predecessor code and
+has no external runtime inputs. The source-history check requires full
+Git history; the direct verifier runs without Git.
+
+Cinna Davis supplied the BIT request context. Source527, commdata2338 and
+Jose Manuel retain the normalizer lineage credit. Chris R / Clear1nsight
+retains the earlier #3950 counting context. The original card is
+explicitly changed from an interface-formalization task to this counting
+side question in TASK.json. Its link to the project is the density of
+headers shared by several requests. It supplies no physical caller.
+
+Only three fixed orthogonal kernel lines, binary arithmetic and complete
+uniform headers are covered. No general negative-association theorem is
+claimed. Odd fields, nonorthogonal kernels, larger blocks and restricted
+header distributions remain outside scope. Selection, emission, dispatch,
+dirty restoration, stock, precision and a complete paid physical invoice
+are unknown. No new kappa, selected-frontier change, supplier admission or
+complete multiplication theorem is claimed. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and selected cold replay
+are unrun. Both registered package modes pass locally. Ruff 0.14.0
+E/F/B/UP and the AST function-size inspection also pass.
+
+The card's historical first command, `scripts/research_baseline.py`, raises
+`KeyError: 'bit_lower'` on the changed selected certificate schema. The
+current replacement, `scripts/research_selected_baseline.py`, passes with
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` at selected kappa 60403/20000000.
+This is source-binding orientation, not a selected-construction replay.
+The historical reporter is outside this package and is unchanged.
+
+The verifier has fixed finite loops, no recursion or dynamic code
+execution, and functions below sixty lines. CPython dynamic allocation
+deviates from fixed allocation. The declared dimension bound 128,
+eight spectral terms, forty retained cases, seven controls and six source
+files of at most one MiB each bound this read-only replay. Invalid-domain
+controls exercise its bounds. Warnings are errors in both registered
+modes. A future expansion must retain or replace these resource bounds.
+
+## Open next questions
+
+1. Does the full three-event Bernoulli vector satisfy negative association?
+   Compare E1 union E2 with E3 using `2p2-p3 < p1(2p1-p2)`. Together with
+   the proved split and pair inequalities, this would cover the remaining
+   increasing-event type on two coordinates. The union comparison is
+   not proved here.
+2. Does the pair-versus-singleton inequality hold over odd finite fields?
+   Start with the cited all-field transfer at k=3 and its grouped ratio.
+   An odd-field triple closed form or another uniform bound is missing.
+3. Can a producer use a shared header with a favorable complete paid bill?
+   Pin its kernel lines and actual header domain, then price selection,
+   emission, dispatch, restoration, precision and stock. No such producer
+   or complete invoice is supplied here.

research/corankone-triple-block-correlation/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/corankone-triple-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8",
+      "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f"
+    },
+    {
+      "path": "research/corankone-pair-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548",
+      "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0"
+    },
+    {
+      "path": "research/projector-header-density/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d",
+      "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262"
+    },
+    {
+      "path": "research/corankone-pair-correlation/README.md",
+      "usage": "provenance",
+      "git_blob": "33aace0134ce06acd03aaa8da1b5be72e353eaaa",
+      "sha256": "891669d5014588da4748501c08a35dc0828541f16fa4955e2a856fc4fdb607ea"
+    }
+  ]
+}