From 788848032c16bbe0a543c1186c6691c66131c090 Mon Sep 17 00:00:00 2001 From: Arham-Tahir64 Date: Wed, 14 Oct 2026 07:39:15 -0600 Subject: [PATCH] Prove sharp energy-ball radix for packed HPE equality --- research/hpe-energy-packed-radix/README.md | 168 ++++++++ research/hpe-energy-packed-radix/RESULT.json | 129 ++++++ research/hpe-energy-packed-radix/SOURCES.json | 36 ++ research/hpe-energy-packed-radix/TASK.json | 116 ++++++ research/hpe-energy-packed-radix/VERIFY.json | 40 ++ .../hpe-energy-packed-radix/test_verify.py | 84 ++++ research/hpe-energy-packed-radix/verify.py | 377 ++++++++++++++++++ 7 files changed, 950 insertions(+) create mode 100644 research/hpe-energy-packed-radix/README.md create mode 100644 research/hpe-energy-packed-radix/RESULT.json create mode 100644 research/hpe-energy-packed-radix/SOURCES.json create mode 100644 research/hpe-energy-packed-radix/TASK.json create mode 100644 research/hpe-energy-packed-radix/VERIFY.json create mode 100644 research/hpe-energy-packed-radix/test_verify.py create mode 100644 research/hpe-energy-packed-radix/verify.py diff --git a/research/hpe-energy-packed-radix/README.md b/research/hpe-energy-packed-radix/README.md new file mode 100644 index 0000000000..e86f475394 --- /dev/null +++ b/research/hpe-energy-packed-radix/README.md @@ -0,0 +1,168 @@ +# Sharp energy-ball radix for packed exact equality + +**A Gaussian-integer row of Euclidean norm at most R is uniquely determined +by its evaluation at integer radix B >= 2R.** For integer R >= 1 this is the +sharp uniform integer threshold for that energy ball, in dimensions at least +two. This supplies a written all-dimension compiler lemma and a source-bound +finite replay, with no new Lean proof or selected-checker change. + +Applied to the validated unitary Clifford grammar retained from Jeremy +Kothe's PR593, this gives **K+1 radix bits**, where K is the larger C-gate +count. It improves the sufficient K+2-bit bound in woklerx's +[PR1859](https://github.com/CrocSwap/integer-mult-bounds/pull/1859), head +`f5e18c0c44371ebfdd46bfe25efe5b49e467fafe`, by using whole-row energy in +place of a componentwise bound. No pending code is imported. + +All three frozen `Exact.lean` pairs pass at **10 bits**, versus PR1859's 11 +and the retained checker's 20. The largest packed input integer has **5,111 +bits**, versus 5,622 and 10,221. These are exact bit lengths, not timings. + +## Quantified lemma and proof + +Let `R >= 1` be an integer, let `B >= 2R` be an integer, and let `u,v` be +finite Gaussian-integer vectors of the same arbitrary length. Define + +`E(u) = sum_j |u_j|^2`, and `P_B(u) = sum_j u_j B^j`. + +If `E(u), E(v) <= R^2`, then `P_B(u) = P_B(v)` **if and only if** `u=v`. + +First consider a nonzero Gaussian-integer vector `d` in the kernel of +`P_B`. Let `t` be its least nonzero index. Dividing the zero evaluation by +`B^t` shows that `d_t` is a nonzero multiple of B in `Z[i]`, so +`|d_t|^2 >= B^2`. At least one higher digit must be nonzero; its squared +modulus is at least one. Consequently + +`E(d) >= B^2+1`. + +This kernel bound is sharp: `d=(B,-1)` has zero evaluation and energy +`B^2+1`. Now put `d=u-v`. The parallelogram identity gives + +`E(u-v) = 2E(u)+2E(v)-E(u+v) <= 4R^2 <= B^2`. + +Thus a nonzero difference cannot be in the kernel. This proves the forward +implication; the converse is immediate. The proof covers complex Gaussian +digits jointly, without floating-point estimates or a dimension-dependent +remainder. It also works for a real positive R if an integer B satisfies +`B >= 2R`; the sharpness assertion below uses integer R. + +**Sharpness for the ball.** For every integer `1 <= B < 2R`, take + +`u=(ceil(B/2),0)`, `v=(-floor(B/2),1)`. + +They differ but both evaluate to `ceil(B/2)`. Their energies are at most +`R^2`: the second is at most `(R-1)^2+1 <= R^2`. Thus every smaller integer +radix fails in dimension two; append zeros for larger dimensions. This is +sharpness for the whole energy ball, **not** optimality for the particular +Clifford circuits or the subset of equal-energy unitary rows. + +## Implication for the retained circuit compiler + +The pinned `Clifford.lean` grammar has invertible binary permutations, XOR +permutations, diagonal/global powers of i, and + +`C_s = ((1+s*i) I + (1-s*i) X)/2`, `s in {1,-1}`. + +Validate the permutation/inverse pair and require XOR masks in the finite +address domain. Then X is a self-adjoint involution. On its +1 and -1 +eigenspaces, C_s acts by 1 and s*i, so it is unitary. All five normalized +gate kinds, and hence their compositions, are unitary. + +For a circuit U with k C gates, omitting each factor 1/2 produces the +Gaussian-integer matrix `Z=2^k U`. Its **rows**, as well as columns, have +energy `4^k`. For two circuits with counts k1,k2, set `K=max(k1,k2)` and +compare `2^(K-k1) Z1` with `2^(K-k2) Z2`. Every row has energy `R^2` for +`R=2^K`. Evaluation on the single input `u_j=B^j`, with + +`B=2R=2^(K+1)`, + +therefore determines each complete row by the lemma. Packed equality is +equivalent to normalized matrix equality, with global phase retained. The +extra unitarity/row-energy premises are material: this does not replace the +original Lean theorem for arbitrary literal gate lists. + +A componentwise bound `|d_j| <= B` alone would admit `(B,-1)`. Its energy +exceeds the permitted difference energy by one, which is exactly what the +new proof uses. Column norm bounds alone also fail: the matrices + +`A=[[1,0],[0,0]]`, `C=[[-1,1],[0,0]]` + +each have column energies at most one and agree on `(1,2)`, although they +differ. C's first row has energy two, violating the required row bound. +Neither matrix pair is being asserted to be a valid normalized circuit. + +## Reproduction and exact evidence + +From the repository root, Python 3.12 with only the standard library: + +```sh +python -I -O -B research/hpe-energy-packed-radix/verify.py +python -I -B -m unittest discover -s research/hpe-energy-packed-radix -p test_verify.py +python scripts/research_package.py --package research/hpe-energy-packed-radix +``` + +Normal verification checks source hashes and the complete deterministic +[RESULT.json](RESULT.json) without writing files. An intentional receipt +rebuild requires `--write /explicit/output/path.json`. + +The checker reuses only commdata2338's closed Lean-literal parser. Its new +executor uses forward permutation scatter and disjoint two-state C +butterflies. A second direct interpreter uses the Lean pullback and +pointwise C formula. They share integer phase helpers and source parsing; +this is differential evidence, not two fully independent implementations. +The replay covers: + +- All three literal pairs at the original, PR1859 and new radices. +- All 3,072 scaled rows of the six literal circuits, obtained as conjugated + adjoint columns: exact equality and energy `4^K`, with row digests. +- Thirty separate interpreter executions on basis and mixed Gaussian data. +- All 5,265 vectors in nine Gaussian-integer balls: R=1,2,3, each in + complex lengths 1,2,3, without any collision at B=2R. +- Exhaustive short-kernel checks in complex length two at B=2..6, + plus the attaining `(B,-1)` relations. +- Actual real and imaginary collisions for all 1,024 unsafe `(R,B)` + pairs with R=1..32 and 1 <= B < 2R. +- Fifteen source controls: phase, input character, omitted scale and + undersized radix for each pair; invalid permutation, invalid XOR mask + and a non-Boolean C sign. The component-only and column-only false + implications are also demonstrated explicitly. + +The quantified lemma rests on the proof above, not this finite census. +There is no supplier/cold replay, Lean build, kernel performance benchmark, +physical hosting proof, production precision change or new kappa claim. +The input exponent range of a real compiler and its arithmetic/memory cost +remain separate obligations. Compiler arguments must be obtained through +the validated literal compiler; arbitrary hand-built compiled lists are +outside the comparator's contract. + +## Scope, sources and credit + +Base current main: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +[TASK.json](TASK.json) records the adversarial-audit draw, refined scope, +bounded stopping rule and overlap coverage. [SOURCES.json](SOURCES.json) +pins the retained parser, literal data and exact gate semantics. Work is +coordinated in [Discussion1896](https://github.com/CrocSwap/integer-mult-bounds/discussions/1896). + +Credit Jeremy Kothe / jeremykothe2's PR593 for the retained Clifford +semantics, packed equality proof and three literal pairs; commdata2338 for +the retained semantic-binding parser and source correspondence; woklerx's +PR1859 for the unitary-premise radix improvement; and the retained Lemma A/G, +icekylinx, Chafik Boukhalfa and jacklightChen lineage. Sagar Thakrar's +PR1781, inspected at `dafbaadeb423b3bc80fbf6fcd6f415400dc0ffbf`, concerns a +separate selected-recipe census at the original radix; it is neither +imported nor replayed here. The selected frontier and frozen files are +unchanged. + +Prepared by Arham Tahir with substantial OpenAI Codex assistance in proof, +implementation, verification and prose. No subagents or independent human +review. Apache-2.0; predecessor source notices are retained. + +## Open next questions + +Can the sharp energy-ball lemma and valid-gate row norms be proved in Lean? +That would permit a proof-preserving change to the retained checker. First +formalize the least-nonzero-digit kernel bound and the parallelogram +inequality, then derive scaled row energies for the valid normalized +grammar. The missing kernel proof and kernel timing block adoption; +[TASK.json](TASK.json) records that precise next step. A smaller radix for +only the three particular matrices would be a different, source-specific +problem and is not claimed here. diff --git a/research/hpe-energy-packed-radix/RESULT.json b/research/hpe-energy-packed-radix/RESULT.json new file mode 100644 index 0000000000..20b1b82db1 --- /dev/null +++ b/research/hpe-energy-packed-radix/RESULT.json @@ -0,0 +1,129 @@ +{ + "status": "PASS_HPE_ENERGY_PACKED_RADIX", + "source": { + "pairs": [ + { + "pair": 1, + "C_left": 9, + "C_right": 7, + "radius": 512, + "radix_bits": 10, + "previous_unitary_radix_bits": 11, + "original_radix_bits": 20, + "largest_input_bits": 5111, + "scaled_row_sha256": "f217217e83d8f49a19df80669c0de735d73edfabecd1eb3e9783b4cb7f311267", + "row_squared_energy": 262144 + }, + { + "pair": 2, + "C_left": 9, + "C_right": 7, + "radius": 512, + "radix_bits": 10, + "previous_unitary_radix_bits": 11, + "original_radix_bits": 20, + "largest_input_bits": 5111, + "scaled_row_sha256": "3ff6f9679256f02a243b1b0fd4b55e50a98d5ca8f282b8d0a948f1598a38fb3e", + "row_squared_energy": 262144 + }, + { + "pair": 3, + "C_left": 9, + "C_right": 7, + "radius": 512, + "radix_bits": 10, + "previous_unitary_radix_bits": 11, + "original_radix_bits": 20, + "largest_input_bits": 5111, + "scaled_row_sha256": "ee5ac2ce8466eeb7b1b8b2766626ed31b266fc8a65b401780954c7bb6dd901fd", + "row_squared_energy": 262144 + } + ], + "scaled_rows_checked": 3072, + "separate_oracle_executions": 30, + "controls": [ + "pair1_phase", + "pair1_input_character", + "pair1_omitted_scale", + "pair1_undersized_radix", + "pair2_phase", + "pair2_input_character", + "pair2_omitted_scale", + "pair2_undersized_radix", + "pair3_phase", + "pair3_input_character", + "pair3_omitted_scale", + "pair3_undersized_radix", + "nonunitary_permutation", + "out_of_domain_X", + "nonboolean_C_sign" + ], + "input_sha256": { + "research/hpe-lean-semantic-binding/verify.py": "7f7d32e5c13625e9e516b96954cbdfb5a3d195638c3ea8b31ea605d560965b49", + "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean": "c0c51407b4fa6ff230a79d5f3b07c83b7d1c4b433ce03513f0c4fb725bf3cbe1", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + } + }, + "energy_balls": { + "gaussian_balls": [ + { + "radius": 1, + "complex_length": 1, + "vectors": 5 + }, + { + "radius": 1, + "complex_length": 2, + "vectors": 9 + }, + { + "radius": 1, + "complex_length": 3, + "vectors": 13 + }, + { + "radius": 2, + "complex_length": 1, + "vectors": 13 + }, + { + "radius": 2, + "complex_length": 2, + "vectors": 89 + }, + { + "radius": 2, + "complex_length": 3, + "vectors": 485 + }, + { + "radius": 3, + "complex_length": 1, + "vectors": 29 + }, + { + "radius": 3, + "complex_length": 2, + "vectors": 425 + }, + { + "radius": 3, + "complex_length": 3, + "vectors": 4197 + } + ], + "vectors": 5265, + "short_kernel_vectors_checked": 11493, + "unsafe_integer_radices": 1024, + "controls": [ + "adjacent_and_smaller_radix_collisions", + "imaginary_collisions", + "component_bounds_do_not_replace_energy", + "column_bounds_do_not_replace_row_bounds", + "strict_kernel_energy_gap" + ] + }, + "new_lean_proof": false, + "selected_checker_changed": false, + "new_kappa": false +} diff --git a/research/hpe-energy-packed-radix/SOURCES.json b/research/hpe-energy-packed-radix/SOURCES.json new file mode 100644 index 0000000000..657eb19620 --- /dev/null +++ b/research/hpe-energy-packed-radix/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/hpe-lean-semantic-binding/verify.py", + "usage": "input", + "git_blob": "234831bc729ef01024d660bb3b82bdffbc371cd4", + "sha256": "7f7d32e5c13625e9e516b96954cbdfb5a3d195638c3ea8b31ea605d560965b49" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean", + "usage": "input", + "git_blob": "5970d81439b8bca2935a935d964779845a45057c", + "sha256": "c0c51407b4fa6ff230a79d5f3b07c83b7d1c4b433ce03513f0c4fb725bf3cbe1" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "usage": "input", + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + } + ] +} diff --git a/research/hpe-energy-packed-radix/TASK.json b/research/hpe-energy-packed-radix/TASK.json new file mode 100644 index 0000000000..b3df5f3434 --- /dev/null +++ b/research/hpe-energy-packed-radix/TASK.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp dimension-independent Gaussian-integer energy-ball packing: prove B=2R suffices for radius R, give the B=2R-1 collision, and source-test B=2^(K+1) on the three retained HPE literal pairs.", + "scope_change_reason": "The drawn adversarial method is refined to a safe compiler boundary plus a sharp adjacent unsafe boundary. This follows the first positive baseline and explicitly uses the card's proof method as the single bounded pivot; it is not a finite smoke test in place of the quantified implication.", + "bottleneck_link": "An exact all-dimension encoding lemma reduces integers in source-bound HPE equality checks by one more radix bit than PR1859 while preserving phase and full-row information. This is verifier arithmetic, not supplier or exponent improvement.", + "budget_minutes": 60, + "stop_rule": "One approximately 60-minute session including setup. Stop after the written energy-ball proof, exhaustive small Gaussian balls, three literal pairs, and meaningful failure controls. No Lean build, selected-checker replacement or larger recipe census.", + "outcome": "completed", + "evidence": "Written dimension-independent least-nonzero-digit kernel proof and sharp unsafe-radix construction; 3072 scaled rows, 5265 Gaussian-ball vectors, 11493 short-kernel vectors, 1024 unsafe radices, 30 differential executions and 15 source controls; four CLI/source/receipt boundary test groups.", + "author": "Arham Tahir with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, implementation, verification and prose. No subagents or independent human proof review.", + "open_questions": [ + { + "question": "Can the row-energy packing lemma and guarded circuit unitarity be formalized in Lean?", + "why_it_matters": "A kernel-checked implication is needed before replacing the retained broader packed checker.", + "first_step": "Formalize the least-nonzero-digit packing-kernel energy bound and parallelogram identity, then derive row norms for valid normalized gates.", + "blocked_by": "This package supplies a written proof and exact checks, not a new Lean theorem or kernel timing." + } + ], + "assignment_nonce": "d17af0bfdda8dde69736e5942d5a7563", + "scope_key": "Gaussian-integer-row-energy-ball/sharp-integer-radix/three-HPE-literal-pairs", + "first_example": "python -B scripts/research_baseline.py: PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "predecessors": [ + { + "pr": 1859, + "head": "f5e18c0c44371ebfdd46bfe25efe5b49e467fafe", + "credit": "woklerx; unitary-premise K+2-bit sufficient radix. Inspected README/proof/code, no pending implementation imported." + }, + { + "pr": 593, + "credit": "Jeremy Kothe / jeremykothe2; retained Clifford semantics, packed equality theorem and literal pairs." + }, + { + "credit": "commdata2338; retained hpe-lean-semantic-binding literal parser, reused as a declared input." + }, + { + "pr": 1781, + "head": "dafbaadeb423b3bc80fbf6fcd6f415400dc0ffbf", + "credit": "Sagar Thakrar; selected-recipe census at the old radix; not imported or replayed." + } + ], + "optimistic_budget": { + "radix_bits": "K+1 instead of K+2 (PR1859) or 2K+2 (retained checker)", + "required_improvement": "All-dimension injectivity at B=2R, with exact source pairs at K=9 using 10 bits." + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1896", + "environment": { + "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr 8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]", + "platform": "Windows-11-10.0.26200-SP0", + "test_temp_directory": "TEMP and TMP set to the checkout root for the Windows sandbox; tests use standard tempfile elsewhere" + }, + "overlap_entry": { + "open_prs_including_drafts": 543, + "discussion_comment_reply_records": 529, + "pr_snapshot_utc": "2026-10-14T13:23:57.128428+00:00", + "discussion_snapshot_utc": "2026-10-14T13:25:06.320256+00:00", + "complete_pagination": true, + "limits": "PR titles/bodies, Discussions including comments/replies, local package notes/metadata/ledger; excludes every diff/nested source and is not a novelty certificate." + }, + "overlap_final": { + "open_prs_including_drafts": 554, + "discussion_comment_reply_records": 535, + "pr_snapshot_utc": "2026-10-14T13:37:04.268127+00:00", + "discussion_snapshot_utc": "2026-10-14T13:38:12.277430+00:00", + "complete_pagination": true, + "predecessor1859_head_unchanged": "f5e18c0c44371ebfdd46bfe25efe5b49e467fafe", + "search_terms": [ + "packed radix", + "energy-ball", + "K+1", + "B=2R" + ], + "nearest_overlap": "PR1859 is the credited sufficient-entry-bound predecessor. No other exact energy-ball radix result was found in this coverage; no novelty guarantee.", + "limits": "PR titles/bodies, Discussions including comments/replies, local package notes/metadata/ledger; excludes every diff/nested source and is not a novelty certificate." + } +} diff --git a/research/hpe-energy-packed-radix/VERIFY.json b/research/hpe-energy-packed-radix/VERIFY.json new file mode 100644 index 0000000000..6b8867a994 --- /dev/null +++ b/research/hpe-energy-packed-radix/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/hpe-lean-semantic-binding/verify.py", + "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full source hashes; three literal pairs at 10/11/20-bit radix; all 3072 scaled rows and energies; complete small Gaussian balls; sharp carry/unsafe-radix/row-column controls; phase, character, scaling and gate controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized source-export relocation and read-only replay, deterministic regeneration, source drift, receipt corruption and duplicate-key rejection." + } + ] +} diff --git a/research/hpe-energy-packed-radix/test_verify.py b/research/hpe-energy-packed-radix/test_verify.py new file mode 100644 index 0000000000..ca7dc9b10b --- /dev/null +++ b/research/hpe-energy-packed-radix/test_verify.py @@ -0,0 +1,84 @@ +"""Source/receipt failure boundaries for the registered exact verifier.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def invoke(root, *args): + return subprocess.run([sys.executable, '-I', '-O', '-B', + str(root/'research/hpe-energy-packed-radix/verify.py'), *map(str, args)], + cwd=root, text=True, capture_output=True, timeout=90) + + +def export(root): + package = root/'research/hpe-energy-packed-radix' + package.mkdir(parents=True) + for name in ('verify.py', 'SOURCES.json', 'RESULT.json'): + shutil.copy2(HERE/name, package/name) + for row in json.loads((HERE/'SOURCES.json').read_text(encoding='utf-8'))['files']: + if row['usage'] == 'input': + dest = root/row['path'] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT/row['path'], dest) + return package + + +class VerifierBoundaryTests(unittest.TestCase): + def test_optimized_relocation_read_only_and_deterministic_rebuild(self): + with tempfile.TemporaryDirectory(prefix='hpe-energy-test-') as directory: + root = Path(directory) + package = export(root) + before = {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + result = invoke(root) + self.assertEqual(result.returncode, 0, result.stderr) + after = {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + self.assertEqual(before, after) + generated = root/'rebuilt.json' + result = invoke(root, '--write', generated) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(generated.read_bytes(), (package/'RESULT.json').read_bytes()) + + def test_source_drift_rejected_before_math(self): + with tempfile.TemporaryDirectory(prefix='hpe-energy-test-') as directory: + root = Path(directory) + export(root) + source = root/'research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean' + source.write_bytes(source.read_bytes()+b'\n-- corrupted source\n') + result = invoke(root) + self.assertNotEqual(result.returncode, 0) + self.assertIn('source drift:', result.stderr) + + def test_receipt_corruption_rejected(self): + with tempfile.TemporaryDirectory(prefix='hpe-energy-test-') as directory: + root = Path(directory) + package = export(root) + receipt = json.loads((package/'RESULT.json').read_text(encoding='utf-8')) + receipt['source']['pairs'][0]['radix_bits'] += 1 + (package/'RESULT.json').write_text(json.dumps(receipt), encoding='utf-8') + result = invoke(root) + self.assertNotEqual(result.returncode, 0) + self.assertIn('receipt mismatch', result.stderr) + + def test_duplicate_receipt_keys_rejected(self): + with tempfile.TemporaryDirectory(prefix='hpe-energy-test-') as directory: + root = Path(directory) + package = export(root) + receipt = (package/'RESULT.json').read_text(encoding='utf-8') + (package/'RESULT.json').write_text('{"status":"duplicate",'+receipt[1:], encoding='utf-8') + result = invoke(root) + self.assertNotEqual(result.returncode, 0) + self.assertIn('duplicate JSON key:', result.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/hpe-energy-packed-radix/verify.py b/research/hpe-energy-packed-radix/verify.py new file mode 100644 index 0000000000..35558ad208 --- /dev/null +++ b/research/hpe-energy-packed-radix/verify.py @@ -0,0 +1,377 @@ +"""Exact energy-ball packing checks and source-bound HPE fixtures; Apache-2.0. + +Arham Tahir with substantial OpenAI Codex assistance. No new Lean theorem. +Only the retained closed literal parser is reused, not its gate interpreter. +""" +import argparse +import hashlib +import importlib.util +import json +import math +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +N = 512 +ZERO = (0, 0) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, 'duplicate JSON key: ' + key) + out[key] = value + return out + + +def read_json(path): + return json.loads(path.read_text(encoding='utf-8'), object_pairs_hook=unique_object) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')) + + +def energy(values): + return sum(a*a + b*b for a, b in values) + + +def pack(values, base): + a = b = 0 + for x, y in reversed(values): + a, b = base*a + x, base*b + y + return a, b + + +def admissible_radix(radius, base): + require(type(radius) is int and radius >= 1, 'positive integer radius') + require(type(base) is int and base >= 2*radius, 'energy-ball radix requires B >= 2R') + + +def integer_ball(dimensions, remaining): + """Every ordered integer vector of the given dimension and squared norm cap.""" + if dimensions == 0: + yield () + return + bound = math.isqrt(remaining) + for value in range(-bound, bound+1): + for tail in integer_ball(dimensions-1, remaining-value*value): + yield (value,) + tail + + +def gaussian_ball(length, squared_radius): + for values in integer_ball(2*length, squared_radius): + yield tuple(zip(values[::2], values[1::2])) + + +def ball_checks(): + cases = [] + total = 0 + for radius in (1, 2, 3): + for length in (1, 2, 3): + seen = {} + for values in gaussian_ball(length, radius*radius): + code = pack(values, 2*radius) + require(code not in seen, 'energy-ball collision at the proved boundary') + seen[code] = values + total += len(seen) + cases.append({'radius': radius, 'complex_length': length, 'vectors': len(seen)}) + # Nonzero kernel vectors have squared norm at least B^2+1. Check all + # vectors of norm squared <= B^2 and the attaining two-digit relation. + kernel_vectors = 0 + for base in range(2, 7): + for values in gaussian_ball(2, base*base): + if any(v != ZERO for v in values): + require(pack(values, base) != ZERO, 'shorter packing-kernel vector') + kernel_vectors += 1 + relation = ((base, 0), (-1, 0)) + require(pack(relation, base) == ZERO and energy(relation) == base*base+1, + 'sharp kernel relation') + unsafe = 0 + for radius in range(1, 33): + for base in range(1, 2*radius): + u = (((base+1)//2, 0), ZERO) + v = ((-(base//2), 0), (1, 0)) + require(u != v and max(energy(u), energy(v)) <= radius*radius, + 'unsafe witness must satisfy both energy bounds') + require(pack(u, base) == pack(v, base), 'unsafe integer-radix witness') + ui = tuple((-b, a) for a, b in u) + vi = tuple((-b, a) for a, b in v) + require(pack(ui, base) == pack(vi, base) and ui != vi, 'imaginary witness') + try: + admissible_radix(radius, base) + except ValueError: + unsafe += 1 + else: + raise ValueError('unsafe radix admitted') + # The componentwise bound |digit| <= B alone permits (B,-1), while + # the energy hypothesis excludes it by exactly one squared unit. + relation = ((2, 0), (-1, 0)) + require(pack(relation, 2) == ZERO and max(abs(a) for a, _ in relation) <= 2 + and energy(relation) == 5, 'component-only false inference') + # Each column has energy <= 1, but a row does not. This defeats substituting + # column bounds for row bounds in the packed operator implication. + first = [((1, 0), ZERO), (ZERO, ZERO)] + second = [((-1, 0), (1, 0)), (ZERO, ZERO)] + require([pack(row, 2) for row in first] == [pack(row, 2) for row in second], + 'column-only false equality') + require(all(sum(row[j][0]**2+row[j][1]**2 for row in matrix) <= 1 + for matrix in (first, second) for j in (0, 1)), 'column-only premises') + require(energy(second[0]) == 2, 'row bound is the missing premise') + return {'gaussian_balls': cases, 'vectors': total, 'short_kernel_vectors_checked': kernel_vectors, + 'unsafe_integer_radices': unsafe, + 'controls': ['adjacent_and_smaller_radix_collisions', 'imaginary_collisions', + 'component_bounds_do_not_replace_energy', + 'column_bounds_do_not_replace_row_bounds', 'strict_kernel_energy_gap']} + + +def rotate(value, phase): + a, b = value + return ((a, b), (-b, a), (-a, -b), (b, -a))[phase % 4] + + +def binary_map(rows, address): + return sum(((row & address).bit_count() & 1) << bit for bit, row in enumerate(rows)) + + +def diagonal_phase(q, alpha, address): + active = [j for j in range(9) if address & (1 << j)] + return (sum(alpha[j] for j in active) + + 2*sum((q[j] >> k) & 1 for j in active for k in active if j < k)) % 4 + + +def compile_circuit(gates): + """Validate a closed grammar; compile permutations as forward scatter maps.""" + operations = [] + count = 0 + for gate in gates: + require(isinstance(gate, list) and gate, 'nonempty literal gate') + tag = gate[0] + if tag == 'pm': + require(len(gate) == 3 and all(isinstance(v, list) and len(v) == 9 for v in gate[1:]), + 'permutation shape') + require(all(type(v) is int and 0 <= v < N for row in gate[1:] for v in row), + 'permutation masks') + forward = tuple(binary_map(gate[1], j) for j in range(N)) + inverse = tuple(binary_map(gate[2], j) for j in range(N)) + require(all(forward[inverse[j]] == inverse[forward[j]] == j for j in range(N)), + 'unitary permutation/inverse') + operations.append(('P', forward)) + elif tag == 'dg': + require(len(gate) == 3 and all(isinstance(v, list) and len(v) == 9 for v in gate[1:]), + 'diagonal shape') + require(all(type(v) is int and v >= 0 for row in gate[1:] for v in row), 'diagonal integers') + operations.append(('D', tuple(diagonal_phase(gate[1], gate[2], j) for j in range(N)))) + elif tag in ('xg', 'cg'): + require(len(gate) == (2 if tag == 'xg' else 3), 'X/C shape') + require(type(gate[1]) is int and 0 <= gate[1] < N, 'involutive XOR domain') + if tag == 'cg': + require(type(gate[2]) is bool, 'C sign') + operations.append(('C', (gate[1], 1 if gate[2] else -1))) + count += 1 + else: + operations.append(('X', gate[1])) + elif tag == 'ph': + require(len(gate) == 2 and type(gate[1]) is int and gate[1] >= 0, 'global phase') + operations.append(('F', gate[1] % 4)) + else: + raise ValueError('unknown literal gate') + return operations, count + + +def execute(compiled, values): + values = list(values) + require(len(values) == N, 'vector length') + for tag, data in compiled[0]: + if tag == 'P': + result = [ZERO]*N + for address, value in enumerate(values): + result[data[address]] = value + values = result + elif tag == 'D': + values = [rotate(v, p) for v, p in zip(values, data)] + elif tag == 'F': + values = [rotate(v, data) for v in values] + elif tag == 'X': + values = [values[j ^ data] for j in range(N)] + else: + mask, sign = data + if mask == 0: + values = [(2*a, 2*b) for a, b in values] + continue + result = [ZERO]*N + for j in range(N): + k = j ^ mask + if j > k: + continue + a, b = values[j] + c, d = values[k] + real, imag = a+c, b+d + dr, di = -sign*(b-d), sign*(a-c) + result[j], result[k] = (real+dr, imag+di), (real-dr, imag-di) + values = result + return values + + +def adjoint(gates): + out = [] + for gate in reversed(gates): + tag = gate[0] + if tag == 'pm': + out.append([tag, gate[2], gate[1]]) + elif tag == 'dg': + out.append([tag, gate[1], [(-v) % 4 for v in gate[2]]]) + elif tag == 'cg': + out.append([tag, gate[1], not gate[2]]) + elif tag == 'ph': + out.append([tag, (-gate[1]) % 4]) + else: + out.append(list(gate)) + return out + + +def direct_execute(gates, values): + """Second gate oracle: direct source pullback and pointwise C formula.""" + values = list(values) + for gate in gates: + tag = gate[0] + if tag == 'pm': + values = [values[binary_map(gate[2], j)] for j in range(N)] + elif tag == 'dg': + values = [rotate(v, diagonal_phase(gate[1], gate[2], j)) for j, v in enumerate(values)] + elif tag == 'ph': + values = [rotate(v, gate[1]) for v in values] + elif tag == 'xg': + values = [values[j ^ gate[1]] for j in range(N)] + else: + sign = 1 if gate[2] else -1 + result = [] + for j, (a, b) in enumerate(values): + c, d = values[j ^ gate[1]] + result.append((a-sign*b+c+sign*d, b+sign*a+d-sign*c)) + values = result + return values + + +def packed_equal(left, right, bits): + kl, kr = left[1], right[1] + common = max(kl, kr) + require(type(bits) is int and bits >= 1, 'positive radix bits') + admissible_radix(1 << common, 1 << bits) + initial = [(1 << (bits*j), 0) for j in range(N)] + a, b = execute(left, initial), execute(right, initial) + return all((x[0] << (common-kl), x[1] << (common-kl)) + == (y[0] << (common-kr), y[1] << (common-kr)) for x, y in zip(a, b)) + + +def source_checks(): + pins = {} + for row in read_json(HERE/'SOURCES.json')['files']: + if row['usage'] == 'input': + actual = hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest() + require(actual == row['sha256'], 'source drift: ' + row['path']) + pins[row['path']] = actual + parser_path = ROOT/'research/hpe-lean-semantic-binding/verify.py' + spec = importlib.util.spec_from_file_location('retained_literal_parser', parser_path) + parser = importlib.util.module_from_spec(spec) + spec.loader.exec_module(parser) + _, circuits = parser.literal_data((ROOT/'research/hyperplane-end-lean/HyperplaneEnd/Exact.lean').read_text(encoding='utf-8')) + pairs, controls = [], [] + row_count = oracle_count = 0 + for index in (1, 2, 3): + lhs, rhs = circuits[f'lhsLit{index}'], circuits[f'rhsLit{index}'] + left, right = compile_circuit(lhs), compile_circuit(rhs) + kl, kr = left[1], right[1] + common = max(kl, kr) + require(packed_equal(left, right, common+1), 'energy-radix exact source equality') + require(packed_equal(left, right, common+2), 'PR1859 sufficient radix') + require(packed_equal(left, right, 2*common+2), 'retained coarse radix') + la, ra = compile_circuit(adjoint(lhs)), compile_circuit(adjoint(rhs)) + digest = hashlib.sha256() + sample_left, sample_right = {}, {} + for address in range(N): + basis = [ZERO]*N + basis[address] = (1, 0) + # Conjugate adjoint columns to obtain forward rows, the coefficients + # relevant to packing input coordinates. Column bounds alone fail. + a = [(x << (common-kl), (-y) << (common-kl)) for x, y in execute(la, basis)] + b = [(x << (common-kr), (-y) << (common-kr)) for x, y in execute(ra, basis)] + require(a == b and energy(a) == energy(b) == 4**common, 'complete scaled row/energy') + digest.update((canonical(a)+'\n').encode()) + if address in (0, 1, 255, 511): + sample_left[address], sample_right[address] = a, b + row_count += 2 + for gates, compiled, sample_rows in ((lhs, left, sample_left), (rhs, right, sample_right)): + fixtures = [] + for address in (0, 1, 255, 511): + basis = [ZERO]*N + basis[address] = (1, 0) + fixtures.append((address, basis)) + fixtures.append((None, [((7*j % 11)-5, (3*j % 7)-3) for j in range(N)])) + for address, initial in fixtures: + actual = execute(compiled, initial) + require(actual == direct_execute(gates, initial), 'separate gate oracle') + if address is not None: + scale = common-compiled[1] + require(all((actual[j][0] << scale, actual[j][1] << scale) == row[address] + for j, row in sample_rows.items()), 'adjoint/forward transpose binding') + oracle_count += 1 + phase = compile_circuit(rhs + [['ph', 1]]) + character = compile_circuit([['dg', [0]*9, [2]+[0]*8]] + rhs) + require(not packed_equal(left, phase, common+1), 'global phase must be retained') + require(not packed_equal(left, character, common+1), 'input character must be retained') + initial = [(1 << ((common+1)*j), 0) for j in range(N)] + require(execute(left, initial) != execute(right, initial), 'omitted normalization') + try: + packed_equal(left, right, common) + except ValueError: + pass + else: + raise ValueError('unsupported radix admitted') + controls.extend([f'pair{index}_phase', f'pair{index}_input_character', + f'pair{index}_omitted_scale', f'pair{index}_undersized_radix']) + pairs.append({'pair': index, 'C_left': kl, 'C_right': kr, 'radius': 1 << common, + 'radix_bits': common+1, 'previous_unitary_radix_bits': common+2, + 'original_radix_bits': 2*common+2, + 'largest_input_bits': (common+1)*(N-1)+1, + 'scaled_row_sha256': digest.hexdigest(), 'row_squared_energy': 4**common}) + bad = [['pm', [0]*9, [1 << j for j in range(9)]]] + for label, gates in (('nonunitary_permutation', bad), ('out_of_domain_X', [['xg', N]]), + ('nonboolean_C_sign', [['cg', 1, 1]])): + try: + compile_circuit(gates) + except ValueError: + controls.append(label) + else: + raise ValueError(label+' accepted') + return {'pairs': pairs, 'scaled_rows_checked': row_count, 'separate_oracle_executions': oracle_count, + 'controls': controls, 'input_sha256': pins} + + +def run(): + source = source_checks() + balls = ball_checks() + return {'status': 'PASS_HPE_ENERGY_PACKED_RADIX', 'source': source, 'energy_balls': balls, + 'new_lean_proof': False, 'selected_checker_changed': False, 'new_kappa': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='Explicit output receipt path; normal replay is read-only') + args = parser.parse_args() + result = run() + if args.write: + args.write.write_text(json.dumps(result, indent=2)+'\n', encoding='utf-8', newline='\n') + else: + require(canonical(result) == canonical(read_json(HERE/'RESULT.json')), 'receipt mismatch') + print(result['status'], 'rows='+str(result['source']['scaled_rows_checked']), + 'ball_vectors='+str(result['energy_balls']['vectors'])) + + +if __name__ == '__main__': + main()