From 196eecafc5700a1503a737e9174af8692f1edb0e Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 09:15:44 +0000 Subject: [PATCH] feat(research): prove five-indicator negative association --- .../PROOF.md | 160 +++++++++ .../README.md | 122 +++++++ .../SOURCES.json | 54 +++ .../TASK.json | 112 +++++++ .../VERIFY.json | 34 ++ .../verify.py | 312 ++++++++++++++++++ 6 files changed, 794 insertions(+) create mode 100644 research/corankone-five-negative-association/PROOF.md create mode 100644 research/corankone-five-negative-association/README.md create mode 100644 research/corankone-five-negative-association/SOURCES.json create mode 100644 research/corankone-five-negative-association/TASK.json create mode 100644 research/corankone-five-negative-association/VERIFY.json create mode 100644 research/corankone-five-negative-association/verify.py diff --git a/research/corankone-five-negative-association/PROOF.md b/research/corankone-five-negative-association/PROOF.md new file mode 100644 index 0000000000..d4b6502710 --- /dev/null +++ b/research/corankone-five-negative-association/PROOF.md @@ -0,0 +1,160 @@ +# Five-indicator negative association + +This proof was produced by Nick Petalas. Apache-2.0. + +## Statement and boundary + +Let m>=5. Let U_1,...,U_5 be pairwise orthogonal rank-one idempotents on +F_2^m. Draw G uniformly from the complete group GL_m(F_2). For each i let +E_i mean that every leading principal minor, of orders 1,...,m-1, of +G(I-U_i)G^-1 is nonzero. Put Z_i=1_{E_i}. + +**Theorem.** For any disjoint nonempty subsets A,B of {1,...,5} and +nonconstant coordinatewise increasing functions f:{0,1}^A->R and +g:{0,1}^B->R, + + Cov(f(Z_A),g(Z_B)) < 0. + +If either function is constant, its covariance is zero. Thus Z is negatively +associated in the usual non-strict sense as well. These hypotheses fix the +field, kernel geometry and probability measure. They do not cover restricted +or conditioned header collections. + +This is a scoped proof with an exact finite component. The new step closes +Open next question 1 of Krzysztof Wojt's PR5093. The moment laws and the +four-event method are cited inputs, not new results or audited deliverables. + +## Counting inputs + +The five image lines together with their common-kernel complement give a +simultaneous basis taking U_i to e_i e_i^T. A fixed change of basis permutes +the whole header domain. Permuting the five distinguished lines also preserves +its uniform measure, so the indicator law is exchangeable. + +Write n=m-1, X=2^(n+1), and p_k=Pr(E_1 and ... and E_k), with p_0=1. +Use Nick Petalas's PR4227/4261/4275 character law and PR4599 four-event +spectrum, and Ryanson Jonathan's PR4607 five-event spectrum: + + p_k = N_k(n) / [2^(kn) product_(j=0)^(k-1)(X-2^j)], + N_k(n) = sum_z s_(k,z) z^n, 0<=k<=5. (1) + +All integer pairs (z,s_(k,z)) are retained as SPECTRA in verify.py. The first +spectra are {1:1}, {3:1}, and {9:1,7:-2,5:1}. The five-event spectrum has 62 +nonzero terms, headed by 243^n-20*189^n+60*171^n. Its published character +computation is a cited mathematical input. It was used once to obtain the +literal table; this contribution does not import or replay that executable +in its verifier, or claim independent validation of that spectrum. SOURCES.json +pins the exact proof and source bytes on the scientific base. + +Use the common strictly positive denominator + + Q(n)=32^n product_(j=0)^4(X-2^j), + A_k(n)=2^((5-k)n) N_k(n) product_(j=k)^4(X-2^j). + +For every n>=4, p_k=A_k/Q and A_0=Q. These identities retain every finite-GL +factor. Replacing X-2^j by X would change the probability law. + +## Exhaustive increasing-event reduction + +Any increasing Boolean function on s bits is determined by its truth table. +A nonconstant such function is zero at the empty subset and one at the full +subset. Enumerate every integer truth table from 1 to 2^(2^s)-2, keeping it +exactly when + + F(x) <= F(x union {j}) for every x and every bit j. (2) + +For s=1,2,3,4 the resulting list lengths are 1,4,18,166. This is an exhaustive +finite loop over at most 65,534 candidates, not a symmetry assumption. + +Subset Mobius inversion gives a unique multilinear expansion + + F(z)=sum_I a_I product_(i in I) z_i. + +Let a_k=sum_(|I|=k) a_I. Then E[F]=sum_k a_k p_k. For a second increasing +event H on disjoint coordinates, with grouped coefficients b_l, exchangeability +and disjointness give + + E[F H]=sum_(k,l) a_k b_l p_(k+l). + +The positive covariance gap therefore is + + Delta(F,H)=E[F]E[H]-E[F H]=P_(a,b)(n)/Q(n)^2, + P_(a,b)=(sum_k a_k A_k)(sum_l b_l A_l) + - Q sum_(k,l) a_k b_l A_(k+l). (3) + +Up to exchanging the two supports and permuting coordinates, all possible +support sizes are + + (1,1), (1,2), (1,3), (1,4), (2,2), (2,3). + +The verifier visits all 277 labelled pairs on these canonical supports, +including functions which ignore an input. It reconstructs each truth table +from its individual Mobius coefficients before grouping by degree. Expanding +(3) and collecting identical power sums gives 37 distinct nonzero polynomials. +The old support types give 11 distinct gaps. The new 4+1 and 3+2 types supply +the other 26. No conjunction-only shortcut is used. + +## Exact signs for every dimension + +For each of the 37 polynomials, write + + P(n)=c B^n + sum_(zb>0 and c,C>0. It checks + + c B^N > C b^N. (4) + +For every n>=N, since b/B<1, + + P(n) >= c B^n-C b^n > 0. + +For each remaining integer 4<=n0 using exact integers, +and separately compares P(n)/Q(n)^2 with direct rational evaluation of (3) +using (1). Thus the finite prefix and the tail cover every n>=4, with no +unchecked interval. N is at most 179, so every gap has an analytic tail from +m=180 onward. Individual gaps often have much earlier tails. + +The complete 37-row certificate is the TAILS tuple in verify.py. Each row +contains integers only and is regenerated and checked, rather than trusted +as an execution receipt. The verifier emits the corresponding support sizes, +coefficient vectors, polynomial lengths and tail data for inspection. + +These exact finite checks and the elementary tail inequality prove +Delta(F,H)>0 for every nonconstant increasing Boolean pair on disjoint +nonempty supports. + +## Increasing real functions + +On a finite Boolean cube, an increasing real function f can be written as its +minimum plus a finite nonnegative linear combination of its nonconstant +increasing superlevel-set indicators. Explicitly, for distinct values +v_0<...=v_j}. + +Every coefficient is positive. The same decomposition holds for g. Covariance +is bilinear, constants contribute zero, and every indicator pair has strictly +negative covariance by the preceding section. If f and g are nonconstant, +there is at least one summand in each decomposition, so their covariance is +strictly negative. This proves the theorem. + +## Verification boundary + +The standard-library verifier also evaluates all 277 truth-table pairs directly +on the 32 atoms at m=5,6,8,16, using inclusion-exclusion from (1). This checks +the grouped-coefficient and disjoint-support calculation by a separate path. +It verifies every atom is nonnegative and the masses sum to one. These are +bounded corroborations, not a separate complete-GL enumeration or an audit of +the moment law. + +Invalid domain, sign, tail-mass and cutoff controls remain active under +optimized Python. A two-point perfectly correlated distribution is detected as +having positive covariance, so exchangeability alone cannot replace (1). +The claim does not supply a physical header sampler, producer, consumer, +restoration protocol, stock/tape budget or supplier admission. It gives no +odd-field, six-indicator or nonorthogonal-kernel theorem. Independent human +and formal proof-kernel review are unclaimed. No multiplication exponent or +selected-frontier change follows. diff --git a/research/corankone-five-negative-association/README.md b/research/corankone-five-negative-association/README.md new file mode 100644 index 0000000000..ca5507464f --- /dev/null +++ b/research/corankone-five-negative-association/README.md @@ -0,0 +1,122 @@ +# Five binary full-guard indicators are negatively associated + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped proof with an exact finite component. No new kappa.** +For five pairwise orthogonal rank-one idempotents U_i on F_2^m, draw a +complete uniform header G in GL_m(F_2), with m>=5. Let Z_i indicate that +all leading principal minors of G(I-U_i)G^-1 through order m-1 are nonzero. +Then any two nonconstant increasing real functions of disjoint nonempty +subsets of the five indicators have strictly negative covariance. + +This settles Open next question 1 of Krzysztof Wojt's +[PR #5093](https://github.com/CrocSwap/integer-mult-bounds/pull/5093). +That predecessor proves the four-indicator theorem. The new comparisons +cover the 4+1 and 3+2 support splits; the existing fivefold-intersection +inequality alone does not settle them. The statement covers every integer +m>=5, rather than extrapolating a finite dimensional sample. + +## Proof and evidence + +[PROOF.md](PROOF.md) gives the argument. Subset Mobius inversion and +exchangeability reduce all 277 labelled increasing-event pairs to 37 +covariance-gap power sums. Eleven correspond to the earlier support types; +26 additional types complete the five-indicator case. Every gap has a +positive exact finite prefix and a strict leading-term tail bound. +Superlevel-set decomposition then gives the assertion for real functions. + +The self-contained standard-library verifier checks: + +- All 1,4,18,166 nonconstant monotone Boolean truth tables on one through + four inputs, including reconstruction of every truth value. +- All 37 expanded gap polynomials, 4,498 exact finite-prefix comparisons, + 37 uniform tail certificates and 111 additional tail identity probes. + The largest tail begins at n=m-1=179, hence m=180. +- All 277 labelled pairs by direct 32-atom truth-table evaluation at + m=5,6,8,16, giving 1,108 independent-path covariance comparisons. +- Ten domain, sign, cutoff, tail-mass, finite-denominator and distribution + controls. Checks use explicit exceptions and remain active with -O. + +Every run prints PASS_CORANKONE_FIVE_NEGATIVE_ASSOCIATION and a generated +receipt bound to all six package-file hashes. It writes no files and needs +neither Git nor network. The moment laws and spectra are cited inputs; +no predecessor executable is imported or independently audited here. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/corankone-five-negative-association/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/corankone-five-negative-association/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-five-negative-association +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-five-negative-association --check-source-history +``` + +Use another CPython 3.12 path on other machines. The publication preflight +requires a committed package and full history. Both registered scientific +commands use warning-strict isolated Python and have a 60-second cap. +Local command times and hosted CI status are recorded in the PR body. + +## Scope and provenance + +Scientific base is canonical main de5ec2e7a6074068452f45b1a191b5c72832df4a, +priority revision 8. TASK.json records the changed formal-interface-lemma +scope: an original dependence side result, without a proof-assistant claim. +SOURCES.json pins predecessor proof texts and code as historical provenance; +none is a runtime import. The selected-baseline source-binding orientation +passes after materializing its sparse inputs. It is not a scientific replay +or a premise of this theorem. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213528) +records the question. Live open/account PR lists, latest handoffs, active +Discussions, distinctive main-tree README searches and merged-PR searches +were checked before claiming. The cached overlap report had incomplete sparse +local-note coverage. Unpublished work and arbitrary historical diffs are not +covered, and global literature priority is unclaimed. Submission freshness +and related open work are recorded in the PR. + +The theorem fixes binary orthogonal kernels and the whole uniform header +measure. It gives no six-indicator, odd-field, conditioned-header or +nonorthogonal-kernel result. Physical header generation, selection, emission, +dispatch, dirty restoration, stock, precision and a paid consumer remain +unpriced. No supplier admission, multiplication theorem or selected-frontier +change is claimed. Independent human and formal proof-kernel review are +unclaimed. No Lean, Docker, native build or selected scientific cold replay +was run. + +The verifier has no recursion or shared mutable state. Functions are under +60 physical lines. Truth-table candidates are bounded by 65,534; moment +fixtures are bounded by m<=359 in the actual run and an enforced m<=513 +entry contract. The largest collected polynomial has 512 terms; every +multiplication enforces a 4,096-base capacity bound. Exact Python integers, +Fractions and bounded containers use managed dynamic allocation. This is a +documented deviation from fixed allocation, with fixed finite data domains; +there is no constant-bit-space claim. The controls use eight explicitly +listed local callbacks, the only indirect test-call targets. Warning-strict +normal and optimized execution supplies the available Python diagnostics. + +## Open next questions + +1. Does negative association persist for six orthogonal binary full-guard + indicators? This would cover larger shared-header groups. First obtain + a justified six-event moment input, then classify the new 5+1, 4+2 and + 3+3 increasing-event comparisons. The six-event spectrum and new mixed + inequalities are absent here; no larger census is reserved. +2. Can a concrete paid caller realize and use the complete uniform-header + premise? Start with its actual request family and sampling rule, then + price selection, emission, dispatch and restoration. The missing physical + consumer and complete bill prevent treating dependence as a kappa gain. + +## Credit + +Krzysztof Wojt #5093 supplies the four-event theorem, explicit five-event +question, and the power-sum/Mobius verification method adapted here. +lee-phys #5073 supplies the three-event theorem and earlier question. +Ryanson Jonathan #4607 supplies the cited five-event signed spectrum. +Nick Petalas #4227/#4261/#4275/#4599 supplies the marginal, joint character +laws and four-event spectrum. Cinna Davis's BIT request context, source527, +commdata2338, Jose Manuel's normalizer/closure lineage and Chris R / +Clear1nsight's counting context retain the attribution in those sources. +The new contribution is the 26 additional gap types and their complete +finite-prefix/tail proof, giving five-indicator negative association. diff --git a/research/corankone-five-negative-association/SOURCES.json b/research/corankone-five-negative-association/SOURCES.json new file mode 100644 index 0000000000..e167a879bf --- /dev/null +++ b/research/corankone-five-negative-association/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/corankone-four-negative-association/README.md", + "usage": "provenance", + "git_blob": "6116dea3ec6cf04bfec67c6f18a48e2a78ce0377", + "sha256": "a3e9fe547ceb22ab158ec4bceaada5f4cf9287269352c1dc4a6380d4c18a37bd" + }, + { + "path": "research/corankone-four-negative-association/verify.py", + "usage": "provenance", + "git_blob": "58cef3248b4852bb2b4f67ff1400860976e92ee3", + "sha256": "01d54f9ecdf56a4e01e5cfa2bd59195835c40f575b7880abe62b63023972a7a8" + }, + { + "path": "research/corankone-triple-header-law/PROOF.md", + "usage": "provenance", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f" + }, + { + "path": "research/corankone-triple-negative-association/README.md", + "usage": "provenance", + "git_blob": "ba63617e44742e116a17e0321dfd0cbc7c358e50", + "sha256": "8e510ddd30971e03210039b6777675f657bfb290710848b72ade9e1d55299d31" + }, + { + "path": "research/five-event-guard-correlation/PROOF.md", + "usage": "provenance", + "git_blob": "a84e5696ab202dfef0296e02d9cf26e85923eb3c", + "sha256": "a46e1d5ede453b996f545f29fa8ed50f9fc05b829192ee81d41ff0424301fc0a" + }, + { + "path": "research/five-event-guard-correlation/verify.py", + "usage": "provenance", + "git_blob": "adff8b585d018929dba12b41fe7041553cb0d403", + "sha256": "a3e16b49286ef9809c4305012155c4030242db7be4a1725b7035a4231120c7bc" + } + ] +} diff --git a/research/corankone-five-negative-association/TASK.json b/research/corankone-five-negative-association/TASK.json new file mode 100644 index 0000000000..3fa3860946 --- /dev/null +++ b/research/corankone-five-negative-association/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Strict negative association of five orthogonal binary full-guard indicators under complete uniform GL_m(F2) headers for every m>=5.", + "scope_change_reason": "The donor asks for an original result rather than a predecessor audit. Take the explicit five-indicator open question in Krzysztof Wojt PR5093 as a written counting side theorem, without proof-assistant or selected-caller admission claims.", + "bottleneck_link": "Shared-header dependence can constrain grouping, but a physical sampler and completed consumer bill remain absent; this is a mathematical side result.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved extension; do not expand to six indicators or physical implementation.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py: 37 gap certificates, 4498 finite-prefix comparisons, 111 tail probes, 1108 atom/truth-table comparisons and 10 controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does negative association hold for six orthogonal binary full-guard indicators?", + "why_it_matters": "Controls larger shared-header groups.", + "first_step": "Obtain a justified six-event moment input and classify new 5+1, 4+2 and 3+3 comparisons.", + "blocked_by": "No six-event spectrum or new gap certificates are supplied." + }, + { + "question": "Can a physical caller use a complete uniform header at favorable complete cost?", + "why_it_matters": "A dependence theorem alone does not yield a recursive supplier saving.", + "first_step": "Pin actual requests and sampling rule, then price selection, emission, dispatch and restoration.", + "blocked_by": "A physical consumer and its complete bill are absent." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213528", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "overlap": { + "coverage": "Live open PRs (limit 100), account PRs (limit 60), latest 30 handoff comments, active Discussion titles, targeted main README and merged PR searches; cached formal-interface-lemma report. Sparse local notes, unpublished work and arbitrary historical diffs are not exhaustively covered.", + "same_account_last_24_hours": "No relevant predecessor PR was opened in the last 24 hours.", + "reservation": "Five-indicator negative association; distinct from other locally reserved questions." + } +} diff --git a/research/corankone-five-negative-association/VERIFY.json b/research/corankone-five-negative-association/VERIFY.json new file mode 100644 index 0000000000..1e0ea80060 --- /dev/null +++ b/research/corankone-five-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": 60, + "checks": "Exhaustive five-indicator monotone-event coverage, all 37 exact prefixes and uniform tail certificates, atom/truth-table comparisons, rejection controls and generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exhaustive five-indicator monotone-event coverage, all 37 exact prefixes and uniform tail certificates, atom/truth-table comparisons, rejection controls and generated file-hash receipt." + } + ] +} diff --git a/research/corankone-five-negative-association/verify.py b/research/corankone-five-negative-association/verify.py new file mode 100644 index 0000000000..39b98c329e --- /dev/null +++ b/research/corankone-five-negative-association/verify.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +"""Exact finite component of five-indicator negative association. + +Nick Petalas. Apache-2.0. The power-sum and Mobius routines adapt +Krzysztof Wojt's PR5093. Moment spectra are credited inputs from +Nick Petalas PR4227/4261/4275/4599 and Ryanson Jonathan PR4607. +No predecessor executable is imported. No files are written. +""" + +from collections import defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from math import comb, prod +from pathlib import Path +import platform + +# Intersection spectra from the cited counting inputs, not a new spectrum claim. +SPECTRA = ( + {1: 1}, + {3: 1}, + {5: 1, 7: -2, 9: 1}, + {9: -2, 11: 9, 13: -18, 15: 16, 17: -6, + 19: 6, 21: -6, 27: 1}, + {17: 6, 19: -48, 21: 144, 23: -332, 25: 523, + 27: -548, 29: 502, 31: -444, 33: 399, 35: -336, + 37: 228, 39: -180, 41: 85, 43: -68, 45: 118, + 47: -48, 49: 18, 51: -24, 55: -8, 57: 24, + 63: -12, 81: 1}, + {33: -24, 35: 240, 37: -1080, 39: 2700, 41: -6620, + 43: 15154, 45: -24920, 47: 37380, 49: -54660, 51: 65830, + 53: -72884, 55: 76440, 57: -72900, 59: 71120, 61: -68780, + 63: 66112, 65: -58760, 67: 50225, 69: -45880, 71: 37000, + 73: -33560, 75: 30950, 77: -24720, 79: 22980, 81: -19520, + 83: 12535, 85: -10940, 87: 12040, 89: -7680, 91: 6600, + 93: -7740, 95: 4640, 97: -3740, 99: 4935, 101: -2200, + 103: 2200, 105: -3500, 107: 1020, 109: -1120, 111: 1680, + 113: -500, 115: 480, 117: -1320, 119: 360, 121: -120, + 123: 676, 125: -140, 127: 200, 129: -460, 131: 150, + 133: -120, 135: 460, 137: -40, 139: 20, 141: -240, + 147: 90, 153: -60, 163: 10, 165: -40, 171: 60, + 189: -20, 243: 1}, +) + +# B, c, b, C, N for the 37 gaps in exhaustive first-occurrence order. +TAILS = ( + (458752, 512, 327680, 46655488, 34), + (344064, 512, 311296, 135826176, 125), + (458752, 1024, 344064, 220461824, 43), + (258048, 384, 233472, 913449728, 147), + (344064, 1024, 311296, 1174723456, 140), + (344064, 1536, 311296, 2218810240, 142), + (458752, 512, 344064, 1090742784, 51), + (458752, 1536, 344064, 1423748864, 48), + (193536, 256, 175104, 13308763072, 178), + (258048, 768, 233472, 15120260416, 168), + (258048, 1152, 233472, 29334772288, 171), + (344064, 512, 311296, 14324733568, 172), + (344064, 1536, 311296, 16417920128, 162), + (258048, 1536, 233472, 43549284160, 172), + (344064, 512, 311296, 28530041344, 179), + (344064, 1024, 311296, 13580415680, 164), + (458752, 512, 327680, 14261167744, 51), + (344064, 2048, 311296, 17454305728, 160), + (344064, 2560, 311296, 32705203584, 164), + (458752, 512, 344064, 16333939968, 61), + (344064, 3072, 311296, 47956101440, 166), + (458752, 512, 344064, 31584838336, 63), + (458752, 1024, 327680, 15213572160, 50), + (458752, 2048, 344064, 17868236992, 56), + (258048, 512, 233472, 945765376, 145), + (344064, 1024, 311296, 1207039232, 140), + (458752, 2048, 344064, 1626164224, 48), + (193536, 384, 175104, 13552200704, 174), + (258048, 1024, 233472, 15425906176, 166), + (258048, 1536, 233472, 29914959808, 168), + (344064, 512, 311296, 14599275456, 172), + (344064, 1536, 311296, 16754670272, 162), + (258048, 768, 233472, 15363698176, 168), + (344064, 2048, 311296, 17759951744, 160), + (344064, 3072, 311296, 34321777088, 163), + (458752, 1024, 344064, 16524500160, 58), + (458752, 3072, 344064, 19578975040, 55), +) + +SPLITS = ((1, 1), (1, 2), (1, 3), (1, 4), (2, 2), (2, 3)) +PACKAGE_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(*terms): + """Add integer multiples of finite power sums.""" + result = defaultdict(int) + for multiplier, polynomial in terms: + for base, coefficient in polynomial.items(): + result[base] += multiplier * coefficient + return {base: value for base, value in result.items() if value} + + +def multiply(left, right): + """Pointwise multiplication of finite exponential sequences.""" + result = defaultdict(int) + for base, coefficient in left.items(): + for other, value in right.items(): + result[base * other] += coefficient * value + require(len(result) <= 4096, "power-sum capacity exceeded") + return {base: value for base, value in result.items() if value} + + +def evaluate(polynomial, n): + return sum(coefficient * base**n for base, coefficient in polynomial.items()) + + +def numerators(): + """p_k=A_k/Q with Q=32^n product_(j=0)^4 (2^(n+1)-2^j).""" + result = [] + for k in range(6): + polynomial = multiply(SPECTRA[k], {2**(5 - k): 1}) + for j in range(k, 5): + polynomial = multiply(polynomial, {2: 2, 1: -(2**j)}) + result.append(polynomial) + return tuple(result) + + +def gap_polynomial(f, g, nums): + left = add(*[(a, nums[i]) for i, a in enumerate(f)]) + right = add(*[(b, nums[j]) for j, b in enumerate(g)]) + joint = add(*[(a * b, nums[i + j]) + for i, a in enumerate(f) for j, b in enumerate(g)]) + return add((1, multiply(left, right)), (-1, multiply(nums[0], joint))) + + +def moments(m): + require(type(m) is int and 5 <= m <= 513, "dimension outside finite checker") + n, x = m - 1, 2**m + return tuple(Fraction(evaluate(SPECTRA[k], n), + 2**(k * n) * prod(x - 2**j for j in range(k))) + for k in range(6)) + + +def gap_value(f, g, p): + return (sum(a * p[i] for i, a in enumerate(f)) * + sum(b * p[j] for j, b in enumerate(g)) - + sum(a * b * p[i + j] for i, a in enumerate(f) for j, b in enumerate(g))) + + +def monotone_tables(size): + """All nonconstant increasing Boolean functions on at most four bits.""" + require(type(size) is int and 1 <= size <= 4, "unsupported Boolean dimension") + return tuple(table for table in range(1, (1 << (1 << size)) - 1) + if all(not (table >> x & 1) or (table >> (x | (1 << j)) & 1) + for x in range(1 << size) for j in range(size))) + + +def expectation_coefficients(table, size): + coefficients = [table >> x & 1 for x in range(1 << size)] + for j in range(size): + for x in range(1 << size): + if x >> j & 1: + coefficients[x] -= coefficients[x ^ (1 << j)] + # Check every truth value before discarding which variables occur. + for x in range(1 << size): + require(sum(coefficients[y] for y in range(1 << size) if y & x == y) + == (table >> x & 1), "Mobius reconstruction differs") + return tuple(sum(coefficients[x] for x in range(1 << size) + if x.bit_count() == k) for k in range(size + 1)) + + +def classify(nums): + tables = {s: monotone_tables(s) for s in range(1, 5)} + require(tuple(len(tables[s]) for s in range(1, 5)) == (1, 4, 18, 166), + "incomplete monotone-function list") + coefficients = {(s, table): expectation_coefficients(table, s) + for s in range(1, 5) for table in tables[s]} + cases, labelled = {}, 0 + for s, t in SPLITS: + for left, right in product(tables[s], tables[t]): + f, g = coefficients[s, left], coefficients[t, right] + polynomial = gap_polynomial(f, g, nums) + key = tuple(sorted(polynomial.items())) + cases.setdefault(key, (s, t, f, g, polynomial)) + labelled += 1 + require(labelled == 277 and len(cases) == 37, "covariance coverage differs") + return tables, coefficients, tuple(cases.values()), labelled + + +def verify_tail(polynomial, certificate): + require(len(certificate) == 5 and all(type(v) is int for v in certificate), + "five exact integer tail parameters required") + bases = sorted(polynomial, reverse=True) + B, c, b, C, N = certificate + actual = (bases[0], polynomial[bases[0]], bases[1], + sum(abs(polynomial[z]) for z in bases[1:])) + require(actual == certificate[:4], "tail parameters differ") + require(B > b > 0 and c > 0 and C > 0 and 4 <= N <= 256, + "invalid tail domain") + require(c * B**N > C * b**N, "strict tail dominance fails") + + +def verify_gaps(cases, nums): + require(len(cases) == len(TAILS), "missing tail certificate") + prefix, probes, rows = 0, 0, [] + maximum = max(certificate[4] for certificate in TAILS) + p_by_m = {m: moments(m) for m in range(5, 2 * maximum + 2)} + q_by_n = {n: evaluate(nums[0], n) for n in range(4, 2 * maximum + 1)} + require(min(q_by_n.values()) > 0, "common denominator is not positive") + for index, (s, t, f, g, polynomial) in enumerate(cases): + certificate = TAILS[index] + verify_tail(polynomial, certificate) + cutoff = certificate[4] + for n in range(4, cutoff): + value = Fraction(evaluate(polynomial, n), q_by_n[n]**2) + require(value == gap_value(f, g, p_by_m[n + 1]) and value > 0, + "finite-prefix sign or expansion differs") + prefix += 1 + for n in (cutoff, cutoff + 1, 2 * cutoff): + value = Fraction(evaluate(polynomial, n), q_by_n[n]**2) + require(value == gap_value(f, g, p_by_m[n + 1]) and value > 0, + "tail-probe identity differs") + probes += 1 + rows.append({"index": index, "split": [s, t], "f": f, "g": g, + "B_c_b_C_N": certificate, "terms": len(polynomial)}) + return rows, prefix, probes + + +def atom_probabilities(p): + return tuple(sum((-1)**j * comb(5 - x.bit_count(), j) * p[x.bit_count() + j] + for j in range(6 - x.bit_count())) for x in range(32)) + + +def literal_gap(left, s, right, t, atoms): + ef = eg = joint = Fraction(0) + for x, mass in enumerate(atoms): + f = left >> (x & ((1 << s) - 1)) & 1 + g = right >> ((x >> s) & ((1 << t) - 1)) & 1 + ef += f * mass + eg += g * mass + joint += f * g * mass + return ef * eg - joint + + +def verify_truth_tables(tables, coefficients): + checks = 0 + for m in (5, 6, 8, 16): + p = moments(m) + atoms = atom_probabilities(p) + require(sum(atoms) == 1 and min(atoms) >= 0, "invalid five-bit law") + for s, t in SPLITS: + for left, right in product(tables[s], tables[t]): + value = literal_gap(left, s, right, t, atoms) + require(value == gap_value(coefficients[s, left], + coefficients[t, right], p) and value > 0, + "truth-table covariance differs") + checks += 1 + return checks + + +def rejection_controls(cases): + polynomial = cases[8][4] + certificate = TAILS[8] + invalid = ( + lambda: moments(4), lambda: moments(True), + lambda: monotone_tables(5), lambda: monotone_tables(True), + lambda: verify_tail(add((-1, polynomial)), certificate), + lambda: verify_tail(polynomial, (*certificate[:4], 4)), + lambda: verify_tail(polynomial, (*certificate[:3], certificate[3] - 1, + certificate[4])), + lambda: verify_tail(polynomial, (*certificate[:4], True)), + ) + for operation in invalid: + try: + operation() + except ValueError: + continue + raise ValueError("invalid proof input was accepted") + atoms = (Fraction(1, 2),) + (Fraction(0),) * 30 + (Fraction(1, 2),) + require(literal_gap(2, 1, 2, 1, atoms) == -Fraction(1, 4), + "positive-covariance distribution control was missed") + exact = moments(5)[1] + require(exact != Fraction(3**4, 2**4 * 2**5), "finite-GL control ineffective") + return len(invalid) + 2 + + +def main(): + nums = numerators() + tables, coefficients, cases, labelled = classify(nums) + rows, prefix, probes = verify_gaps(cases, nums) + truth_checks = verify_truth_tables(tables, coefficients) + controls = rejection_controls(cases) + package = Path(__file__).resolve().parent + receipt = {"python": platform.python_version(), + "sha256": {name: sha256((package / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES}} + result = {"claim_type": "scoped proof with exact finite component", + "claim": "strict negative association for every integer m >= 5", + "monotone_functions": [len(tables[s]) for s in range(1, 5)], + "labelled_cases": labelled, "distinct_gaps": len(rows), + "prefix_checks": prefix, "tail_probes": probes, + "truth_table_checks": truth_checks, "rejection_controls": controls, + "tails": rows, "receipt": receipt, "new_kappa": False} + print("PASS_CORANKONE_FIVE_NEGATIVE_ASSOCIATION") + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()