Prove sharp energy-ball radix for packed HPE equality

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.

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
+}

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"
+    }
+  ]
+}