diff --git a/research/corankone-triple-block-correlation/PROOF.md b/research/corankone-triple-block-correlation/PROOF.md new file mode 100644 index 0000000000..0f205f5b91 --- /dev/null +++ b/research/corankone-triple-block-correlation/PROOF.md @@ -0,0 +1,131 @@ +# A pair of binary full guards is negatively correlated with a third guard + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let U1,U2,U3 be pairwise orthogonal rank-one idempotents on F2^m, +where m>=3, and let Ei be the event that every leading principal minor +through rank m-1 of G(I-Ui)G^-1 is nonzero. All three events use the same +uniform complete header G in GL_m(F2). + +**Theorem.** Pr(E1 E2 E3) < Pr(E1 E2)Pr(E3), for every m>=3. + +This is a scoped counting proof with an exact computer-assisted finite +component. It answers the first bounded step in Open next question 1 of +Nick Petalas's [#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767). +The pair and triple counting laws below are cited predecessor theorems, +not re-proved or independently audited here. The new result compares a +two-event block with a singleton. Symmetry gives every permutation of +the split. No statement about arbitrary increasing functions is claimed. + +## Cited inputs and the new reduction + +Write n=m-1, X=2^m, and define + +```text +A = 9^n - 2*7^n + 5^n, +B = 3^n A = 27^n - 2*21^n + 15^n, +T = 27^n - 6*21^n + 6*19^n - 6*17^n + 16*15^n + - 18*13^n + 9*11^n - 2*9^n. +``` + +Nick Petalas's #4227, #4261 and #4275 respectively supply + +```text +p1 = Pr(E3) = 3^n / ((X-1)2^n), +p2 = Pr(E1 E2) = A / ((X-1)(X-2)2^(2n)), +p3 = Pr(E1 E2 E3) = T / ((X-1)(X-2)(X-4)2^(3n)). +``` + +These are complete-header probabilities. All source proofs are pinned as +historical provenance in SOURCES.json. No predecessor executable is used. +The sharp difference from the earlier comparison p3=2, A>0 by strict convexity of t^n at 5,7,9. Equivalently, the +even terms of (7+2)^n+(7-2)^n-2*7^n are positive. Thus B>0, and + +```text +R = p3/(p2 p1) = (T/B)(X-1)/(X-4). +R<1 iff (X-4)B - (X-1)T > 0. (1) +``` + +The factor (X-1)/(X-4) must be retained. Treating complete headers as +independent factor coordinates would omit it. + +## Uniform tail, n>=42 + +Put x=(7/9)^n. The terms of T below base 21 have absolute coefficient +sum 57 and bases at most 19. Exact integer arithmetic gives + +```text +57*19^42 < 21^42. +``` + +Since 19/21<1, for every n>=42, + +```text +0 <= T <= 27^n - 6*21^n + 57*19^n < 27^n - 5*21^n. +``` + +The lower bound uses the cited interpretation as a count. Since +27^n-2*21^n < B < 27^n, this yields + +```text +T < B - 3*21^n, +T/B < 1 - 3*21^n/B < 1 - 3x. +``` + +The last upper bound is positive at n=42, as checked by +3*7^42<9^42, and remains positive for larger n. + +For n>=3, X>=16, so X-4>=3X/4. Also +2<(14/9)^2 and 14/9>1 imply 2/2^n < (7/9)^n for n>=2. Consequently + +```text +(X-1)/(X-4) = 1 + 3/(X-4) <= 1 + 4/X + = 1 + 2/2^n < 1 + x. +``` + +Every factor needed to multiply these upper bounds is nonnegative. +Therefore, for n>=42, + +```text +0 <= R < (1-3x)(1+x) = 1-2x-3x^2 < 1. +``` + +## Exact finite component, 3<=m<=42 + +The verifier evaluates all 40 integers in (1), using unrestricted-precision +integer arithmetic, and requires each to be strictly positive. It also +computes p1,p2,p3 independently as rational expressions and requires their +ratio to equal (1)'s ratio. The generated stdout receipt lists every m, +its integer gap and its exact ratio. There is no floating-point tolerance. +At m=3 the triple count is zero and the pair count is positive. At m=4, + +```text +p1=9/40, p2=1/80, p3=1/1680, R=40/189. +``` + +This finite component and the uniform tail cover every m>=3. The extra +86 exact comparisons at 43<=m<=128 corroborate the tail bound, without +being a substitute for its quantified proof. The verifier also rejects +grouped independence, a reversed leading spectral sign, an omitted +finite-GL correction and invalid replay dimensions. QED. + +## Scope + +Only binary arithmetic, orthogonal kernel lines and uniformly weighted +complete GL headers are covered. The pairwise inequality from #4767 and +the three-independent-marginal inequality from #4275 do not imply this +split inequality; those predecessor results retain their credit. + +This result alone does not prove negative association of the three-event +Bernoulli vector. For example, comparison of E1 union E2 with E3 would +require a second inequality. Larger blocks, odd fields and restricted +header distributions remain open. A request producer, header selection, +emission, dispatch, dirty restoration, stock, precision and a full paid +physical caller are not supplied. No new kappa, supplier admission or +complete multiplication theorem follows. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/corankone-triple-block-correlation/README.md b/research/corankone-triple-block-correlation/README.md new file mode 100644 index 0000000000..7a9246f081 --- /dev/null +++ b/research/corankone-triple-block-correlation/README.md @@ -0,0 +1,104 @@ +# A binary corank-one pair is negatively correlated with a third full guard + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped counting proof with an exact computer-assisted finite +component. For three pairwise orthogonal rank-one idempotents Ui on F2^m, +m>=3, let Ei mean that every leading principal minor through rank m-1 of +G(I-Ui)G^-1 is nonzero. With one uniformly weighted complete GL_m(F2) header, + +```text +Pr(E1 E2 E3) < Pr(E1 E2)Pr(E3), every m>=3. +``` + +This answers the first bounded step in Open next question 1 of +[#4767](https://github.com/CrocSwap/integer-mult-bounds/pull/4767). +The earlier comparison with three independent marginals does not imply +this stronger two-block inequality. [PROOF.md](PROOF.md) cites the triple, +pair and marginal laws, derives the new ratio, and proves its uniform +tail for m>=43. Forty exact integer comparisons cover 3<=m<=42. +At m=4, the ratio of the joint probability to the block product is 40/189. +The result holds for each permutation of the split by symmetry. + +## Reproduction and evidence + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-triple-block-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-triple-block-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-triple-block-correlation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-triple-block-correlation --check-source-history +``` + +Another CPython 3.12 interpreter can replace the local path. The direct +verifier prints `PASS_CORANKONE_TRIPLE_BLOCK_CORRELATION` in generated JSON. +It writes no files, uses only the standard library, and hashes all six +package files. Its receipt enumerates each finite proof case with its +positive integer gap and exact rational ratio. Nothing is handwritten +as a verification receipt. + +The checks cover all 40 finite proof cases, all 86 additional dimensions +43<=m<=128, the exact integer constants of the uniform tail, and seven +controls. The controls detect grouped independence, a reversed leading +spectral sign, omission of the finite-GL correction, and four invalid +replay dimensions. Explicit checks remain active under optimized Python. +The three cited m=4 probabilities are 9/40, 1/80 and 1/1680. + +## Scope, credit and limits + +The counting laws are cited mathematical inputs, not the subject of an +independent audit. Nick Petalas's #4275 supplies the binary triple law, +#4261 the pair law, #4227 the marginal law, and #4767 the open grouped +question. Their exact retained-main source bytes are pinned as historical +provenance in SOURCES.json. The verifier imports no predecessor code and +has no external runtime inputs. The source-history check requires full +Git history; the direct verifier runs without Git. + +Cinna Davis supplied the BIT request context. Source527, commdata2338 and +Jose Manuel retain the normalizer lineage credit. Chris R / Clear1nsight +retains the earlier #3950 counting context. The original card is +explicitly changed from an interface-formalization task to this counting +side question in TASK.json. Its link to the project is the density of +headers shared by several requests. It supplies no physical caller. + +Only three fixed orthogonal kernel lines, binary arithmetic and complete +uniform headers are covered. No general negative-association theorem is +claimed. Odd fields, nonorthogonal kernels, larger blocks and restricted +header distributions remain outside scope. Selection, emission, dispatch, +dirty restoration, stock, precision and a complete paid physical invoice +are unknown. No new kappa, selected-frontier change, supplier admission or +complete multiplication theorem is claimed. Independent human and formal +proof-kernel review are unclaimed. Lean, Docker and selected cold replay +are unrun. Both registered package modes pass locally. Ruff 0.14.0 +E/F/B/UP and the AST function-size inspection also pass. + +The card's historical first command, `scripts/research_baseline.py`, raises +`KeyError: 'bit_lower'` on the changed selected certificate schema. The +current replacement, `scripts/research_selected_baseline.py`, passes with +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` at selected kappa 60403/20000000. +This is source-binding orientation, not a selected-construction replay. +The historical reporter is outside this package and is unchanged. + +The verifier has fixed finite loops, no recursion or dynamic code +execution, and functions below sixty lines. CPython dynamic allocation +deviates from fixed allocation. The declared dimension bound 128, +eight spectral terms, forty retained cases, seven controls and six source +files of at most one MiB each bound this read-only replay. Invalid-domain +controls exercise its bounds. Warnings are errors in both registered +modes. A future expansion must retain or replace these resource bounds. + +## Open next questions + +1. Does the full three-event Bernoulli vector satisfy negative association? + Compare E1 union E2 with E3 using `2p2-p3 < p1(2p1-p2)`. Together with + the proved split and pair inequalities, this would cover the remaining + increasing-event type on two coordinates. The union comparison is + not proved here. +2. Does the pair-versus-singleton inequality hold over odd finite fields? + Start with the cited all-field transfer at k=3 and its grouped ratio. + An odd-field triple closed form or another uniform bound is missing. +3. Can a producer use a shared header with a favorable complete paid bill? + Pin its kernel lines and actual header domain, then price selection, + emission, dispatch, restoration, precision and stock. No such producer + or complete invoice is supplied here. diff --git a/research/corankone-triple-block-correlation/SOURCES.json b/research/corankone-triple-block-correlation/SOURCES.json new file mode 100644 index 0000000000..c2af66e067 --- /dev/null +++ b/research/corankone-triple-block-correlation/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + }, + { + "path": "research/corankone-pair-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548", + "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0" + }, + { + "path": "research/projector-header-density/PROOF.md", + "usage": "provenance", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + }, + { + "path": "research/corankone-pair-correlation/README.md", + "usage": "provenance", + "git_blob": "33aace0134ce06acd03aaa8da1b5be72e353eaaa", + "sha256": "891669d5014588da4748501c08a35dc0828541f16fa4955e2a856fc4fdb607ea" + } + ] +} diff --git a/research/corankone-triple-block-correlation/TASK.json b/research/corankone-triple-block-correlation/TASK.json new file mode 100644 index 0000000000..318d1c3ca2 --- /dev/null +++ b/research/corankone-triple-block-correlation/TASK.json @@ -0,0 +1,123 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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 Pr(E1 E2 E3)=3, under one uniform complete GL_m header.", + "scope_change_reason": "Take the first bounded step in Open next question 1 of PR4767 as an original grouped counting inequality, rather than formalizing or auditing an existing theorem.", + "bottleneck_link": "This is a counting side result on shared-header density. Pairwise anticorrelation and the existing comparison with independent marginals do not settle a pair-versus-singleton demand. No physical caller or paid invoice is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved split inequality; package it without extending to union events, general negative association or odd fields.", + "outcome": "completed", + "evidence": "PROOF.md gives a uniform spectral bound for m>=43. verify.py enumerates all 40 finite proof cases for 3<=m<=42, corroborates the tail in 86 further dimensions, checks its exact constants and exercises seven mutation/domain controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the full three-event Bernoulli vector satisfy negative association?", + "why_it_matters": "The new AND split does not compare every increasing event on a two-coordinate block.", + "first_step": "Prove or refute 2p2-p3 < p1(2p1-p2), the comparison of E1 union E2 with E3.", + "blocked_by": "The union-event comparison is not proved here." + }, + { + "question": "Does the pair-versus-singleton inequality hold over odd finite fields?", + "why_it_matters": "Binary arithmetic is outside the retained odd-prime normalizer executable domain.", + "first_step": "Reduce the all-field k=3 transfer to a grouped probability bound.", + "blocked_by": "An odd-field triple closed form or uniform bound is missing." + }, + { + "question": "Can a physical producer exploit a shared header?", + "why_it_matters": "A joint density alone supplies no physical saving.", + "first_step": "Pin its kernel lines and header domain, then price selection, emission, dispatch, restoration, precision and stock.", + "blocked_by": "No producer or complete physical invoice is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131530", + "overlap": { + "checked_at_utc": "2026-10-22T19:48:53.802833+00:00", + "open_pr_records": 299, + "discussion_records": 3712, + "remote_pagination_complete": true, + "local_notes_searched": 109, + "head_note_paths": 6319, + "local_omissions": 6210, + "related_open_prs": [], + "limits": "Sparse local-note coverage is incomplete. Live open PR titles and bodies, latest handoff/account posts, active discussions, several distinctive all-main README searches and merged-PR searches supplemented it. No same-target result was found; absence of matches does not prove novelty. Predecessor PR4767 leaves this exact question open.", + "precommit_checked_at_utc": "2026-10-22T19:50:16.335717+00:00", + "refreshed_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "precommit_related_open_prs": [], + "active_distinct_claim": "The one-way-coupled two-request all-field correlation claim in #1166 differs in request count and kernel contract. It is outside this three-request orthogonal-kernel split." + } +} diff --git a/research/corankone-triple-block-correlation/VERIFY.json b/research/corankone-triple-block-correlation/VERIFY.json new file mode 100644 index 0000000000..2f2e3f6139 --- /dev/null +++ b/research/corankone-triple-block-correlation/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Forty exact finite proof cases, 86 tail corroborations, uniform-tail constants, seven mutation/domain controls and six-file hash receipt; read-only." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Forty exact finite proof cases, 86 tail corroborations, uniform-tail constants, seven mutation/domain controls and six-file hash receipt; read-only." + } + ] +} diff --git a/research/corankone-triple-block-correlation/verify.py b/research/corankone-triple-block-correlation/verify.py new file mode 100644 index 0000000000..a672fc5f1f --- /dev/null +++ b/research/corankone-triple-block-correlation/verify.py @@ -0,0 +1,183 @@ +#!/usr/bin/env python3 +"""Check the new grouped inequality, using cited probability formulas. + +Produced by Nick Petalas. Apache-2.0. +""" + +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path + + +MAX_DIMENSION = 128 +TAIL_START = 42 +TRIPLE_TERMS = ( + (27, 1), + (21, -6), + (19, 6), + (17, -6), + (15, 16), + (13, -18), + (11, 9), + (9, -2), +) +FILES = ( + "PROOF.md", + "README.md", + "SOURCES.json", + "TASK.json", + "VERIFY.json", + "verify.py", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def power_sums(m): + require(type(m) is int and 3 <= m <= MAX_DIMENSION, "invalid replay dimension") + n = m - 1 + pair = 9**n - 2 * 7**n + 5**n + triple = sum(coefficient * base**n for base, coefficient in TRIPLE_TERMS) + block = 3**n * pair + require(pair > 0 and triple >= 0, "cited count outside its probability range") + require(block == 27**n - 2 * 21**n + 15**n, "pair normalization failed") + return n, block, triple + + +def probabilities(m): + n, block, triple = power_sums(m) + size = 2**m + single = Fraction(3**n, (size - 1) * 2**n) + pair = Fraction(block // 3**n, (size - 1) * (size - 2) * 2 ** (2 * n)) + joint = Fraction(triple, (size - 1) * (size - 2) * (size - 4) * 2 ** (3 * n)) + require(0 <= joint <= pair <= single <= 1, "invalid probability ordering") + return single, pair, joint + + +def check_split(single, pair, joint): + require(joint < pair * single, "strict grouped inequality failed") + return joint / (pair * single) + + +def check_dimensions(): + finite = [] + tail_cases = 0 + for m in range(3, MAX_DIMENSION + 1): + n, block, triple = power_sums(m) + size = 2**m + ratio = check_split(*probabilities(m)) + require( + ratio == Fraction((size - 1) * triple, (size - 4) * block), + "finite-GL ratio normalization failed", + ) + gap = (size - 4) * block - (size - 1) * triple + require(gap > 0, "integer gap is not positive") + if n < TAIL_START: + finite.append( + {"m": m, "integer_gap": gap, "joint_over_pair_single": str(ratio)} + ) + else: + x = Fraction(7, 9) ** n + require(ratio < (1 - 3 * x) * (1 + x) < 1, "tail bound failed") + tail_cases += 1 + require(len(finite) == 40 and tail_cases == 86, "dimension coverage changed") + return finite, tail_cases + + +def check_tail_constants(): + residual = TRIPLE_TERMS[2:] + require( + sum(abs(coefficient) for _, coefficient in residual) == 57, + "spectral remainder bound changed", + ) + require(max(base for base, _ in residual) == 19, "spectral remainder base changed") + require(57 * 19**TAIL_START < 21**TAIL_START, "tail cutoff is insufficient") + require(3 * 7**TAIL_START < 9**TAIL_START, "tail upper bound is not positive") + require(2 * 9**2 < 14**2, "geometric GL comparison base failed") + return { + "n_start": TAIL_START, + "remainder_weight": 57, + "remainder_base": 19, + "cutoff_left": 57 * 19**TAIL_START, + "cutoff_right": 21**TAIL_START, + } + + +def check_controls(): + single, pair, joint = probabilities(4) + require( + (single, pair, joint) == (Fraction(9, 40), Fraction(1, 80), Fraction(1, 1680)), + "cited m=4 fixture changed", + ) + mutations = (pair * single, joint + Fraction(12 * 21**3, 15 * 14 * 12 * 2**9)) + for mutated_joint in mutations: + try: + check_split(single, pair, mutated_joint) + except ValueError as error: + require( + str(error) == "strict grouped inequality failed", + "wrong mutation rejection", + ) + else: + raise ValueError("grouped-independence/sign mutant survived") + _, block, triple = power_sums(4) + require( + joint / (pair * single) != Fraction(triple, block), + "missing finite-GL correction went undetected", + ) + for invalid in (2, MAX_DIMENSION + 1, 3.0, True): + try: + power_sums(invalid) + except ValueError as error: + require(str(error) == "invalid replay dimension", "wrong domain rejection") + else: + raise ValueError("invalid replay dimension accepted") + require( + check_split(single, pair, joint) == Fraction(40, 189), + "split ratio fixture changed", + ) + return [ + "grouped independence", + "leading-mode sign", + "finite-GL correction", + "dimension below domain", + "dimension above bound", + "noninteger dimension", + "boolean dimension", + ] + + +def main(): + tail = check_tail_constants() + finite, tail_cases = check_dimensions() + controls = check_controls() + package = Path(__file__).resolve().parent + hashes = {} + for name in FILES: + path = package / name + require( + path.stat().st_size <= 1024 * 1024, "package file exceeds receipt bound" + ) + hashes[name] = sha256(path.read_bytes()).hexdigest() + print( + json.dumps( + { + "status": "PASS_CORANKONE_TRIPLE_BLOCK_CORRELATION", + "finite_proof_cases": finite, + "tail_corroboration_cases": tail_cases, + "tail_constants": tail, + "controls": controls, + "sha256": hashes, + }, + sort_keys=True, + indent=2, + ) + ) + + +if __name__ == "__main__": + main()