diff --git a/research/sparse-cyclic-quotient-obstructions/PROOF.md b/research/sparse-cyclic-quotient-obstructions/PROOF.md new file mode 100644 index 0000000000..d6ee1cb9e5 --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/PROOF.md @@ -0,0 +1,120 @@ +# Sharp obstructions to sparse cyclic compression + +Let S be a finite subset of Z^d. A cyclic projection is a homomorphism + + phi_w,q(x) = w dot x modulo q, q >= 2, w in Z^d. + +Call it faithful on S when its restriction to S is injective. The ambient +lattice Z^d is fixed. We optimize over all integer weights; weights need +not be units. This concerns a certificate's exponent support, not a physical +address operation. + +## Two-point supports + +**Theorem 1.** Let S={u,v}, u != v, and let h>0 be the gcd of the coordinates +of v-u. A faithful projection to Z/q exists if and only if q does not divide h. +Consequently its smallest possible modulus is + + mu(h) = min { q >= 2 : q does not divide h }. + +**Proof.** If q divides every coordinate difference, every dot product +vanishes modulo q. Conversely, if q does not divide h, it fails to divide +at least one coordinate difference. The corresponding coordinate weight +vector separates the two points. The gcd characterization follows because +q divides h exactly when it divides every coordinate difference. Translation +only adds a constant residue and does not affect injectivity. QED. + +**Corollary 1.** Every mu(h) is a prime power, and every prime power occurs. +No bound depending only on |S| or d bounds a faithful modulus, even for +|S|=2 and d=1. + +**Proof.** Put m=mu(h). Every positive integer below m divides h. If m has +at least two distinct prime factors, all its maximal prime-power factors +are below m and divide h. Their least common multiple is m, a contradiction. +Thus m is a prime power. Conversely, for a prime power m=p^a, set +h=lcm(1,...,m-1). Its p-adic valuation is a-1, so m does not divide h, while +every smaller positive integer does. Thus mu(h)=m. Arbitrarily large prime +powers give the unboundedness. QED. + +This is an existence minimum, not merely a failure of one weight heuristic. +The support points remain distinct over the integers throughout. +The fixed ambient lattice matters. If the allowed domain instead becomes +the subgroup generated by the differences, then {0,h} in hZ maps faithfully +to Z/2 by sending h to one. That map need not extend to the original Z. +The unboundedness therefore does not obstruct a frontend that first rebases +the generated subgroup. It is a precise limitation of integer weights on +the supplied coordinates. + +**Corollary 2.** For integer H>=1, the sharp worst-case minimum among +two-point differences with maximum absolute coordinate at most H is + + max mu(h) = min { m >= 2 : lcm(1,...,m) > H }. + +**Proof.** Write L_m=lcm(1,...,m), and let m be the first index with L_m>H. +For any 1<=h<=H, the supposition mu(h)>m implies L_m divides h, +contradicting L_m>H. Thus mu(h)<=m. The scalar difference h=L_(m-1) +is at most H. Also m does not divide it, since otherwise L_m=L_(m-1)<=H. +Every smaller integer divides it, so this difference attains mu(h)=m. +Every nonzero vector difference in the stated box has gcd at most H, and +the scalar witness embeds into any positive dimension. QED. + +For example, S={0,6} has optimal modulus four. Restricting the search to +prime moduli can therefore miss the optimum. + +## Pairwise possibility does not give a common projection + +**Theorem 2.** The support + + S = {(0,0), (1,0), (0,1), (1,1), (2,2)} + +has minimum faithful cyclic modulus six. At modulus five, every pair admits +a separating weight vector, but no weight vector separates all five points. +The mixed-radix box bound is nine. + +**Proof.** Cardinality excludes moduli below five. Suppose weights (a,b) +are injective modulo five. The first four points have images 0,a,b,a+b. +Their distinctness forces a,b != 0 and b/a not in {0,1,-1}. Over F5 the +remaining possibilities are b/a=2 or 3. Scale by a^-1. If b/a=2, the final +point has image 2(1+2)=1, colliding with (1,0). If b/a=3, it has image +2(1+3)=3, colliding with (0,1). Thus modulus five is impossible. + +For every pair, the coordinate difference is nonzero modulo five. At least +one coordinate projection separates it, proving the pairwise assertion. +At modulus six, weights (1,3) give the distinct residues (0,1,3,4,2), +in the displayed order. The coordinate widths are both two, so the box +construction gives (2+1)(2+1)=9. QED. + +The first four points are exactly the subset sums of paid labels +(1,0),(0,1); the last point can be a target exponent. Thus this is a +subset-sum-plus-target support of the predecessor's declared form. It can +be used at any register count. No candidate word or true target identity +is asserted merely from this support description. +Here the support generates all of Z^2, so rebasing its generated subgroup +cannot avoid the optimum. All homomorphisms out of that group are already +among the integer weights considered above. + +## Consequence for finite replay + +PR #1440 supplies the sufficient mixed-radix projection and faithful +regular-action criterion. We use that criterion without replaying its +fixtures or claiming it as new. For completeness, a binary formal coefficient +vector supported on S maps to a cyclic coefficient vector by XORing terms +with equal residues. If the projection is injective, different support terms +cannot cancel, so this coefficient map is injective. If two points collide, +their two-term sum is a nonzero formal polynomial with zero cyclic image. +The regular action recovers cyclic coefficients by acting on the basis +vector at address zero. Checking every role/address column detects exactly +the cyclic coefficient map, including its kernel at an unfaithful projection. + +The new fixture has 32 binary support polynomials. The checker enumerates +them all, with all weights modulo one through six, and compares direct +translated address columns with coefficient convolution. Each noninjective +weight gets an actual two-term kernel witness. Modulus one is a rejection +control, not an allowed optimum. The written proofs establish the unbounded +statements; finite checks do not extrapolate them. + +This is not an error in PR #1440 or an obstruction to its valid box bound. +It explains why a smaller exact quotient needs arithmetic information and +a simultaneous injection check. Native realization, physical conversion, +complete signed moment, supplier admission and the multiplication theorem +remain outside this result. diff --git a/research/sparse-cyclic-quotient-obstructions/README.md b/research/sparse-cyclic-quotient-obstructions/README.md new file mode 100644 index 0000000000..8df4b876ef --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/README.md @@ -0,0 +1,114 @@ +# Sharp sparse cyclic quotient obstructions + +Scoped algebraic proof with exact finite corroboration. No new kappa. + +For a two-point exponent support {u,v}, let h be the positive gcd of the +coordinates of v-u. With the ambient integer lattice fixed, its smallest +faithful cyclic quotient has size + + mu(h) = min { q >= 2 : q does not divide h }. + +Every such minimum is a prime power, and every prime power occurs. Thus even +two points in one dimension can require arbitrarily large moduli. For maximum +coordinate difference H, the sharp worst-case minimum is the first m with +`lcm(1,...,m)>H`. These statements optimize over every integer weight vector. + +A separate exact fixture shows the simultaneous constraint. The support + + {(0,0), (1,0), (0,1), (1,1), (2,2)} + +has optimum modulus **six**, versus its mixed-radix box bound **nine**. +Weights (1,3) give residues (0,1,3,4,2) modulo six. Modulus five fails for every +weight, although all ten pairs can be separated individually modulo five. +The first four points are the subset sums of (1,0),(0,1), and the last is a +target exponent. No true register identity is asserted from that support alone. + +[PROOF.md](PROOF.md) proves the unbounded laws and the exact fixture minimum. +The result answers the short-quotient question in woklerx's +[PR #1440](https://github.com/CrocSwap/integer-mult-bounds/pull/1440). +It gives a smaller finite representation on a new support and two exact +obstructions to support-size or pairwise-only compression rules. The source's +mixed-radix theorem remains valid and is not audited here. + +## Reproduce + +From the repository root, using the local CPython 3.12 interpreter: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sparse-cyclic-quotient-obstructions/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sparse-cyclic-quotient-obstructions/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sparse-cyclic-quotient-obstructions +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sparse-cyclic-quotient-obstructions --check-source-history +``` + +Another CPython 3.12 path can replace the absolute interpreter path. Only the +standard library is needed. The verifier writes no files and has no executable +predecessor dependency. Both registered commands produce +`PASS_SPARSE_CYCLIC_QUOTIENT_OBSTRUCTIONS no_new_kappa`; the runner also reports +`PASS_REGISTERED_RESEARCH_PACKAGE`. A generated stdout receipt binds all six +package files by SHA256. No handwritten receipt is used. + +The declared finite corroboration is: + +- All 4,096 scalar heights through 4,096, with the exact minimax envelope at + every height, and all 27 prime-power realizations through 64. +- All 1,176 vector/modulus cases for nonzero differences in [-6,6]^2 and + moduli 2 through 8, enumerating 34,104 weight vectors. +- All 91 weight vectors modulo 1 through 6 on the new support. The numbers + of injective projections are (0,0,0,0,0,8). +- All 32 binary support polynomials at every such projection, comparing + 14,112 regular-action columns against direct integer-exponent translations. + Every unfaithful projection gets an explicit nonzero two-term kernel witness. +- All ten pairs modulo five, four rejected unsafe projections and three + semantic controls for an omitted target, prime-only search and a modulus + bound based solely on support size. + +Finite enumeration is evidence for the implementation. The written proof, +not extrapolation from those counts, establishes the general statements. + +## Scope and limitations + +This is a verification side result under a changed task-card scope. It does +not satisfy the card's complete decoder/supplier acceptance gate. The modulus +is a certificate representation size; a smaller modulus is not a runtime +speedup or a legal physical address realization. No larger-register candidate, +selected paid/target profile, complete native/ordinary invoice, all-size +compiler, precision, tape/stock bound or multiplication theorem is supplied. +No selected cold replay, proof kernel or independent human review was run. + +The two-point obstruction assumes integer weights on the supplied ambient +lattice. A frontend may evade it by first rebasing the subgroup generated +by the differences: {0,h} inside hZ then needs only modulus two. That is a +different domain for the homomorphism. The five-point support generates +all of Z^2, so its optimum six survives such a change of group basis. + +[SOURCES.json](SOURCES.json) pins the source README, original catalogue and +selected record as historical provenance at canonical main +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. They are not executable inputs. +The package itself can replay without Git or a network. Predecessor code, +frozen evidence and the selected frontier are unchanged. + +The Python checker uses bounded finite loops and functions below 60 lines. +Managed-runtime allocation is the Power of Ten deviation: live collections +are limited to 32 polynomial images, six fixture success counts and a fixed +six-file hash receipt, plus fixed-size vectors. Integer values are bounded +by the displayed scalar and prime-power domains. It has no recursive calls, +code generation, subprocesses or hidden runtime dispatch. + +## Open next questions + +Can one compress the full support of an actual larger-register candidate +below its mixed-radix box bound? First retain every subset sum and target +exponent, test arithmetic pair obstructions, then certify one simultaneous +injective weight vector. A specified candidate and an explicit representation +cost allowance are missing. [TASK.json](TASK.json) records this handoff. + +## Credit + +The sharp sparse-support analysis, new five-point fixture, proof and checker +were produced by Nick Petalas. Credit woklerx's PR #1440 for posing the +short-quotient question, its sufficient mixed-radix injection and faithful +regular-action criterion, and its retained eumemic PR #288 / huxint PR #203 +register-model lineage. Gcd, least-common-multiple and regular-representation +facts are classical; no general literature-priority claim is made. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/sparse-cyclic-quotient-obstructions/SOURCES.json b/research/sparse-cyclic-quotient-obstructions/SOURCES.json new file mode 100644 index 0000000000..0dac7764d9 --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/bit-faithful-finite-address/README.md", + "usage": "provenance", + "git_blob": "0f3c0ded3e2ec8af5e50d9919784cde88ab29bb4", + "sha256": "b4e345bc8e86d069979a57ade7cb381812474ffbb0d7033d5a1283fc99eb16cb" + } + ] +} diff --git a/research/sparse-cyclic-quotient-obstructions/TASK.json b/research/sparse-cyclic-quotient-obstructions/TASK.json new file mode 100644 index 0000000000..9c413914d8 --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "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": "Sharp fixed-ambient-lattice obstructions and exact smallest faithful cyclic quotients for two-point supports and one five-point subset-sum/target support.", + "scope_change_reason": "The selected baseline binds correctly, but this is an explicitly scoped verification side result answering PR1440's short-quotient question. It does not price a changed decoder or satisfy the original complete supplier gate.", + "bottleneck_link": "A faithful cyclic quotient can reduce the exact finite certificate representation. The result identifies arithmetic and simultaneous-separation barriers to compressing that representation. It does not change a recursive invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first checked exact modulus improvement and sparse-support obstruction; package the five-point optimum and two-point law without extending to a larger search.", + "outcome": "completed", + "evidence": "PROOF.md gives the unbounded gcd/LCM laws and exact five-point minimum. verify.py generates a SHA256-bound receipt for all six package files and exhausts the declared finite domains.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one compress the full support of an actual larger-register candidate below its mixed-radix box bound?", + "why_it_matters": "This would turn the sparse-support criteria into a concrete reduction of finite replay state and column count.", + "first_step": "Retain every subset sum and target exponent of one newly proposed candidate, test arithmetic pair obstructions, and certify one simultaneous injective weight vector.", + "blocked_by": "A specified candidate with a complete support and an explicit representation-cost allowance; pairwise separation alone is insufficient." + } + ] +} diff --git a/research/sparse-cyclic-quotient-obstructions/VERIFY.json b/research/sparse-cyclic-quotient-obstructions/VERIFY.json new file mode 100644 index 0000000000..0f0fffa02b --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/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 two-point gcd/LCM laws on the stated finite domains; all small-fixture projections and binary regular-action columns; unsafe quotient, omitted-target, prime-only and support-size controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact two-point gcd/LCM laws on the stated finite domains; all small-fixture projections and binary regular-action columns; unsafe quotient, omitted-target, prime-only and support-size controls." + } + ] +} diff --git a/research/sparse-cyclic-quotient-obstructions/verify.py b/research/sparse-cyclic-quotient-obstructions/verify.py new file mode 100644 index 0000000000..a6608ed29e --- /dev/null +++ b/research/sparse-cyclic-quotient-obstructions/verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Read-only exact corroboration of the sparse cyclic quotient proof.""" + +from hashlib import sha256 +from itertools import combinations, product +import json +from math import gcd, lcm +from pathlib import Path +import sys + + +SUPPORT = ((0, 0), (1, 0), (0, 1), (1, 1), (2, 2)) +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def least_nondivisor(value: int) -> int: + """The finite range includes value+1, which cannot divide positive value.""" + for modulus in range(2, value + 2): + if value % modulus: + return modulus + raise ValueError("positive integer has no nondivisor") + + +def prime_power(value: int) -> bool: + for prime in range(2, value + 1): + if value % prime == 0: + remainder = value + for _ in range(value.bit_length()): + if remainder % prime: + break + remainder //= prime + return remainder == 1 + raise ValueError("prime-power test requires value >= 2") + + +def images(support: tuple, weights: tuple, modulus: int) -> tuple: + return tuple(sum(a * b for a, b in zip(point, weights)) % modulus + for point in support) + + +def require_injection(support: tuple, weights: tuple, modulus: int) -> tuple: + residues = images(support, weights, modulus) + need(len(set(residues)) == len(support), "cyclic projection aliases support") + return residues + + +def scalar_checks() -> dict: + largest_minimum = 0 + for height in range(1, 4097): + minimum = least_nondivisor(height) + need(prime_power(minimum), "minimum is not a prime power") + largest_minimum = max(largest_minimum, minimum) + running_lcm = 1 + for modulus in range(2, height + 2): + running_lcm = lcm(running_lcm, modulus) + if running_lcm > height: + need(modulus == largest_minimum, "minimax LCM formula failed") + break + else: + raise ValueError("LCM never exceeded height") + realizations = 0 + for minimum in range(2, 65): + if prime_power(minimum): + value = lcm(*range(1, minimum)) + need(value % minimum != 0, "prime-power realization aliases") + need(all(value % q == 0 for q in range(2, minimum)), + "realization has smaller faithful modulus") + realizations += 1 + return {"scalar_heights": 4096, "prime_power_realizations": realizations, + "largest_minimum_through_4096": largest_minimum} + + +def vector_checks() -> dict: + cases = 0 + projections = 0 + for delta in product(range(-6, 7), repeat=2): + if delta == (0, 0): + continue + content = gcd(*delta) + for modulus in range(2, 9): + separated = False + for weights in product(range(modulus), repeat=2): + projections += 1 + if images(((0, 0), delta), weights, modulus)[1] != 0: + separated = True + need(separated == (content % modulus != 0), "content criterion failed") + cases += 1 + return {"vector_modulus_cases": cases, "vector_projections": projections} + + +def polynomial_image(mask: int, residues: tuple) -> int: + coefficients = 0 + for index, residue in enumerate(residues): + if mask & (1 << index): + coefficients ^= 1 << residue + return coefficients + + +def literal_column(mask: int, weights: tuple, modulus: int, source: int) -> int: + """Act directly on an address column using the integer exponents.""" + result = 0 + for index, (x, y) in enumerate(SUPPORT): + if mask & (1 << index): + destination = (source + x * weights[0] + y * weights[1]) % modulus + result ^= 1 << destination + return result + + +def rotated_column(coefficients: int, modulus: int, source: int) -> int: + output = 0 + for address in range(modulus): + if coefficients & (1 << address): + output |= 1 << ((address + source) % modulus) + return output + + +def fixture_checks() -> dict: + successes = [] + columns = 0 + projections = 0 + for modulus in range(1, 7): + successful = 0 + for weights in product(range(modulus), repeat=2): + projections += 1 + residues = images(SUPPORT, weights, modulus) + faithful = len(set(residues)) == len(SUPPORT) + successful += faithful + coefficient_images = set() + for mask in range(1 << len(SUPPORT)): + coefficients = polynomial_image(mask, residues) + coefficient_images.add(coefficients) + for source in range(modulus): + need(literal_column(mask, weights, modulus, source) + == rotated_column(coefficients, modulus, source), + "formal coefficients and regular action disagree") + columns += 1 + need((len(coefficient_images) == 32) == faithful, + "regular representation does not match support injection") + if not faithful: + left, right = next((i, j) for i, j in combinations(range(5), 2) + if residues[i] == residues[j]) + need(polynomial_image((1 << left) | (1 << right), residues) == 0, + "alias does not give a nonzero formal kernel element") + successes.append(successful) + need(successes[:5] == [0] * 5 and successes[5] > 0, "minimum is not six") + witness = require_injection(SUPPORT, (1, 3), 6) + need(witness == (0, 1, 3, 4, 2), "wrong six-point residue witness") + pair_checks = 0 + for left, right in combinations(SUPPORT, 2): + delta = tuple(a - b for a, b in zip(left, right)) + need(gcd(*delta) % 5 != 0, "pair is unavoidably aliased modulo five") + need(any(images((left, right), weights, 5)[0] + != images((left, right), weights, 5)[1] + for weights in product(range(5), repeat=2)), + "pairwise separation failed") + pair_checks += 1 + return {"fixture_minimum": 6, "box_modulus": 9, + "successful_projections_by_modulus_1_to_6": successes, + "fixture_projections": projections, "regular_action_columns": columns, + "separable_pairs_modulo_5": pair_checks} + + +def rejection_controls() -> dict: + rejected = 0 + for weights, modulus in (((1, 2), 5), ((1, 3), 5), ((1, 2), 6)): + try: + require_injection(SUPPORT, weights, modulus) + except ValueError: + rejected += 1 + else: + raise ValueError("unsafe fixture projection was accepted") + try: + require_injection(((0,), (2,)), (1,), 2) + except ValueError: + rejected += 1 + else: + raise ValueError("two-point torsion control was accepted") + require_injection(SUPPORT[:4], (1, 2), 5) + need(images(SUPPORT, (1, 2), 5)[-1] == 1, + "omitted-target control did not expose the collision") + need(least_nondivisor(6) == 4, "prime-only search misses optimum four") + need(least_nondivisor(lcm(*range(1, 17))) == 17, + "support-size-only modulus control failed") + return {"rejected_projections": rejected, "semantic_controls": 3} + + +def main() -> None: + need(len(sys.argv) == 1, "this read-only verifier accepts no arguments") + receipt = {} + for result in (scalar_checks(), vector_checks(), fixture_checks(), + rejection_controls()): + receipt.update(result) + root = Path(__file__).resolve().parent + receipt["files_sha256"] = { + name: sha256((root / name).read_bytes()).hexdigest() for name in PACKAGE_FILES + } + receipt["python"] = sys.version.split()[0] + print(json.dumps(receipt, indent=2, sort_keys=True)) + print("PASS_SPARSE_CYCLIC_QUOTIENT_OBSTRUCTIONS no_new_kappa") + + +if __name__ == "__main__": + main()