From c16deb7f640e2833097d8fd67e83ec179156aba5 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:24:25 +0100 Subject: [PATCH] feat(research): prove all-field corank-one pair anticorrelation --- research/corankone-pair-correlation/PROOF.md | 92 +++++++++++ research/corankone-pair-correlation/README.md | 116 +++++++++++++ .../corankone-pair-correlation/SOURCES.json | 50 ++++++ research/corankone-pair-correlation/TASK.json | 153 ++++++++++++++++++ .../corankone-pair-correlation/VERIFY.json | 32 ++++ research/corankone-pair-correlation/verify.py | 124 ++++++++++++++ 6 files changed, 567 insertions(+) create mode 100644 research/corankone-pair-correlation/PROOF.md create mode 100644 research/corankone-pair-correlation/README.md create mode 100644 research/corankone-pair-correlation/SOURCES.json create mode 100644 research/corankone-pair-correlation/TASK.json create mode 100644 research/corankone-pair-correlation/VERIFY.json create mode 100644 research/corankone-pair-correlation/verify.py diff --git a/research/corankone-pair-correlation/PROOF.md b/research/corankone-pair-correlation/PROOF.md new file mode 100644 index 0000000000..fd2522be59 --- /dev/null +++ b/research/corankone-pair-correlation/PROOF.md @@ -0,0 +1,92 @@ +# Strict pair correlation over every finite field + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K be a finite field of order q and m >= 2. Let U,V be rank-one +idempotents on K^m with UV=VU=0. Set P=I-U and Q=I-V. Choose G uniformly +from the complete group GL_m(K). Let A and B be the events that every +leading principal minor, through rank m-1, of GPG^-1 and GQG^-1, +respectively, is nonzero. Write p=Pr(A)=Pr(B) and J=Pr(A and B). + +Then + +```text +J < (1 - q^(-m)) p^2 < p^2. +``` + +In particular the two indicator variables have strictly negative covariance, +with Cov(1_A,1_B) < -q^(-m) p^2. This is a scoped algebraic proof using +the cited counting laws. It answers Open next question 1 of #4747. The +binary and ternary strict-correlation results were already proved in #4261 +and #4273, respectively. The all-field conclusion is the new result. + +## Cited formulas and their normalization + +Use Nick Petalas's marginal theorem in #4227 and joint theorem in #4747, +the latter pinned at f51dcebce79b8b8958427a9a9b7bc8feca352c9d. We use these +as predecessor results, without auditing or replaying their counting proofs. +Put n=m-1 >= 1 and + +```text +s = q^2-q+1, alpha=s^2, beta=q^3-q+1, gamma=q^3-q^2+1. + +p = (q-1) s^n / [q^n (q^(n+1)-1)], + +J = (q-1)^2 (alpha^n - 2 beta^n + gamma^n) + / [q^(2n) (q^(n+1)-1)(q^(n+1)-q)]. +``` + +All denominators are positive, and p>0. Division gives + +```text +J/p^2 = [(q^(n+1)-1)/(q^(n+1)-q)] + * [1 - (2 beta^n - gamma^n)/alpha^n]. (1) +``` + +## The comparison + +For every real q >= 2, the following factorizations are positive: + +```text +beta - gamma = q(q-1) > 0, +q beta - alpha = (q-1)(2q^2-2q+1) > 0. +``` + +Also gamma=q^2(q-1)+1>0 and alpha>0. Since n is a positive integer, + +```text +2 beta^n - gamma^n > beta^n > alpha^n/q^n. (2) +``` + +Insert (2) into (1), multiplying only by positive quantities: + +```text +J/p^2 < [(q^(n+1)-1)/(q^(n+1)-q)] (1-q^(-n)) + = (q^(n+1)-1)/q^(n+1) + = 1-q^(-m). +``` + +This proves the quantitative bound in every characteristic, including +nonprime fields. No finite cutoff, estimate of a remainder, or untested +interval is used. The algebraic comparison itself holds for every integer +q >= 2, while its probability interpretation requires q to be a prime power. + +At q=2,m=2 the cited joint fraction is zero, which satisfies the strict +bound because p>0. No positive-common-header assumption is needed. + +## Scope + +Uniform sampling from the complete GL group is essential. For example, +over F_3 with m=2, take U=diag(1,0), V=diag(0,1), and the single header +G=[[1,1],[1,2]]. Its inverse is [[2,2],[2,1]]. Both conjugated requests +have first diagonal entry 2, so both pass. Restricting the domain to this +one header gives J=p=1, violating the displayed bound. Thus this theorem +cannot price an arbitrary restricted header catalogue. + +Nothing here supplies header selection, emission, dispatch, dirty +restoration, stock, precision or a complete physical caller. Those costs +remain unknown. No new kappa, supplier admission, selected-frontier change +or complete multiplication theorem is claimed. Independent human and +formal proof-kernel review are unclaimed. diff --git a/research/corankone-pair-correlation/README.md b/research/corankone-pair-correlation/README.md new file mode 100644 index 0000000000..33aace0134 --- /dev/null +++ b/research/corankone-pair-correlation/README.md @@ -0,0 +1,116 @@ +# Strict corank-one pair correlation over every finite field + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. For two +requests I-U,I-V with orthogonal rank-one kernels on F_q^m, m>=2, and +uniformly weighted complete GL_m headers, let A,B be their full-leading-minor +passing events. Then + +```text +Pr(A and B) < (1-q^(-m)) Pr(A)Pr(B) < Pr(A)Pr(B). +``` + +[PROOF.md](PROOF.md) answers Open next question 1 of +[#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747). +It cites that predecessor's joint law and #4227's marginal law, then proves +the new inequality by two positive polynomial factorizations. The binary +and ternary strict-correlation cases retain #4261 and #4273's credit. +There is no cutoff or unrun infinite tail in the written proof. + +## 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-pair-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-pair-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-pair-correlation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-pair-correlation --check-source-history +``` + +The direct verifier emits `PASS_CORANKONE_PAIR_CORRELATION` in generated +JSON with hashes of all six package files. It writes no receipt or other +file. Its evidence covers: + +- Exact integer and rational comparisons for all 4,032 pairs + 2<=q<=64, 2<=m<=65. Non-prime-power integers test the algebra only. + This checks the new comparison and normalization, not the predecessor + counting proofs. +- An exact polynomial coefficient identity for + q beta-alpha=(q-1)(2q^2-2q+1), independent of evaluations at chosen q. +- Nine controls covering independence, two correction-term mutations, + restricted header domains and five invalid replay inputs. A separate + reversed-polynomial-sign check also rejects its mutant. +- Exact joint-to-product ratios 28/243 at q=2,m=3, 24/49 at q=3,m=2, + and 40/49 at q=5,m=2. These preserve the predecessor numerical values. + +The written proof quantifies over every finite field and dimension. The +finite checks corroborate it; they are not formal proof-kernel acceptance. + +## Scope and remaining obligations + +This is an original consequence of cited formulas, not an independent audit +of them. Pending #4747 is an explicit mathematical dependency, pinned in +[SOURCES.json](SOURCES.json); no predecessor code or proof file is imported +at runtime. The source manifest binds retained-main provenance through +exact Git objects. +Its separate external citation records the pending theorem by immutable URL +and hash; the framework does not validate that bibliography entry. + +The result assumes two orthogonal rank-one kernels and the complete uniform +header domain. Nonorthogonal kernels, restricted domains and three or more +requests are outside scope. PROOF.md gives a singleton-domain counterexample +to extending the inequality to restricted catalogues. + +No producer, selection/emission, dispatch, dirty restoration, stock, +precision or complete physical invoice is supplied. These costs remain +unknown. No new kappa, supplier admission, selected-frontier change or +complete multiplication theorem is claimed. Independent human and formal +proof-kernel review are unclaimed. Selected cold replay, Lean and Docker +are unrun. Both registered package commands passed locally. + +The verifier has fixed finite loops, no recursion and functions below +60 lines. CPython's required dynamic allocation is a deviation from fixed +allocation. Its scope is this bounded, read-only finite replay, with at most +one parameter pair active, six file hashes, three retained examples and +polynomials of at most seven coefficients. The declared q,m limits bound +integer sizes. Invalid-domain controls exercise exhaustion behavior. +Warnings are errors in both registered modes. Ruff E/F/B/UP passes locally. +Follow-up: retain these bounds if adding replay inputs; a larger search +needs a fresh resource bound. + +## Related work and credit + +- Nick Petalas's [#4747](https://github.com/CrocSwap/integer-mult-bounds/pull/4747), + head f51dcebce79b8b8958427a9a9b7bc8feca352c9d, supplies the all-field + joint law. At q=5,m=2, J=2/5 and p=7/10 give ratio 40/49, checked here. +- Nick Petalas's #4227 supplies the marginal law. #4261 and #4273 supply + the binary and ternary pair laws and their strict negative correlation. + New here is the all-field inequality and its explicit relative gap. +- #4599 and Ryanson Jonathan's #4607 prove binary four- and five-request + product inequalities. Ryanson Jonathan's #4606 independently checks the + four-event inequality. Their request counts differ from this two-event + theorem; no four- or five-event number is claimed here. +- Ryanson Jonathan's #4605 recounts binary threshold headers. At its + overlapping k=2,m=3 case, J=1/84 and p=9/28 give ratio 28/243, + checked here; 168J=2 headers. +- Nick Petalas's #4598 and Ryanson Jonathan's #4619 count and classify + five-request threshold decompositions. Their k=5 counts do not overlap + this two-request theorem. + +The earlier counting packages above are produced by Nick Petalas unless +otherwise attributed. Cinna Davis supplies the BIT request context; +source527, commdata2338 and Jose Manuel retain the normalizer lineage credit. +The card's scope change and overlap coverage are recorded in TASK.json. + +## Open next questions + +1. Does negative association hold for disjoint groups in larger orthogonal + kernel families? First compare Pr(A1 A2 A3) with Pr(A1 A2)Pr(A3) using + #4275's binary three-request law. Pairwise negative correlation alone + does not imply this stronger property. +2. Can an actual odd-field producer exploit a shared header with a complete + paid invoice? Pin its kernel lines and header domain before charging + selection, emission, dispatch, restoration and stock. No caller is + supplied here. diff --git a/research/corankone-pair-correlation/SOURCES.json b/research/corankone-pair-correlation/SOURCES.json new file mode 100644 index 0000000000..4716876627 --- /dev/null +++ b/research/corankone-pair-correlation/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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", + "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/projector-header-density/PROOF.md", + "git_blob": "d434098ed952493ee2ef6b39b547fb4b8a790f8d", + "sha256": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262" + }, + { + "path": "research/corankone-pair-header-law/PROOF.md", + "usage": "provenance", + "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/corankone-pair-header-law/PROOF.md", + "git_blob": "2493784dba9f7a6b9251df6c2ea3b7bea1eb3548", + "sha256": "8e0c312af799f42e4a66a79ff9f1658761b55de4f1c732c700eec583a8ce21d0" + }, + { + "path": "research/ternary-corankone-pair-law/PROOF.md", + "usage": "provenance", + "pin": "head:b58ad9ef4d4e861b0eaa5dba41742bdc072dca51:research/ternary-corankone-pair-law/PROOF.md", + "git_blob": "c91f551dcf370de1c5d2860d3c75e74bc1d88d6e", + "sha256": "096b3acfd46f905553f3145f5714d57a7f0141028c50fad04eea0ec4b252564f" + } + ], + "external_citations": [ + { + "description": "Cited joint-law theorem, not imported code or machine-validated provenance. The source-history gate applies to files only.", + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4747", + "commit": "f51dcebce79b8b8958427a9a9b7bc8feca352c9d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f51dcebce79b8b8958427a9a9b7bc8feca352c9d/research/corankone-all-field-law/PROOF.md", + "path": "research/corankone-all-field-law/PROOF.md", + "git_blob": "ac0152e05a5c050bbd740ddbe6d0cbaaecbb6cd8", + "sha256": "ca7762bea269445f7b30c59c7b6161282483da5fd191faa668145f1ad6d8ade4" + } + ] +} diff --git a/research/corankone-pair-correlation/TASK.json b/research/corankone-pair-correlation/TASK.json new file mode 100644 index 0000000000..54c90da03e --- /dev/null +++ b/research/corankone-pair-correlation/TASK.json @@ -0,0 +1,153 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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 correlation, with relative deficit greater than q^(-m), for two full-guard corank-one requests with orthogonal kernels over every finite field and every m>=2.", + "scope_change_reason": "This takes explicit Open next question 1 of PR4747 as original algebraic work rather than formalizing or auditing an existing result. It is a counting side result, not a mechanism or supplier admission.", + "bottleneck_link": "Shared-header pricing cannot multiply the individual full-guard densities. The new inequality gives an all-field obstruction to that independence assumption; physical caller costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop immediately at the first proved all-field inequality; package its proof and exact finite corroboration without extending to larger families.", + "outcome": "completed", + "evidence": "PROOF.md derives J < (1-q^(-m))p^2 from two cited formulas and positive factorizations. verify.py checks the polynomial identity, 4032 integer parameter pairs, three cited numerical fixtures and explicit mutation/domain controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does negative association hold for disjoint groups of events in larger orthogonal-kernel families?", + "why_it_matters": "Pairwise negative correlation does not settle grouped shared-header demands.", + "first_step": "Compare the binary three-event probability in PR4275 with the pair law times the marginal.", + "blocked_by": "No negative-association theorem is supplied; joint laws for grouped events are needed." + }, + { + "question": "Can a real odd-field producer use a fully charged shared-header caller?", + "why_it_matters": "A probability inequality alone yields no physical saving.", + "first_step": "Pin the producer and header domain, then charge selection, emission, dispatch, restoration and stock.", + "blocked_by": "No producer or complete physical invoice is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131124", + "overlap": { + "checked_at_utc": "2026-10-22T19:23:41.647699+00:00", + "open_pr_records": 521, + "discussion_records": 3678, + "remote_pagination_complete": true, + "local_notes_searched": 105, + "head_note_paths": 5860, + "local_omissions": 5757, + "limits": "Sparse local coverage is incomplete; targeted all-main README and merged PR searches supplement it. No absence of matches is a novelty certificate. All related live PR titles and bodies were read. Full bodies of all seven directly related PRs were read; their live states and exact heads were refreshed before committing.", + "related_open_prs": [ + 4747, + 4619 + ], + "related_prs": [ + { + "number": 4747, + "state": "OPEN", + "head": "f51dcebce79b8b8958427a9a9b7bc8feca352c9d" + }, + { + "number": 4598, + "state": "MERGED", + "head": "c80f445e8c3c22d341d467254b89245fbddb9eb2" + }, + { + "number": 4599, + "state": "MERGED", + "head": "19ca650c67ad2722790dc60c0bfd12989479b06a" + }, + { + "number": 4605, + "state": "MERGED", + "head": "fe99331d0735c7a3d61babedb003188a1bfaa815" + }, + { + "number": 4606, + "state": "MERGED", + "head": "3bd2fdd9632841bf8d25b0baa09b81a7b8d1e8f8" + }, + { + "number": 4607, + "state": "MERGED", + "head": "00f4eebeb11dec452082131fe102d077d786cdd9" + }, + { + "number": 4619, + "state": "OPEN", + "head": "0f62abfdbb7e24659b218aa20cfbaefc7d771f4b" + } + ] + } +} diff --git a/research/corankone-pair-correlation/VERIFY.json b/research/corankone-pair-correlation/VERIFY.json new file mode 100644 index 0000000000..fe238d8091 --- /dev/null +++ b/research/corankone-pair-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": "Exact polynomial identity and 4032 inequality comparisons, three overlap fixtures, mutation/domain controls and package SHA256 receipt; read-only." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical explicit checks under optimized Python; read-only." + } + ] +} diff --git a/research/corankone-pair-correlation/verify.py b/research/corankone-pair-correlation/verify.py new file mode 100644 index 0000000000..382e175fa5 --- /dev/null +++ b/research/corankone-pair-correlation/verify.py @@ -0,0 +1,124 @@ +"""Exact corroboration of the new correlation inequality; no file writes.""" + +from fractions import Fraction +from hashlib import sha256 +import json +from pathlib import Path + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def multiply(left: tuple[int, ...], right: tuple[int, ...]) -> tuple[int, ...]: + need(1 <= len(left) <= 4 and 1 <= len(right) <= 4, "polynomial degree") + result = [0] * (len(left) + len(right) - 1) + for i, first in enumerate(left): + for j, second in enumerate(right): + result[i + j] += first * second + return tuple(result) + + +def polynomial_check() -> dict[str, list[int]]: + square = multiply((1, -1, 1), (1, -1, 1)) + qb = (0, 1, -1, 0, 1) + difference = tuple(qb[i] - square[i] for i in range(5)) + factorization = multiply((-1, 1), (1, -2, 2)) + (0,) + need(difference == factorization, "q beta - alpha factorization") + need(difference != (0, -1, 3, -2, 0), "reversed-sign control") + return {"alpha": list(square), "q_beta_minus_alpha": list(difference)} + + +def probabilities(q: int, m: int) -> tuple[Fraction, Fraction]: + need(type(q) is int and 2 <= q <= 64, "q outside finite replay domain") + need(type(m) is int and 2 <= m <= 65, "m outside finite replay domain") + n = m - 1 + s, beta, gamma = q * q - q + 1, q**3 - q + 1, q**3 - q * q + 1 + marginal = Fraction((q - 1) * s**n, q**n * (q**m - 1)) + joint = Fraction( + (q - 1) ** 2 * (s ** (2 * n) - 2 * beta**n + gamma**n), + q ** (2 * n) * (q**m - 1) * (q**m - q), + ) + return marginal, joint + + +def compare(q: int, m: int) -> Fraction: + marginal, joint = probabilities(q, m) + n, total = m - 1, q**m + alpha = (q * q - q + 1) ** 2 + beta, gamma = q**3 - q + 1, q**3 - q * q + 1 + need(beta - gamma == q * (q - 1) > 0, "ordered correction bases") + need(q * beta - alpha == (q - 1) * (2 * q * q - 2 * q + 1) > 0, + "positive factored polynomial") + need(q**n * (2 * beta**n - gamma**n) > alpha**n, "power comparison") + ratio = joint / marginal**2 + expression = Fraction( + (total - 1) * (alpha**n - 2 * beta**n + gamma**n), + (total - q) * alpha**n, + ) + need(ratio == expression, "ratio algebra") + need(0 <= joint <= marginal <= 1, "probability ranges") + need(ratio < Fraction(total - 1, total) < 1, "strict quantitative bound") + return ratio + + +def controls() -> int: + q, m = 5, 2 + marginal, joint = probabilities(q, m) + upper = Fraction(q**m - 1, q**m) * marginal**2 + need(not marginal**2 < upper, "independence control") + alpha, beta, gamma = 441, 121, 101 + denominator = q**2 * (q**m - 1) * (q**m - q) + for wrong_sum in (alpha + gamma, alpha - 2 * gamma + beta): + mutant = Fraction((q - 1) ** 2 * wrong_sum, denominator) + need(not mutant < upper, "correction-term mutation") + header, inverse = ((1, 1), (1, 2)), ((2, 2), (2, 1)) + for i in range(2): + for j in range(2): + entry = sum(header[i][k] * inverse[k][j] for k in range(2)) % 3 + need(entry == int(i == j), "restricted-header inverse") + for kernel in range(2): + diagonal = header[0][1 - kernel] * inverse[1 - kernel][0] % 3 + need(diagonal == 2, "singleton full guard") + need(not Fraction(1) < Fraction(8, 9), "restricted-header control") + rejected = 0 + for args in ((1, 2), (5, 1), (65, 2), (5, 66), (2.0, 2)): + try: + probabilities(*args) + except ValueError: + rejected += 1 + need(rejected == 5, "finite-domain rejection controls") + need(joint == Fraction(2, 5), "cited q=5,m=2 fixture") + return 4 + rejected + + +def main() -> None: + polynomials = polynomial_check() + cases = 0 + for q in range(2, 65): + for m in range(2, 66): + compare(q, m) + cases += 1 + fixtures = ((2, 3, Fraction(28, 243)), (3, 2, Fraction(24, 49)), + (5, 2, Fraction(40, 49))) + examples = [] + for q, m, expected in fixtures: + ratio = compare(q, m) + need(ratio == expected, "published overlap fixture") + examples.append({"q": q, "m": m, "joint_to_product": str(ratio)}) + control_count = controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + print(json.dumps({"status": "PASS_CORANKONE_PAIR_CORRELATION", + "claim_type": "scoped proof with finite corroboration", + "integer_parameter_cases": cases, "q_range": [2, 64], + "m_range": [2, 65], "controls": control_count, + "polynomial_identities": polynomials, "examples": examples, + "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()