Audit: in-repo HPE checkers do not read the pre-wrapper recipe

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.

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

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

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

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()