diff --git a/research/corankone-triple-negative-association/README.md b/research/corankone-triple-negative-association/README.md new file mode 100644 index 0000000000..ba63617e44 --- /dev/null +++ b/research/corankone-triple-negative-association/README.md @@ -0,0 +1,260 @@ +# Negative association of three binary full-guard events + +**A dimension-uniform proof with independent exact corroboration. No new kappa.** + +For three pairwise orthogonal rank-one idempotents over the binary field, the +three full-guard indicators under one uniformly sampled complete header are +negatively associated in every dimension `m >= 3`. In fact, any two nonconstant +increasing real functions on disjoint, nonempty sets of these indicators have +strictly negative covariance. + +This answers Open next question 1 of Nick Petalas's +[PR #4777](https://github.com/CrocSwap/integer-mult-bounds/pull/4777). +The new step is an all-dimension **union-versus-singleton bound** using only the +known marginal and pair formulas and nonnegativity of the triple probability. +Section 4 proves why the checked event types exhaust negative association. +The counting laws and conjunction inequality remain predecessor results. + +Prepared for lee-phys with substantial OpenAI Codex assistance. Apache-2.0. +Independent human and proof-kernel review are unclaimed. + +## 1. Domain and cited results + +Let `m >= 3` and let `U_1,U_2,U_3` be rank-one idempotents on `F_2^m`, with +`U_i U_j = 0` whenever `i != j`. Put `P_i = I-U_i`. Choose `G` uniformly from +the whole group `GL_m(F_2)`. Event `E_i` means that every leading principal +minor of `G P_i G^-1`, of orders 1 through `m-1`, is nonzero. All three events +use the same header `G`. + +The three image lines and their common-kernel complement give a simultaneous +basis with `U_i=e_i e_i^T`. Right multiplication of `G` by this fixed change +of basis permutes the complete header domain. Permuting the distinguished +lines likewise preserves that domain, so the event vector is exchangeable. +Write + +```text +n=m-1, X=2^m, A=9^n-2*7^n+5^n, +p=Pr(E_i), p2=Pr(E_i and E_j), p3=Pr(E_1 and E_2 and E_3). +``` + +The following are cited results, not new claims: + +```text +p = 3^n / [(X-1)2^n], (#4227) +p2 = A / [(X-1)(X-2)2^(2n)], (#4261) +p3 < p*p2 for every m >= 3. (#4777) +``` + +See the retained [marginal proof](../projector-header-density/PROOF.md), +[pair proof](../corankone-pair-header-law/PROOF.md), and +[conjunction proof](../corankone-triple-block-correlation/PROOF.md). +The [triple law from #4275](../corankone-triple-header-law/PROOF.md) supplies +the exact `p3` used by the verifier and the conjunction proof. These source +files are pinned at this package's base in `SOURCES.json`. No predecessor +executable or live source file is imported by `verify.py`. + +## 2. A quantitative pair deficit + +Set `r=(7/9)^n`, `s=(5/9)^n` and `delta=1-p2/p^2`. The pair formula gives + +```text +delta = [(X-1)(2r-s)-1]/(X-2). +``` + +We have `02`. Hence + +```text +delta > [(X-1)r-1]/(X-2) + = r/2 + (Xr-2)/[2(X-2)] + > r/2, +``` + +since `Xr=2*(14/9)^n>2`. In particular `p2=0`, `delta>r/2` and `r>p` yields the new explicit bound + +```text +Delta > p^2[(1+p/2)r-p] >= p^2(r-p) > 0. +``` + +Thus, for every `m>=3`, + +```text +2p2-p3 < p(2p-p2), +Cov(1_(E_1 or E_2),1_E3) < -p^2[(7/9)^(m-1)-p] < 0. +``` + +No triple closed form or positive triple probability is needed. In particular, +`m=3` is included although `p3=0`. The exact gaps at `m=3,4` are `421/2352` +and `199/2688` respectively. + +## 4. Complete negative association + +Put `Z_i=1_Ei`. Negative association requires + +```text +Cov(f((Z_i)_(i in I)),g((Z_j)_(j in J))) <= 0 +``` + +for disjoint index sets `I,J` and coordinatewise nondecreasing real functions +`f,g`. With three coordinates, nonempty disjoint sets have sizes `1,1` or +`2,1`, up to exchange. A function on one bit is `a+bZ_i` with `b>=0`. +The nonempty proper increasing subsets of a two-bit square are exactly + +```text +{11}, {10,11}, {01,11}, {01,10,11}. +``` + +Their indicators are AND, the first coordinate, the second coordinate, and OR. +Every increasing real function on that square is a constant plus a nonnegative +linear combination of those indicators: if its distinct values are +`t_0<...=t_j). +``` + +Each nontrivial superlevel set is one of the four sets above. Their covariances +with the remaining coordinate are all strictly negative: + +```text +AND: p3-p*p2 < 0 (cited #4777), +coordinate: p2-p^2 < 0 (Section 2), +OR: 2p2-p3-p(2p-p2) < 0 (Section 3). +``` + +Covariance linearity proves the theorem. If both functions are nonconstant, +at least one coefficient from each is positive, giving strict negativity. +Constant functions or an empty index set give zero. This covers arbitrary +increasing functions, not only intersections of the events. QED. + +## 5. A control showing why the new step matters + +Negative pair and AND covariances do not suffice for negative association. +Consider the exchangeable three-bit distribution assigning `13/100` to `000`, +`8/100` to each weight-one state, `21/100` to each weight-two state, and zero +to `111`. Then + +```text +p=1/2, p2=21/100, p3=0, +p2-p^2=-1/25, p3-p*p2=-21/200, +Cov(OR(Z_1,Z_2),Z_3)=1/40 > 0. +``` + +This is a control distribution, not a header counterexample. The independent +increasing-event checker rejects it; a pair/AND-only checker would accept it. + +## 6. Exact verification and the cited conjunction lemma + +`verify.py` uses Python 3.12's standard library, exact integers and rational +numbers, and explicit checks active under `-O`. It imports no external data. + +- Complete `GL_3(F_2)` and `GL_4(F_2)` enumeration constructs the conjugated + requests by matrix multiplication and tests each leading minor by binary + elimination. All eight atom counts match the cited moments. Group orders + are 168 and 20,160. +- Independent enumeration of factor increments `y*x^T` gives convolution + counts on the one-, two-, and three-kernel safe partial-Gram spaces. + Evaluation of all 64 three-kernel characters recovers #4275's signed + eigenvalue multiplicities. Walk counts match the formulas through dimension + 25 where their domains are defined. +- All six increasing subsets of a two-bit square are enumerated. Every + nontrivial block-versus-singleton covariance and the new quantitative bound + is checked exactly at every `3<=m<=256`. + +The verifier also independently checks the finite component and constants of +the *cited* conjunction proof. For clarity, its all-dimension argument is +restated here with #4777's credit. Write + +```text +B=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. +p3/(p*p2) = (T/B)*(X-1)/(X-4). +``` + +Strict convexity of `t^n` at `9,7,5` gives `B>0`; its formula also gives +`B<27^n`. The inequality `T>=0` follows from its walk-count interpretation. +After the terms of bases 27 and 21, the absolute coefficients of `T` sum to +57 and all bases are at most 19. For `n>=42`, `57*19^42<21^42` and `19/21<1` +therefore give `T<27^n-5*21^n=16`, `(X-1)/(X-4)<=1+4/X`, and +`2/2^n=2`, since `(14/9)^2>2`. Thus the ratio is below +`(1-3r)(1+r)=1-2r-3r^2<1`. The remaining forty dimensions `3<=m<=42` +have strictly positive integer gaps `(X-4)B-(X-1)T`, checked exhaustively. + +This is a replay of the existing conjunction proof, not a new theorem about +that comparison. Section 3's new union proof is analytic for all dimensions. +Finite header counts and the extra sampled dimensions are corroboration, +not extrapolation to an infinite domain. + +Controls reject the pair/AND-only false positive, identical events, independent +events falsely claimed strictly negatively associated, malformed atom laws, a missing +finite-GL normalization, and a changed triple spectrum. + +Reproduce from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/corankone-triple-negative-association --check-only +python3.12 -B scripts/research_package.py --package research/corankone-triple-negative-association +python3.12 -I -B research/corankone-triple-negative-association/verify.py +python3.12 -I -O -B research/corankone-triple-negative-association/verify.py +``` + +The direct command prints `PASS_CORANKONE_TRIPLE_NEGATIVE_ASSOCIATION` and a +deterministic exact-check summary. It writes no files and needs no Git. The +registered metadata check separately binds historical source provenance. + +## Scope, provenance and credit + +The theorem requires three orthogonal kernel lines over `F_2` and a complete +uniform `GL` header distribution. Four or more indicators, odd fields, +nonorthogonal kernels, and restricted/nonuniform header collections are not +covered. No header-selection algorithm, physical caller, supplier admission, +or multiplication exponent follows. The selected kappa remains unchanged. + +Base: canonical main `4c0a359d88f22f05189d51f48387750b801a45d4`. +`TASK.json` records the explicit mathematical assignment as a changed scope of +`formal-interface-lemma`; there is no Lean claim. `SOURCES.json` pins retained +proofs and orientation metadata as provenance, not runtime inputs. The counting +proofs were read; a new independent proof of every predecessor is not claimed. +The [canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141140) +records overlap and progress. + +Credit Nick Petalas for #4227, #4261, #4275, #4767, and #4777, including the +explicit open question; Cinna Davis for the BIT request context; source527, +commdata2338 and Jose Manuel for the normalizer/closure lineage; and Chris R / +Clear1nsight for the earlier counting context credited by #4777. No predecessor +executable is copied. New proof and verification: lee-phys with substantial +OpenAI Codex assistance, Apache-2.0. No independent human or proof-kernel +verification is claimed. + +## Open next questions + +1. Does negative association hold for four orthogonal binary kernel lines? + Start by listing the increasing events for the `2+2` and `3+1` splits and + using the known four-event law. These additional event types are not covered + by the three-variable reduction; an intersection product bound is insufficient. +2. Does the three-event result hold over odd finite fields? Start with the + three-kernel partial-Gram transfer and exact small-field atom laws before + conjecturing a sign. The binary safe-state group and pair-deficit estimate + do not automatically generalize. + +Structured first steps and blockers are in `TASK.json`. diff --git a/research/corankone-triple-negative-association/SOURCES.json b/research/corankone-triple-negative-association/SOURCES.json new file mode 100644 index 0000000000..a8c256e19a --- /dev/null +++ b/research/corankone-triple-negative-association/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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/projector-header-density/PROOF.md", + "usage": "provenance", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + }, + { + "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-block-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "0f205f5b9179402b7fd733134c2a73d65e1a8963", + "sha256": "949436e5a9df0ab035d07eb460224c2d5f0fbbf5bda3744d51e046335c93de12" + }, + { + "path": "research/corankone-pair-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "fd2522be59e8c4d992688c4b5a229e88792e136b", + "sha256": "a3db8d9bfb191e7cbeb04dd3b2844692e0e5e3574f0f4d461a5e685f17f24716" + } + ] +} diff --git a/research/corankone-triple-negative-association/TASK.json b/research/corankone-triple-negative-association/TASK.json new file mode 100644 index 0000000000..09ee5a5869 --- /dev/null +++ b/research/corankone-triple-negative-association/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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 negative association of the three binary orthogonal-kernel full-guard indicators under a uniformly sampled complete GL_m(F_2) header, for every m >= 3; close PR4777 open question 1.", + "scope_change_reason": "The donor explicitly selected this mathematical question. The contribution is a written dimension-uniform inequality and an increasing-function reduction, with exact independent corroboration, rather than a proof-assistant formalization of a selected caller.", + "bottleneck_link": "Scoped algebraic probability side result: shared-header admission events need joint rather than independent probability reasoning. No physical header-selection or supplier cost is supplied and no kappa improvement follows.", + "budget_minutes": 60, + "stop_rule": "Stop after proving or refuting the union-versus-singleton inequality for every m >= 3, justifying the complete negative-association reduction, and independently checking finite header distributions and cited inputs. Do not extend to odd fields or four requests in this contribution.", + "outcome": "completed", + "evidence": "README Sections 2-4 give an analytic union gap Delta > p^2*((7/9)^(m-1)-p) > 0 and complete monotone-function reduction, using credited predecessor laws and conjunction theorem. The stdlib verifier independently enumerates 20,328 complete GL3/GL4 headers, 71 Gram-walk comparisons, all 64 triple characters, 3,048 strict covariance comparisons over 254 dimensions, the 40 finite cases of the cited conjunction proof and its tail constants, and nine rejecting controls. These finite checks corroborate, rather than extrapolate, the universal argument.", + "author": "lee-phys, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, source inspection, implementation, validation and writing. No independent human or formal proof-kernel review claimed.", + "open_questions": [ + { + "question": "Does negative association hold for four orthogonal binary kernel lines under the complete uniform header distribution?", + "why_it_matters": "A four-request result would extend the dependence theorem beyond the first complete three-event case.", + "first_step": "Enumerate all increasing events in the 2+2 and 3+1 splits, and use the known four-event moment law to test their exact covariances before attempting a uniform proof.", + "blocked_by": "Additional increasing-event types and cross-block inequalities are not implied by a fourfold intersection bound." + }, + { + "question": "Does the three-event negative-association result hold over odd finite fields?", + "why_it_matters": "Odd fields are closer to the retained normalizer domain, but the present binary theorem supplies no such conclusion.", + "first_step": "Use the three-kernel partial-Gram transfer to obtain exact small-field atom distributions and identify the signs of the union and conjunction comparisons.", + "blocked_by": "The binary safe-state group and the specific pair-deficit estimate do not automatically extend to odd characteristic." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141140", + "overlap": { + "snapshot": "2026-10-23T07:52:46.419795+00:00", + "open_prs": 323, + "discussion_records": 4172, + "coverage": "Complete reported remote pagination; all-state PR search and targeted retained proofs. Sparse local notes, arbitrary diffs and unpublished work are not exhaustively covered." + }, + "validation": { + "registered_replay": "Python 3.12 normal and optimized commands passed; exact metadata/source pins passed.", + "actual_mutations": "Three disposable optimized verifier mutations rejected: changed pair coefficient, weakened strictness, and omitted OR event type.", + "orientation": "Selected record and current guidance read. The optional research_selected_baseline.py source-closure orientation stopped because the sparse checkout omits certificates/checkpoints/frontier4359.json; no source-closure or selected scientific replay success is claimed. This mathematical package has no runtime dependency on that closure.", + "unrun": "Independent human review, formal proof-kernel verification, selected scientific cold replay, and the optional full-history preflight in this shallow checkout." + } +} diff --git a/research/corankone-triple-negative-association/VERIFY.json b/research/corankone-triple-negative-association/VERIFY.json new file mode 100644 index 0000000000..5f47f04aae --- /dev/null +++ b/research/corankone-triple-negative-association/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete GL3/GL4 literal atom enumeration; independent Gram walks and character spectrum; quantitative union proof identities; all increasing-event types; exact cited conjunction certificate and nine failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the exact verification with assertions disabled; all mathematical checks use explicit exceptions." + } + ] +} diff --git a/research/corankone-triple-negative-association/verify.py b/research/corankone-triple-negative-association/verify.py new file mode 100644 index 0000000000..80c07f68a9 --- /dev/null +++ b/research/corankone-triple-negative-association/verify.py @@ -0,0 +1,295 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the written three-guard negative-association proof. + +lee-phys, with substantial OpenAI Codex assistance. Apache-2.0. +Counting formulas: Nick Petalas, PR4227/4261/4275/4777 (see README). +No predecessor code, external data, numerical tolerance, or assertions. +""" + +from collections import Counter +from fractions import Fraction as F +from itertools import product +from math import prod +import json + + +SPECTRA = { + 1: {3: 1}, + 2: {9: 1, 7: -2, 5: 1}, + 3: {27: 1, 21: -6, 19: 6, 17: -6, 15: 16, 13: -18, 11: 9, 9: -2}, +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def probability(k, m): + require(type(k) is int and k in SPECTRA, "kernel domain") + require(type(m) is int and m >= max(2, k), "dimension domain") + n, x = m - 1, 2**m + numerator = sum(c * a**n for a, c in SPECTRA[k].items()) + denominator = prod(x - 2**i for i in range(k)) * 2 ** (k * n) + return F(numerator, denominator) + + +def atoms(m): + p, p2, p3 = (probability(k, m) for k in (1, 2, 3)) + by_weight = (1 - 3*p + 3*p2 - p3, p - 2*p2 + p3, p2 - p3, p3) + return tuple(by_weight[x.bit_count()] for x in range(8)) + + +def validate_atoms(weights): + require(len(weights) == 8, "eight atoms required") + require(all(w >= 0 for w in weights), "negative atom") + require(sum(weights) == 1, "atom normalization") + + +def upsets(): + # Generate the monotone Boolean functions, not a hand-selected test list. + return tuple(mask for mask in range(16) if all( + not ((x & y) == x and (mask >> x) & 1) or (mask >> y) & 1 + for x in range(4) for y in range(4) + )) + + +def covariances(weights): + validate_atoms(weights) + answer = [] + for singleton in range(3): + j, k = (i for i in range(3) if i != singleton) + ey = sum(w for x, w in enumerate(weights) if (x >> singleton) & 1) + for mask in upsets(): + if mask in (0, 15): + continue + ef, efy = F(0), F(0) + for x, w in enumerate(weights): + pair = ((x >> j) & 1) | (((x >> k) & 1) << 1) + if (mask >> pair) & 1: + ef += w + if (x >> singleton) & 1: + efy += w + answer.append((singleton, mask, efy - ef*ey)) + return answer + + +def check_strict_na(weights): + values = covariances(weights) + require(len(values) == 12, "increasing-event coverage") + require(all(c < 0 for _, _, c in values), "nonnegative increasing covariance") + + +def inverse(rows, m): + augmented = [row | (1 << (m+i)) for i, row in enumerate(rows)] + for col in range(m): + pivot = next((i for i in range(col, m) if (augmented[i] >> col) & 1), None) + if pivot is None: + return None + augmented[col], augmented[pivot] = augmented[pivot], augmented[col] + for i in range(m): + if i != col and (augmented[i] >> col) & 1: + augmented[i] ^= augmented[col] + return tuple(row >> m for row in augmented) + + +def multiply(a, b): + result = [] + for row in a: + out = 0 + while row: + bit = row & -row + out ^= b[bit.bit_length() - 1] + row ^= bit + result.append(out) + return tuple(result) + + +def rank(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in basis: + basis[pivot] = row + break + row ^= basis[pivot] + return len(basis) + + +def full_guard(rows, m): + for size in range(1, m): + mask = (1 << size) - 1 + if rank(tuple(row & mask for row in rows[:size])) != size: + return False + return True + + +def literal_headers(m): + ident = tuple(1 << i for i in range(m)) + requests = [tuple(v if j != i else 0 for j, v in enumerate(ident)) + for i in range(3)] + histogram = [0] * 8 + for g in product(range(1 << m), repeat=m): + inv = inverse(g, m) + if inv is None: + continue + require(multiply(g, inv) == ident, "literal inverse") + mask = 0 + for i, request in enumerate(requests): + conjugate = multiply(multiply(g, request), inv) + mask |= int(full_guard(conjugate, m)) << i + histogram[mask] += 1 + total = prod(2**m - 2**i for i in range(m)) + require(sum(histogram) == total, "complete GL enumeration") + observed = tuple(F(c, total) for c in histogram) + require(observed == atoms(m), "literal header atom law") + check_strict_na(observed) + return histogram + + +def safe_steps(k): + positions = [(i, j) for i in range(k) for j in range(k) if i != j] + weights = [0] * (1 << len(positions)) + # Each actual pair (y,x) is counted, including all zero factorizations. + for y, x in product(range(1 << k), repeat=2): + if y & x: + continue + mask = sum((((y >> i) & 1) * ((x >> j) & 1)) << bit + for bit, (i, j) in enumerate(positions)) + weights[mask] += 1 + require(sum(weights) == 3**k, "safe factor count") + return weights + + +def character_spectrum(weights): + result = Counter() + for character in range(len(weights)): + eigenvalue = sum(w * (-1)**((character & step).bit_count()) + for step, w in enumerate(weights)) + result[eigenvalue] += (-1)**character.bit_count() + return {a: c for a, c in result.items() if c} + + +def check_spectrum(actual, expected): + require(actual == expected, "signed character spectrum") + + +def check_walks(): + checks = 0 + spectra = {} + for k in (1, 2, 3): + weights = safe_steps(k) + spectrum = character_spectrum(weights) + check_spectrum(spectrum, SPECTRA[k]) + spectra[k] = spectrum + states = [1] + [0] * (len(weights) - 1) + nonzero = [(s, w) for s, w in enumerate(weights) if w] + for n in range(1, 25): + states = [sum(states[x ^ step] * w for step, w in nonzero) + for x in range(len(weights))] + m = n + 1 + if m < k: + continue + denominator = prod(2**m - 2**i for i in range(k)) * 2**(k*(m-k)) + require(F(states[-1], denominator) == probability(k, m), "Gram walk law") + require(sum(states) == 3**(k*n), "Gram walk total") + checks += 1 + return checks, spectra + + +def check_dimensions(): + require(upsets() == (0, 8, 10, 12, 14, 15), "complete Boolean upsets") + count = 0 + for m in range(3, 257): + n, x = m - 1, 2**m + p, p2, p3 = (probability(k, m) for k in (1, 2, 3)) + r, s = F(7, 9)**n, F(5, 9)**n + delta = 1 - p2/p**2 + require(delta == F((x-1)*(2*r-s)-1, x-2), "pair deficit identity") + require(delta > r/2 and 0 < p < r, "analytic comparison") + gap = p*(2*p-p2) - (2*p2-p3) + require(gap == p**2*((2+p)*delta-p) + p3, "union gap identity") + require(gap > p**2*(r-p) > 0, "quantitative union bound") + require(p3 < p*p2, "cited conjunction inequality") + check_strict_na(atoms(m)) + count += 1 + require(probability(3, 3) == 0, "zero-triple boundary") + for m, expected in ((3, F(421, 2352)), (4, F(199, 2688))): + p, p2, p3 = (probability(k, m) for k in (1, 2, 3)) + require(p*(2*p-p2)-(2*p2-p3) == expected, "exact gap fixture") + return count + + +def check_cited_tail(): + require(57 * 19**42 < 21**42, "conjunction remainder constant") + require(3 * 7**42 < 9**42, "positive conjunction upper bound") + require(14**2 > 2 * 9**2, "finite-GL comparison constant") + checked = 0 + for m in range(3, 43): + n, x = m - 1, 2**m + b = 27**n - 2*21**n + 15**n + t = sum(c * a**n for a, c in SPECTRA[3].items()) + integer_gap = (x-4)*b - (x-1)*t + require(b > 0 and integer_gap > 0, "finite conjunction proof case") + p, p2, p3 = (probability(k, m) for k in (1, 2, 3)) + require(p3/(p*p2) == F(t*(x-1), b*(x-4)), "conjunction ratio normalization") + checked += 1 + return checked + + +def expect_rejection(operation, name): + try: + operation() + except ValueError: + return name + raise ValueError("control accepted: " + name) + + +def controls(header4, spectra): + by_weight = (F(13, 100), F(8, 100), F(21, 100), F(0)) + deceptive = tuple(by_weight[x.bit_count()] for x in range(8)) + values = {(i, mask): c for i, mask, c in covariances(deceptive)} + require(values[0, 8] == -F(21, 200), "control AND covariance") + require(values[0, 10] == -F(1, 25), "control pair covariance") + require(values[0, 14] == F(1, 40), "control OR covariance") + broken_spectrum = dict(SPECTRA[3]) + broken_spectrum[19] += 1 + wrong_pair = F(9**3 - 2*7**3 + 5**3, 15**2 * 2**6) + observed_pair = F(sum(c for x, c in enumerate(header4) if x & 3 == 3), sum(header4)) + tests = [ + (lambda: check_strict_na(deceptive), "pair-AND-only false positive"), + (lambda: check_strict_na((F(1, 2),) + (F(0),)*6 + (F(1, 2),)), "identical events"), + (lambda: check_strict_na((F(1, 8),)*8), "independence is not strict"), + (lambda: validate_atoms((F(-1), F(2)) + (F(0),)*6), "negative atom"), + (lambda: validate_atoms((F(1, 9),)*8), "unnormalized law"), + (lambda: require(wrong_pair == observed_pair, "finite-GL factor"), "missing GL normalization"), + (lambda: check_spectrum(spectra[3], broken_spectrum), "changed triple coefficient"), + (lambda: probability(3, 2), "insufficient dimension"), + (lambda: probability(3, True), "Boolean dimension"), + ] + return [expect_rejection(f, name) for f, name in tests] + + +def main(): + histograms = {m: literal_headers(m) for m in (3, 4)} + walk_checks, spectra = check_walks() + dimensions = check_dimensions() + finite_cases = check_cited_tail() + rejected = controls(histograms[4], spectra) + summary = { + "literal_header_atoms": histograms, + "literal_headers": sum(map(sum, histograms.values())), + "walk_comparisons": walk_checks, + "three_kernel_signed_spectrum": spectra[3], + "dimensions_checked": dimensions, + "strict_covariances_checked": 12 * dimensions, + "cited_finite_conjunction_cases": finite_cases, + "rejected_controls": rejected, + } + print(json.dumps(summary, sort_keys=True)) + print("PASS_CORANKONE_TRIPLE_NEGATIVE_ASSOCIATION") + + +if __name__ == "__main__": + main()