From 94d77d2cf19b5fbf3d14cd145fc5fd6ad8d24bd6 Mon Sep 17 00:00:00 2001 From: Riquelme Soares <104222380+hevlyo@users.noreply.github.com> Date: Thu, 15 Oct 2026 14:53:35 -0300 Subject: [PATCH] Show that the in-repo HPE checkers miss the pre-wrapper recipe. factor_iff_pre needs the executed recipe to equal the certified (E, U) monomial before hpe_word_exact can drop the factorization hypothesis. Both shipped checkers accept a synthetic word whose pre-wrapper records name the FULL key. --- research/hpe-prewrapper-binding/README.md | 76 +++++++++++ research/hpe-prewrapper-binding/SOURCES.json | 42 ++++++ research/hpe-prewrapper-binding/TASK.json | 60 +++++++++ research/hpe-prewrapper-binding/VERIFY.json | 23 ++++ research/hpe-prewrapper-binding/verify.py | 135 +++++++++++++++++++ 5 files changed, 336 insertions(+) create mode 100644 research/hpe-prewrapper-binding/README.md create mode 100644 research/hpe-prewrapper-binding/SOURCES.json create mode 100644 research/hpe-prewrapper-binding/TASK.json create mode 100644 research/hpe-prewrapper-binding/VERIFY.json create mode 100644 research/hpe-prewrapper-binding/verify.py diff --git a/research/hpe-prewrapper-binding/README.md b/research/hpe-prewrapper-binding/README.md new file mode 100644 index 0000000000..44f436edd9 --- /dev/null +++ b/research/hpe-prewrapper-binding/README.md @@ -0,0 +1,76 @@ +# The in-repo HPE checkers do not bind the pre-wrapper recipe + +**Interface audit; no new kappa.** `hpe_word_exact` concludes that a hyperplane-ended +helper stream ends as `C₇ ⊗ id` only after hypothesis `hrec`. That hypothesis +includes the existing fact `factor_iff_pre`: the pre-wrapper that ran must be +the `(E, U)` recipe, not a different recipe such as `(E, FULL)`. + +The two checkers that ship in this repository do not read that recipe. This +note states the missing boundary implication and gives a synthetic witness. +It does not reprove the Clifford identities. + +```sh +python3 -B research/hpe-prewrapper-binding/verify.py +``` + +Expected: + +```text +PASS_HPE_PREWRAPPER_BINDING full_recipe_accepted=true record_optional=true phase_rejected=true coefficient_rejected=true pairs=3 +``` + +Python 3.10+. No Lean build and no emitted HPE run. + +## The boundary lemma + +Let (N) hold for a certified pair (E, U): T_U T_E^{-1} = L (C_7 ⊗ id) R, with C_7 invertible. If the pre-wrapper that ran executed R'^{-1}, then L^{-1} T_U T_E^{-1} R'^{-1} = C_7 ⊗ id if and only if R' = R. A FULL recipe fails this equality when it differs from R. + +This is the statement already proved as `factor_iff_pre` in +`research/hyperplane-end-lean/HyperplaneEnd/Labels.lean`. `hpe_word_exact` in +`Exact.lean` still takes `hrec` after it discharges (N) for the three certified +pairs. The arithmetic is not repeated here. + +## What the checkers accept + +`scripts/verify_hpe_lean_binding.py` compares `RESIDUAL-ADAPTERS.json` monomials +with the three literal Lean pairs and rejects a changed phase. +`research/hyperplane-end-lean/code/check_hpe_pairs.py` checks tail shape, +frame dimensions, the wrapper-status string, and membership in those same +pairs. Neither function reads a pre-wrapper record. + +The witness is synthetic, not an emitted word. It has 38 tail gates, split +24/8/6 across the three Lean pairs, with matching adapter monomials and +`PASS_RESIDUAL_WRAPPERS_ARE_EXACT`. Every pre-wrapper record names `E:FULL`. +Both checkers accept it. Deleting the record also leaves both accepting. +Changing one adapter phase, or turning one gate into `h += p`, is rejected. +So the checkers do see monomials and the tail coefficient. They do not see +`R'`. + +Acceptance of those two checkers therefore does not prove `R' = R`, and does +not discharge `hrec` in `hpe_word_exact`. + +## Open next questions + +Where is the control `hpe_pre_wrapper_resolved_to_full_recipe` stored, and +does a shipped artifact show that the executed pre-wrapper was the `(E, U)` +recipe? That would supply the `hrec` conjunct this audit leaves open. The +first step is to search the retained HPE tool sources for that control and +the fifth wrapper field. It is blocked here because that replay is not in +this package, and this audit does not invent its result. + +## Credit and limits + +The Lean interface is Jeremy Kothe's, with the multi-gate extension retained +beside it. The two checkers are the existing maintainer and instance checks. +This package only separates their acceptance from `factor_iff_pre`. + +No selected certificate or kappa changes. The selected baseline was not rerun: +this sparse checkout does not contain `research/community-frontier1094-audit/ASSEMBLY.json`. +The selected record sha256 remains +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Footprints, well-labelled prefixes, the unit row, and the external wrapper +replay remain assumptions. All-size, hosting, precision and analytic assumptions +of the selected construction remain open. + +Prepared by Riquelme Soares (@hevlyo) with substantial AI assistance. +Apache-2.0. No independent human peer review is asserted. diff --git a/research/hpe-prewrapper-binding/SOURCES.json b/research/hpe-prewrapper-binding/SOURCES.json new file mode 100644 index 0000000000..4cbf94f6e9 --- /dev/null +++ b/research/hpe-prewrapper-binding/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "b5ea56e0a5ac4552166253b1fa4be0753bb38c30", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "usage": "input", + "git_blob": "1af33a206a9ba6c4826b3a1516d104e770380869", + "sha256": "eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183" + }, + { + "path": "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean", + "usage": "input", + "git_blob": "8315bdda8db4993ef713b24a01ce0e7c1837dff1", + "sha256": "febdc3f1734281178b043d714ab70b197d1c34d58ad15462386060b821b80e0c" + }, + { + "path": "research/hyperplane-end-lean/code/check_hpe_pairs.py", + "usage": "input", + "git_blob": "ec1c53f5e4788e2fa9e758eb82b09fca790c2a8c", + "sha256": "4acca21683503a41bf9c01f93f897dcaa8d455752dcec942a804f9e98aabb405" + }, + { + "path": "scripts/verify_hpe_lean_binding.py", + "usage": "input", + "git_blob": "d295b028edc531dfbfaa023370a9528bada35572", + "sha256": "52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03" + } + ] +} diff --git a/research/hpe-prewrapper-binding/TASK.json b/research/hpe-prewrapper-binding/TASK.json new file mode 100644 index 0000000000..cc79747926 --- /dev/null +++ b/research/hpe-prewrapper-binding/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 5, + "base_commit": "b5ea56e0a5ac4552166253b1fa4be0753bb38c30", + "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": "Does acceptance of the two in-repo HPE checkers supply R' = R, the pre-wrapper equality that factor_iff_pre requires before hpe_word_exact can drop (N)?", + "scope_change_reason": "The card allows one theorem-to-certificate binding. The object is the hrec conjunct of hpe_word_exact against scripts/verify_hpe_lean_binding.py and research/hyperplane-end-lean/code/check_hpe_pairs.py. It does not formalize new arithmetic.", + "bottleneck_link": "hpe_word_exact is an interface between the helper word and Lemma A. A checker that never reads the executed pre-wrapper does not close that interface, even though it does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the synthetic FULL-recipe witness and the two rejection controls. Do not rerun Lean, the external HPE replay, or a supplier.", + "outcome": "negative-result", + "evidence": "Both pinned checkers accept a 38-helper synthetic word whose pre-wrapper records name E:FULL, and still accept when that record is deleted. A phase flip and an h += p gate are rejected. factor_iff_pre and hpe_word_exact's hrec stay in the pinned Lean sources.", + "author": "Riquelme Soares (@hevlyo)", + "ai_assistance": "Substantial AI assistance in comparing the pinned checkers with factor_iff_pre, the synthetic witness, and the write-up. No proof assistant was used.", + "open_questions": [ + { + "question": "Where is hpe_pre_wrapper_resolved_to_full_recipe stored, and does a shipped artifact show that the executed pre-wrapper was the (E, U) recipe?", + "why_it_matters": "That control is the hrec conjunct this audit does not discharge.", + "first_step": "Search the retained HPE tool sources for that control and the fifth wrapper field.", + "blocked_by": "The external replay is not in this package. This audit does not invent its result." + } + ] +} diff --git a/research/hpe-prewrapper-binding/VERIFY.json b/research/hpe-prewrapper-binding/VERIFY.json new file mode 100644 index 0000000000..5db20292bc --- /dev/null +++ b/research/hpe-prewrapper-binding/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean", + "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean", + "research/hyperplane-end-lean/code/check_hpe_pairs.py", + "scripts/verify_hpe_lean_binding.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned Lean snippets, agreement of the two pair tables, FULL-recipe acceptance, optional pre-wrapper record, and rejection of a phase flip and h += p." + } + ] +} diff --git a/research/hpe-prewrapper-binding/verify.py b/research/hpe-prewrapper-binding/verify.py new file mode 100644 index 0000000000..baa1149bff --- /dev/null +++ b/research/hpe-prewrapper-binding/verify.py @@ -0,0 +1,135 @@ +#!/usr/bin/env python3 +"""The in-repo HPE checkers do not read the pre-wrapper recipe. + +Synthetic word only. This does not rerun Lean, the external HPE replay, or a supplier. +""" +import copy +import importlib.util +import inspect +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +BIND_PATH = ROOT / "scripts/verify_hpe_lean_binding.py" +INST_PATH = ROOT / "research/hyperplane-end-lean/code/check_hpe_pairs.py" +LABELS = ROOT / "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean" +EXACT = ROOT / "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean" + +LEMMA = ( + "Let (N) hold for a certified pair (E, U): " + "T_U T_E^{-1} = L (C_7 ⊗ id) R, with C_7 invertible. " + "If the pre-wrapper that ran executed R'^{-1}, then " + "L^{-1} T_U T_E^{-1} R'^{-1} = C_7 ⊗ id if and only if R' = R. " + "A FULL recipe fails this equality when it differs from R." +) + + +def require(ok, message): + if not ok: + raise SystemExit(message) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def fixture(pairs): + keys = list(pairs) + require(len(keys) == 3, "expected the three Lean pairs") + frames = [list(rows) for key in keys for rows in key] + slots = ((0, 1), (2, 3), (4, 5)) + counts = (24, 8, 6) + start = [0] * 200 + final = [0] * 200 + tail = [] + recipes = {} + recorded = [] + pre = [] + helper = 0 + for count, (entrance, terminal), key in zip(counts, slots, keys, strict=True): + recipes[f"{entrance}:{terminal}"] = { + "rank": 7, + "left": pairs[key]["left"], + "right": pairs[key]["right"], + } + recorded.append({"frame": entrance, "terminal": terminal, "residual_width": 7}) + for _ in range(count): + start[helper] = entrance + final[helper] = terminal + tail.append(["add", helper, 100 + helper, -1, 1, terminal]) + pre.append({"helper": helper, "recipe": f"{entrance}:FULL"}) + helper += 1 + word = { + "frames": frames, + "start": start, + "final": final, + "tail": tail, + "cleanup": [], + "pre_wrappers": pre, + } + wrap = { + "status": "PASS_RESIDUAL_WRAPPERS_ARE_EXACT", + "hyperplane_end_pairs": recorded, + } + return word, {"recipes": recipes}, wrap + + +def main(): + labels = LABELS.read_text(encoding="utf-8") + exact = EXACT.read_text(encoding="utf-8") + require("pre wrapper decoded against the FULL recipe" in labels, "factor_iff_pre text moved") + require("theorem factor_iff_pre" in labels, "missing factor_iff_pre") + require("(hrec : RecipesExact (Text T ent term Lw Rw) rec" in exact, "hpe_word_exact lost hrec") + require("The exact factorization is no longer a hypothesis" in exact, "hpe_word_exact text moved") + readme = (PACKAGE / "README.md").read_text(encoding="utf-8") + require(LEMMA in readme, "README dropped the boundary lemma") + + bind = load(BIND_PATH, "hpe_bind") + inst = load(INST_PATH, "hpe_inst") + require("pre_wrappers" not in inspect.getsource(bind.check), "binding checker now reads pre_wrappers") + require("pre_wrappers" not in inspect.getsource(inst.check), "instance checker now reads pre_wrappers") + pairs = bind.literal_pairs() + require(set(pairs) == inst.LEAN_PAIRS, "the two checkers disagree on the Lean pairs") + + word, adapters, wrap = fixture(pairs) + require({row["recipe"] for row in word["pre_wrappers"]} == {"0:FULL", "2:FULL", "4:FULL"}, + "fixture did not name FULL recipes") + violations, helpers, found = inst.check(word, wrap) + require(violations == [] and len(helpers) == 38 and len(found) == 3, "instance checker saw the FULL names") + bind.check(word, adapters, pairs) + + omitted = copy.deepcopy(word) + del omitted["pre_wrappers"] + violations, _, _ = inst.check(omitted, wrap) + require(violations == [], "instance checker requires a pre-wrapper record") + bind.check(omitted, adapters, pairs) + + phased = copy.deepcopy(adapters) + phased["recipes"]["0:1"]["left"]["phase"] ^= 1 + try: + bind.check(word, phased, pairs) + except ValueError as exc: + require("Emitted recipe differs from Lean: left" in str(exc), "unexpected phase failure") + else: + raise SystemExit("phase mutation accepted") + + flipped = copy.deepcopy(word) + flipped["tail"][0][3] = 1 + violations, _, _ = inst.check(flipped, wrap) + require(violations, "instance checker accepted h += p") + try: + bind.check(flipped, adapters, pairs) + except ValueError as exc: + require("Tail is not h -= p" in str(exc), "unexpected coefficient failure") + else: + raise SystemExit("binding checker accepted h += p") + + print("PASS_HPE_PREWRAPPER_BINDING full_recipe_accepted=true " + "record_optional=true phase_rejected=true coefficient_rejected=true pairs=3") + + +if __name__ == "__main__": + main()