From 18785ebf02a5976a8c16a747d0095ca4766ca0ae Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 11:06:12 +0000 Subject: [PATCH] feat(research): sharpen matched phase-query event floors --- research/matched-phase-integrality/PROOF.md | 130 +++++++++++++ research/matched-phase-integrality/README.md | 107 +++++++++++ .../matched-phase-integrality/SOURCES.json | 24 +++ research/matched-phase-integrality/TASK.json | 95 ++++++++++ .../matched-phase-integrality/VERIFY.json | 34 ++++ research/matched-phase-integrality/verify.py | 179 ++++++++++++++++++ 6 files changed, 569 insertions(+) create mode 100644 research/matched-phase-integrality/PROOF.md create mode 100644 research/matched-phase-integrality/README.md create mode 100644 research/matched-phase-integrality/SOURCES.json create mode 100644 research/matched-phase-integrality/TASK.json create mode 100644 research/matched-phase-integrality/VERIFY.json create mode 100644 research/matched-phase-integrality/verify.py diff --git a/research/matched-phase-integrality/PROOF.md b/research/matched-phase-integrality/PROOF.md new file mode 100644 index 0000000000..daca5caa6e --- /dev/null +++ b/research/matched-phase-integrality/PROOF.md @@ -0,0 +1,130 @@ +# One more event from Fourier integrality + +This proof and its finite corroboration were produced by Nick Petalas. + +## Claim and inherited contract + +Under Jose Manuel's [PR2070](https://github.com/CrocSwap/integer-mult-bounds/pull/2070) +matched P112 endpoint and commuting-phase program contract, one bank requires +at least **140** nontrivial single-array phase events. Four independent banks, +even with shared role-linear processing and private workspace, require at least +**556**. These are lower bounds, with no attaining constructions claimed. + +We use the mathematical conclusions in the pinned predecessor README, +Sections 1 through 3, as premises. We do not audit them or replay its code. +In particular, the new result is conditional on the same causal factorization, +character-sector construction and matched-endpoint rank statements. + +The contract permits fixed constant complex linear processing of the role +coordinates, including singular COPY/CLEAR, clean private scratch, finite +restored dirty workspace, and uniform tensor Paulis. A paid event acts on +one role by a commuting directional-phase product with a nonzero binary +symmetric polar. It excludes nonlinear or data-dependent programs, +noncommuting payload adapters, arbitrary payload-coordinate mixing, and +new joint multirole child interfaces. All independent inputs and declared +outputs are retained exactly as in PR2070. + +This theorem concerns one direct matched bank or four independent direct +matched banks. It does not claim a stronger normalized bound for nonuniform +coherent-cover programs, a new physical tariff, or a full supplier. + +## Cited rank and character premises + +Write G for the binary vector space of symmetric polars. Every character +chi of G is simultaneously available in the predecessor's common +Pauli-trivial sector at a sufficiently large tensor length. Each of k +nontrivial events has a fixed nonzero polar p_j in G, and acts by +(-1)^(chi(p_j)). Repetitions among the p_j are allowed. + +Let t(chi) count the active events, those with chi(p_j)=1. The predecessor's +causal rank inequality is + + rank Delta_chi >= d_image + d_row - 2k + t(chi). + +For b independent matched P112 banks its stated premises are + + d_image = d_row = 112b, + rank Delta_chi <= 16b for every chi. + +Consequently every character must satisfy + + t(chi) <= 2k - 208b. (1) + +Each p_j is nonzero, so averaging t over all characters gives k/2. +Thus k >= ceil(416b/3), the predecessor's 139 and 555 bounds for b=1 +and b=4. No computation in this package re-establishes the quoted +source dimensions, endpoint, or tensor-sector realization. + +## A finite-group rigidity lemma + +Let G be any finite binary vector space. Let p_1,...,p_k be a multiset +of nonzero elements, with k positive and odd. If + + t(chi) <= (k+1)/2 for every character chi, (2) + +then the multiset is exactly H minus {0}, each element occurring once, +for a nonzero linear subspace H of G. In particular k+1 is a power of two. +Conversely, every such multiset satisfies (2). + +Proof. Set f(0)=1, and set f(g) to the multiplicity of g for g nonzero. +Its unnormalized real Fourier transform is + + f_hat(chi) = 1 + sum_j (-1)^(chi(p_j)) + = 1 + k - 2t(chi) >= 0. + +Fourier inversion at zero gives sum_chi f_hat(chi)=|G|. Therefore +w_chi=f_hat(chi)/|G| is a probability distribution, and inversion gives + + f(g) = sum_chi w_chi (-1)^(chi(g)). (3) + +Equation (3) implies |f(g)|<=1. The multiplicities are nonnegative +integers, so f takes only values 0 and 1. Moreover, f(g)=1 exactly when +every character with w_chi>0 vanishes on g. The set H on which f is 1 +is therefore the intersection of the kernels of those characters, a +linear subspace. This proves both the support statement and the absence +of repeated polars. Since sum_g f(g)=k+1, we get |H|=k+1. + +Conversely, if f is the indicator of H, summing a character over H gives +|H| if the character vanishes on H, and zero otherwise. Hence f_hat>=0, +which is (2). This completes the proof for every finite dimension. + +Equivalently, if positive odd k has k+1 not a power of two, some character +activates at least (k+3)/2 events. This is an arithmetic obstruction; +it does not depend on the ambient dimension or on a bound on repetitions. +Finite-group Fourier inversion and positivity are classical ingredients. +No global priority for the abstract lemma is claimed. + +## The new matched-endpoint bounds + +For b=1, the cited average bound already gives k>=139. If k=139, +(1) requires t(chi)<=70 for every chi. This equals (k+1)/2, so the +lemma would require 140 to be a power of two. It is not. Thus k>=140. + +For b=4, the cited average bound gives k>=555. If k=555, (1) requires +t(chi)<=278 for every chi. Again this is (k+1)/2, but 556 is not a +power of two. Thus k>=556. + +The argument applies separately at every sufficiently large tensor length +in the cited character-sector construction, even if the program and its +constant coefficients depend on that length. Its polar multiset at that +length is still finite and subject to the same lemma. + +## Limits and relevance + +This strengthens the historical matched terminal obstruction by one event. +PR2070 already excluded its stated comparison invoice; we do not recompute +that invoice, claim a new exclusion of the selected PR6030 caller, or change +kappa. The result explains one additional reason the averaged event-count +boundary cannot be attained in this alphabet. + +A zero-polar event violates the lemma's premise. Uncharged adapters that +move between character sectors violate the common-character premise. +Different terminal endpoints need their own image, row and defect bounds. +Event counts do not by themselves determine a native tariff or a complete +signed target/paid moment. The five selected framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. + +The verifier enumerates only its explicitly reported small multisets. Its +finite checks corroborate the new Fourier argument and its implementation; +they do not enumerate candidate 139-event or 555-event circuits, and they +do not replace this all-dimension proof. diff --git a/research/matched-phase-integrality/README.md b/research/matched-phase-integrality/README.md new file mode 100644 index 0000000000..5060f9e457 --- /dev/null +++ b/research/matched-phase-integrality/README.md @@ -0,0 +1,107 @@ +# Matched phase-query floors of 140 and 556 + +This contribution was produced by Nick Petalas. + +A Fourier integrality argument raises Jose Manuel's +[PR2070](https://github.com/CrocSwap/integer-mult-bounds/pull/2070) +commuting-phase lower bound from 139 to **140** single-array phase events +for one matched P112 bank, and from 555 to **556** for four independent +banks. Shared role-linear processing, COPY/CLEAR and private workspace +remain permitted under the predecessor's contract. + +Claim type: scoped mathematical proof with exact finite corroboration. +The bounds are not claimed optimal. There is no new kappa, physical supplier +or selected-frontier change. This is a terminal-interface side result on +the centre-path-sharing card, rather than a completed current-caller change. + +The new lemma says that an odd multiset of k nonzero binary polars with +at most (k+1)/2 active events in every character must consist of all nonzero +elements of a subspace, each once. Thus k+1 must be a power of two. +PR2070's cited rank inequality forces exactly this threshold at k=139 and +k=555; neither 140 nor 556 is a power of two. Read [PROOF.md](PROOF.md). + +The predecessor's causal inequality, common Pauli-trivial character sector, +P112 span dimensions and defect-rank bound are mathematical premises. +They are not new results here, and no predecessor scientific executable +is imported, audited or replayed. [SOURCES.json](SOURCES.json) pins its +README as historical provenance at canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. + +## Reproduce + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/matched-phase-integrality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/matched-phase-integrality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/matched-phase-integrality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/matched-phase-integrality --check-source-history +``` + +Elsewhere substitute a local CPython 3.12 path. The direct marker is +`PASS_MATCHED_PHASE_INTEGRALITY`. Direct runs generate a deterministic +receipt on stdout, bound to the SHA256 of all six package files. They write +no files. No hand-written receipt is committed. + +The checker exhausts every odd-size nonzero-polar multiset of sizes 1 through +9 in dimensions 1 through 3, and sizes 1 through 5 in dimension 4. It checks +19,727 multisets, including repetitions. Exactly 70 satisfy the character +threshold; each is a subspace with zero omitted. Direct character evaluation +and a separate butterfly transform agree. Fourier inversion, exact multiset +counts and Gaussian-binomial subspace counts also agree. Thirteen invalid +domains are rejected. Five semantic control groups cover two simplex sizes, +repeated polars, the essential zero-polar exclusion and the exact threshold. +Normal and optimized modes keep all checks active. + +These finite cases support the new lemma. They do not enumerate circuits +with 139 or 555 events, prove the predecessor premises, or replace the +all-dimension written argument. + +## Limits + +The proof requires fixed role-linear programs, nonzero commuting phase +polars and the complete common-character family. Noncommuting payload +adapters, nonlinear or data-dependent programs, changed endpoints and +new multirole child interfaces require other arguments. This package does +not strengthen the normalized nonuniform coherent-cover bound. + +The selected record at the pinned base is PR6030, conditional +kappa 0.003125804. Its five framework assumptions remain. Native realization, +physical tariffs, routing, ownership/erasure, restoration implementation, +precision/tape, stock, compiler closure and complete supplier/outer bills +are unprovided. The selected scientific cold replay, Lean and Docker are +unrun. Independent human and formal proof-kernel review are unclaimed. + +The checker has no recursion or subprocesses. Every enumerated domain has +an explicit bound. New functions are below 60 physical lines. Managed Python +allocation is a Power-of-Ten rule-3 deviation; live mathematical arrays have +at most 16 entries and each multiset has at most 9 entries. The 18 summary +rows and fixed package-file hashes are bounded. It does not claim a fixed +allocation runtime. Warnings are errors in both registered commands. + +## Open next questions + +- Can the 140-event or 556-event floor be attained in the exact matched + alphabet? An explicit polar multiset satisfying the necessary per-character + inequalities is a first step. It still needs a causal role-linear + realization and complete endpoint proof. No such construction is supplied. +- Can one priced noncommuting payload adapter change the matched endpoint's + complete cost? Start with its explicit tensor-valid action between two + phase events. This is the predecessor's retained opening; the common + character decomposition and a physical price are the blockers. + +[TASK.json](TASK.json) records these questions, the scope change, live overlap +coverage and the advance claim. + +## Credit + +Jose Manuel / jmbarrancoml supplies PR2070's causal, character and P112 +endpoint results. Credit eumemic / PR288 and Ali Romman / PR468 for the +compact-WY, image/row-span and character lineage; Ali Romman / PR1862/1969 +for the source codes and phase conventions; Rohan Arun / PR1931 for source +continuation; and Douglas Colkitt for the predecessor's arithmetic lineage. +Their complete notices remain in the unmodified source package. Classical +finite-group Fourier inversion and positivity retain their credit; no +global priority for the abstract rigidity lemma is claimed. The new step +is its integrality application to this matched endpoint. New work is +Apache-2.0. diff --git a/research/matched-phase-integrality/SOURCES.json b/research/matched-phase-integrality/SOURCES.json new file mode 100644 index 0000000000..c097496bc9 --- /dev/null +++ b/research/matched-phase-integrality/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-log-phase-query-bound/README.md", + "usage": "provenance", + "git_blob": "0c7957111a8fc894cc01f017d221bf0f9c4673a6", + "sha256": "271300f434301af469026f0945d01ebf9108c50ccb7e1158170574b07f9455a4" + } + ] +} diff --git a/research/matched-phase-integrality/TASK.json b/research/matched-phase-integrality/TASK.json new file mode 100644 index 0000000000..217dc31037 --- /dev/null +++ b/research/matched-phase-integrality/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "centre-path-sharing", + "question": "Can a specified persistent boundary eliminate a repeated centre operation in the current caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Write a two-call input/output contract on the current source word, including arbitrary centre baselines and every later read. Price producer, retention, native alignment and restoration jointly. Historical 64-per-call and 1.90x figures are not current budgets. Stop if a missing consumer or restored-input obligation consumes the saving; reopen only with a changed legal boundary.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "centre path", + "persistent boundary", + "dirty recoding" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Fourier integrality raises the cited matched P112 commuting-phase event floors from 139 to 140 and 555 to 556, for one and four independent direct banks.", + "scope_change_reason": "The current-caller centre-sharing assignment is narrowed to an original historical terminal-interface obstruction. This does not meet the constructive supplier acceptance gate.", + "bottleneck_link": "A stronger necessary event count rules out attainment of the averaged terminal-query boundary within the cited alphabet. It supplies no new current-supplier invoice or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved integrality improvement; package it without searching for a larger bound.", + "outcome": "completed", + "evidence": "Written all-dimension Fourier proof; exact exhaustive small-multiset corroboration and domain/scope controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the 140-event or 556-event floor be attained in the exact matched alphabet?", + "why_it_matters": "The new result is a necessary lower bound, with no matching construction.", + "first_step": "Find an explicit polar multiset satisfying all necessary per-character inequalities, then attempt causal realization.", + "blocked_by": "No causal role-linear endpoint construction or complete physical bill is supplied." + }, + { + "question": "Can one priced noncommuting payload adapter change the complete matched-endpoint cost?", + "why_it_matters": "Such an adapter can escape the common-character premise.", + "first_step": "Specify its exact tensor-valid action between two phase events and its physical price.", + "blocked_by": "A realizable adapter and complete cost are missing; this is the predecessor opening, not new work here." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372194", + "predecessor": { + "pr": 2070, + "author": "jmbarrancoml", + "premises": "Causal rank inequality, common real-character sector, P112 spans and defect rank are cited without replay." + }, + "overlap": { + "checked_at_utc": "2026-11-03T11:05:19Z", + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "selected_pr": 6030, + "source": "PR #2070", + "source_author": "jmbarrancoml", + "coverage": "Live recent handoffs and active Discussions; open/account PRs; source PR body; main README and merged general-form/object/formula searches; cached card overlap; local reservations.", + "limits": "Sparse local notes, arbitrary historical diffs and unpublished work are not covered." + } +} diff --git a/research/matched-phase-integrality/VERIFY.json b/research/matched-phase-integrality/VERIFY.json new file mode 100644 index 0000000000..ab96c19151 --- /dev/null +++ b/research/matched-phase-integrality/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new Fourier rigidity census, independent character evaluation, inversion, combinatorial counts and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete finite corroboration and controls with optimized assertions disabled." + } + ] +} diff --git a/research/matched-phase-integrality/verify.py b/research/matched-phase-integrality/verify.py new file mode 100644 index 0000000000..f65338e9dc --- /dev/null +++ b/research/matched-phase-integrality/verify.py @@ -0,0 +1,179 @@ +"""Exact finite corroboration of the Fourier integrality lemma. + +Produced by Nick Petalas. Apache-2.0. +No predecessor scientific executable is imported or replayed. +""" + +from hashlib import sha256 +from itertools import combinations_with_replacement +from math import comb +import json +from pathlib import Path +import sys + + +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def validate(dimension: int, polars: tuple[int, ...]) -> None: + require(type(dimension) is int and 1 <= dimension <= 4, "dimension domain") + require(type(polars) is tuple, "tuple domain") + require(1 <= len(polars) <= 9 and len(polars) % 2 == 1, "odd size domain") + require(all(type(p) is int and 0 < p < (1 << dimension) for p in polars), + "nonzero polar domain") + + +def character_weights(dimension: int, polars: tuple[int, ...]) -> tuple[int, ...]: + """Direct character evaluation, independent of the butterfly transform.""" + return tuple(sum((p & chi).bit_count() % 2 for p in polars) + for chi in range(1 << dimension)) + + +def walsh(values: tuple[int, ...]) -> tuple[int, ...]: + require(len(values) in (2, 4, 8, 16), "transform size domain") + result = list(values) + for level in range(len(values).bit_length() - 1): + step = 1 << level + for start in range(0, len(values), 2 * step): + for offset in range(step): + left = start + offset + a, b = result[left], result[left + step] + result[left], result[left + step] = a + b, a - b + return tuple(result) + + +def is_subspace_indicator(multiplicities: tuple[int, ...]) -> bool: + if any(value not in (0, 1) for value in multiplicities): + return False + support = tuple(i for i, value in enumerate(multiplicities) if value) + return 0 in support and all(multiplicities[a ^ b] == 1 + for a in support for b in support) + + +def analyze(dimension: int, polars: tuple[int, ...]) -> bool: + validate(dimension, polars) + counts = [0] * (1 << dimension) + counts[0] = 1 + for polar in polars: + counts[polar] += 1 + weights = character_weights(dimension, polars) + spectrum = walsh(tuple(counts)) + require(spectrum == tuple(1 + len(polars) - 2 * t for t in weights), + "direct and butterfly characters differ") + inversion = walsh(spectrum) + require(inversion == tuple(len(counts) * x for x in counts), + "Fourier inversion failed") + positive = min(spectrum) >= 0 + require(positive == (max(weights) <= (len(polars) + 1) // 2), + "threshold mismatch") + require(positive == is_subspace_indicator(tuple(counts)), + "subspace rigidity failed") + if positive: + require((len(polars) + 1).bit_count() == 1, "non-power subspace order") + require(len(set(polars)) == len(polars), "repeated positive polar") + else: + require(max(weights) >= (len(polars) + 3) // 2, + "missing strict character witness") + return positive + + +def subspace_count(dimension: int, size: int) -> int: + if (size + 1).bit_count() != 1: + return 0 + rank = (size + 1).bit_length() - 1 + if rank > dimension: + return 0 + numerator = denominator = 1 + for i in range(rank): + numerator *= (1 << dimension) - (1 << i) + denominator *= (1 << rank) - (1 << i) + require(numerator % denominator == 0, "nonintegral subspace count") + return numerator // denominator + + +def enumerate_multisets() -> list[dict[str, int]]: + rows = [] + for dimension, maximum_size in ((1, 9), (2, 9), (3, 9), (4, 5)): + for size in range(1, maximum_size + 1, 2): + total = positive = 0 + for polars in combinations_with_replacement(range(1, 1 << dimension), size): + positive += analyze(dimension, polars) + total += 1 + require(total == comb((1 << dimension) + size - 2, size), + "multiset enumeration incomplete") + require(positive == subspace_count(dimension, size), + "subspace count disagrees with direct enumeration") + rows.append({"dimension": dimension, "size": size, + "multisets": total, "rigid": positive}) + return rows + + +def matched_boundary(banks: int) -> dict[str, int]: + require(type(banks) is int and banks in (1, 4), "bank domain") + # These dimensions and rank bounds are cited PR2070 premises. + span, defect = 112 * banks, 16 * banks + old_bound = (4 * span - 2 * defect + 2) // 3 + cap = defect - 2 * span + 2 * old_bound + require(old_bound % 2 == 1, "odd boundary missing") + require(cap == (old_bound + 1) // 2, "half-weight boundary missing") + require((old_bound + 1).bit_count() != 1, "simplex boundary cannot be excluded") + return {"banks": banks, "cited_span_each": span, "cited_defect_cap": defect, + "cited_average_bound": old_bound, "active_cap_at_boundary": cap, + "forced_active_witness": (old_bound + 3) // 2, + "new_event_lower_bound": old_bound + 1} + + +def rejection_controls() -> int: + invalid = ((0, (1,)), (5, (1,)), (True, (1,)), (2, ()), + (2, (1, 2)), (2, (0, 1, 2)), (2, (1, 2, 4)), + (2, (True,)), (2, [1]), (2, (1,) * 11)) + for dimension, polars in invalid: + try: + analyze(dimension, polars) + except ValueError: + continue + raise ValueError("invalid multiset accepted") + require(analyze(2, (1, 2, 3)), "simplex positive control failed") + require(analyze(3, tuple(range(1, 8))), "larger simplex control failed") + require(not analyze(2, (1, 1, 1)), "repeated-polar control failed") + require(max(character_weights(2, (0, 0, 1, 2, 3))) <= 3, + "zero-polar scope witness disappeared") + require(max(character_weights(2, (1, 2, 3))) > 1, + "incorrect lower threshold would pass simplex") + for invalid_banks in (0, 2, True): + try: + matched_boundary(invalid_banks) + except ValueError: + continue + raise ValueError("invalid bank count accepted") + return len(invalid) + 3 + + +def main() -> None: + require(len(sys.argv) == 1, "this verifier accepts no arguments") + rows = enumerate_multisets() + boundaries = [matched_boundary(banks) for banks in (1, 4)] + controls = rejection_controls() + package = Path(__file__).resolve().parent + hashes = {name: sha256((package / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + receipt = {"marker": "PASS_MATCHED_PHASE_INTEGRALITY", + "claim_type": "scoped proof with exact finite corroboration", + "source_premises": "cited PR2070 conclusions, not replayed", + "multisets": sum(row["multisets"] for row in rows), + "rigid_multisets": sum(row["rigid"] for row in rows), + "domain_rejections": controls, "semantic_control_groups": 5, + "domains": rows, "matched_boundaries": boundaries, + "sha256": hashes} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()