From dedb8bd4a53ecf7b36975941a872173ed8f2a1ba Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 12:05:49 +0000 Subject: [PATCH] feat(research): prove sharp even-residue zero-phase length --- research/zero-phase-even-residue/PROOF.md | 149 ++++++++++++ research/zero-phase-even-residue/README.md | 88 +++++++ research/zero-phase-even-residue/SOURCES.json | 24 ++ research/zero-phase-even-residue/TASK.json | 103 ++++++++ .../zero-phase-even-residue/VALIDATION.md | 63 +++++ research/zero-phase-even-residue/VERIFY.json | 34 +++ research/zero-phase-even-residue/verify.py | 228 ++++++++++++++++++ 7 files changed, 689 insertions(+) create mode 100644 research/zero-phase-even-residue/PROOF.md create mode 100644 research/zero-phase-even-residue/README.md create mode 100644 research/zero-phase-even-residue/SOURCES.json create mode 100644 research/zero-phase-even-residue/TASK.json create mode 100644 research/zero-phase-even-residue/VALIDATION.md create mode 100644 research/zero-phase-even-residue/VERIFY.json create mode 100644 research/zero-phase-even-residue/verify.py diff --git a/research/zero-phase-even-residue/PROOF.md b/research/zero-phase-even-residue/PROOF.md new file mode 100644 index 0000000000..3579348a93 --- /dev/null +++ b/research/zero-phase-even-residue/PROOF.md @@ -0,0 +1,149 @@ +# Shortest zero-phase tuples when n is two modulo four + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and boundary + +Let n=4k+2, k>=0. A tuple x_1,...,x_f in F_2^n has zero +nonconstant quadratic phase when + + sum_t x_tj = 0 mod 4, + sum_t x_tj x_tl = 0 mod 2 for j. + +For any x in F_2^N, sum i^wt(x+c) over c in C. Double evenness gives + + sum_(c in C) i^wt(x+c) = i^wt(x) sum_(c in C) (-1)^(x dot c). + +The inner character sum is zero unless x belongs to C-perp, and equals +2^n otherwise. Summing by cosets of C therefore leaves exactly two +contributing cosets, C and 1_N+C. Consequently + + (1+i)^N = sum_(x in F_2^N) i^wt(x) = 2^n (1+i^N). + +But n=4k+2 gives N=8k+5. The left side is -2^n(1+i), whereas the right +side is +2^n(1+i). This contradiction excludes every f<=2n+1. + +The coset calculation is classical binary coding theory. The new step +here is its application to the n=2 mod 4 zero-phase boundary, which the +cited #5635 result leaves open. No new coding classification is claimed. + +## 3. An attaining tuple of length 2n+2 + +On each of k disjoint eight-column blocks use the four rows + + 11111111 + 10101010 + 11001100 + 11110000 + +and on six final columns use the two rows + + 111100 + 110011. + +All other entries of each row are zero. There are 4k+2=n independent +rows and 8k+6=2n+2 columns. Each eight-column block has independent, +doubly even, mutually orthogonal rows. The final two rows have weights +four and intersection two. Disjoint blocks preserve these properties. +Thus the columns give a zero-phase tuple. + +The final block's row span consists of 000000 and three weight-four +words, and does not contain 111111. The all-one word on all columns +therefore cannot lie in the full row span. The homogeneous rank is n+1, +so the tuple has full affine span. This attains the lower bound. + +At n=6 the six rows are the four displayed eight-column rows extended +by six zeroes and the two displayed six-column rows preceded by eight +zeroes. This is a completely explicit 14-column witness. + +## 4. First visibility of the cited zero-phase residual + +This corollary uses, without re-proving or replaying, #5635 Sections 3-4. +In that grammar let A_n be its cuspidal affine cancellation element. Its +coefficient at the identity is Psi(1)>0, and it annihilates every tuple +of proper affine span. Let E_r be its diagonal Fourier projector onto +zero nonconstant phase and width residue r modulo four. Set P_r=A_n E_r. +These are fixed group-algebra elements over Q(i); their coefficients +stay outside tensor powers. + +For each r the first positive matching width where P_r is visible is + + L_r = 2n+2 + ((r-(2n+2)) mod 4). + +Below L_r every tuple surviving E_r has proper affine span by Section 2, +so A_n kills it. At a wrong residue E_r is zero. At L_r append zero +points to the Section 3 witness. This preserves both phase and full +affine span. Only the identity affine map fixes this ordered tuple, so +its diagonal coefficient under P_r is Psi(1)>0. Further groups of four +zero points show visibility at every larger matching width. + +Thus for n=6 these first-visible widths are (16,17,14,15), in residue +order (0,1,2,3). They are thresholds for this zero-phase residual, not +claimed thresholds for the complete representation kernel. In particular, +P_r lies outside the central ideal I_r yet vanishes at every smaller +matching positive width, giving a necessary test-width obstruction. +No all-character upper certificate is supplied. + +## Verification and limits + +The standalone checker constructs this new family, evaluates its literal +phase generators and homogeneous ranks, exhausts all ordered two-axis +tuples through length six, and checks the exact Gaussian-integer +contradiction. Its source proof is authenticated but no predecessor +executable is imported or run. The corollary inherits #5635's cuspidal +cancellation lemma and Green's classical character theorem as cited +mathematical inputs. It does not expand a large affine group. + +There is no new kappa, physical native caller, paid invoice, compiler, +precision, tape, stock or complete multiplication theorem. Independent +human and formal proof-kernel review are unclaimed. The selected frontier +and all five framework assumptions retain their status. + +Credit Ali Romman #5635/#5529/#5369/#5622, Joseph Anglada #5542, Hiroki +KUMAZAKI #5522, Mihir Srivastava #5521, Jose Manuel, ywz65, Chris R and +the retained native/phase lineage. The length-eight doubly-even code, +finite-field character orthogonality and Gauss-sum method are classical. diff --git a/research/zero-phase-even-residue/README.md b/research/zero-phase-even-residue/README.md new file mode 100644 index 0000000000..8666be9cc5 --- /dev/null +++ b/research/zero-phase-even-residue/README.md @@ -0,0 +1,88 @@ +# Sharp zero-phase native witness length for n=2 mod 4 + +This contribution was produced by Nick Petalas. Apache-2.0. + +For every n=4k+2>=2, the shortest binary tuple with zero nonconstant +quadratic phase and full affine span has exactly **2n+2 columns**. +At six axes the minimum is 14. A two-coset Gauss-sum contradiction gives +the lower bound; disjoint length-eight code blocks and a six-column block +attain it. [PROOF.md](PROOF.md) gives the uniform argument and explicit rows. + +The cited cuspidal cancellation lemma of Ali Romman's +[PR #5635](https://github.com/CrocSwap/integer-mult-bounds/pull/5635) then +makes the first-visible widths of its zero-phase residual exactly +`L_r=2n+2+((r-(2n+2)) mod 4)`. At six axes these are `(16,17,14,15)` in +residue order `(0,1,2,3)`. These are **not claimed complete native cutoff +thresholds**. An upper construction for every phase character remains open. + +This is a scoped algebraic proof with finite corroboration, answering part +of #5635's explicit other-axis-residues question. The new unbounded domain +starts at six axes. Two axes supply a small exhaustive control. No new +kappa, physical supplier or selected-frontier change is claimed. + +## Evidence and reproduction + +Use the repository CPython 3.12 interpreter from the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/zero-phase-even-residue +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/zero-phase-even-residue --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/zero-phase-even-residue/verify.py +``` + +On another machine substitute a CPython 3.12 executable. Standard library +only. The direct verifier prints `PASS_ZERO_PHASE_EVEN_RESIDUE` in its +JSON receipt; the registered runner prints `PASS_REGISTERED_RESEARCH_PACKAGE`. +Receipt hashes bind every package file and the exact cited source proof. +No receipt is handwritten, and the verifier writes no files. + +The bounded check covers 132 attaining padded tuples on dimensions +2,6,...,130, 20 independent literal-column checks, 1,092 explicit codewords, +33 exact Gaussian-integer contradictions, two other-residue controls and +18 rejected malformed or mathematically invalid inputs. The complete +ordered two-axis census has 5,461 tuples and 174,752 literal phase checks. +There are exactly 90 full-span zero-phase tuples at length six and none +at shorter lengths. Each of those 90 is a permutation of `(1,1,2,2,3,3)`. +This finite census does not stand in for the all-size proof. + +[VALIDATION.md](VALIDATION.md) records capacities and verification limits. +No predecessor executable, fixture or reported count is replayed. Its proof +is cited and source-bound as an input for the residual corollary. + +## Limits + +The complete all-character kernel cutoff, efficient expansion of a large +group-algebra residual, actual native inputs and returns, paid invoices, +compiler, precision, tapes and stock are outside this result. The corollary +uses #5635's cuspidal cancellation lemma and its classical character-theory +input. Independent human and formal proof-kernel review are unclaimed. +All five framework assumptions retain their status. + +The original formal-interface card is explicitly changed to a written +native-interface side result. This does not discharge a selected all-size +assumption. Base main is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority +revision 8. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216168). +Published overlap was checked through current open PRs and Discussion +claims, with separate main/merged searches. Sparse local notes and unpublished +work remain coverage limits; a search with no hit does not prove novelty. + +## Open next questions + +- Determine whether every nonconstant phase character has a full-affine-span + realization at the proposed widths in six dimensions. Start with a + character-orbit reduction and a constructive upper bound. The present + theorem handles only the zero character, so it does not settle this. +- Determine the complete test cutoff in the other higher-dimensional residue + classes. Start with a matching all-character upper construction; the + existence of a zero-phase witness alone is insufficient. + +## Credit + +Credit Ali Romman #5635 for the question and code/phase/cuspidal interface, +#5369/#5529/#5622 for the retained grammar and Fourier framework, Joseph +Anglada #5542, Hiroki KUMAZAKI #5522, Mihir Srivastava #5521, Jose Manuel, +ywz65, Chris R and the retained native/phase contributors. Doubly-even +codes, character orthogonality, Gauss sums and Green's character theorem +are classical. No global literature-priority claim is made. New work is +the n=2 mod 4 length theorem, its attaining family and zero-phase +first-visibility application. diff --git a/research/zero-phase-even-residue/SOURCES.json b/research/zero-phase-even-residue/SOURCES.json new file mode 100644 index 0000000000..d87e694b52 --- /dev/null +++ b/research/zero-phase-even-residue/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/nine-axis-cutoff-sharpness/PROOF.md", + "usage": "input", + "git_blob": "1ba92a64c521f25f7aa50ff95731ba893be5fe56", + "sha256": "e4e38b0559b0d64de095bee68c0d7bddc61020e843d75f8ca66e3c7b6655a8c3" + } + ] +} diff --git a/research/zero-phase-even-residue/TASK.json b/research/zero-phase-even-residue/TASK.json new file mode 100644 index 0000000000..b80dedf6c9 --- /dev/null +++ b/research/zero-phase-even-residue/TASK.json @@ -0,0 +1,103 @@ +{ + "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": "Prove the exact zero-nonconstant-phase full-affine-span tuple length 2n+2 for n=2 modulo four, and apply the cited cuspidal cancellation lemma to first visibility of that zero-phase residual.", + "scope_change_reason": "The formal-interface card is narrowed away from proof-assistant formalization and selected callers to the explicitly open other-axis-residues question in Ali Romman PR5635. This is a written native-interface side result, not a discharge of a selected framework assumption.", + "bottleneck_link": "A sharp phase-specific witness length gives a necessary test-width obstruction for the fixed native monomial grammar; an all-character upper bound and physical supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact length theorem; do not expand into a complete cutoff or a larger construction.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py exact finite corroboration and generated hash-bound stdout receipt", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does every phase character admit a full-span tuple at the proposed six-axis widths?", + "why_it_matters": "A matching all-character upper certificate could settle the complete native cutoff.", + "first_step": "Reduce six-axis phase characters by affine equivalence, then construct and check one tuple per orbit.", + "blocked_by": "Only the zero-character length is established here." + }, + { + "question": "What are the complete native test cutoffs in the remaining higher-axis residue classes?", + "why_it_matters": "Zero-phase visibility alone does not characterize the full kernel.", + "first_step": "Find a matching all-character upper construction and compare its worst character with a scoped lower witness.", + "blocked_by": "No general matching all-character upper bound below the cited 2n+3 guarantee is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216168", + "question_source": "PR #5635" +} diff --git a/research/zero-phase-even-residue/VALIDATION.md b/research/zero-phase-even-residue/VALIDATION.md new file mode 100644 index 0000000000..11d19db24f --- /dev/null +++ b/research/zero-phase-even-residue/VALIDATION.md @@ -0,0 +1,63 @@ +# Validation and bounded implementation + +This contribution was produced by Nick Petalas. Apache-2.0. + +The written proof covers every n=4k+2>=2. The Python program is finite +corroboration and does not enumerate six-axis tuples or a large affine group. +It authenticates the cited source proof without importing predecessor code. +All mathematical checks use explicit exceptions and remain active under -O. + +The registered normal and optimized commands run with warning-strict +CPython 3.12, using only the standard library. Each has a 120-second bound. +The receipt reports actual enumeration counts and file hashes. Direct, +registered, committed-byte/source-history and export checks are distinct; +local success does not claim hosted scientific certification. + +## Capacities and control flow + +The constructor accepts only n=2,6,...,130. Witness validation accepts at +most 130 coordinate rows and 265 bits per row. Its phase-pair loop has at +most 8,385 iterations. Binary elimination has at most 131 rows by 265 +pivots. Each function is below 60 physical lines. There is no recursion, +dynamic evaluation, external command, network access or concurrent writer. + +The family sweep has 33 dimensions and four pads. The independent literal +column check is called only through 18 axes and 41 columns. Its span has +at most 2^18 elements. Explicit codeword enumeration is capped at 2^10. +The complete two-axis census has sum_(f=0..6) 4^f=5,461 iterations and 32 +phase choices per tuple. Its affine closure contains at most four values. +The Gaussian-integer check uses at most 262 binomial coefficients per +case. Input/domain failures raise ValueError and return a nonzero status. + +## Managed-runtime deviations from Power of Ten + +Rule: 3, fix memory capacity before steady operation. +Location: verify.py, especially literal_witness and two_axis_census. +Reason: Python's integer, list, set and JSON operations allocate dynamically. +Scope: this standalone finite verifier only. +Compensating control: fixed enumeration domains above; the largest explicit +set contains at most 2^18 bounded integers. Package hashing reads at most +ten package files and one source proof, whose byte sizes are source-bound. +Verification: direct and registered normal/optimized checks exercise every +stated finite domain. No persistent allocations or generated files remain. +Follow-up: if dimensions are raised, replace explicit span enumeration with +a separately checked bounded elimination before increasing these caps. + +Rule: 10, maximum diagnostics. +Location: verify.py. +Reason: Python has no compiler warning level, and no optional static checker +is installed in this environment. +Scope: the new standalone standard-library verifier. +Compensating control: warning-strict normal/optimized execution, explicit +contracts, independent row/column arithmetic, exhaustive small cases and +rejection controls. Checks remain enabled under interpreter optimization. +Verification: the exact commands are in README.md and VERIFY.json. +Follow-up: run a project-adopted static checker when one is available; this +package adds no global tooling configuration. + +## Unrun obligations + +No Lean, Docker, selected cold replay, hardware rounding, physical native +execution or all-character upper certificate is needed for or supplied by +this scoped result. The source's Green-character lemma is a cited dependency, +not a new independent review claim. Hosted status belongs in the PR body. diff --git a/research/zero-phase-even-residue/VERIFY.json b/research/zero-phase-even-residue/VERIFY.json new file mode 100644 index 0000000000..aee9aefb5a --- /dev/null +++ b/research/zero-phase-even-residue/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/nine-axis-cutoff-sharpness/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New attaining family, independent literal-column arithmetic, exhaustive two-axis tuples and phase characters, Gaussian-integer contradiction, hypothesis and rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete finite check with optimization; every contract remains active." + } + ] +} diff --git a/research/zero-phase-even-residue/verify.py b/research/zero-phase-even-residue/verify.py new file mode 100644 index 0000000000..2cd8bdfd00 --- /dev/null +++ b/research/zero-phase-even-residue/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration for the new zero-phase length theorem. + +Produced by Nick Petalas. Apache-2.0. Standard library only. +""" +from hashlib import sha256 +from itertools import product +import json +from math import comb +from pathlib import Path +import sys + +MAX_AXES = 130 +MAX_WIDTH = 265 +PACKAGE = Path(__file__).resolve().parent +SOURCE = "research/nine-axis-cutoff-sharpness/PROOF.md" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def binary_rank(words): + """Internal bounded input, at most MAX_AXES+1 words of MAX_WIDTH bits.""" + basis = [0] * MAX_WIDTH + result = 0 + for original in words: + word = original + for pivot in range(MAX_WIDTH - 1, -1, -1): + if not (word >> pivot) & 1: + continue + if basis[pivot]: + word ^= basis[pivot] + else: + basis[pivot] = word + result += 1 + break + return result + + +def witness(n, width, rows): + require(type(n) is int and 1 <= n <= MAX_AXES, "axis capacity") + require(type(width) is int and 1 <= width <= MAX_WIDTH, "width capacity") + require(len(rows) == n, "coordinate row count") + require(all(type(r) is int and 0 <= r < 1 << width for r in rows), + "row range") + require(all(r.bit_count() % 4 == 0 for r in rows), "linear phase") + require(all((rows[j] & rows[l]).bit_count() % 2 == 0 + for j in range(n) for l in range(j)), "quadratic phase") + require(binary_rank([*rows, (1 << width) - 1]) == n + 1, + "full affine span") + + +def construct(n): + require(type(n) is int and 2 <= n <= MAX_AXES and n % 4 == 2, + "constructor domain") + rows = [] + for block in range((n - 2) // 4): + rows.extend(r << (8 * block) + for r in (0b11111111, 0b10101010, 0b11001100, 0b11110000)) + offset = 2 * (n - 2) + rows.extend(r << offset for r in (0b111100, 0b110011)) + return rows + + +def points(rows, width): + return [sum(((r >> t) & 1) << j for j, r in enumerate(rows)) + for t in range(width)] + + +def literal_witness(n, width, rows): + """Independent column-oriented phase sums and affine-difference rank.""" + require(1 <= n <= 18 and 1 <= width <= 41, "literal capacity") + xs = points(rows, width) + for j in range(n): + require(sum((x >> j) & 1 for x in xs) % 4 == 0, "literal linear") + for l in range(j): + require(sum(((x >> j) & 1) * ((x >> l) & 1) for x in xs) % 2 == 0, + "literal quadratic") + differences = [x ^ xs[0] for x in xs[1:]] + # The alternate rank implementation grows a set only for n<=18. + span = {0} + for word in differences: + if word not in span: + span.update([word ^ x for x in span]) + require(len(span) == 1 << n, "literal affine span") + + +def family_checks(): + cases = literal = codewords = 0 + for n in range(2, MAX_AXES + 1, 4): + rows = construct(n) + for pad in range(4): + width = 2 * n + 2 + pad + witness(n, width, rows) + cases += 1 + if n <= 18: + literal_witness(n, width, rows) + literal += 1 + if n <= 10: + for mask in range(1 << n): + word = 0 + for j in range(n): + if (mask >> j) & 1: + word ^= rows[j] + require(word.bit_count() % 4 == 0, "literal code weight") + codewords += 1 + return {"padded_witnesses": cases, "literal_column_witnesses": literal, + "explicit_codewords": codewords} + + +def two_axis_census(): + counts = [] + total = phase_tests = 0 + for width in range(7): + zero = full = 0 + for xs in product(range(4), repeat=width): + rows = [sum(((x >> j) & 1) << t for t, x in enumerate(xs)) + for j in range(2)] + packed = all(r.bit_count() % 4 == 0 for r in rows) + packed = packed and (rows[0] & rows[1]).bit_count() % 2 == 0 + literal = True + for a, b, c in product(range(4), range(4), range(2)): + exponent = sum(a * (x & 1) + b * ((x >> 1) & 1) + + 2 * c * (x & 1) * ((x >> 1) & 1) for x in xs) + literal = literal and exponent % 4 == 0 + phase_tests += 1 + require(packed == literal, "phase character equivalence") + total += 1 + if not literal: + continue + zero += 1 + differences = {x ^ xs[0] for x in xs} if xs else {0} + closure = {a ^ b for a in differences for b in differences} + affine = len(closure | differences) == 4 + homogeneous = binary_rank([*rows, (1 << width) - 1]) == 3 + require(affine == homogeneous, "two affine criteria") + if affine: + require(width == 6 and sorted(xs) == [1, 1, 2, 2, 3, 3], + "two-axis minimal tuple classification") + full += 1 + counts.append({"width": width, "zero_phase": zero, "full_span": full}) + require(sum(row["full_span"] for row in counts) == 90, "minimal permutation count") + return {"ordered_tuples": total, "literal_phase_tests": phase_tests, + "by_width": counts} + + +def gaussian_sum(width): + """Literal binomial expansion, no floating point or complex numbers.""" + powers = ((1, 0), (0, 1), (-1, 0), (0, -1)) + real = imag = 0 + for weight in range(width + 1): + a, b = powers[weight % 4] + real += comb(width, weight) * a + imag += comb(width, weight) * b + return real, imag + + +def gauss_checks(): + cases = 0 + for n in range(2, MAX_AXES + 1, 4): + width = 2 * n + 1 + actual = gaussian_sum(width) + required = (1 << n, 1 << n) + require(actual == (-required[0], -required[1]), "Gauss obstruction sign") + require(actual != required, "Gauss contradiction") + cases += 1 + # These genuine witnesses show why the residue hypothesis matters. + witness(3, 7, [0b1010101, 0b1100110, 0b1111000]) + witness(4, 9, [0b11111111, 0b10101010, 0b11001100, 0b11110000]) + require(gaussian_sum(7) == (8, -8), "compatible odd residue") + require(gaussian_sum(9) == (16, 16), "compatible even residue") + return {"gauss_contradictions": cases, "other_residue_controls": 2} + + +def rejection_checks(): + rejected = 0 + for invalid in (-2, 0, 1, 3, 4, 5, 131, True): + try: + construct(invalid) + except ValueError: + rejected += 1 + else: + raise ValueError("accepted invalid constructor input") + rows = construct(6) + bad_rows = [rows[:-1], [*rows[:-1], rows[0]], + [rows[0] ^ 1, *rows[1:]], [-1, *rows[1:]], + [1 << 14, *rows[1:]]] + fixtures = [(6, 14, r) for r in bad_rows] + fixtures.extend([(2, 8, [0b11110000, 0b00001111]), + (2, 6, [0b111100, 0b111010]), + (2, 6, [0b110000, 0b001100]), + (6, 266, rows), (6, 0, rows)]) + for n, width, fixture in fixtures: + try: + witness(n, width, fixture) + except ValueError: + rejected += 1 + else: + raise ValueError("accepted invalid witness") + return {"rejection_controls": rejected} + + +def bindings(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + records = [r for r in manifest["files"] if r["path"] == SOURCE] + require(len(records) == 1 and records[0]["usage"] == "input", "source declaration") + source_hash = sha256((PACKAGE.parents[1] / SOURCE).read_bytes()).hexdigest() + require(source_hash == records[0]["sha256"], "cited source proof hash") + files = sorted(p for p in PACKAGE.iterdir() if p.is_file()) + require(len(files) <= 10, "package receipt file capacity") + return {**{p.name: sha256(p.read_bytes()).hexdigest() for p in files}, + SOURCE: source_hash} + + +def main(): + require(len(sys.argv) == 1, "this bounded verifier takes no arguments") + hashes = bindings() + result = {"status": "PASS_ZERO_PHASE_EVEN_RESIDUE", "family": family_checks(), + "two_axis": two_axis_census(), "gauss": gauss_checks(), + "controls": rejection_checks(), "file_sha256": hashes, + "claim_type": "scoped proof with finite corroboration"} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()