From c2809adad3fafb2a19f3dbf13753cf4d3865b9bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 10:49:39 +0200 Subject: [PATCH] Prove negative association of four binary full-guard indicators --- .../README.md | 264 ++++++++++++++ .../SOURCES.json | 48 +++ .../TASK.json | 126 +++++++ .../VERIFY.json | 34 ++ .../boundary.py | 330 ++++++++++++++++++ .../verify.py | 269 ++++++++++++++ 6 files changed, 1071 insertions(+) create mode 100644 research/corankone-four-negative-association/README.md create mode 100644 research/corankone-four-negative-association/SOURCES.json create mode 100644 research/corankone-four-negative-association/TASK.json create mode 100644 research/corankone-four-negative-association/VERIFY.json create mode 100644 research/corankone-four-negative-association/boundary.py create mode 100644 research/corankone-four-negative-association/verify.py diff --git a/research/corankone-four-negative-association/README.md b/research/corankone-four-negative-association/README.md new file mode 100644 index 0000000000..6116dea3ec --- /dev/null +++ b/research/corankone-four-negative-association/README.md @@ -0,0 +1,264 @@ +# Negative association of four binary full-guard indicators + +**A dimension-uniform proof with an exact finite component. No new kappa.** + +For four pairwise orthogonal rank-one idempotents over `F_2`, the full-guard +indicators under one complete uniformly sampled `GL_m(F_2)` header are +negatively associated for every `m >= 4`. The covariance is strictly negative +for any two nonconstant increasing real functions of disjoint, nonempty +sets of these four indicators. + +This answers Open next question 1 of **lee-phys's #5073**, whose theorem covers +three indicators. **Nick Petalas's #4599** proves the four-way intersection +bound, explicitly leaving general negative association outside its scope. +The new work proves the eight additional mixed-event inequalities required +by the `3+1` and `2+2` splits. It cites the known counting laws; it does not +claim a new law or another independent audit of the predecessor proofs. + +## 1. Domain and counting inputs + +Let `U_1,...,U_4` be rank-one idempotents on `F_2^m` with `U_i U_j=0` for +`i != j`, and put `P_i=I-U_i`. Draw `G` uniformly from the whole group +`GL_m(F_2)`. Event `E_i` says that all leading principal minors of +`G P_i G^-1`, of orders `1,...,m-1`, are nonzero. Write `Z_i=1_Ei`. + +The four image lines and their common-kernel complement give a simultaneous +basis in which `U_i=e_i e_i^T`. A fixed right change of basis permutes the +complete header domain, as does a permutation of the four distinguished +lines. Thus the law of `Z` is exchangeable. This also proves that checking +the standard diagonal idempotents loses no admissible quadruple. + +Put `n=m-1`, `X=2^(n+1)`, and let `p_k` be the probability that any specified +`k` of the events occur (`p_0=1`). The exact laws in Petalas's +#4227/#4261/#4275 give, for `0 <= k <= 4`, + +```text +p_k = N_k(n) / [2^(kn) product_(j=0)^(k-1) (X-2^j)], +N_0(n)=1. +``` + +For `k>=1`, Theorem 2 of the retained +[character-law proof](../corankone-triple-header-law/PROOF.md) defines + +```text +N_k(n) = sum_c (-1)^|c| Z_k(c)^n, +Z_k(c) = sum_(sigma in {0,1,2}^k) + (-1)^(sum_(i,j: sigma_i=1, sigma_j=2) c_ij), +``` + +where `c` ranges over zero-diagonal binary `k` by `k` matrices. +The factors `2^(k(k-1))` from Fourier inversion and +`2^(k(m-k))` from the completion denominator combine to `2^(kn)`. +In particular `N_1=3^n` and `N_2=9^n-2*7^n+5^n`. +The collected spectra for `k=3,4` are the cited #4275 corollary and +[#4599 Section 2](../corankone-four-correlation/PROOF.md). +`SPECTRA` in [verify.py](verify.py) records those exact integer data. +All proof sources are pinned as historical provenance in [SOURCES.json](SOURCES.json). + +The complete finite-GL denominator is retained throughout. No asymptotic +replacement of the header distribution is used. + +## 2. Exhausting the increasing-event types + +For a disjoint pair of increasing events `F,H`, define the positive gap + +```text +Delta(F,H) = Pr(F) Pr(H) - Pr(F and H) = -Cov(1_F,1_H). +``` + +Up to exchanging the two supports, their sizes are `1+1`, `2+1`, `3+1`, +or `2+2`. The nonconstant increasing Boolean functions number `1,4,18` +on one, two and three bits. On three bits their complete list, up to input +permutation, is + +| Type | Number of labelled functions | Expectation | +|---|---:|---| +| `x` | 3 | `p1` | +| `AND2` | 3 | `p2` | +| `OR2` | 3 | `2p1-p2` | +| `AND3` | 1 | `p3` | +| `x AND (y OR z)` | 3 | `2p2-p3` | +| `MAJ3` (at least two) | 1 | `3p2-2p3` | +| `x OR (y AND z)` | 3 | `p1+p2-p3` | +| `OR3` | 1 | `3p1-3p2+p3` | + +This list can also be obtained by listing the nonempty antichains of nonempty +subsets of a three-element set; their minimal true inputs determine each +increasing event. The verifier independently enumerates all truth tables, +checks monotonicity, and applies subset Mobius inversion. It does not assume +that checking conjunctions suffices. + +If the two expectations are `sum_i a_i p_i` and `sum_j b_j p_j`, disjointness +and multilinearity give + +```text +Delta = (sum_i a_i p_i)(sum_j b_j p_j) - sum_(i,j) a_i b_j p_(i+j). (1) +``` + +The 39 labelled event pairs for canonical splits reduce to exactly these +11 gap polynomials. Letters in the two columns always use disjoint inputs. + +| Row | First event | Second | Gap | +|---|---|---|---| +| 1 | `x` | `x` | `p1^2-p2` | +| 2 | `AND2` | `x` | `p1*p2-p3` | +| 3 | `OR2` | `x` | `2p1^2-p1*p2-2p2+p3` | +| 4 | `AND3` | `x` | `p1*p3-p4` | +| 5 | `x AND (y OR z)` | `x` | `2p1*p2-p1*p3-2p3+p4` | +| 6 | `MAJ3` | `x` | `3p1*p2-2p1*p3-3p3+2p4` | +| 7 | `x OR (y AND z)` | `x` | `p1^2+p1*p2-p1*p3-p2-p3+p4` | +| 8 | `OR3` | `x` | `3p1^2-3p1*p2+p1*p3-3p2+3p3-p4` | +| 9 | `AND2` | `AND2` | `p2^2-p4` | +| 10 | `AND2` | `OR2` | `2p1*p2-p2^2-2p3+p4` | +| 11 | `OR2` | `OR2` | `4p1^2-4p1*p2+p2^2-4p2+4p3-p4` | + +Rows 1-3 are already covered by #5073. Rows 4-11 are the new inequalities. +Including all eleven in one small certificate checks completeness of the +four-variable argument without making predecessor replay the contribution. + +## 3. Exact certificates for every dimension + +Use the common positive denominator + +```text +Q(n) = 16^n product_(j=0)^3 (2^(n+1)-2^j), +A_k(n) = 2^((4-k)n) N_k(n) product_(j=k)^3 (2^(n+1)-2^j). +``` + +For `n>=3`, `Q>0`, `A_0=Q`, and `p_k=A_k/Q`. Substitution in (1) gives + +```text +S(n) = Q(n)^2 Delta + = (sum_i a_i A_i(n))(sum_j b_j A_j(n)) + - Q(n) sum_(i,j) a_i b_j A_(i+j)(n). (2) +``` + +Every expression here is a finite signed power sum `sum_b c_b b^n` with +positive integer bases. It is enough to store a dictionary `b -> c_b`: +addition adds coefficients and multiplication sends `(b,d)` to `b*d`. +Each factor `2^(n+1)-2^j` is exactly the dictionary `{2:2, 1:-2^j}`. +Consequently (2) specifies the entire expansion by integer operations, +including all cancellations; no fitting from numerical samples occurs. + +**Tail lemma.** Let `B` be the largest surviving base with coefficient `c>0`, +let `b C b^N`, then for every integer `n>=N`, + +```text +S(n) >= c B^n - C b^n > 0. +``` + +Indeed, the ratio `(b/B)^n` decreases. This is a uniform proof after one +exact integer comparison, not extrapolation from finitely many dimensions. + +Expanding (2) gives the following certificate. The verifier recomputes each +tuple and checks its strict tail inequality. For each row it separately +checks `S(n)>0` for every `3<=n=4`. + +Finally, any increasing real function on a finite cube is a constant plus +a nonnegative linear combination of increasing-event indicators: use its +successive nontrivial superlevel sets. For a nonconstant function at least +one coefficient is positive. Bilinearity of covariance and the strict event +inequalities therefore give strict negativity for two nonconstant functions +on disjoint nonempty supports. Constants and empty supports give zero. QED. + +## 4. Corroboration and a necessary sampling hypothesis + +The finite proof component is author-checked, not proof-kernel verified. +[verify.py](verify.py) also checks all 39 labelled cases directly from the +16-atom law for `4<=m<=104`: **3,939 truth-table comparisons**, plus 33 +tail probes and eight explicit rejection/domain controls. The truth-table +and rational evaluations use the cited moments, so they are separately +represented calculations, not independent validations of those counting laws. + +[boundary.py](boundary.py) is a separately implemented calculation with no +spectra or moment formulas. It enumerates all **20,160** invertible `4x4` +binary matrices, explicitly forms each `G P_i G^-1`, and computes the three +principal determinants. Each specified atom of weight `0,1,2,3,4` occurs +`3480,3816,228,12,0` times respectively. The intersection counts for each +specified subset of sizes `1,2,3,4` are `4536,252,12,0`. +It checks all support placements: **174** nonconstant increasing-event pairs +have strictly negative covariance; **444** constant-involved pairs have zero. + +The same checker restricts the header to the **1,344** matrices with first row +`[0,1,1,1]`. The pair `E_1` and `E_2 AND E_3` then has counts `432,4` and +joint count `2`, giving positive covariance +`(1344*2-432*4)/1344^2 = 960/1344^2`. +Thus arbitrary restricted header collections are genuinely outside the theorem. +A further control replaces `G^-1` by `G`; it changes both an explicit atom +and the full law. These controls remain active under optimized Python. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/corankone-four-negative-association --check-only +python3.12 -B scripts/research_package.py --package research/corankone-four-negative-association +``` + +The registered replay runs both files in normal and optimized isolated Python. +For a Git-free package directory, run `python3.12 -I -B verify.py` and +`python3.12 -I -B boundary.py`, and repeat with `-O`. Both are read-only. +The proof checker prints `PASS_CORANKONE_FOUR_NEGATIVE_ASSOCIATION`; the +boundary checker prints `PASS_GL4_FOUR_GUARD_BOUNDARY`. + +## Scope, provenance and credit + +Scientific base: fresh canonical main `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`, +priority revision 7. [Discussion #5086](https://github.com/CrocSwap/integer-mult-bounds/discussions/5086) +is the canonical claim/result. [TASK.json](TASK.json) records a changed scope +of `formal-interface-lemma`: a counting side result, with no Lean claim. + +Credit **lee-phys** for the three-event theorem and explicit open question in +#5073, head `1aace155467e4a560bdb5b28f4f0fdc60a45c29d`; **Nick Petalas** for +#4227/#4261/#4275, the grouped comparison #4777, and #4599 (head +`19ca650c67ad2722790dc60c0bfd12989479b06a`). Retain Cinna Davis's BIT request +context, source527, commdata2338 and Jose Manuel's normalizer/closure lineage, +and Chris R / Clear1nsight's earlier counting context. New proof and integration: +**Krzysztof Wojt with substantial OpenAI Codex assistance**; bounded Luna agents +independently enumerated event types and constructed the literal GL4 check, +which the primary agent inspected and reran. No independent human review or +formal proof-kernel acceptance is claimed. Apache-2.0. + +This is not a physical supplier or a multiplication-exponent improvement. +The result covers exactly four orthogonal binary kernel lines and a complete +uniform header. Five or more events, odd fields, nonorthogonal kernels and +conditioned/restricted header laws are not covered. Header production, selection, +emission, dispatch, dirty restoration, stock and whole-caller costs remain +unpriced; unknown costs are not zero. No selected-frontier change, selected +scientific cold replay, native/Lean/Docker build or all-size admission is claimed. +The selected-baseline sparse-input diagnostic reported 503 omitted files; +the full selected source-binding orientation was not run in this scoped checkout. + +## Open next questions + +1. Does negative association persist for five orthogonal binary kernel lines? + This would control larger shared-header groupings. First derive the `3+2` + increasing-event comparisons from the existing general character law and + test their signs; the four-event table and its tail bounds do not settle + them. No additional census or follow-up is reserved here. +2. Can a concrete paid caller realize the complete uniform-header premise and + use this dependence bound? Pin its sampling/conditioning rule first, since + the fixed-row counterexample excludes a free transfer to restricted headers. + Then price selection, emission, dispatch and restoration against an actual + consumer. That physical construction and its complete bill are absent. diff --git a/research/corankone-four-negative-association/SOURCES.json b/research/corankone-four-negative-association/SOURCES.json new file mode 100644 index 0000000000..56ccae92b3 --- /dev/null +++ b/research/corankone-four-negative-association/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "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-four-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "6309eb879c93a3270a0912b40275c5678185b2a8", + "sha256": "c8966a14b9151ce0b94ee0c512dc81ba8cd537f01bd0c8fd6c1f27c97f275951" + }, + { + "path": "research/corankone-pair-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548", + "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0" + }, + { + "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/projector-header-density/PROOF.md", + "usage": "provenance", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + } + ] +} diff --git a/research/corankone-four-negative-association/TASK.json b/research/corankone-four-negative-association/TASK.json new file mode 100644 index 0000000000..b6405bb42b --- /dev/null +++ b/research/corankone-four-negative-association/TASK.json @@ -0,0 +1,126 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove strict negative association for four orthogonal binary rank-one-kernel full-guard indicators under one complete uniform GL_m(F2) header for every m >= 4, closing PR5073 Open next question 1 via the missing 3+1 and 2+2 increasing-event inequalities.", + "scope_change_reason": "Handoff-first selection of lee-phys's explicit open question in PR5073. This is a dimension-uniform counting side result, not formalization of the catalogue's compact-switch caller or a repeat of the three-event theorem/four-way intersection bound.", + "bottleneck_link": "Shared-header pricing needs joint laws for grouped acceptance events. The result controls all increasing groupings of four orthogonal binary requests; it does not construct or price a physical shared-header caller.", + "budget_minutes": 240, + "stop_rule": "Stop after proving/refuting the eight missing mixed-event inequalities, proving complete monotone-event coverage, and corroborating the GL4 boundary. No extension to five events, odd fields or physical supplier construction in this contribution.", + "outcome": "completed", + "evidence": "Written power-sum tail lemma; eleven exactly regenerated dominance certificates; 692 finite-prefix comparisons; all 39 labelled monotone-event pairs across m=4..104 (3939 truth-table comparisons); 33 tail probes; 8 rejection/domain controls. A separately implemented literal GL4 enumeration checks all 20160 headers, 16 atoms, 174 strict nonconstant event pairs, 444 constant-involved pairs, and actual restricted-header/forward-only controls. Normal/optimized registered replay and publication checks are recorded in the PR.", + "author": "Krzysztof Wojt", + "ai_assistance": "Krzysztof Wojt with substantial OpenAI Codex assistance. Bounded Luna agents inventoried recent claims, independently classified monotone events and implemented the literal GL4 boundary check; the primary agent inspected and reran supporting work. No independent human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Does negative association hold for five orthogonal binary kernel lines?", + "why_it_matters": "This would control larger shared-header groupings beyond the four-request theorem.", + "first_step": "Derive the 3+2 increasing-event comparisons from the known general character law and test their signs before seeking a uniform proof.", + "blocked_by": "The present finite event list and power-sum certificates only use moments through four. No follow-up is reserved." + }, + { + "question": "Can a paid physical caller realize the complete uniform-header premise and use the dependence bound?", + "why_it_matters": "The actual restricted-header control has positive covariance, so arbitrary conditioning invalidates automatic use of the theorem.", + "first_step": "Pin an actual caller and its sampling/conditioning rule; then charge header selection, emission, dispatch, dirty restoration and stock against its consumer.", + "blocked_by": "No physical producer, consumer or complete cost bill is supplied; unknown costs are not zero." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5086", + "handoff_taken": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141140", + "checked_main": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e", + "preclaim_checked_utc": "2026-10-23T08:36:33Z", + "overlap_coverage": "Complete cached pagination of 307 open PR bodies and 4207 Discussion records, refreshed live open PRs/handoffs/newest roots, own-account claims over six hours, targeted all-state PR searches and main-tree note searches. No same-question claim found. Sparse local notes, arbitrary diffs and unpublished work remain non-exhaustive.", + "excluded_own_topics": [ + "PR3281", + "PR3261", + "PR3301", + "PR3334", + "PR5003/address twist", + "PR5024/intact-region frames", + "PR5045/two-row dirty fanout", + "PR5063/permutation cuts", + "all other recent krzysztofwojt claims" + ], + "parallel_round_check": "No additional krzysztofwojt claim near 08:10 was visible in the complete snapshot or fresh newest-root/comment pass; every identified recent own-account topic was excluded." + }, + "orientation": { + "selected_record": "certificates/selected-result.json", + "selected_kappa": "60403/20000000", + "sparse_baseline_diagnostic": "SPARSE_SELECTED_INPUTS_ABSENT: 503 files. Full selected source-binding orientation and scientific cold replay not run; selected review and assumptions were read.", + "scientific_base_preserved": true + } +} diff --git a/research/corankone-four-negative-association/VERIFY.json b/research/corankone-four-negative-association/VERIFY.json new file mode 100644 index 0000000000..58d75feefe --- /dev/null +++ b/research/corankone-four-negative-association/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All eleven gap expansions, exact finite prefixes, uniform tail certificates, exhaustive monotone-event coverage and rejection controls." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "The same proof checks remain active with Python assertions disabled." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/boundary.py"], + "timeout_seconds": 120, + "checks": "Independent literal enumeration of complete GL4, all atoms and all monotone event placements; actual restricted-header and incorrect-inverse controls." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/boundary.py"], + "timeout_seconds": 120, + "checks": "The independent GL4 boundary and controls remain active under optimized Python." + } + ] +} diff --git a/research/corankone-four-negative-association/boundary.py b/research/corankone-four-negative-association/boundary.py new file mode 100644 index 0000000000..6fc4897fe9 --- /dev/null +++ b/research/corankone-four-negative-association/boundary.py @@ -0,0 +1,330 @@ +#!/usr/bin/env python3 +# Copyright 2026 Krzysztof Wojt. +# Created with substantial assistance from OpenAI Codex and Luna. +# SPDX-License-Identifier: Apache-2.0 + +"""Independent exact enumeration of a four-indicator GL_4(F_2) law. + +Each 4x4 matrix is stored as four row bitmasks. The four indicators are +X_i = 1 exactly when all three leading principal minors of orders 1, 2, and 3 +of G (I - e_i e_i^T) G^{-1} are nonzero. All arithmetic is over F_2. + +This is a bounded finite check for this specified distribution. It does not +establish a claim in other dimensions or over other fields. +""" + +from collections import Counter +from itertools import combinations, product + + +N = 4 +FIELD_MATRIX_BITS = 1 << (N * N) +IDENTITY = tuple(1 << r for r in range(N)) +SPLIT_SIZES = ((1, 1), (1, 2), (1, 3), (2, 2)) + + +def require(condition, message): + """A check that remains active when Python is run with -O.""" + if not condition: + raise RuntimeError(message) + + +def columns(matrix): + return tuple( + sum(((matrix[r] >> c) & 1) << r for r in range(N)) + for c in range(N) + ) + + +def matmul(left, right): + right_columns = columns(right) + return tuple( + sum(((row & col).bit_count() & 1) << c for c, col in enumerate(right_columns)) + for row in left + ) + + +def inverse(matrix): + """Return the literal GF(2) inverse, or None if matrix is singular.""" + augmented = [matrix[r] | (1 << (N + r)) for r in range(N)] + for c in range(N): + pivot = next((r for r in range(c, N) if (augmented[r] >> c) & 1), None) + if pivot is None: + return None + augmented[c], augmented[pivot] = augmented[pivot], augmented[c] + for r in range(N): + if r != c and ((augmented[r] >> c) & 1): + augmented[r] ^= augmented[c] + result = tuple((augmented[r] >> N) & ((1 << N) - 1) for r in range(N)) + require(matmul(matrix, result) == IDENTITY, "computed right inverse failed") + require(matmul(result, matrix) == IDENTITY, "computed left inverse failed") + return result + + +def leading_minor_nonzero(matrix, order): + """Compute the determinant of the top-left order x order block over F_2.""" + block = [matrix[r] & ((1 << order) - 1) for r in range(order)] + rank = 0 + for c in range(order): + pivot = next((r for r in range(rank, order) if (block[r] >> c) & 1), None) + if pivot is None: + return False + block[rank], block[pivot] = block[pivot], block[rank] + for r in range(rank + 1, order): + if (block[r] >> c) & 1: + block[r] ^= block[rank] + rank += 1 + return True + + +PROJECTORS = tuple( + tuple((1 << r) ^ ((1 << r) if r == i else 0) for r in range(N)) + for i in range(N) +) + + +def indicators_for(matrix, inv, use_inverse=True): + values = [] + for projector in PROJECTORS: + if use_inverse: + conjugate = matmul(matmul(matrix, projector), inv) + else: + # Deliberately incorrect control: use G on both sides. + conjugate = matmul(matmul(matrix, projector), matrix) + minors = tuple(leading_minor_nonzero(conjugate, k) for k in (1, 2, 3)) + values.append(int(all(minors))) + return tuple(values) + + +def all_gl4(): + """Yield every invertible 4x4 GF(2) matrix exactly once.""" + for encoding in range(FIELD_MATRIX_BITS): + matrix = tuple((encoding >> (N * r)) & ((1 << N) - 1) for r in range(N)) + inv = inverse(matrix) + if inv is not None: + yield matrix, inv + + +def atom_label(bits): + return "".join(str(bit) for bit in bits) + + +def monotone_event_masks(width): + """Enumerate event truth tables of all increasing Boolean functions.""" + assignment_count = 1 << width + for event in range(1 << assignment_count): + increasing = True + for x in range(assignment_count): + if (event >> x) & 1: + for y in range(assignment_count): + if (x & y) == x and not ((event >> y) & 1): + increasing = False + break + if not increasing: + break + if increasing: + yield event + + +def local_assignment(atom, coordinates): + return sum(atom[c] << j for j, c in enumerate(coordinates)) + + +def event_true(event_mask, atom, coordinates): + assignment = local_assignment(atom, coordinates) + return (event_mask >> assignment) & 1 + + +def split_covariances(atom_counts): + """Return exact covariance numerators for every monotone event pair. + + For a distribution with total mass M, the numerator is + M * count(A and B) - count(A) * count(B), so its sign is the covariance + sign and the exact covariance equals numerator / M**2. + """ + total = sum(atom_counts.values()) + reports = {} + for sizes in SPLIT_SIZES: + left_size, right_size = sizes + pairs = [] + if left_size == right_size: + for left in combinations(range(N), left_size): + remaining = tuple(c for c in range(N) if c not in left) + for right in combinations(remaining, right_size): + if left < right: + pairs.append((left, right)) + else: + for left in combinations(range(N), left_size): + remaining = tuple(c for c in range(N) if c not in left) + for right in combinations(remaining, right_size): + pairs.append((left, right)) + + left_events = tuple(monotone_event_masks(left_size)) + right_events = tuple(monotone_event_masks(right_size)) + values = [] + strict_values = [] + constant_involved = 0 + witness = None + strict_witness = None + for left, right in pairs: + for event_left in left_events: + count_left = sum( + mass for atom, mass in atom_counts.items() + if event_true(event_left, atom, left) + ) + for event_right in right_events: + count_right = sum( + mass for atom, mass in atom_counts.items() + if event_true(event_right, atom, right) + ) + count_both = sum( + mass for atom, mass in atom_counts.items() + if event_true(event_left, atom, left) + and event_true(event_right, atom, right) + ) + covariance_numerator = total * count_both - count_left * count_right + values.append(covariance_numerator) + left_constant = event_left in (0, (1 << (1 << left_size)) - 1) + right_constant = event_right in (0, (1 << (1 << right_size)) - 1) + if left_constant or right_constant: + require(covariance_numerator == 0, + f"constant event has nonzero covariance for split {sizes}") + constant_involved += 1 + else: + strict_values.append(covariance_numerator) + if witness is None or covariance_numerator > witness[0]: + witness = ( + covariance_numerator, + left, + right, + event_left, + event_right, + count_left, + count_right, + count_both, + ) + if not (left_constant or right_constant): + if strict_witness is None or covariance_numerator > strict_witness[0]: + strict_witness = ( + covariance_numerator, + left, + right, + event_left, + event_right, + count_left, + count_right, + count_both, + ) + reports[sizes] = ( + min(values), max(values), len(values), witness, + min(strict_values), max(strict_values), len(strict_values), strict_witness, + constant_involved, + ) + return reports + + +def law_for_header(predicate): + """Enumerate a restricted family with prescribed first-row predicate.""" + law = Counter() + count = 0 + for matrix, inv in all_gl4(): + if predicate(matrix[0]): + count += 1 + law[indicators_for(matrix, inv)] += 1 + return count, law + + +def main(): + law = Counter() + wrong_law = Counter() + total = 0 + identity_atom = None + noninvolution_witness = None + + for matrix, inv in all_gl4(): + total += 1 + atom = indicators_for(matrix, inv) + law[atom] += 1 + if matrix == IDENTITY: + identity_atom = atom + if noninvolution_witness is None and matmul(matrix, matrix) != IDENTITY: + wrong_atom = indicators_for(matrix, inv, use_inverse=False) + if wrong_atom != atom: + noninvolution_witness = (matrix, atom, wrong_atom) + wrong_law[indicators_for(matrix, inv, use_inverse=False)] += 1 + + require(total == 20160, f"expected |GL_4(F_2)|=20160, got {total}") + require(sum(law.values()) == total, "atom masses do not sum to group size") + expected_by_weight = (3480, 3816, 228, 12, 0) + require(all(law[atom] == expected_by_weight[sum(atom)] + for atom in product((0, 1), repeat=N)), "complete atom fixture differs") + require(identity_atom == (0, 0, 0, 1), f"identity control changed: {identity_atom}") + require(noninvolution_witness is not None, "no forward-only witness found") + require(law != wrong_law, "forward-only mutation unexpectedly has the same atom law") + + moments = {} + for size in range(1, N + 1): + for subset in combinations(range(N), size): + moments[subset] = sum( + mass for atom, mass in law.items() + if all(atom[i] for i in subset) + ) + + print(f"GL4_F2_count={total}") + print("indicator_definition=Xi iff all leading principal minors of orders 1,2,3 of G P_i G^-1 are nonzero") + print("atom_counts (bits in i=0,1,2,3 order):") + for atom in product((0, 1), repeat=N): + print(f" {atom_label(atom)}: {law[atom]}") + print("product_moment_counts (subset -> count where all selected Xi=1):") + for subset, count in sorted(moments.items(), key=lambda item: (len(item[0]), item[0])): + print(f" {''.join(str(i) for i in subset)}: {count}") + + reports = split_covariances(law) + print("monotone_event_covariance_numerator_ranges (covariance = numerator / 20160^2):") + for sizes in SPLIT_SIZES: + report = reports[sizes] + minimum, maximum, tested = report[:3] + strict_minimum, strict_maximum, strict_tested = report[4:7] + constants_tested = report[8] + print(f" {sizes[0]}+{sizes[1]}: all_min={minimum} all_max={maximum} all_pairs={tested}") + print(f" constants_zero_pairs={constants_tested}; strict_nonconstant_pairs={strict_tested}; strict_min={strict_minimum} strict_max={strict_maximum}") + require(maximum == 0, f"constants or nonconstant events gave positive covariance for split {sizes}: {report[3]}") + require(strict_maximum < 0, f"nonconstant events were not strictly negative for split {sizes}: {report[7]}") + + # A fixed first-row header slice. This is a reproducible restriction of + # GL_4(F_2), not the full uniform law; it deliberately supplies a positive + # covariance control showing that the full-law conclusion is not automatic + # for arbitrary restricted families. + header_count, header_law = law_for_header(lambda row: row == 0b1110) + header_reports = split_covariances(header_law) + header_violations = [ + (sizes, report[3]) + for sizes, report in header_reports.items() + if report[1] > 0 + ] + require(header_count == 1344, f"unexpected fixed-row header size: {header_count}") + require(header_violations, "fixed-row header control did not violate negative association") + print(f"header_control=first row [0,1,1,1] (columns 0,1,2,3); matrices={header_count}") + print(f"header_control_positive_covariance_splits={len(header_violations)}") + if header_violations: + sizes, witness = header_violations[0] + numerator, left, right, event_left, event_right, count_left, count_right, count_both = witness + left_table = ''.join(str((event_left >> x) & 1) for x in range(1 << len(left))) + right_table = ''.join(str((event_right >> x) & 1) for x in range(1 << len(right))) + require((numerator, count_left, count_right, count_both) == (960, 432, 4, 2), + "fixed-row positive-covariance witness changed") + print(f" witness_split={sizes}; left_coordinates={left}; right_coordinates={right}") + print(f" left_event_truth_table={left_table}; right_event_truth_table={right_table}") + print(f" counts: total={header_count}, left={count_left}, right={count_right}, joint={count_both}") + print(f" covariance_numerator={numerator}; covariance={numerator}/{header_count**2} > 0") + + matrix, correct_atom, forward_atom = noninvolution_witness + print("forward_only_control=G P_i G instead of G P_i G^-1") + print(f" sample_G_rows={[[(row >> c) & 1 for c in range(N)] for row in matrix]}") + print(f" correct_atom={atom_label(correct_atom)} forward_only_atom={atom_label(forward_atom)}") + print(f" full_forward_only_law_differs={law != wrong_law}") + print("PASS_GL4_FOUR_GUARD_BOUNDARY") + + +if __name__ == "__main__": + main() diff --git a/research/corankone-four-negative-association/verify.py b/research/corankone-four-negative-association/verify.py new file mode 100644 index 0000000000..58cef3248b --- /dev/null +++ b/research/corankone-four-negative-association/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Exact finite component of the four-guard negative-association proof. + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. +Intersection spectra: Nick Petalas, PR4227/4261/4275/4599. +No predecessor executable is imported. +""" + +import json +from collections import defaultdict +from fractions import Fraction +from itertools import product +from math import comb, prod + + +SPECTRA = ( + {1: 1}, + {3: 1}, + {9: 1, 7: -2, 5: 1}, + {27: 1, 21: -6, 19: 6, 17: -6, 15: 16, 13: -18, 11: 9, 9: -2}, + {81: 1, 63: -12, 57: 24, 55: -8, 51: -24, 49: 18, 47: -48, + 45: 118, 43: -68, 41: 85, 39: -180, 37: 228, 35: -336, 33: 399, + 31: -444, 29: 502, 27: -548, 25: 523, 23: -332, 21: 144, 19: -48, 17: 6}, +) + +# Coefficient of p_j in the expectation of each increasing event. +EVENTS = { + "x": (0, 1), "AND2": (0, 0, 1), "OR2": (0, 2, -1), + "AND3": (0, 0, 0, 1), "xAND(yORz)": (0, 0, 2, -1), + "MAJ3": (0, 0, 3, -2), "xOR(yANDz)": (0, 1, 1, -1), + "OR3": (0, 3, -3, 1), +} +CASES = tuple((name, "x") for name in EVENTS) + ( + ("AND2", "AND2"), ("AND2", "OR2"), ("OR2", "OR2"), +) +# B, c, b, C, N: largest base and coefficient, next base, remaining mass, cutoff. +TAILS = ( + (28672, 128, 20480, 143872, 21), + (21504, 128, 19456, 419520, 81), + (28672, 256, 21504, 680640, 28), + (16128, 96, 14592, 2820224, 103), + (21504, 256, 19456, 3626656, 96), + (21504, 384, 19456, 6850144, 98), + (28672, 128, 21504, 3367488, 36), + (28672, 384, 21504, 4395776, 33), + (16128, 128, 14592, 2919872, 101), + (21504, 256, 19456, 3726336, 96), + (28672, 512, 21504, 5020608, 32), +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(*terms): + """Add (integer multiplier, {positive base: integer coefficient}) pairs.""" + result = defaultdict(int) + for multiplier, polynomial in terms: + for base, coefficient in polynomial.items(): + result[base] += multiplier * coefficient + return {base: value for base, value in result.items() if value} + + +def multiply(left, right): + """Pointwise multiply sequences represented as finite power sums.""" + result = defaultdict(int) + for b, a in left.items(): + for d, c in right.items(): + result[b * d] += a * c + return {base: value for base, value in result.items() if value} + + +def evaluate(polynomial, n): + return sum(coefficient * base**n for base, coefficient in polynomial.items()) + + +def numerator(k): + """A_k with p_k=A_k/Q, Q=16^n product_(j=0)^3 (2^(n+1)-2^j).""" + result = multiply(SPECTRA[k], {2**(4 - k): 1}) + for j in range(k, 4): + result = multiply(result, {2: 2, 1: -(2**j)}) + return result + + +def gap_polynomial(f, g): + numerators = tuple(numerator(k) for k in range(5)) + left = add(*[(a, numerators[i]) for i, a in enumerate(f)]) + right = add(*[(a, numerators[i]) for i, a in enumerate(g)]) + joint = add(*[(a * b, numerators[i + j]) + for i, a in enumerate(f) for j, b in enumerate(g)]) + return add((1, multiply(left, right)), (-1, multiply(numerators[0], joint))) + + +def moments(m): + require(type(m) is int and m >= 4, "dimension must be an integer at least four") + n, x = m - 1, 2**m + return tuple(Fraction(evaluate(SPECTRA[k], n), + 2**(k * n) * prod(x - 2**j for j in range(k))) + for k in range(5)) + + +def gap_value(f, g, p): + return (sum(a * p[i] for i, a in enumerate(f)) * + sum(b * p[j] for j, b in enumerate(g)) - + sum(a * b * p[i + j] for i, a in enumerate(f) for j, b in enumerate(g))) + + +def tail_parameters(polynomial): + require(len(polynomial) >= 2, "nontrivial tail required") + bases = sorted(polynomial, reverse=True) + require(all(type(b) is int and b > 0 for b in bases), "positive integer bases required") + return (bases[0], polynomial[bases[0]], bases[1], + sum(abs(polynomial[b]) for b in bases[1:])) + + +def verify_tail(polynomial, certificate): + require(len(certificate) == 5 and all(type(v) is int for v in certificate), + "five exact integer tail parameters required") + require(tail_parameters(polynomial) == certificate[:4], "tail parameters differ") + B, c, b, C, N = certificate + require(B > b > 0 and c > 0 and C > 0 and N >= 3, "invalid strict tail domain") + require(c * B**N > C * b**N, "tail dominance fails") + + +def monotone_tables(size): + """Enumerate Boolean truth tables; bit x is the value at subset x.""" + return [table for table in range(1, (1 << (1 << size)) - 1) + if all(not (table >> x & 1) or (table >> (x | (1 << i)) & 1) + for x in range(1 << size) for i in range(size))] + + +def expectation_coefficients(table, size): + """Subset Mobius inversion, then group coefficients by degree.""" + coefficients = [table >> x & 1 for x in range(1 << size)] + for i in range(size): + for x in range(1 << size): + if x >> i & 1: + coefficients[x] -= coefficients[x ^ (1 << i)] + result = [0] * (size + 1) + for x, coefficient in enumerate(coefficients): + result[x.bit_count()] += coefficient + while result and not result[-1]: + result.pop() + return tuple(result) + + +def event_classification(): + expected = ( + {EVENTS["x"]: 1}, + {EVENTS["x"]: 2, EVENTS["AND2"]: 1, EVENTS["OR2"]: 1}, + {EVENTS["x"]: 3, EVENTS["AND2"]: 3, EVENTS["OR2"]: 3, + EVENTS["AND3"]: 1, EVENTS["xAND(yORz)"]: 3, EVENTS["MAJ3"]: 1, + EVENTS["xOR(yANDz)"]: 3, EVENTS["OR3"]: 1}, + ) + tables = {s: monotone_tables(s) for s in (1, 2, 3)} + for size in (1, 2, 3): + histogram = defaultdict(int) + for table in tables[size]: + histogram[expectation_coefficients(table, size)] += 1 + require(dict(histogram) == expected[size - 1], "monotone classification differs") + known = {tuple(sorted(gap_polynomial(EVENTS[a], EVENTS[b]).items())) + for a, b in CASES} + seen, total = set(), 0 + for a, b in ((1, 1), (1, 2), (1, 3), (2, 2)): + for f, g in product(tables[a], tables[b]): + polynomial = gap_polynomial(expectation_coefficients(f, a), + expectation_coefficients(g, b)) + seen.add(tuple(sorted(polynomial.items()))) + total += 1 + require(seen == known and len(known) == 11, "incomplete covariance list") + return tables, total + + +def atom_probabilities(p, size): + """Probability of each specified binary word from intersection moments.""" + return tuple(sum((-1)**j * comb(size - x.bit_count(), j) * p[x.bit_count() + j] + for j in range(size - x.bit_count() + 1)) + for x in range(1 << size)) + + +def literal_gap(f, a, g, b, atoms): + """Truth-table evaluation without multilinear coefficients.""" + ef = eg = joint = Fraction(0) + for x, mass in enumerate(atoms): + fv = f >> (x & ((1 << a) - 1)) & 1 + gv = g >> ((x >> a) & ((1 << b) - 1)) & 1 + ef += fv * mass + eg += gv * mass + joint += fv * gv * mass + return ef * eg - joint + + +def rejection_controls(): + p = gap_polynomial(EVENTS["AND3"], EVENTS["x"]) + tests = [ + lambda: moments(3), lambda: moments(True), + lambda: verify_tail(add((-1, p)), TAILS[3]), + lambda: verify_tail(p, (*TAILS[3][:4], 3)), + lambda: verify_tail(p, (*TAILS[3][:3], TAILS[3][3] - 1, TAILS[3][4])), + lambda: verify_tail(p, (*TAILS[3][:4], True)), + ] + for operation in tests: + try: + operation() + except ValueError: + continue + raise ValueError("invalid proof input was accepted") + bad_atoms = [Fraction(0)] * 16 + bad_atoms[0] = bad_atoms[15] = Fraction(1, 2) + require(literal_gap(2, 1, 2, 1, bad_atoms) == -Fraction(1, 4), + "positive-covariance control was not detected") + wrong = Fraction(3**3, 2**3 * 16) + require(wrong != Fraction(9, 40), "finite-GL denominator control is ineffective") + return len(tests) + 2 + + +def main(): + tables, labelled_cases = event_classification() + require(moments(4) == (1, Fraction(9, 40), Fraction(1, 80), Fraction(1, 1680), 0), + "complete GL4 moment fixture differs") + atoms4 = atom_probabilities(moments(4), 4) + require(tuple(20160 * q for q in atoms4) == + (3480, 3816, 3816, 228, 3816, 228, 228, 12, + 3816, 228, 228, 12, 228, 12, 12, 0), "GL4 atom fixture differs") + rows, prefix_checks = [], 0 + Q = numerator(0) + for (left, right), certificate in zip(CASES, TAILS, strict=True): + f, g = EVENTS[left], EVENTS[right] + polynomial = gap_polynomial(f, g) + verify_tail(polynomial, certificate) + N = certificate[4] + for n in range(3, N): + direct = gap_value(f, g, moments(n + 1)) + expanded = Fraction(evaluate(polynomial, n), evaluate(Q, n)**2) + require(direct == expanded and direct > 0, "finite prefix sign/identity failed") + prefix_checks += 1 + for n in (N, N + 1, 2 * N): + require(Fraction(evaluate(polynomial, n), evaluate(Q, n)**2) == + gap_value(f, g, moments(n + 1)) > 0, "tail probe failed") + rows.append({"events": [left, right], "terms": len(polynomial), + "B_c_b_C_N": certificate}) + truth_checks = 0 + for m in range(4, max(row[4] for row in TAILS) + 2): + p = moments(m) + atoms = atom_probabilities(p, 4) + require(sum(atoms) == 1 and min(atoms) >= 0, "invalid four-bit distribution") + for a, b in ((1, 1), (1, 2), (1, 3), (2, 2)): + for f, g in product(tables[a], tables[b]): + literal = literal_gap(f, a, g, b, atoms) + algebraic = gap_value(expectation_coefficients(f, a), + expectation_coefficients(g, b), p) + require(literal == algebraic and literal > 0, "truth-table covariance failed") + truth_checks += 1 + controls = rejection_controls() + print("PASS_CORANKONE_FOUR_NEGATIVE_ASSOCIATION") + print(json.dumps({"claim": "strict negative association for every integer m >= 4", + "proof": "exact finite prefixes plus strict monotone power-sum tails", + "nonconstant_monotone_functions": [len(tables[s]) for s in (1, 2, 3)], + "labelled_cases": labelled_cases, "distinct_gap_types": len(rows), + "finite_prefix_comparisons": prefix_checks, + "truth_table_comparisons": truth_checks, + "tail_probe_comparisons": 3 * len(rows), + "rejection_controls": controls, "tails": rows}, sort_keys=True)) + + +if __name__ == "__main__": + main()