diff --git a/research/hpe-energy-independent-audit/PR1906-RESULT.json b/research/hpe-energy-independent-audit/PR1906-RESULT.json new file mode 100644 index 0000000000..20b1b82db1 --- /dev/null +++ b/research/hpe-energy-independent-audit/PR1906-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-independent-audit/README.md b/research/hpe-energy-independent-audit/README.md new file mode 100644 index 0000000000..c189f943e4 --- /dev/null +++ b/research/hpe-energy-independent-audit/README.md @@ -0,0 +1,160 @@ +# Independent full-matrix audit of the HPE energy radix + +**PR1906's three literal HPE pairs are independently corroborated.** A separate +closed parser and direct integer realification reconstruct all six matrices, +including global phase. All 3,072 complex rows have the claimed common energy +and reproduce the predecessor's three whole-matrix row digests. No discrepancy, +new radix bound, Lean proof, supplier or multiplication exponent is claimed. + +Audited predecessor: Arham Tahir's +[PR1906](https://github.com/CrocSwap/integer-mult-bounds/pull/1906), exact head +`788848032c16bbe0a543c1186c6691c66131c090`. Base main is +`0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA256 is +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +The selection remains the conditional finite frontier1094 result. This audit +does not run its cold replay or change any selected source. + +## What this audit adds + +PR1906 obtains rows by conjugating columns of an adjoint interpreter. It checks +all those rows, but its forward/adjoint correspondence check samples the 4 by 4 +entries at indices `{0,1,255,511}` per circuit. Its second forward interpreter +shares parsing and phase helpers. Those are disclosed limitations, not evidence +that its formulas are wrong. + +This audit imports **no predecessor code**. It independently parses the six +`lhsLit1..3` / `rhsLit1..3` definitions in the pinned `Exact.lean`, then propagates +the identity matrix through every gate in chronological order. The representation +is an integer matrix on 1,024 interleaved real/imaginary coordinates. Permutations +use explicit binary dot products and inverse pullback; C gates use integer +four-row combinations. No packed evaluation or adjoint is used for acceptance. +Extraction is specific to these authenticated definitions; this is not a general +Lean parser for arbitrary comments, layout or continued expressions. + +For every complex coefficient, all four entries of its real 2-by-2 block are +checked against `[[Re,-Im],[Im,Re]]`. Each LHS/RHS comparison covers every +normalized matrix entry, including implicit sparse zeros. The six matrices +cover **6,291,456 real entries**. Their six row-digest calculations agree in +three pairs with the pinned precursor receipt; digests corroborate that receipt +and do not substitute for the direct matrix equality. + +| Literal pair | LHS C count | RHS C count | Common row energy | Safe radix bits | +|---|---:|---:|---:|---:| +| 1 | 9 | 7 | 262,144 | 10 | +| 2 | 9 | 7 | 262,144 | 10 | +| 3 | 9 | 7 | 262,144 | 10 | + +Each raw realification has 262,144 nonzero integer entries. Every row and column +has its correct squared energy, with common normalization applied to the rows. +The unchanged safe radix is `2^10`; the largest 512-coordinate packed input +would have 5,111 bits. No performance measurement or optimal radix for these +particular matrices follows. + +## Independent mathematical review + +A separately delegated exact-circuit specialist reviewed the written argument, +source gate semantics, normalization and this oracle. The parent also checked +the argument. This is independent AI review, not human review or a kernel proof. + +The decisive argument is sound. For positive integer B and a nonzero finite +Gaussian vector d with `sum d_j B^j=0`, its first nonzero digit is a nonzero +Gaussian multiple of B. At least one later digit is nonzero, so +`E(d)>=B^2+1`. If `E(u),E(v)<=R^2`, the parallelogram identity gives +`E(u-v)<=4R^2`. Thus `B>=2R` excludes every nonzero kernel difference, including +the equality boundary. For integer `R>=1`, all smaller positive integer radices +have the two-coordinate collision +`u=(ceil(B/2),0)`, `v=(-floor(B/2),1)`. This establishes sharpness for the whole +ball in dimensions at least two, not for equal-energy unitary rows. Length zero +is vacuous and length one is injective at every positive radix. + +The extra gate premise is essential. Mutual-inverse finite permutation maps and +involutive XOR maps make P and X unitary. With `P_+=(I+X)/2`, `P_-=(I-X)/2`, +the normalized C gate is `P_+ + s*i*P_-`; diagonal/global i-powers are also +unitary. Hence a normalized circuit U is unitary, and dropping k halves gives +`Z=2^k U` with both row and column energy `4^k`. Scaling each side to +`K=max(k_left,k_right)` supplies the row premise with `R=2^K`. A column-energy +bound alone is insufficient. Numeric energy checks do not independently prove +orthogonality; the gate-level argument supplies unitarity. + +The retained generic Lean equality theorem accepts arbitrary literal lists. +The stricter valid-gate premise cannot be silently omitted when using the +improved energy bound. For a concrete failure, take an invalid permutation +pullback mapping every address to zero, then phase `i^x0`, then `C(1,+)`. +Its unnormalized output row zero is `(2+2i)e_0`, energy eight, while one C gate +would predict four. The new and predecessor validators both reject that +permutation. The test intentionally disables validation to expose this exact +mathematical failure. + +## Reproduction and controls + +Python 3.12, standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/hpe-energy-independent-audit +``` + +Normal replay is read-only and requires the fixed `RESULT.json`. Explicit +regeneration is separate: + +```sh +python3.12 -I -B research/hpe-energy-independent-audit/verify.py --write /tmp/hpe-energy-audit.json +``` + +The registered replay checks complete matrices and three semantic faults per +pair: global phase, input character and omitted common normalization. A C gate +followed by its inverse is accepted even though its raw integer scale changes. +Seven test groups additionally cover: + +- All 585 words of lengths zero through three over eight two-qubit gates, + against independently specified dense Gaussian-rational matrices. The + alphabet includes noncommuting gates, a non-self-inverse permutation, + both C signs, zero-mask C, quadratic phase, XOR and global phase. +- Wrong permutation direction, reversed noncommuting order, valid phase + periodicity, the nonunitary energy witness, and complete realification. +- Closed literal inventory, malformed tokens, missing/duplicate definitions + and a harmless whitespace presentation change. +- Seven scientific predecessor-receipt corruptions with checksum guards + bypassed; actual detector removal makes the rejection harness fail. +- Missing/duplicate/corrupted evidence, source drift, explicit byte-identical + regeneration, and an optimized read-only export without Git. + +Detector-removal controls disable the named whole predicates to test the rejection +harness. They do not establish sensitivity to every possible implementation fault. + +The primary PR1906 direct verifier was also replayed from its exact Git head +in isolated scratch and passed. That is a reproduction, distinct from the new +oracle. The written all-dimension proof is not inferred from finite tests. +No Lean toolchain was available locally. No Lean build, supplier cold replay, +new canonical-frame derivation, physical hosting/restoration proof, precision +or tape-cost admission, or all-size multiplication proof was performed. + +## Sources and credit + +`SOURCES.json` pins both live Lean inputs and the original task provenance. +`PR1906-RESULT.json` is the unmodified precursor receipt, reproduced under its +Apache-2.0 license with exact source head and SHA256. Its row digests are used +only as comparison evidence. No predecessor implementation is copied. + +Credit Arham Tahir / PR1906 for the sharp energy-ball result; woklerx / PR1859 +for the earlier unitary-premise radix; Jeremy Kothe / PR593 for the retained +Lean semantics, proof and literal circuits; commdata2338 for the earlier +semantic-binding work and parser (not reused here); Sagar Thakrar / PR1781 for +the distinct selected-recipe census; and the inherited Lemma A/G and Clifford +work by DreamingOfClouds, icekylinx, Chafik Boukhalfa and Zhihao Chen. Their +source notices remain unchanged. The added value is deliberate independent +verification, not priority for their construction or proof. + +Prepared for Ross with substantial OpenAI Codex assistance in implementation, +mathematics, testing and prose. One exact-circuit specialist supplied separate +proof and code review. Apache-2.0. Task draw and refined scope are in `TASK.json`; +coordination is in [Discussion1896](https://github.com/CrocSwap/integer-mult-bounds/discussions/1896). + +## Open next questions + +Formalize the least-nonzero-digit energy bound and valid-gate row norms in Lean, +then connect them to the retained packed comparator. This is the remaining +formal adoption step, already identified by PR1906. The concrete first step is +the Gaussian kernel-energy lemma plus the parallelogram implication; the +blocker is the missing kernel proof. Kernel timing and compiler resource bounds +are separate. Repeating this six-matrix census is unnecessary unless its sources +or arithmetic change. Structured details are in `TASK.json`. diff --git a/research/hpe-energy-independent-audit/RESULT.json b/research/hpe-energy-independent-audit/RESULT.json new file mode 100644 index 0000000000..a1c6e53697 --- /dev/null +++ b/research/hpe-energy-independent-audit/RESULT.json @@ -0,0 +1,97 @@ +{ + "status": "PASS_INDEPENDENT_HPE_ENERGY_AUDIT", + "predecessor_head": "788848032c16bbe0a543c1186c6691c66131c090", + "pairs": [ + { + "pair": 1, + "common_C": 9, + "radix_bits": 10, + "sides": [ + { + "scaled_row_sha256": "f217217e83d8f49a19df80669c0de735d73edfabecd1eb3e9783b4cb7f311267", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 9 + }, + { + "scaled_row_sha256": "f217217e83d8f49a19df80669c0de735d73edfabecd1eb3e9783b4cb7f311267", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 7 + } + ], + "controls": [ + "global_phase", + "input_character", + "omitted_normalization" + ], + "positive_control": "C_inverse_pair_with_changed_raw_scale" + }, + { + "pair": 2, + "common_C": 9, + "radix_bits": 10, + "sides": [ + { + "scaled_row_sha256": "3ff6f9679256f02a243b1b0fd4b55e50a98d5ca8f282b8d0a948f1598a38fb3e", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 9 + }, + { + "scaled_row_sha256": "3ff6f9679256f02a243b1b0fd4b55e50a98d5ca8f282b8d0a948f1598a38fb3e", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 7 + } + ], + "controls": [ + "global_phase", + "input_character", + "omitted_normalization" + ], + "positive_control": "C_inverse_pair_with_changed_raw_scale" + }, + { + "pair": 3, + "common_C": 9, + "radix_bits": 10, + "sides": [ + { + "scaled_row_sha256": "ee5ac2ce8466eeb7b1b8b2766626ed31b266fc8a65b401780954c7bb6dd901fd", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 9 + }, + { + "scaled_row_sha256": "ee5ac2ce8466eeb7b1b8b2766626ed31b266fc8a65b401780954c7bb6dd901fd", + "row_squared_energy": 262144, + "real_rows": 1024, + "real_columns": 1024, + "nonzero_real_entries": 262144, + "C_count": 7 + } + ], + "controls": [ + "global_phase", + "input_character", + "omitted_normalization" + ], + "positive_control": "C_inverse_pair_with_changed_raw_scale" + } + ], + "complex_rows_checked": 3072, + "real_matrix_entries_covered": 6291456, + "new_lean_proof": false, + "new_kappa": false +} diff --git a/research/hpe-energy-independent-audit/SOURCES.json b/research/hpe-energy-independent-audit/SOURCES.json new file mode 100644 index 0000000000..a2eb2ad56d --- /dev/null +++ b/research/hpe-energy-independent-audit/SOURCES.json @@ -0,0 +1,39 @@ +{ + "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/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" + } + ], + "external_result": { + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "head": "788848032c16bbe0a543c1186c6691c66131c090", + "path": "research/hpe-energy-packed-radix/RESULT.json", + "local_path": "PR1906-RESULT.json", + "sha256": "594e9dda27116fbc7c11549a2d886e5bb6eb7c9258b043ee7e0a927b777f57e6", + "author": "Arham Tahir; substantial OpenAI Codex assistance", + "license": "Apache-2.0" + } +} diff --git a/research/hpe-energy-independent-audit/TASK.json b/research/hpe-energy-independent-audit/TASK.json new file mode 100644 index 0000000000..96d6003ba2 --- /dev/null +++ b/research/hpe-energy-independent-audit/TASK.json @@ -0,0 +1,167 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "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" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently corroborate PR1906 at 788848032c16bbe0a543c1186c6691c66131c090: all six HPE literal circuits on 512 complex coordinates, complete normalized matrices, row-energy hypotheses, and all-dimension written packing argument.", + "scope_change_reason": "Audit the written row-energy replacement lemma and its finite source binding in PR1906 using a separate parser and direct integer realification matrices; no formal kernel extension is claimed.", + "bottleneck_link": "Independent source-bound verification checks the row-energy premise needed for a proof-preserving smaller packed radix; it does not alter the paid supplier profile or current complex bottleneck.", + "budget_minutes": 60, + "stop_rule": "One approximately 60-minute session; stop after one independently reviewable audit, preserving final quarter for verification and handoff.", + "outcome": "completed", + "evidence": "RESULT.json: full direct Gaussian-integer realifications for all six literal circuits, 3072 complex rows, 6291456 real entries, independently matching the pinned PR1906 row digests and energies. Seven focused test groups and separate specialist proof review; no discrepancy.", + "author": "Ross, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; one separate exact-circuit specialist reviews the proof. No human or Lean-kernel review.", + "open_questions": [ + { + "question": "Can the energy-ball kernel bound and valid-gate row energies be proved in Lean?", + "why_it_matters": "These are the missing formal premises for adopting the reduced-radix checker.", + "first_step": "Prove the least-nonzero Gaussian digit energy lower bound, then connect valid normalized gate semantics to scaled row energies.", + "blocked_by": "No Lean proof of the new energy argument or guarded circuit implication is supplied here." + } + ], + "draw": { + "seed": "cfbe139628a1920458d65ac59391c82d", + "track": "independent-verification", + "suggestions": [ + { + "task_id": "formal-interface-lemma", + "scope_key": "e3ffea67887eeb4c396c", + "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?", + "method": "Audit a formal theorem-to-certificate binding independently.", + "starting_points": [ + "certificates/selected-result.json", + "research/hyperplane-end-lean/PROOF.md" + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.", + "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" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "independent-moment", + "scope_key": "c191650c0fa8d2fa514e", + "question": "Can one selected pricing or assembly claim be checked by a genuinely independent exact implementation?", + "method": "Implement certified moment inequalities through a different exact enclosure method.", + "starting_points": [ + "certificates/selected-result.json" + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Recompute one small part of the ledger or one certified enclosure using an independent implementation.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." + }, + "nearest_overlap": [ + { + "pr": 1906, + "head": "788848032c16bbe0a543c1186c6691c66131c090", + "delta": "Intentional independent corroboration; new parser/direct realification matrix method versus shared-parser, adjoint-row predecessor." + }, + { + "pr": 1859, + "head": "f5e18c0c44371ebfdd46bfe25efe5b49e467fafe", + "delta": "Earlier sufficient radix; no claim of a new bound." + }, + { + "pr": 1781, + "head": "dafbaadeb423b3bc80fbf6fcd6f415400dc0ffbf", + "delta": "Different selected recipe census; not imported or independently repeated." + } + ], + "budget": "No new supplier invoice: verification only; approximately 60 minutes, final quarter reserved for checks and handoff." +} diff --git a/research/hpe-energy-independent-audit/VERIFY.json b/research/hpe-energy-independent-audit/VERIFY.json new file mode 100644 index 0000000000..7e6ff4722a --- /dev/null +++ b/research/hpe-energy-independent-audit/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Separate closed parser; complete direct integer realification matrices and row-energy/digest binding for six literal circuits; phase, character, scale and equivalent-presentation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-m", + "unittest", + "discover", + "-s", + "{package}", + "-p", + "test_verify.py" + ], + "timeout_seconds": 180, + "checks": "585 exact dense rational short-word comparisons, parser and guard boundaries, detector-removal sensitivity, seven checksum-free scientific receipt corruptions, source/missing/duplicate evidence rejection, explicit regeneration and optimized read-only relocation." + } + ] +} diff --git a/research/hpe-energy-independent-audit/test_verify.py b/research/hpe-energy-independent-audit/test_verify.py new file mode 100644 index 0000000000..2d0bb84833 --- /dev/null +++ b/research/hpe-energy-independent-audit/test_verify.py @@ -0,0 +1,265 @@ +"""Independent small dense oracle and failure-boundary controls. Apache-2.0.""" +import copy +from fractions import Fraction as Q +import importlib.util +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location('energy_audit', HERE/'verify.py') +v = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(v) +ZERO, ONE, I = (Q(0), Q(0)), (Q(1), Q(0)), (Q(0), Q(1)) + + +def add(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 identity(n=4): + return [[ONE if j == k else ZERO for k in range(n)] for j in range(n)] + + +def product(a, b): + n = len(a) + result = [[ZERO]*n for _ in range(n)] + for j in range(n): + for k in range(n): + for l in range(n): + result[j][k] = add(result[j][k], mul(a[j][l], b[l][k])) + return result + + +def permutation(mapping): + return [[ONE if row == mapping[column] else ZERO for column in range(4)] + for row in range(4)] + + +def diagonal(entries): + return [[entries[j] if j == k else ZERO for k in range(4)] for j in range(4)] + + +def c_gate(mapping, sign): + a, b = (Q(1, 2), Q(sign, 2)), (Q(1, 2), Q(-sign, 2)) + return [[add(a if j == k else ZERO, b if j == mapping[k] else ZERO) + for k in range(4)] for j in range(4)] + + +def alphabet(): + # Matrices are hard-coded from mathematical action on four addresses; + # no production phase, parity, parser or realification helper is used. + return [ + (['cg', 1, True], c_gate([1, 0, 3, 2], 1)), + (['cg', 1, False], c_gate([1, 0, 3, 2], -1)), + (['cg', 2, False], c_gate([2, 3, 0, 1], -1)), + (['cg', 0, True], identity()), + (['ph', 1], diagonal([I]*4)), + (['dg', [2, 0], [1, 2]], diagonal([ONE, I, (-Q(1), Q(0)), I])), + (['pm', [2, 3], [3, 1]], permutation([0, 2, 3, 1])), + (['xg', 1], permutation([1, 0, 3, 2])), + ] + + +def dense_of_result(result): + rows, count = result + return [[(Q(a, 1 << count), Q(b, 1 << count)) for a, b in row] + for row in v.gaussian_rows(rows, 0)] + + +class AuditTests(unittest.TestCase): + def test_complete_short_word_oracle(self): + letters = alphabet() + cases = 0 + for length in range(4): + for word in itertools.product(letters, repeat=length): + expected = identity() + for _, gate_matrix in word: + expected = product(gate_matrix, expected) + actual = v.matrix([gate for gate, _ in word], n=2) + self.assertEqual(dense_of_result(actual), expected) + v.row_record(actual, actual[1]) + cases += 1 + self.assertEqual(cases, 585) + + def test_semantic_controls_and_detector_sensitivity(self): + unit = v.matrix([], n=2) + wrong_phase = v.matrix([['ph', 1]], n=2) + wrong_character = v.matrix([['dg', [0, 0], [2, 0]]], n=2) + equivalent = v.matrix([['cg', 1, True], ['cg', 1, False]], n=2) + self.assertTrue(v.normalized_equal(unit, equivalent)) + self.assertTrue(v.normalized_equal(equivalent, unit)) + for bad in (wrong_phase, wrong_character, (equivalent[0], 0)): + v.must_reject(lambda: v.require(v.normalized_equal(unit, bad), 'operator mismatch'), + 'operator mismatch') + # If the detector is removed, the rejection harness must fail. + with patch.object(v, 'normalized_equal', return_value=True): + with self.assertRaisesRegex(ValueError, 'unexpected acceptance'): + v.must_reject(lambda: v.require(v.normalized_equal(unit, bad), 'operator mismatch'), + 'operator mismatch') + forward = v.matrix([['pm', [2, 3], [3, 1]]], n=2) + backward = v.matrix([['pm', [3, 1], [2, 3]]], n=2) + self.assertFalse(v.normalized_equal(forward, backward)) + c, d = ['cg', 1, True], ['dg', [0, 0], [1, 0]] + self.assertFalse(v.normalized_equal(v.matrix([c, d], n=2), v.matrix([d, c], n=2))) + self.assertTrue(v.normalized_equal(v.matrix([d], n=2), + v.matrix([['dg', [0, 0], [5, 4]]], n=2))) + for sign in (True, False): + self.assertTrue(v.normalized_equal(unit, v.matrix([['cg', 0, sign]], n=2))) + + def test_guard_energy_and_realification_obligations(self): + malformed = [([['pm', [0, 0], [0, 0]]], 'permutation inverse'), + ([['xg', 4]], 'XOR domain'), + ([['cg', 1, 1]], 'Boolean C sign')] + for gates, message in malformed: + v.must_reject(lambda: v.validate(gates, 2), message) + with patch.object(v, 'validate', return_value=None): + with self.assertRaisesRegex(ValueError, 'unexpected acceptance'): + v.must_reject(lambda: v.validate(gates, 2), message) + # This actual invalid literal program has energy 8 at row zero, + # despite k=1 predicting 4. It isolates the unitarity premise. + invalid = [['pm', [0], [0]], ['dg', [0], [1]], ['cg', 1, True]] + with patch.object(v, 'validate', return_value=None): + result = v.matrix(invalid, n=1) + row = next(v.gaussian_rows(result[0], 0)) + self.assertEqual(row, [[2, 2], [0, 0]]) + v.must_reject(lambda: v.row_record(result, 1), 'scaled row energy') + with patch.object(v, 'row_record', return_value={}): + with self.assertRaisesRegex(ValueError, 'unexpected acceptance'): + v.must_reject(lambda: v.row_record(result, 1), 'scaled row energy') + damaged = copy.deepcopy(v.matrix([], n=1)) + damaged[0][1][0] = 1 + v.must_reject(lambda: list(v.gaussian_rows(damaged[0], 0)), 'realification') + + def test_parser_closed_inventory(self): + source = (v.ROOT/v.EXACT).read_text(encoding='utf-8') + circuits = v.literals(source) + self.assertEqual(len(circuits), 6) + # Explicit tokens, gate order and both directions of a non-self-inverse map. + self.assertEqual(circuits['lhsLit1'][2], ['cg', 1, False]) + for change in [source.replace('.cg 1 false', '.cg 1 0'), + source.replace('def lhsLit1 :', 'def missingLit1 :'), + source.replace('.ph 1,', '.ph (1+0),'), + source + '\ndef lhsLit1 : List Gate :=\n [.ph 0]\n\n']: + with self.assertRaises(ValueError): + v.literals(change) + # Layout changes inside a pinned closed literal grammar are harmless. + self.assertEqual(v.literals(source.replace(' .cg', ' .cg')), circuits) + + def test_energy_boundary_witnesses(self): + # Independent exact arithmetic corroboration, not proof by sampling. + for radius in (1, 2, 3, 16, 512): + for base in (1, 2*radius-1): + upper, lower = (base+1)//2, base//2 + self.assertEqual(upper, -lower+base) + self.assertLessEqual(upper*upper, radius*radius) + self.assertLessEqual(lower*lower+1, radius*radius) + base = 2*radius + self.assertGreater(base*base+1, 4*radius*radius) + # Column energies <=1 do not provide the row premise. + a, b = [[1, 0], [0, 0]], [[-1, 1], [0, 0]] + self.assertEqual([r[0]+2*r[1] for r in a], [r[0]+2*r[1] for r in b]) + self.assertTrue(all(sum(r[j]**2 for r in m) <= 1 for m in (a, b) for j in (0, 1))) + self.assertEqual(sum(x*x for x in b[0]), 2) + + def test_predecessor_scientific_receipt_controls(self): + expected = v.read_json(HERE/'PR1906-RESULT.json')['source']['pairs'][0] + record = {'scaled_row_sha256': expected['scaled_row_sha256'], + 'row_squared_energy': 4**9} + v.bind_record([record, record], 9, 7, 9, expected) + for field, value, message in ( + ('scaled_row_sha256', '0'*64, 'row digest'), + ('row_squared_energy', 4**8, 'energy'), + ('C_left', 8, 'C counts'), ('C_right', 6, 'C counts'), + ('radix_bits', 9, 'radix binding'), ('radius', 256, 'radix binding'), + ('largest_input_bits', 5110, 'packed input length')): + bad = dict(expected, **{field: value}) + # Bypass checksum guards to test the mathematical receipt binding. + v.must_reject(lambda: v.bind_record([record, record], 9, 7, 9, bad), message) + with patch.object(v, 'bind_record', return_value=None): + with self.assertRaisesRegex(ValueError, 'unexpected acceptance'): + v.must_reject(lambda: v.bind_record([record, record], 9, 7, 9, bad), message) + + def test_export_source_receipt_and_read_only_replay(self): + with tempfile.TemporaryDirectory(prefix='hpe-energy-audit-') as directory: + root = Path(directory) + package = root/'research'/HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + for name in (v.EXACT, v.CLIFFORD): + target = root/name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(v.ROOT/name, target) + + def invoke(*args): + return subprocess.run([sys.executable, '-I', '-O', '-B', str(package/'verify.py'), *args], + cwd=root, text=True, capture_output=True, timeout=120) + + receipt = package/'RESULT.json' + original = receipt.read_bytes() + receipt.unlink() + result = invoke() + self.assertNotEqual(result.returncode, 0) + self.assertFalse(receipt.exists()) + receipt.write_bytes(original) + data = json.loads(original) + data['pairs'][0]['radix_bits'] += 1 + receipt.write_text(json.dumps(data), encoding='utf-8') + result = invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn('audit receipt mismatch', result.stderr) + receipt.write_bytes(original) + source = root/v.EXACT + source.write_bytes(source.read_bytes()+b'\n') + result = invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn('source drift', result.stderr) + shutil.copy2(v.ROOT/v.EXACT, source) + predecessor = package/'PR1906-RESULT.json' + pred_bytes = predecessor.read_bytes() + predecessor.write_bytes(pred_bytes+b'\n') + result = invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn('predecessor receipt drift', result.stderr) + predecessor.write_bytes(pred_bytes) + receipt.write_text('{"x":1,"x":2}', encoding='utf-8') + result = invoke() + self.assertNotEqual(result.returncode, 0) + self.assertIn('duplicate JSON key', result.stderr) + receipt.write_bytes(original) + generated = root/'regenerated.json' + result = invoke('--write', str(generated)) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(generated.read_bytes(), original) + files = [p for p in root.rglob('*') if p.is_file()] + directories = [p for p in root.rglob('*') if p.is_dir()] + before = {str(p.relative_to(root)): p.read_bytes() for p in files} + try: + for path in files: + path.chmod(0o444) + for path in reversed(directories): + path.chmod(0o555) + root.chmod(0o555) + result = invoke() + self.assertEqual(result.returncode, 0, result.stderr) + after = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob('*') if p.is_file()} + self.assertEqual(before, after) + finally: + root.chmod(0o755) + for path in directories: + path.chmod(0o755) + for path in files: + path.chmod(0o644) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/hpe-energy-independent-audit/verify.py b/research/hpe-energy-independent-audit/verify.py new file mode 100644 index 0000000000..2467b23364 --- /dev/null +++ b/research/hpe-energy-independent-audit/verify.py @@ -0,0 +1,323 @@ +"""Independent direct realification audit of PR1906. Apache-2.0. + +Prepared for Ross with OpenAI Codex assistance. No predecessor code is imported. +Matrices are sparse integer matrices on interleaved real/imaginary coordinates. +We do not use adjoints, packed vectors, or the predecessor's literal parser. +""" +import argparse +import hashlib +import json +import re +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +EXACT = 'research/hyperplane-end-lean/HyperplaneEnd/Exact.lean' +CLIFFORD = 'research/hyperplane-end-lean/HyperplaneEnd/Clifford.lean' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique(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) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')) + + +def literals(source): + """Parse only six closed List Gate definitions, consuming every token. + + No eval, AST conversion, imported parser, or Lean expression evaluation. + The scientific input is separately authenticated before this is called. + """ + found = {} + pattern = r'^def ((?:lhs|rhs)Lit[123]) : List Gate :=\s*(.*?)\n\n' + for match in re.finditer(pattern, source, re.M | re.S): + name, body = match.groups() + require(name not in found, 'duplicate literal definition') + tokens = re.findall(r'\s+|\.(?:pm|dg|cg|xg|ph)\b|true\b|false\b|[0-9]+|[\[\],]|\S', body) + tokens = [token for token in tokens if not token.isspace()] + index = 0 + + def take(expected=None): + nonlocal index + require(index < len(tokens), 'truncated literal') + token = tokens[index] + index += 1 + require(expected is None or token == expected, 'unexpected literal token') + return token + + def peek(): + require(index < len(tokens), 'truncated literal') + return tokens[index] + + def natural(): + token = take() + require(re.fullmatch(r'[0-9]+', token) is not None, 'natural literal required') + return int(token) + + def array(): + take('[') + result = [] + if peek() != ']': + result.append(natural()) + while peek() == ',': + take(',') + result.append(natural()) + take(']') + return result + + gates = [] + take('[') + while peek() != ']': + tag = take() + if tag in ('.pm', '.dg'): + gate = [tag[1:], array(), array()] + elif tag == '.cg': + mask, sign = natural(), take() + require(sign in ('true', 'false'), 'Boolean C sign required') + gate = ['cg', mask, sign == 'true'] + else: + require(tag in ('.xg', '.ph'), 'unknown gate literal') + gate = [tag[1:], natural()] + gates.append(gate) + if peek() != ',': + break + take(',') + take(']') + require(index == len(tokens), 'unconsumed literal expression') + found[name] = gates + require(set(found) == {side + str(i) for side in ('lhsLit', 'rhsLit') for i in (1, 2, 3)}, + 'six literal definitions required') + return found + + +def binary_image(rows, address): + # Explicit coordinate dot products, rather than bit_count/table parity. + result = 0 + for index, row in enumerate(rows): + bit = 0 + for column in range(len(rows)): + bit ^= ((row >> column) & 1) * ((address >> column) & 1) + result += bit << index + return result + + +def phase_exponent(q, alpha, address): + n = len(alpha) + bits = [(address >> j) & 1 for j in range(n)] + return (sum(alpha[j]*bits[j] for j in range(n)) + + 2*sum(((q[j] >> k) & 1)*bits[j]*bits[k] + for j in range(n) for k in range(j+1, n))) % 4 + + +def validate(gates, n): + require(type(n) is int and n >= 1, 'positive qubit count') + size = 1 << n + for g in gates: + require(type(g) is list and g, 'gate shape') + tag = g[0] + if tag in ('pm', 'dg'): + require(len(g) == 3 and all(type(v) is list and len(v) == n for v in g[1:]), + 'matrix/diagonal shape') + require(all(type(x) is int and x >= 0 for v in g[1:] for x in v), + 'matrix/diagonal natural entries') + if tag == 'pm': + require(all(x < size for v in g[1:] for x in v), 'binary matrix domain') + forward = [binary_image(g[1], x) for x in range(size)] + backward = [binary_image(g[2], x) for x in range(size)] + require(all(forward[backward[x]] == backward[forward[x]] == x + for x in range(size)), 'permutation inverse') + elif tag in ('cg', 'xg'): + require(len(g) == (3 if tag == 'cg' else 2) and + type(g[1]) is int and 0 <= g[1] < size, 'XOR domain') + if tag == 'cg': + require(type(g[2]) is bool, 'Boolean C sign') + else: + require(tag == 'ph' and len(g) == 2 and type(g[1]) is int and g[1] >= 0, + 'phase or unknown gate') + + +def combine(*terms): + out = {} + for coefficient, row in terms: + for column, value in row.items(): + out[column] = out.get(column, 0) + coefficient*value + return {column: value for column, value in out.items() if value} + + +def rotate_rows(real, imag, phase): + # Repeated exact multiplication by the integer matrix [[0,-1],[1,0]]. + for _ in range(phase % 4): + real, imag = {j: -x for j, x in imag.items()}, real + return real, imag + + +def matrix(gates, n=9): + """Return the full realification of 2^k U and its omitted-half count k.""" + validate(gates, n) + size = 1 << n + rows = [{j: 1} for j in range(2*size)] + count = 0 + for gate in gates: + tag = gate[0] + next_rows = [] + if tag == 'pm': + for x in range(size): + y = binary_image(gate[2], x) + next_rows.extend((rows[2*y], rows[2*y+1])) + elif tag in ('dg', 'ph'): + for x in range(size): + phase = phase_exponent(gate[1], gate[2], x) if tag == 'dg' else gate[1] + next_rows.extend(rotate_rows(rows[2*x], rows[2*x+1], phase)) + elif tag == 'xg': + for x in range(size): + y = x ^ gate[1] + next_rows.extend((rows[2*y], rows[2*y+1])) + else: + sign = 1 if gate[2] else -1 + for x in range(size): + y = x ^ gate[1] + real, imag, r_other, i_other = rows[2*x], rows[2*x+1], rows[2*y], rows[2*y+1] + next_rows.append(combine((1, real), (-sign, imag), (1, r_other), (sign, i_other))) + next_rows.append(combine((1, imag), (sign, real), (1, i_other), (-sign, r_other))) + count += 1 + rows = next_rows + return rows, count + + +def normalized_equal(left, right): + a, ka = left + b, kb = right + if len(a) != len(b): + return False + for r, s in zip(a, b): + if any((r.get(j, 0) << kb) != (s.get(j, 0) << ka) for j in r.keys() | s.keys()): + return False + return True + + +def gaussian_rows(rows, shift): + size = len(rows)//2 + for x in range(size): + real, imag = rows[2*x], rows[2*x+1] + row = [] + for j in range(size): + a, b = real.get(2*j, 0), imag.get(2*j, 0) + require(real.get(2*j+1, 0) == -b and imag.get(2*j+1, 0) == a, + 'complete complex-linear realification') + row.append([a << shift, b << shift]) + yield row + + +def row_record(result, common): + rows, count = result + require(common >= count, 'common normalization') + digest = hashlib.sha256() + energies = set() + for row in gaussian_rows(rows, common-count): + energies.add(sum(a*a+b*b for a, b in row)) + digest.update((canonical(row)+'\n').encode()) + require(energies == {4**common}, 'scaled row energy') + column_energies = [0]*len(rows) + for row in rows: + for j, x in row.items(): + column_energies[j] += x*x + require(set(column_energies) == {4**count}, 'scaled column energy') + return {'scaled_row_sha256': digest.hexdigest(), 'row_squared_energy': 4**common, + 'real_rows': len(rows), 'real_columns': len(rows), + 'nonzero_real_entries': sum(map(len, rows)), 'C_count': count} + + +def must_reject(operation, message): + try: + operation() + except ValueError as error: + require(message in str(error), 'wrong rejection reason: ' + str(error)) + else: + raise ValueError('unexpected acceptance: ' + message) + + +def fixed_sources(root=ROOT): + pins = read_json(HERE/'SOURCES.json') + for row in pins['files']: + if row['usage'] == 'input': + require(hashlib.sha256((root/row['path']).read_bytes()).hexdigest() == row['sha256'], + 'source drift: ' + row['path']) + external = pins['external_result'] + require(hashlib.sha256((HERE/external['local_path']).read_bytes()).hexdigest() == external['sha256'], + 'predecessor receipt drift') + return literals((root/EXACT).read_text(encoding='utf-8')), read_json(HERE/external['local_path']) + + +def bind_record(records, left_count, right_count, common, expected): + """Compare the scientific receipt fields after computing the full matrices.""" + for record in records: + require(record['scaled_row_sha256'] == expected['scaled_row_sha256'], 'predecessor row digest') + require(record['row_squared_energy'] == expected['row_squared_energy'], 'predecessor energy') + require([left_count, right_count] == [expected['C_left'], expected['C_right']], 'predecessor C counts') + require(expected['radix_bits'] == common+1 and expected['radius'] == 1 << common, + 'predecessor radix binding') + require(expected['largest_input_bits'] == 511*(common+1)+1, 'packed input length') + + +def run(root=ROOT): + circuits, predecessor = fixed_sources(root) + pairs = [] + for i in (1, 2, 3): + lhs, rhs = circuits['lhsLit'+str(i)], circuits['rhsLit'+str(i)] + left, right = matrix(lhs), matrix(rhs) + require(normalized_equal(left, right), 'normalized matrix equality') + common = max(left[1], right[1]) + records = [row_record(result, common) for result in (left, right)] + expected = predecessor['source']['pairs'][i-1] + bind_record(records, left[1], right[1], common, expected) + # Operator controls are semantic: no source hash stands in for rejection. + phase = matrix(rhs + [['ph', 1]]) + require(not normalized_equal(left, phase), 'phase defect accepted') + character = matrix([['dg', [0]*9, [2]+[0]*8]] + rhs) + require(not normalized_equal(left, character), 'input-character defect accepted') + require(not normalized_equal((left[0], 0), (right[0], 0)), 'omitted scale accepted') + # Harmless C C^-1 insertion changes the raw scale, but not the operator. + gauge = matrix(rhs + [['cg', 1, True], ['cg', 1, False]]) + require(normalized_equal(left, gauge), 'equivalent normalized presentation') + pairs.append({'pair': i, 'common_C': common, 'radix_bits': common+1, + 'sides': records, + 'controls': ['global_phase', 'input_character', 'omitted_normalization'], + 'positive_control': 'C_inverse_pair_with_changed_raw_scale'}) + return {'status': 'PASS_INDEPENDENT_HPE_ENERGY_AUDIT', + 'predecessor_head': '788848032c16bbe0a543c1186c6691c66131c090', + 'pairs': pairs, 'complex_rows_checked': 3072, + 'real_matrix_entries_covered': 6*1024*1024, + 'new_lean_proof': False, 'new_kappa': False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='Explicit receipt generation; default is read-only') + args = parser.parse_args() + if not args.write: + expected = read_json(HERE/'RESULT.json') # Missing evidence fails before computation. + 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(expected), 'audit receipt mismatch') + print(result['status'], 'complex_rows=3072 real_entries=6291456 no_new_kappa') + + +if __name__ == '__main__': + main()