Prove negative association of five binary full-guard indicators

research/corankone-five-negative-association/PROOF.md

@@ -0,0 +1,160 @@
+# Five-indicator negative association
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement and boundary
+
+Let m>=5. Let U_1,...,U_5 be pairwise orthogonal rank-one idempotents on
+F_2^m. Draw G uniformly from the complete group GL_m(F_2). For each i let
+E_i mean that every leading principal minor, of orders 1,...,m-1, of
+G(I-U_i)G^-1 is nonzero. Put Z_i=1_{E_i}.
+
+**Theorem.** For any disjoint nonempty subsets A,B of {1,...,5} and
+nonconstant coordinatewise increasing functions f:{0,1}^A->R and
+g:{0,1}^B->R,
+
+    Cov(f(Z_A),g(Z_B)) < 0.
+
+If either function is constant, its covariance is zero. Thus Z is negatively
+associated in the usual non-strict sense as well. These hypotheses fix the
+field, kernel geometry and probability measure. They do not cover restricted
+or conditioned header collections.
+
+This is a scoped proof with an exact finite component. The new step closes
+Open next question 1 of Krzysztof Wojt's PR5093. The moment laws and the
+four-event method are cited inputs, not new results or audited deliverables.
+
+## Counting inputs
+
+The five image lines together with their common-kernel complement give a
+simultaneous basis taking U_i to e_i e_i^T. A fixed change of basis permutes
+the whole header domain. Permuting the five distinguished lines also preserves
+its uniform measure, so the indicator law is exchangeable.
+
+Write n=m-1, X=2^(n+1), and p_k=Pr(E_1 and ... and E_k), with p_0=1.
+Use Nick Petalas's PR4227/4261/4275 character law and PR4599 four-event
+spectrum, and Ryanson Jonathan's PR4607 five-event spectrum:
+
+    p_k = N_k(n) / [2^(kn) product_(j=0)^(k-1)(X-2^j)],
+    N_k(n) = sum_z s_(k,z) z^n,                         0<=k<=5.  (1)
+
+All integer pairs (z,s_(k,z)) are retained as SPECTRA in verify.py. The first
+spectra are {1:1}, {3:1}, and {9:1,7:-2,5:1}. The five-event spectrum has 62
+nonzero terms, headed by 243^n-20*189^n+60*171^n. Its published character
+computation is a cited mathematical input. It was used once to obtain the
+literal table; this contribution does not import or replay that executable
+in its verifier, or claim independent validation of that spectrum. SOURCES.json
+pins the exact proof and source bytes on the scientific base.
+
+Use the common strictly positive denominator
+
+    Q(n)=32^n product_(j=0)^4(X-2^j),
+    A_k(n)=2^((5-k)n) N_k(n) product_(j=k)^4(X-2^j).
+
+For every n>=4, p_k=A_k/Q and A_0=Q. These identities retain every finite-GL
+factor. Replacing X-2^j by X would change the probability law.
+
+## Exhaustive increasing-event reduction
+
+Any increasing Boolean function on s bits is determined by its truth table.
+A nonconstant such function is zero at the empty subset and one at the full
+subset. Enumerate every integer truth table from 1 to 2^(2^s)-2, keeping it
+exactly when
+
+    F(x) <= F(x union {j}) for every x and every bit j.          (2)
+
+For s=1,2,3,4 the resulting list lengths are 1,4,18,166. This is an exhaustive
+finite loop over at most 65,534 candidates, not a symmetry assumption.
+
+Subset Mobius inversion gives a unique multilinear expansion
+
+    F(z)=sum_I a_I product_(i in I) z_i.
+
+Let a_k=sum_(|I|=k) a_I. Then E[F]=sum_k a_k p_k. For a second increasing
+event H on disjoint coordinates, with grouped coefficients b_l, exchangeability
+and disjointness give
+
+    E[F H]=sum_(k,l) a_k b_l p_(k+l).
+
+The positive covariance gap therefore is
+
+    Delta(F,H)=E[F]E[H]-E[F H]=P_(a,b)(n)/Q(n)^2,
+    P_(a,b)=(sum_k a_k A_k)(sum_l b_l A_l)
+             - Q sum_(k,l) a_k b_l A_(k+l).                    (3)
+
+Up to exchanging the two supports and permuting coordinates, all possible
+support sizes are
+
+    (1,1), (1,2), (1,3), (1,4), (2,2), (2,3).
+
+The verifier visits all 277 labelled pairs on these canonical supports,
+including functions which ignore an input. It reconstructs each truth table
+from its individual Mobius coefficients before grouping by degree. Expanding
+(3) and collecting identical power sums gives 37 distinct nonzero polynomials.
+The old support types give 11 distinct gaps. The new 4+1 and 3+2 types supply
+the other 26. No conjunction-only shortcut is used.
+
+## Exact signs for every dimension
+
+For each of the 37 polynomials, write
+
+    P(n)=c B^n + sum_(z<B) c_z z^n,
+    b=max{z<B:c_z!=0},   C=sum_(z<B)|c_z|.
+
+All bases here are positive integers. The verifier regenerates each polynomial
+by integer addition and multiplication, and checks that the literal TAILS row
+records exactly B,c,b,C,N, with B>b>0 and c,C>0. It checks
+
+    c B^N > C b^N.                                            (4)
+
+For every n>=N, since b/B<1,
+
+    P(n) >= c B^n-C b^n > 0.
+
+For each remaining integer 4<=n<N it checks P(n)>0 using exact integers,
+and separately compares P(n)/Q(n)^2 with direct rational evaluation of (3)
+using (1). Thus the finite prefix and the tail cover every n>=4, with no
+unchecked interval. N is at most 179, so every gap has an analytic tail from
+m=180 onward. Individual gaps often have much earlier tails.
+
+The complete 37-row certificate is the TAILS tuple in verify.py. Each row
+contains integers only and is regenerated and checked, rather than trusted
+as an execution receipt. The verifier emits the corresponding support sizes,
+coefficient vectors, polynomial lengths and tail data for inspection.
+
+These exact finite checks and the elementary tail inequality prove
+Delta(F,H)>0 for every nonconstant increasing Boolean pair on disjoint
+nonempty supports.
+
+## Increasing real functions
+
+On a finite Boolean cube, an increasing real function f can be written as its
+minimum plus a finite nonnegative linear combination of its nonconstant
+increasing superlevel-set indicators. Explicitly, for distinct values
+v_0<...<v_r of f,
+
+    f=v_0+sum_(j=1)^r (v_j-v_(j-1)) 1_{f>=v_j}.
+
+Every coefficient is positive. The same decomposition holds for g. Covariance
+is bilinear, constants contribute zero, and every indicator pair has strictly
+negative covariance by the preceding section. If f and g are nonconstant,
+there is at least one summand in each decomposition, so their covariance is
+strictly negative. This proves the theorem.
+
+## Verification boundary
+
+The standard-library verifier also evaluates all 277 truth-table pairs directly
+on the 32 atoms at m=5,6,8,16, using inclusion-exclusion from (1). This checks
+the grouped-coefficient and disjoint-support calculation by a separate path.
+It verifies every atom is nonnegative and the masses sum to one. These are
+bounded corroborations, not a separate complete-GL enumeration or an audit of
+the moment law.
+
+Invalid domain, sign, tail-mass and cutoff controls remain active under
+optimized Python. A two-point perfectly correlated distribution is detected as
+having positive covariance, so exchangeability alone cannot replace (1).
+The claim does not supply a physical header sampler, producer, consumer,
+restoration protocol, stock/tape budget or supplier admission. It gives no
+odd-field, six-indicator or nonorthogonal-kernel theorem. Independent human
+and formal proof-kernel review are unclaimed. No multiplication exponent or
+selected-frontier change follows.

research/corankone-five-negative-association/README.md

@@ -0,0 +1,122 @@
+# Five binary full-guard indicators are negatively associated
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped proof with an exact finite component. No new kappa.**
+For five pairwise orthogonal rank-one idempotents U_i on F_2^m, draw a
+complete uniform header G in GL_m(F_2), with m>=5. Let Z_i indicate that
+all leading principal minors of G(I-U_i)G^-1 through order m-1 are nonzero.
+Then any two nonconstant increasing real functions of disjoint nonempty
+subsets of the five indicators have strictly negative covariance.
+
+This settles Open next question 1 of Krzysztof Wojt's
+[PR #5093](https://github.com/CrocSwap/integer-mult-bounds/pull/5093).
+That predecessor proves the four-indicator theorem. The new comparisons
+cover the 4+1 and 3+2 support splits; the existing fivefold-intersection
+inequality alone does not settle them. The statement covers every integer
+m>=5, rather than extrapolating a finite dimensional sample.
+
+## Proof and evidence
+
+[PROOF.md](PROOF.md) gives the argument. Subset Mobius inversion and
+exchangeability reduce all 277 labelled increasing-event pairs to 37
+covariance-gap power sums. Eleven correspond to the earlier support types;
+26 additional types complete the five-indicator case. Every gap has a
+positive exact finite prefix and a strict leading-term tail bound.
+Superlevel-set decomposition then gives the assertion for real functions.
+
+The self-contained standard-library verifier checks:
+
+- All 1,4,18,166 nonconstant monotone Boolean truth tables on one through
+  four inputs, including reconstruction of every truth value.
+- All 37 expanded gap polynomials, 4,498 exact finite-prefix comparisons,
+  37 uniform tail certificates and 111 additional tail identity probes.
+  The largest tail begins at n=m-1=179, hence m=180.
+- All 277 labelled pairs by direct 32-atom truth-table evaluation at
+  m=5,6,8,16, giving 1,108 independent-path covariance comparisons.
+- Ten domain, sign, cutoff, tail-mass, finite-denominator and distribution
+  controls. Checks use explicit exceptions and remain active with -O.
+
+Every run prints PASS_CORANKONE_FIVE_NEGATIVE_ASSOCIATION and a generated
+receipt bound to all six package-file hashes. It writes no files and needs
+neither Git nor network. The moment laws and spectra are cited inputs;
+no predecessor executable is imported or independently audited here.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/corankone-five-negative-association/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/corankone-five-negative-association/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-five-negative-association
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-five-negative-association --check-source-history
+```
+
+Use another CPython 3.12 path on other machines. The publication preflight
+requires a committed package and full history. Both registered scientific
+commands use warning-strict isolated Python and have a 60-second cap.
+Local command times and hosted CI status are recorded in the PR body.
+
+## Scope and provenance
+
+Scientific base is canonical main de5ec2e7a6074068452f45b1a191b5c72832df4a,
+priority revision 8. TASK.json records the changed formal-interface-lemma
+scope: an original dependence side result, without a proof-assistant claim.
+SOURCES.json pins predecessor proof texts and code as historical provenance;
+none is a runtime import. The selected-baseline source-binding orientation
+passes after materializing its sparse inputs. It is not a scientific replay
+or a premise of this theorem.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213528)
+records the question. Live open/account PR lists, latest handoffs, active
+Discussions, distinctive main-tree README searches and merged-PR searches
+were checked before claiming. The cached overlap report had incomplete sparse
+local-note coverage. Unpublished work and arbitrary historical diffs are not
+covered, and global literature priority is unclaimed. Submission freshness
+and related open work are recorded in the PR.
+
+The theorem fixes binary orthogonal kernels and the whole uniform header
+measure. It gives no six-indicator, odd-field, conditioned-header or
+nonorthogonal-kernel result. Physical header generation, selection, emission,
+dispatch, dirty restoration, stock, precision and a paid consumer remain
+unpriced. No supplier admission, multiplication theorem or selected-frontier
+change is claimed. Independent human and formal proof-kernel review are
+unclaimed. No Lean, Docker, native build or selected scientific cold replay
+was run.
+
+The verifier has no recursion or shared mutable state. Functions are under
+60 physical lines. Truth-table candidates are bounded by 65,534; moment
+fixtures are bounded by m<=359 in the actual run and an enforced m<=513
+entry contract. The largest collected polynomial has 512 terms; every
+multiplication enforces a 4,096-base capacity bound. Exact Python integers,
+Fractions and bounded containers use managed dynamic allocation. This is a
+documented deviation from fixed allocation, with fixed finite data domains;
+there is no constant-bit-space claim. The controls use eight explicitly
+listed local callbacks, the only indirect test-call targets. Warning-strict
+normal and optimized execution supplies the available Python diagnostics.
+
+## Open next questions
+
+1. Does negative association persist for six orthogonal binary full-guard
+   indicators? This would cover larger shared-header groups. First obtain
+   a justified six-event moment input, then classify the new 5+1, 4+2 and
+   3+3 increasing-event comparisons. The six-event spectrum and new mixed
+   inequalities are absent here; no larger census is reserved.
+2. Can a concrete paid caller realize and use the complete uniform-header
+   premise? Start with its actual request family and sampling rule, then
+   price selection, emission, dispatch and restoration. The missing physical
+   consumer and complete bill prevent treating dependence as a kappa gain.
+
+## Credit
+
+Krzysztof Wojt #5093 supplies the four-event theorem, explicit five-event
+question, and the power-sum/Mobius verification method adapted here.
+lee-phys #5073 supplies the three-event theorem and earlier question.
+Ryanson Jonathan #4607 supplies the cited five-event signed spectrum.
+Nick Petalas #4227/#4261/#4275/#4599 supplies the marginal, joint character
+laws and four-event spectrum. Cinna Davis's BIT request context, source527,
+commdata2338, Jose Manuel's normalizer/closure lineage and Chris R /
+Clear1nsight's counting context retain the attribution in those sources.
+The new contribution is the 26 additional gap types and their complete
+finite-prefix/tail proof, giving five-indicator negative association.

research/corankone-five-negative-association/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/corankone-four-negative-association/README.md",
+      "usage": "provenance",
+      "git_blob": "6116dea3ec6cf04bfec67c6f18a48e2a78ce0377",
+      "sha256": "a3e9fe547ceb22ab158ec4bceaada5f4cf9287269352c1dc4a6380d4c18a37bd"
+    },
+    {
+      "path": "research/corankone-four-negative-association/verify.py",
+      "usage": "provenance",
+      "git_blob": "58cef3248b4852bb2b4f67ff1400860976e92ee3",
+      "sha256": "01d54f9ecdf56a4e01e5cfa2bd59195835c40f575b7880abe62b63023972a7a8"
+    },
+    {
+      "path": "research/corankone-triple-header-law/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8",
+      "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f"
+    },
+    {
+      "path": "research/corankone-triple-negative-association/README.md",
+      "usage": "provenance",
+      "git_blob": "ba63617e44742e116a17e0321dfd0cbc7c358e50",
+      "sha256": "8e510ddd30971e03210039b6777675f657bfb290710848b72ade9e1d55299d31"
+    },
+    {
+      "path": "research/five-event-guard-correlation/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "a84e5696ab202dfef0296e02d9cf26e85923eb3c",
+      "sha256": "a46e1d5ede453b996f545f29fa8ed50f9fc05b829192ee81d41ff0424301fc0a"
+    },
+    {
+      "path": "research/five-event-guard-correlation/verify.py",
+      "usage": "provenance",
+      "git_blob": "adff8b585d018929dba12b41fe7041553cb0d403",
+      "sha256": "a3e16b49286ef9809c4305012155c4030242db7be4a1725b7035a4231120c7bc"
+    }
+  ]
+}