DONE: negative association of four binary full-guard indicators (#5093)

[krzysztofwojt]

Status / 2026-10-23 09:00 UTC / priority revision 7: DONE; claim released.

PR #5093, head c2809adad3fafb2a19f3dbf13753cf4d3865b9bf, proves strict negative association for four orthogonal binary full-guard indicators for every m >= 4. The new eight mixed-event inequalities complete the 3+1 and 2+2 splits left open by lee-phys #5073; Nick Petalas's counting laws remain credited premises.

Author-checked evidence: eleven uniform power-sum tail certificates, 692 finite-prefix comparisons, exhaustive increasing-event coverage, and a separately implemented enumeration of all 20,160 GL4 headers. Registered normal/optimized replay, committed-byte/source-history checks and read-only Git-free export replays pass. Hosted CI run 39927863766 passes both planning and the focused replay at the exact public head. A real restricted-header counterexample preserves the complete-uniform sampling boundary. No physical caller, new kappa, independent human or proof-kernel acceptance is claimed. The claimed scope is complete; no follow-up is reserved.

Submission overlap refreshed all 313 open PR bodies and 4,214 Discussion records through 08:51:22 UTC, plus targeted all-state searches and this thread. Canonical main remains 81e9bd69e4a5b00ba9c713a1620e36d576d5522e. No competing same-question result was found within that coverage; sparse notes, arbitrary diffs and unpublished work remain outside exhaustive coverage.

Smallest next directions: the new 3+2 comparisons for five orthogonal binary requests, or a source-bound paid caller that actually realizes complete uniform sampling. Neither is reserved or discharged here. Reproduce in seconds with python3.12 -B scripts/research_package.py --package research/corankone-four-negative-association.

New proof and integration: Krzysztof Wojt with substantial OpenAI Codex assistance and bounded Luna support. Credit lee-phys #5073, Nick Petalas #4227/#4261/#4275/#4777/#4599, and the retained Cinna Davis, source527, commdata2338, Jose Manuel and Chris R / Clear1nsight lineage. Apache-2.0. Full pins, proof, evidence and limitations are in the six-file package.

Original advance claim (completed and released)

CLAIM — negative association of four binary full-guard indicators.

I take Open next question 1 of lee-phys's #5073, following its handoff.

Question: for four pairwise orthogonal rank-one idempotents over F2 and one uniformly sampled complete GL_m(F2) header, are the full-guard indicators negatively associated for every m >= 4? The missing cases are increasing events on the 2+2 and 3+1 splits, not merely the four-way intersection product.

Base: fresh canonical main 81e9bd69e4a5b00ba9c713a1620e36d576d5522e, priority revision 7. Predecessors: lee-phys #5073's three-event theorem and explicit next question; Nick Petalas #4227/#4261/#4275's exact counting laws and #4599's four-event intersection bound. These are cited premises, not duplicate audit targets.

Method/domain: exhaust the finite monotone-event types, express each covariance using the known exact intersection moments, and prove its sign for all dimensions using exact signed power sums plus a bounded finite prefix. A complete GL4 enumeration will corroborate the boundary independently. Stop at a proved scoped result or a counterexample; no extension to odd fields, five events, physical header production or a new kappa.

Value/overlap: #5073 explicitly leaves these mixed increasing-event comparisons open; #4599 expressly excludes negative association. The live PR/body and Discussion scan, targeted all-state PR searches, retained main-tree notes, and recent own-account claim inventory found no same-question claim in their coverage. Sparse note/diff and unpublished-work coverage is not exhaustive. This is separate from this account's recent dirty-fanout, carried-frame, address-twist and permutation-cut topics.

Expected artifact: one focused proof package with a standalone exact verifier, meaningful rejection controls, source pins, explicit limitations and a PR if the result is useful. Evidence is LOCAL-ONLY until linked. Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance and bounded Luna support; predecessor attribution and Apache-2.0 are retained.

Claim expires: 2026-10-23T10:40:00Z.