diff --git a/research/equal-energy-radix-parity/README.md b/research/equal-energy-radix-parity/README.md new file mode 100644 index 0000000000..82637e77e3 --- /dev/null +++ b/research/equal-energy-radix-parity/README.md @@ -0,0 +1,203 @@ +# A smaller even radix for equal-energy packed rows + +Scoped written proof with exact finite corroboration, produced by Nick Petalas. +Apache-2.0. No new kappa or complete multiplication theorem is claimed. + +Equal-energy Gaussian-integer rows admit a smaller sufficient even packing +radix than the whole-ball threshold in +[Arham Tahir's PR #1906](https://github.com/CrocSwap/integer-mult-bounds/pull/1906). +At row energy `512^2`, **B=726 suffices instead of B=1024**. For 512 columns, +the largest packed input `B^511` has **4,857 bits instead of 5,111**, a +reduction of 254 bits. These are exact integer lengths, not runtime measurements. +The row-energy hypothesis is essential. + +## Theorem and proof + +For a finite vector z over Z[i], define + +``` +E(z) = sum_j |z_j|^2, P_B(z) = sum_j z_j B^j. +``` + +**Sharp even-energy kernel bound.** For every even integer B>=2, a nonzero +finite Gaussian-integer vector d with P_B(d)=0 and even E(d) satisfies + +``` +E(d) >= 2(B^2-B+1). (1) +``` + +Equality is attained by d=(B,B-1,-1), and by appending zero coordinates. +Thus (1) is sharp uniformly in dimensions at least three. No assertion of +sharpness for differences of unitary rows follows from this witness. + +To prove (1), regard d as the coefficients of D(x). Since D(B)=0, +monic division gives D(x)=(x-B)Q(x) with Gaussian-integer coefficients q. +The finite nonzero q has at most one fewer coefficient than d. Extend q +by zeros at both ends and put + +``` +S = sum_j |q_j|^2, +V = |q_0|^2 + sum_j |q_(j+1)-q_j|^2 + |q_last|^2. +``` + +The sum in V runs over consecutive coefficients inside q. Expansion gives + +``` +E(d) = (B^2+1) S - 2B Re sum_j q_j conjugate(q_(j+1)) + = (B-1)^2 S + B V. (2) +``` + +The first jump from zero to a nonzero Gaussian integer and the last jump +back to zero each contribute at least one to V, even if the supplied +coefficient list contains leading or trailing zeros. Therefore V>=2. +Since B is even, (2) gives E(d)=S modulo 2. The assumed even energy forces +S to be a positive even integer, hence S>=2. Equation (2) now yields + +``` +E(d) >= 2(B-1)^2 + 2B = 2(B^2-B+1). +``` + +The displayed d evaluates to zero and has exactly that energy, proving +sharpness. The parity step is the new restriction absent from the +whole-ball B^2+1 argument. + +**Equal-energy comparator.** Let u,v be Gaussian-integer rows of the same +finite length, with E(u)=E(v)<=M. If B>=2 is even and + +``` +B^2-B+1 > 2M, (3) +``` + +then P_B(u)=P_B(v) if and only if u=v. Indeed d=u-v has even energy because + +``` +E(d) = 2E(u) - 2 Re sum_j u_j conjugate(v_j). +``` + +The parallelogram identity also gives E(d)<=4M. A nonzero packing-kernel +difference would contradict (1) and (3). This proves the statement in every +finite dimension, jointly for real and imaginary components, including +absolute phase. The sufficient condition (3) is not claimed optimal. + +## Application and exact improvement + +PR #1906 supplies the retained gate-valid unitary premise and the scaling +contract. If U1,U2 are square unitary matrices, R U1 and R U2 are +Gaussian-integer matrices, and R is a positive integer, every scaled row +has the same energy R^2. Apply (3) row by row with M=R^2. Evaluation on the +single vector (1,B,...,B^(N-1)) then determines the complete matrices. + +For two retained circuits with C-gate counts k1,k2, that predecessor sets +K=max(k1,k2), rescales both integer executions to R=2^K, and obtains the +required equal row energies. Those premises are cited, not re-audited here. +The new lemma applies to every such matrix pair; no particular predecessor +circuit or recorded receipt is replayed. + +At the N=512, K=9 parameters reported in #1906: + +``` +M = 262144, 2M = 524288, +726^2-726+1 = 526351 > 524288, +724^2-724+1 = 523453 < 524288. +bit_length(726^511) = 4857, +bit_length(1024^511) = 5111. +``` + +Thus 726 is the least even radix satisfying **this criterion**, rather than +an asserted minimum radix for the actual rows. It is smaller than the +whole-ball threshold 2R by 298. A power-of-two radix remains 1024 under this +criterion; exploiting 726 requires general integer multiplication in the +packing recurrence. A speedup, lower total execution cost, production adoption +and a new Lean theorem are all outside this contribution. + +## Reproduction and evidence + +From the repository root, with the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/equal-energy-radix-parity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/equal-energy-radix-parity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/equal-energy-radix-parity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/equal-energy-radix-parity --check-source-history +``` + +Expected marker: `PASS_EQUAL_ENERGY_RADIX_PARITY`. The proof supplies the +unbounded conclusion. The standalone verifier corroborates it with: + +- 6,200 constructed quotient/kernel identities, including 3,112 nonzero + even-energy kernel vectors, and 256 sharp witnesses at even B=2..128. +- Independent direct polynomial sums on all 3,051 real three-digit words + with digits in [-B,B] at B=2,4,6, and 1,875 complex two-digit words with + real/imaginary digits in [-2,2]. Respectively six and four are nonzero + even-energy kernel vectors. +- 19,800 complete equal-energy shell vectors at energies 2,6,10 and complex + lengths 1..4, obtained by filtering 6,299,180 bounded digit words. The + (energy,packed-value) keys have no collision at the proved radices. +- Thirty new small scaled-unitary fixtures at dimensions 2,4,8 and C counts + 0..9, 840 exact Gram entries, 300 normalized matrix comparisons across + unequal C counts, and thirty rejected absolute-phase mutations. +- Four explicit hypothesis countercontrols and thirteen input rejections. + Odd radix B=3 admits the even-energy kernel (3,-1) below (1). At even + B=2 the odd-energy vector (2,-1) also violates (1). Two rows of energies + 36 and 37 collide at B=12 while satisfying the other M=64 hypotheses. + Distinct rows of equal energy three collide at the unsafe radix two. +- Exact least-even-criterion arithmetic at all M=1..4096, plus the stated + R=512 application. This is not a search for optimal comparator radices. + +`--receipt /absolute/path/outside/checkout.json` optionally writes the actual +executed counts, interpreter version and SHA256 of all five package files. +Default replay writes nothing. The receipt is generated, not hand-written. +The source README and orientation records are pinned as provenance only; +no predecessor executable or numeric receipt is imported. Direct replay is +Git-free and supports read-only exported package files. + +Power-of-ten scope: no recursion, no external solver, no dynamic code generation, +functions under 60 lines and explicit contracts that remain active under -O. +All loops use fixed domains. The largest enumeration has 7^8 digit words; +its set is bounded by that domain. Integer and collection allocation in Python +is a managed-runtime deviation from fixed allocation, constrained here by the +fixed dimensions, digit bounds and gate counts. The comparator boundary caps +rows at sixteen coordinates, components at 2^32 and M at 2^64. Warning-strict +normal and optimized replays supply the applicable interpreter diagnostics. + +## Scope, overlap and credit + +The formal-interface-lemma card is changed to a written algebraic side result. +Its first baseline command passed with `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`. +The selected result and all five framework assumptions are untouched. + +Credit Arham Tahir / Arham-Tahir64 #1906 for the energy-ball method and its +explicitly excluded equal-energy sharpness scope; woklerx #1859 for the +unitary premise; Jeremy Kothe / jeremykothe2 #593 for the retained Clifford +semantics and packed equality argument; commdata2338 for semantic binding; +Ross Richardson #1934 for separate full-matrix corroboration; ywz65 #2499 +for the separate formal energy law; and the retained Lemma A/G, icekylinx, +Chafik Boukhalfa and jacklightChen lineage. Polynomial division, the +parallelogram identity and the discrete quadratic-energy expansion are classical. +The new step is their parity-sensitive packing-kernel application and its +smaller sufficient equal-energy radix. No literature-wide priority is claimed. +Predecessor credit lines and files are unchanged. + +Overlap checks read live open PRs, this account's recent PRs, active Discussions, +local reservations, relevant merged PR bodies and all-main README searches for +packed radix, equal-energy packing, the new formula and the value 726. +The cached card scan covered 310 open PRs and 5,456 Discussion records, with +7,902 sparse local notes omitted. Separate Git searches covered relevant +omitted README text. Closed PR diffs, nested code and unpublished work remain +coverage limits. The prospective +[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19219147) +records the target. These checks are not proof of novelty. + +## Open next questions + +What is the smallest common energy of a genuine pair of colliding rows at an +even radix, and which such rows extend to scaled Clifford matrices? Start with +a fixed B and minimize both row energies subject to equal packing. The sharp +kernel witness alone need not be realizable at the radius used by the bound. +This blocks any claim that (3) or 726 is optimal for actual unitary rows. + +Can the quotient energy identity and finite-path variation bound be proved in +Lean and connected to an actual comparator? The first step is that exact +integer lemma, followed by the gate-valid equal-row-energy interface. +No kernel proof, implementation-cost study, supplier replay or complete +multiplication proof was run. Structured questions are in TASK.json. diff --git a/research/equal-energy-radix-parity/SOURCES.json b/research/equal-energy-radix-parity/SOURCES.json new file mode 100644 index 0000000000..fc90786a57 --- /dev/null +++ b/research/equal-energy-radix-parity/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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/hpe-energy-packed-radix/README.md", + "usage": "provenance", + "git_blob": "e86f4753945427dc3ac5076c6c8ecc5de8671132", + "sha256": "5cd9319919128c1f976ec48e86858f697b5a7f77b012183b1909a2d3df33ae43" + } + ] +} diff --git a/research/equal-energy-radix-parity/TASK.json b/research/equal-energy-radix-parity/TASK.json new file mode 100644 index 0000000000..50cfcfafb3 --- /dev/null +++ b/research/equal-energy-radix-parity/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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": "Prove a sharp even-energy Gaussian packing-kernel bound and a smaller sufficient even radix for equal-energy rows.", + "scope_change_reason": "A written algebraic side result changes the whole-ball premise in PR1906 to equal-energy rows. It supplies no new proof-assistant theorem or selected caller admission.", + "bottleneck_link": "Exact operator equality can use smaller packed integers while retaining every row and absolute phase, under explicit equal-row-energy premises.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved radix reduction and standalone finite corroboration; do not replay predecessor circuit inventories or extend to an optimal unitary radix.", + "outcome": "completed", + "evidence": "Written proof and standalone exact kernel, sphere, scaled-unitary, phase and hypothesis controls; generated hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the minimum sufficient radix for equal-energy Gaussian rows, or for the smaller subset of actual Clifford rows?", + "why_it_matters": "The sharp even-kernel bound does not make the row-comparison criterion sharp.", + "first_step": "Find the least common energy of two distinct rows with the same packing at a fixed even radix.", + "blocked_by": "Equal-energy realizability and complete unitary extension are stronger than even difference energy." + }, + { + "question": "Can the parity-sensitive kernel bound be formalized and connected to a production comparator?", + "why_it_matters": "The result presently supplies a written lemma, not a replacement kernel-checked comparator.", + "first_step": "Formalize the quotient energy identity and finite-path variation bound, then retain exact row-energy and gate-validity guards.", + "blocked_by": "No new Lean proof or implementation/cost study is supplied." + } + ] +} diff --git a/research/equal-energy-radix-parity/VERIFY.json b/research/equal-energy-radix-parity/VERIFY.json new file mode 100644 index 0000000000..972d6271de --- /dev/null +++ b/research/equal-energy-radix-parity/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": "Exact kernel and equal-energy sphere enumeration; scaled-unitary comparisons and phase/contract rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same finite coverage and all explicit rejection controls with assertions disabled." + } + ] +} diff --git a/research/equal-energy-radix-parity/verify.py b/research/equal-energy-radix-parity/verify.py new file mode 100644 index 0000000000..0407386b56 --- /dev/null +++ b/research/equal-energy-radix-parity/verify.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written equal-energy radix theorem.""" +import argparse +import hashlib +import itertools +import json +import math +from pathlib import Path +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def energy(row): + return sum(a * a + b * b for a, b in row) + + +def pack(row, radix): + value = (0, 0) + for a, b in reversed(row): + value = (value[0] * radix + a, value[1] * radix + b) + return value + + +def safe_radix(bound): + require(type(bound) is int and 1 <= bound <= 1 << 64, "energy bound outside 1..2^64") + radix = max(2, math.isqrt(2 * bound)) + radix += radix % 2 + if radix * radix - radix + 1 <= 2 * bound: + radix += 2 + require(radix * radix - radix + 1 > 2 * bound, "radix construction failed") + require(radix == 2 or (radix - 2) ** 2 - (radix - 2) + 1 <= 2 * bound, + "not the smallest even radix satisfying this criterion") + return radix + + +def admitted_pair(left, right, radix, bound): + require(type(radix) is int and radix >= 2 and radix % 2 == 0, "invalid even radix") + require(type(bound) is int and 1 <= bound <= 1 << 64, "invalid energy bound") + require(radix * radix - radix + 1 > 2 * bound, "unproved radix") + require(1 <= len(left) == len(right) <= 16, "invalid row lengths") + for row in (left, right): + for z in row: + require(isinstance(z, tuple) and len(z) == 2 and + all(type(x) is int and abs(x) <= 1 << 32 for x in z), "invalid digit") + require(energy(left) == energy(right) <= bound, "unequal or excessive row energy") + return pack(left, radix) == pack(right, radix) + + +def quotient_checks(): + alphabet = ((0, 0), (1, 0), (-1, 0), (0, 1), (0, -1), (1, 1)) + counts = dict(quotients=0, even_kernel_vectors=0, sharp_vectors=0) + for length in range(1, 5): + for q in itertools.product(alphabet, repeat=length): + if energy(q) == 0: + continue + padded = ((0, 0),) + q + ((0, 0),) + variation = sum(energy((sub(b, a),)) for a, b in zip(padded, padded[1:])) + require(variation >= 2, "finite path variation") + for radix in (2, 4, 6, 10): + d = tuple(sub(a, (radix * b[0], radix * b[1])) + for a, b in zip(padded, padded[1:])) + e = energy(d) + require(pack(d, radix) == (0, 0), "quotient not in kernel") + require(e == (radix - 1) ** 2 * energy(q) + radix * variation, + "discrete energy identity") + require(e % 2 == energy(q) % 2, "parity identity") + counts['quotients'] += 1 + if e % 2 == 0: + require(e >= 2 * (radix * radix - radix + 1), "even kernel bound") + counts['even_kernel_vectors'] += 1 + for radix in range(2, 130, 2): + for phase in ((1, 0), (-1, 0), (0, 1), (0, -1)): + d = tuple(mul(phase, (x, 0)) for x in (radix, radix - 1, -1)) + require(pack(d, radix) == (0, 0), "sharp witness packing") + require(energy(d) == 2 * (radix * radix - radix + 1), "sharp energy") + counts['sharp_vectors'] += 1 + return counts + + +def direct_kernel_checks(): + counts = dict(real_digit_words=0, real_even_kernels=0, + complex_digit_words=0, complex_even_kernels=0) + for radix in (2, 4, 6): + for digits in itertools.product(range(-radix, radix + 1), repeat=3): + value = sum(digits[j] * radix ** j for j in range(3)) + e = sum(x * x for x in digits) + counts['real_digit_words'] += 1 + if value == 0 and e > 0 and e % 2 == 0: + require(e >= 2 * (radix * radix - radix + 1), "direct real kernel") + counts['real_even_kernels'] += 1 + for digits in itertools.product(range(-2, 3), repeat=4): + value = (digits[0] + radix * digits[2], digits[1] + radix * digits[3]) + e = sum(x * x for x in digits) + counts['complex_digit_words'] += 1 + if value == (0, 0) and e > 0 and e % 2 == 0: + require(e >= 2 * (radix * radix - radix + 1), "direct complex kernel") + counts['complex_even_kernels'] += 1 + return counts + + +def sphere_checks(): + counts = dict(sphere_candidates=0, admitted_sphere_vectors=0) + for bound in (2, 6, 10): + radius = math.isqrt(bound) + radix = safe_radix(bound) + for length in range(1, 5): + seen = set() + for digits in itertools.product(range(-radius, radius + 1), repeat=2 * length): + counts['sphere_candidates'] += 1 + e = sum(x * x for x in digits) + if e != bound: + continue + row = tuple((digits[2 * j], digits[2 * j + 1]) for j in range(length)) + key = (e, pack(row, radix)) + require(key not in seen, "equal-energy packing collision") + seen.add(key) + counts['admitted_sphere_vectors'] += 1 + return counts + + +def matrix_fixtures(): + counts = dict(unitary_matrices=0, gram_entries=0, matrix_pairs=0, phase_mutants=0) + for width in (2, 4, 8): + rows = tuple(tuple((int(i == j), 0) for j in range(width)) for i in range(width)) + matrices = [(0, rows)] + for step in range(9): + mask = 1 << (step % (width.bit_length() - 1)) + rows = tuple(tuple(add(mul((1, 1), rows[i][j]), mul((1, -1), rows[i ^ mask][j])) + for j in range(width)) for i in range(width)) + matrices.append((step + 1, rows)) + for k, matrix in matrices: + for i in range(width): + require(energy(matrix[i]) == 4 ** k, "scaled row energy") + for j in range(width): + gram = (0, 0) + for a, b in zip(matrix[i], matrix[j]): + gram = add(gram, mul(a, (b[0], -b[1]))) + require(gram == (4 ** k if i == j else 0, 0), "scaled unitarity") + counts['gram_entries'] += 1 + counts['unitary_matrices'] += 1 + for (k, left), (ell, right) in itertools.product(matrices, repeat=2): + top = max(k, ell) + a = tuple(tuple((x << (top - k), y << (top - k)) for x, y in row) for row in left) + b = tuple(tuple((x << (top - ell), y << (top - ell)) for x, y in row) for row in right) + same = all(admitted_pair(u, v, safe_radix(4 ** top), 4 ** top) for u, v in zip(a, b)) + require(same == (a == b), "packed versus full matrix equality") + counts['matrix_pairs'] += 1 + for k, matrix in matrices: + mutant = tuple(mul((0, 1), z) for z in matrix[0]) + require(not admitted_pair(matrix[0], mutant, safe_radix(4 ** k), 4 ** k), + "absolute phase mutant") + counts['phase_mutants'] += 1 + return counts + + +def controls(): + odd = ((3, 0), (-1, 0)) + require(pack(odd, 3) == (0, 0) and energy(odd) < 2 * (9 - 3 + 1), "odd radix control") + low = ((2, 0), (-1, 0)) + require(energy(low) % 2 == 1 and energy(low) < 2 * (4 - 2 + 1), "odd energy control") + unequal = (((6, 0), (0, 0)), ((-6, 0), (1, 0))) + require(pack(unequal[0], 12) == pack(unequal[1], 12), "unequal-energy collision") + require(energy(unequal[0]) != energy(unequal[1]) and + max(map(energy, unequal)) <= 64 and 12 ** 2 - 12 + 1 > 128, + "unequal-energy control must satisfy the other hypotheses") + collision = (((1, 1), (0, -1)), ((-1, -1), (1, 0))) + require(energy(collision[0]) == energy(collision[1]) == 3 and + pack(collision[0], 2) == pack(collision[1], 2), "unsafe equal-energy control") + zero = ((0, 0),) + cases = [(zero, zero, 3, 1), (zero, zero, True, 1), (zero, zero, 2, 3), + (*unequal, 12, 64), (*collision, 2, 3), (zero, (), 2, 1), + (zero, zero, 2, -1), (zero, zero, 2, True), (((True, 0),), zero, 2, 1)] + for args in cases: + try: + admitted_pair(*args) + except ValueError: + continue + raise ValueError("invalid pair admitted") + for bound in (0, -1, True, 1 << 65): + try: + safe_radix(bound) + except ValueError: + continue + raise ValueError("invalid energy bound admitted") + return dict(discriminating_controls=4, rejection_controls=len(cases) + 4) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--receipt', type=Path, help='write generated JSON outside checkout') + args = parser.parse_args() + counts = {} + counts.update(quotient_checks()) + counts.update(direct_kernel_checks()) + counts.update(sphere_checks()) + counts.update(matrix_fixtures()) + counts.update(controls()) + for bound in range(1, 4097): + safe_radix(bound) + counts['minimal_even_criterion_radices'] = 4096 + radix = safe_radix(512 ** 2) + require(radix == 726 and (radix ** 511).bit_length() == 4857, 'application arithmetic') + counts.update(R512_radix=radix, N512_largest_input_bits=4857, + old_N512_largest_input_bits=(1024 ** 511).bit_length()) + root = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py')} + report = dict(status='PASS_EQUAL_ENERGY_RADIX_PARITY', python=platform.python_version(), + counts=counts, sha256=hashes) + encoded = json.dumps(report, sort_keys=True, indent=2) + '\n' + if args.receipt: + args.receipt.write_text(encoded, encoding='utf-8') + print(encoded, end='') + + +if __name__ == '__main__': + main()