From 19ca650c67ad2722790dc60c0bfd12989479b06a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 10:22:55 +0100 Subject: [PATCH] feat(research): prove the four-request header product inequality --- research/corankone-four-correlation/PROOF.md | 188 +++++++++++++++++ research/corankone-four-correlation/README.md | 120 +++++++++++ .../corankone-four-correlation/SOURCES.json | 24 +++ research/corankone-four-correlation/TASK.json | 85 ++++++++ .../corankone-four-correlation/VERIFY.json | 32 +++ research/corankone-four-correlation/verify.py | 195 ++++++++++++++++++ 6 files changed, 644 insertions(+) create mode 100644 research/corankone-four-correlation/PROOF.md create mode 100644 research/corankone-four-correlation/README.md create mode 100644 research/corankone-four-correlation/SOURCES.json create mode 100644 research/corankone-four-correlation/TASK.json create mode 100644 research/corankone-four-correlation/VERIFY.json create mode 100644 research/corankone-four-correlation/verify.py diff --git a/research/corankone-four-correlation/PROOF.md b/research/corankone-four-correlation/PROOF.md new file mode 100644 index 0000000000..6309eb879c --- /dev/null +++ b/research/corankone-four-correlation/PROOF.md @@ -0,0 +1,188 @@ +# Four binary full-guard events lie below the product of their marginals + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and dependencies + +Let m >= 4, and let U_1,...,U_4 be pairwise orthogonal rank-one idempotents +on F_2^m. Put P_t = I-U_t. Choose G uniformly from the complete group +GL_m(F_2). Event E_t means that every leading principal minor of +G P_t G^-1 of orders 1 through m-1 is nonzero. + +Write n=m-1, X=2^m, and + +```text +s_m = 3^n / [(X-1)2^n], +rho_m = Pr(E_1 intersect E_2 intersect E_3 intersect E_4) / s_m^4. +``` + +**Theorem.** For every m >= 4, + +```text +Pr(E_1 intersect E_2 intersect E_3 intersect E_4) < s_m^4. +``` + +Moreover, + +```text +1-rho_m = 12(7/9)^n + O((19/27)^n), +lim_(m->infinity) (1-rho_m)/(7/9)^n = 12. +``` + +This is a scoped counting proof with an exact finite component. It answers +k=4 of Open next question 2 in #4275. The theorem does not assert negative +association for arbitrary functions or arbitrary groups of events. + +The marginal s_m is the corank-one law of Nick Petalas's #4227. The joint +character law is Theorem 2 of Nick Petalas's #4275, retained at canonical +main f626db5c3a3d781d8f7695038776c621651f75e1 in +`research/corankone-triple-header-law/PROOF.md`. These theorems are cited +steps, not new results or audit deliverables here. SOURCES.json binds the +exact predecessor proof. The new result is the four-event inequality and +the leading correlation deficit. The character calculation below is the +finite component needed for that new inequality. + +## 1. Normalize the joint law + +Let c run over the 4-by-4 binary matrices with zero diagonal. There are +2^12=4096 such characters. Define + +```text +Z(c) = sum_(sigma in {0,1,2}^4) + (-1)^(sum_(i,j: sigma_i=1, sigma_j=2) c_ij), +N_n = sum_c (-1)^|c| Z(c)^n. +``` + +The cited character law gives a numerator C_n=N_n/4096 and denominator + +```text +D_m = (X-1)(X-2)(X-4)(X-8) 2^(4m-16). +``` + +Consequently, with all powers of two canceled exactly, + +```text +rho_m = (N_n/81^n) H(X), +H(X) = (X-1)^3 / [(X-2)(X-4)(X-8)]. (1) +``` + +The finite-GL factor H(X) is greater than one. It cannot be dropped when +proving the product inequality. + +## 2. Exact finite character calculation + +Grouping every character by Z(c) gives the following signed multiplicities +b_z, so that N_n=sum_z b_z z^n. Zero signed multiplicities are omitted. + +```text + z b_z z b_z +81 1 37 228 +63 -12 35 -336 +57 24 33 399 +55 -8 31 -444 +51 -24 29 502 +49 18 27 -548 +47 -48 25 523 +45 118 23 -332 +43 -68 21 144 +41 85 19 -48 +39 -180 17 6 +``` + +The finite calculation is independently executable in two forms in +verify.py. `literal_characters` evaluates the definition of Z(c) on all +4096 characters, each over all 81 ternary assignments. `step_weights` +enumerates all 256 pairs x,y in F_2^4, retains disjoint supports, and counts +their zero-diagonal rectangles y x^T. Its XOR-convolution transform, +computed by twelve exact Hadamard stages, agrees character by character. +The signed table then follows by weighting each character by (-1)^|c|. +A direct integer walk without diagonalization corroborates C_n for +0 <= n <= 12. No sampled character or floating-point arithmetic is used. + +In particular, + +```text +N_n = 81^n - 12*63^n + R_n, +|R_n| <= 4083*57^n, (2) +``` + +because the absolute signed multiplicities below 63 sum to 4083 and their +largest base is 57. The signed spectrum itself is predecessor counting +data; its use to settle the four-event inequality is the contribution. + +## 3. All large dimensions + +Put x=(7/9)^n. The exact integer inequality + +```text +4083*57^84 < 63^84 +``` + +and monotonicity of (57/63)^n show, for every n >= 84, that + +```text +N_n/81^n <= 1-11x. (3) +``` + +For X >= 32 the denominator of H(X) is at least + +```text +(15/16)(7/8)(3/4) X^3 = (315/512) X^3. +``` + +Its numerator minus its denominator is 11X^2-53X+63 <= 11X^2. +Since 11*512 < 18*315, + +```text +H(X)-1 < 18/X = 9/2^n. (4) +``` + +The exact inequality 9*9^84 < 14^84 and monotonicity show that +9/2^n < x for every n >= 84. Also 11*7^84 < 9^84, so 1-11x is +positive there. Combining (1), (3), and (4) gives + +```text +rho_m < (1-11x)(1+x) = 1-10x-11x^2 < 1. +``` + +This proves the theorem for m >= 85. All constants in this argument are +checked with exact integers by `proof_checks`. + +## 4. Remaining finite dimensions + +For every integer 4 <= m <= 84, `proof_checks` evaluates the character +count and the fractions in (1), then checks the strict rational inequality +Pr(intersection E_t)=4, with no unchecked interval. This is a computer-assisted finite +component of a written proof, without a proof-kernel certificate. + +## 5. Leading deficit + +Equation (2) gives + +```text +N_n/81^n = 1-12(7/9)^n + O((19/27)^n). +``` + +Equation (4) gives H(X)=1+O(2^-n). Since 1/2<19/27<7/9, multiplying these +expressions in (1) proves the asserted deficit and limit. The limit is an +analytic consequence of the bounds, rather than a numerical extrapolation. + +## Scope + +The theorem requires exactly four fixed, pairwise orthogonal rank-one +kernel projectors over F_2 and uniform weighting of complete GL headers. +It does not settle k>=5, odd characteristic, restricted header covers, +nonorthogonal kernels or general dependence properties. The minimal-dimension +classification reserved by another contributor is not a deliverable here. + +Binary header arithmetic extends beyond the retained odd-prime normalizer's +executable domain. A producer, header selection/emission, dispatch, dirty +restoration, stock, precision and complete physical caller remain open. +Their costs are unknown. No supplier, new kappa or complete multiplication +theorem follows from this density inequality. diff --git a/research/corankone-four-correlation/README.md b/research/corankone-four-correlation/README.md new file mode 100644 index 0000000000..b5c890357f --- /dev/null +++ b/research/corankone-four-correlation/README.md @@ -0,0 +1,120 @@ +# Four binary full-guard events are strictly below independent marginals + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: **scoped counting proof with an exact finite component**. +For four pairwise orthogonal rank-one idempotents U_t on F_2^m, put +P_t=I-U_t. Under one uniform complete GL_m(F_2) header, let E_t mean that +all leading-minor guards through rank m-1 pass. For every m>=4, + +```text +Pr(E_1 intersect E_2 intersect E_3 intersect E_4) + < [3^(m-1)/((2^m-1)2^(m-1))]^4. +``` + +If rho_m is the joint fraction divided by that product, then + +```text +1-rho_m = 12(7/9)^(m-1) + O((19/27)^(m-1)). +``` + +This answers k=4 of Open next question 2 in +[#4275](https://github.com/CrocSwap/integer-mult-bounds/pull/4275). +That predecessor proves k<=3 and supplies the character law and k=4 +spectrum. The new result proves the four-event product inequality and its +leading deficit. It is original successor work, with the predecessor laws +cited as steps. No new kappa or selected-frontier change is claimed. + +[PROOF.md](PROOF.md) combines a uniform spectral tail bound for m>=85 with +81 exact rational comparisons covering 4<=m<=84. The first positive joint +fraction is 1/208320 at m=5; its marginal is 81/496. + +## Reproduction and evidence + +From the repository root, replace this local path with another CPython +3.12 interpreter if needed: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-four-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-four-correlation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-four-correlation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-four-correlation --check-source-history +``` + +The scientific marker is `PASS_CORANKONE_FOUR_CORRELATION`. The generated +stdout JSON enumerates all 81 finite comparisons and both character +multiplicities, and binds all six package files by SHA256. No receipt is +handwritten or stored. The verifier writes no files and uses only Python's +standard library. There are no live external inputs or imported predecessor +code. Historical provenance is pinned in SOURCES.json. + +The executable finite component checks: + +- All 4096 characters, with all 81 ternary assignments per character, agree + with the Hadamard transform of independently generated factor weights. +- A direct integer convolution agrees with the spectral count at every + n=0..12, without using diagonalization. +- All 81 finite product inequalities and the exact constants for the + uniform proof pass. The asymptotic coefficient 12 follows analytically. +- Five controls detect independence, a missing finite-GL correction, a + wrong zero-factor eigenvalue, its changed positive count, and a missing + leading negative mode. + +The loops have fixed finite bounds. The largest state vector has 4096 +integers and walk depth is at most twelve. No function exceeds sixty lines +and no recursion or dynamic code execution is used. CPython allocates +integers and containers dynamically; fixed character, dimension and walk +bounds constrain this managed-runtime deviation from fixed allocation. +Warnings are errors in both registered modes. Independent human and formal +proof-kernel review are unclaimed. + +Local CPython 3.12.15 on macOS arm64 passes both registered commands. +Direct normal and optimized checks each took 0.12 seconds, below their +120-second registered limits; these are check durations. Ruff 0.14.0 +E/F/B/UP and the AST syntax/function-size inspection also pass. + +## Limitations + +Only four fixed orthogonal kernel lines over F_2 and uniform complete +headers are covered. This is a four-event product inequality, without an +assertion of general negative association. k>=5 and odd fields remain +open. Binary arithmetic is outside the retained odd-prime normalizer's +executable domain. No producer, header selection/emission, dispatch, dirty +return, stock, precision or fully charged physical caller is supplied. +Unknown costs are not zero. Selected cold replay, Lean, Docker and a full +multiplication theorem were not run or claimed. + +The card's baseline binding check reached the selected source validation, +which passes at kappa 23/10000, but its old arithmetic summary raises +`KeyError: 'bit_lower'` on the selected productive-helper certificate. +This unrelated orientation incompatibility is not changed here. The +registered scientific checks are self-contained. + +## Related work and credit + +- Nick Petalas's [#4275](https://github.com/CrocSwap/integer-mult-bounds/pull/4275) + supplies the all-k character law, its k=4 signed spectrum and the k<=3 + product inequalities. The new theorem settles k=4 for every dimension. +- Nick Petalas's [#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227) + supplies the single corank-one marginal used in the comparison. +- The concurrent minimal-dimension rectangle question from #4275 is + separate from this dependence question. No classification is claimed. +- Cinna Davis supplies the #4100 BIT request context. Source527, + commdata2338 and Jose Manuel retain normalizer and recursive-closure + credit. No predecessor credit or frozen package is changed. + +Live PRs, recent handoff claims, local reservations, main README searches +and merged-title/body searches were consulted. They are partial overlap +coverage, without a novelty guarantee. TASK.json records the explicit +scope change from the audit card to original counting work. + +## Open next questions + +1. Does the product inequality hold for every k>=5? The next useful step + is a structural bound on the nontrivial character eigenvalues and + their signed multiplicities. A larger table alone is not a uniform + proof. This package only settles k=4. +2. Can an actual producer use a fully charged shared-header caller? + Start by pinning its kernel lines and header domain, then price + selection, emission, dispatch, dirty restoration and stock. No such + producer or complete invoice is supplied here. diff --git a/research/corankone-four-correlation/SOURCES.json b/research/corankone-four-correlation/SOURCES.json new file mode 100644 index 0000000000..ff176ead90 --- /dev/null +++ b/research/corankone-four-correlation/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + } + ] +} diff --git a/research/corankone-four-correlation/TASK.json b/research/corankone-four-correlation/TASK.json new file mode 100644 index 0000000000..0f6dde844e --- /dev/null +++ b/research/corankone-four-correlation/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "For four binary corank-one requests with pairwise orthogonal rank-one kernels, prove the joint full-guard probability is strictly below the product of marginals in every m>=4, and prove the leading relative deficit is 12(7/9)^(m-1).", + "scope_change_reason": "Original successor counting work on Open next question 2 of PR4275, using its character law as a cited step. This is not an audit of another result or a full supplier.", + "bottleneck_link": "Shared-header pricing requires joint probabilities. This proves a dependence penalty in a fixed binary model; physical caller costs remain unknown and kappa is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop after the four-event all-dimension product inequality and leading asymptotic deficit; package the first verified result without extending to k>=5.", + "outcome": "completed", + "evidence": "PROOF.md combines a uniform tail estimate for m>=85 with 81 exact finite comparisons. verify.py enumerates all 4096 characters by two evaluations and checks a separate bounded convolution.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the product inequality hold for every k>=5?", + "why_it_matters": "It would determine the shared-header dependence penalty for larger orthogonal-kernel families.", + "first_step": "Bound the nontrivial character eigenvalues and signed multiplicities structurally.", + "blocked_by": "Only k<=4 has an all-dimension product inequality." + }, + { + "question": "Can an actual producer use a fully charged shared-header caller?", + "why_it_matters": "A density calculation alone gives no physical saving.", + "first_step": "Pin a producer and header domain, then charge selection, emission, dispatch, dirty return and stock.", + "blocked_by": "No producer or complete physical invoice is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19119376", + "checked_main": "f626db5c3a3d781d8f7695038776c621651f75e1", + "overlap_coverage": "Live open PR bodies, recent handoff and active Discussion comments, own recent PRs, local claims, cached overlap tool, main README search and merged searches; historical and unpublished coverage partial." + } +} diff --git a/research/corankone-four-correlation/VERIFY.json b/research/corankone-four-correlation/VERIFY.json new file mode 100644 index 0000000000..432ba12eff --- /dev/null +++ b/research/corankone-four-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": "Complete 4096-character spectrum by two exact evaluations, direct convolution through n=12, all 81 finite product comparisons, uniform-tail constants and five controls; emits six-file hash-bound receipt without writing files." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite proof component and controls under optimized Python, using explicit checks." + } + ] +} diff --git a/research/corankone-four-correlation/verify.py b/research/corankone-four-correlation/verify.py new file mode 100644 index 0000000000..1bb4eef597 --- /dev/null +++ b/research/corankone-four-correlation/verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Exact finite component of the four-request correlation proof. + +Produced by Nick Petalas. Apache-2.0. +""" + +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +K = 4 +BITS = 12 +STATES = 1 << BITS +OFF = tuple((i, j) for i in range(K) for j in range(K) if i != j) +TERMS = { + 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, +} +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rectangle(y, x): + return sum(1 << bit for bit, (i, j) in enumerate(OFF) + if (y >> i) & (x >> j) & 1) + + +def step_weights(zero_weight=31): + """Enumerate all 256 factor pairs, retaining their disjoint supports.""" + weights = [0] * STATES + for y in range(1 << K): + for x in range(1 << K): + if not y & x: + weights[rectangle(y, x)] += 1 + need(weights[0] == 31 and sum(weights) == 81, "factor multiplicities") + weights[0] = zero_weight + return weights + + +def hadamard(weights): + """The twelve bounded butterfly stages diagonalize XOR convolution.""" + need(len(weights) == STATES, "Hadamard input size") + values = list(weights) + for stage in range(BITS): + width = 1 << stage + for start in range(0, STATES, 2 * width): + for offset in range(width): + a, b = start + offset, start + offset + width + left, right = values[a], values[b] + values[a], values[b] = left + right, left - right + return values + + +def literal_characters(): + """Evaluate the cited character sum directly over all 3^4 assignments.""" + masks = [] + for labels in product(range(3), repeat=K): + mask = sum(1 << bit for bit, (i, j) in enumerate(OFF) + if labels[i] == 1 and labels[j] == 2) + masks.append(mask) + need(len(masks) == 81, "ternary domain size") + return [sum(1 - 2 * ((character & mask).bit_count() % 2) + for mask in masks) for character in range(STATES)] + + +def spectral_data(): + eigenvalues = hadamard(step_weights()) + need(eigenvalues == literal_characters(), "two character evaluations") + signed = Counter() + unsigned = Counter(eigenvalues) + for character, value in enumerate(eigenvalues): + signed[value] += 1 - 2 * (character.bit_count() % 2) + signed = {value: count for value, count in signed.items() if count} + need(signed == TERMS, "complete signed spectrum") + need(sum(unsigned.values()) == STATES, "complete character domain") + need(unsigned[81] == 1 and unsigned[63] == 12, "leading modes") + need(min(eigenvalues) >= 0, "nonnegative spectrum") + return signed, unsigned + + +def count(n, terms=TERMS): + need(0 <= n <= 84, "declared count domain") + numerator = sum(mult * value ** n for value, mult in terms.items()) + need(numerator % STATES == 0, "integral Fourier count") + result = numerator // STATES + need(result >= 0, "nonnegative count") + return result + + +def walk_counts(maximum, zero_weight=31): + """A separate integer convolution check, without diagonalization.""" + need(0 <= maximum <= 12, "bounded walk depth") + moves = tuple((mask, weight) for mask, weight in + enumerate(step_weights(zero_weight)) if weight) + state = [0] * STATES + state[0] = 1 + results = [state[-1]] + for _ in range(maximum): + following = [0] * STATES + for source, multiplicity in enumerate(state): + if multiplicity: + for mask, weight in moves: + following[source ^ mask] += multiplicity * weight + state = following + results.append(state[-1]) + return results + + +def fractions_at(m): + need(4 <= m <= 85, "declared dimension domain") + n, x = m - 1, 1 << m + denominator = (2 ** (4 * m - 16) + * (x - 1) * (x - 2) * (x - 4) * (x - 8)) + joint = Fraction(count(n), denominator) + marginal = Fraction(3 ** n, (x - 1) * 2 ** n) + correction = Fraction((x - 1) ** 3, (x - 2) * (x - 4) * (x - 8)) + ratio = joint / marginal ** 4 + need(ratio == Fraction(STATES * count(n), 81 ** n) * correction, + "ratio normalization including finite-GL correction") + return joint, marginal, ratio + + +def proof_checks(): + tail = sum(abs(mult) for value, mult in TERMS.items() if value < 63) + need(tail == 4083, "absolute signed tail mass") + need(max(value for value in TERMS if value < 63) == 57, "tail radius") + need(4083 * 57 ** 84 < 63 ** 84, "uniform spectral tail threshold") + need(9 * 9 ** 84 < 14 ** 84, "finite-GL correction threshold") + need(Fraction(15, 16) * Fraction(7, 8) * Fraction(3, 4) + == Fraction(315, 512), "denominator lower bound") + need(11 * 512 < 18 * 315, "correction bound constant") + need(11 * 7 ** 84 < 9 ** 84, "positive uniform ratio upper bound") + rows = [] + for m in range(4, 85): + joint, marginal, ratio = fractions_at(m) + need(joint < marginal ** 4, "strict four-event product inequality") + rows.append({"m": m, "joint": str(joint), "ratio": str(ratio)}) + return rows + + +def controls(): + joint, marginal, ratio = fractions_at(5) + need(joint == Fraction(1, 208320), "first positive dimension") + need(joint != marginal ** 4, "independence control") + need(ratio != Fraction(STATES * count(4), 81 ** 4), + "finite-GL correction control") + wrong = step_weights(1) + need(hadamard(wrong)[0] != 81, "zero-factor multiplicity control") + wrong_walk = walk_counts(5, zero_weight=1) + need(wrong_walk[5] != count(5), "zero-factor changes a positive count") + missing_mode = dict(TERMS) + del missing_mode[63] + need(sum(mult * value ** 4 for value, mult in missing_mode.items()) + != STATES * count(4), "leading negative mode control") + return 5 + + +def main(): + signed, unsigned = spectral_data() + walks = walk_counts(12) + need(walks == [count(n) for n in range(13)], "walk versus spectral count") + rows = proof_checks() + result = { + "status": "PASS_CORANKONE_FOUR_CORRELATION", + "claim_type": "scoped counting proof with exact finite component", + "characters_enumerated": STATES, + "signed_spectrum": sorted(signed.items(), reverse=True), + "unsigned_spectrum": sorted(unsigned.items(), reverse=True), + "walk_counts_n_0_through_12": walks, + "finite_dimensions_checked": len(rows), + "finite_comparisons": rows, + "uniform_tail_starts_at_n": 84, + "asymptotic_deficit_coefficient": 12, + "controls": controls(), + } + package = Path(__file__).resolve().parent + result["package_sha256"] = { + name: sha256((package / name).read_bytes()).hexdigest() for name in FILES + } + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()