State the phase-sharp pre-wrapper extension of factor_iff_pre.

research/hpe-pre-wrapper-phase/README.md

@@ -0,0 +1,108 @@
+# Phase-sharp pre-wrapper uniqueness
+
+**One interface lemma. No new κ, no supplier, no selected-frontier change.**
+
+`HyperplaneEnd/Labels.lean` proves `factor_iff_pre` only for scale `1`: if `(N)`
+holds and `C` is invertible, then
+
+```text
+L^{-1} T_U T_E^{-1} R'^{-1} = C ⊗ id    iff    R' = R.
+```
+
+The post-wrapper package `research/hpe-post-wrapper-lemma` states the matching
+phase-sharp fact for `L'` and explicitly does not claim the pre-side extension.
+This package states that extension and checks it.
+
+## Lemma
+
+Assume `(N)`, `T_U T_E^{-1} = L (C ⊗ id) R`, with `L`, `R'` and `C` invertible
+and `λ` a scalar. Then
+
+```text
+L^{-1} T_U T_E^{-1} R'^{-1} = λ (C ⊗ id)    iff    R' = λ^{-1} R.
+```
+
+In particular `λ = 1` is `factor_iff_pre`. For monomial wrappers the only scales
+are `λ ∈ {1, i, -1, -i}`, so the pre-wrapper phase field is the whole freedom:
+`R' = i^t R` satisfies the identity at `λ = i^{-t}` and at no other fourth root
+of unity.
+
+**Proof.** Substitute `(N)`. The left side is `(C ⊗ id) R R'^{-1}`. Invertibility
+of `C ⊗ id` forces `R R'^{-1} = λ I`, hence `R' = λ^{-1} R`. The converse is
+substitution. Equality is of linear maps, global phase included. ∎
+
+Invertibility of `C` is necessary. A rank-1 residual can satisfy the scaled
+equation for an `R'` that is not `λ^{-1} R`.
+
+## What was checked
+
+Equational replay over `Q(i)`, sizes 2 and 3, five scalars
+(`1, i, -1, -i, 2+i`): ten forward-and-converse replays, each with an
+invertible one-entry shift that must fail, plus one singular-`C` control.
+
+Exact `Z[i]` circuits, standard library only, on the three certified pairs in
+`HyperplaneEnd/Exact.lean`. Ports reproduce `lhsLit` / `rhsLit` and the
+monomial gate lists. For each pair the pre-wrapper is varied and the post
+wrapper stays the shipped `L`:
+
+| mutant | result |
+|---|---|
+| shipped `R`, and a dead low-triangle quadratic bit | holds only at `λ = 1` |
+| phase `+1`, `-1`, `+2` | holds only at `i^{-t}` |
+| offset xor, linear `Z/4` flip, live quadratic bit, `L` used as `R'` | fails all four roots of unity, with an exact `(row, column)` witness |
+| residual `C8 ⊗ id` | rejected for the shipped pre-wrapper |
+
+`--self-test` shifts the shipped pre-wrapper phase by one, keeps the port
+literals consistent with that shift, and requires the `λ = 1` clause to reject
+it. It holds at `i^3` instead.
+
+## Not claimed
+
+No Lean kernel proof. `Labels.lean` still has neither `factor_iff_post` nor a
+scalar on `factor_iff_pre`. No cold `(E = 0)` pair, no multi-gate tail, no
+`hrec` climb, unit row, footprint or whole-invocation discharge. No
+multiplication theorem and no κ. Selected κ stays `0.001672660197076918`.
+
+## Reproduce
+
+From the repository root, CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/hpe-pre-wrapper-phase
+```
+
+Expected first lines include `PASS_HPE_PRE_WRAPPER_PHASE` and
+`PASS_SELF_TEST`. Direct checks:
+
+```sh
+python3 -B research/hpe-pre-wrapper-phase/verify.py
+python3 -B research/hpe-pre-wrapper-phase/verify.py --self-test
+```
+
+## Open next questions
+
+Kernel-check the scalar pre-wrapper statement beside `factor_iff_pre`. That
+would put the phase freedom at the same trust level as the `λ = 1` theorem.
+First step: add the `λ` hypothesis to a successor of `Labels.lean` without
+editing the frozen file, and extend `PrintAxioms`. Blocked here by the absence
+of a Lean/Mathlib 4.21.0 toolchain.
+
+The same scalar statement for a cold `(E = 0)` literal is open. The three
+certified pairs are non-cold. First step: bind one cold `(N)` circuit with
+this verifier's gate semantics. Blocked because no cold literal pair is in
+`Exact.lean`.
+
+## Credit
+
+Jeremy Kothe (`jeremykothe2`) proved `factor_iff_pre` in
+[PR 593](https://github.com/CrocSwap/integer-mult-bounds/pull/593). The
+post-side phase-sharp lemma and its exact arithmetic are
+`research/hpe-post-wrapper-lemma` (Aaron Wang). The pre-side audit that left
+the arithmetic unrun is `research/hpe-prewrapper-binding`
+([PR 2706](https://github.com/CrocSwap/integer-mult-bounds/pull/2706), Riquelme
+Soares). Gate semantics follow the five kinds documented in
+`HyperplaneEnd/Clifford.lean`. This package adds the pre-side scalar extension
+and its checks.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review.

research/hpe-pre-wrapper-phase/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "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"
+    }
+  ]
+}

research/hpe-pre-wrapper-phase/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "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": "Phase-sharp pre-wrapper uniqueness extending factor_iff_pre from lambda 1 to an invertible scalar, bound to the three certified Exact.lean pairs",
+  "scope_change_reason": "The card asks for one scoped interface lemma. factor_iff_post is already stated in research/hpe-post-wrapper-lemma. This package takes the pre-side scalar extension that lemma explicitly does not claim, which is still the lambda=1 theorem in Labels.lean.",
+  "bottleneck_link": "A missing interface proof can narrow the conditional gap without changing kappa. factor_iff_pre fixes only the unscaled pre-wrapper; the phase field is the remaining monomial freedom on that side of (N).",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after this one pre-wrapper lemma, its equational replay and the three certified pairs. No second lemma, no Lean build, no supplier or kappa claim.",
+  "outcome": "completed",
+  "evidence": "Equational replay over Q(i) at sizes 2 and 3 for five scalars, with invertible failure shifts and one singular-C control. Exact Z[i] circuits on pair1-3: shipped and dead-bit pre-wrappers hold only at lambda 1; three phase shifts hold only at i^{-t}; four non-phase pre-wrappers miss all four roots of unity; C8 is rejected. Self-test rejects a phase-shifted shipped pre-wrapper as lambda 1.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok 4.7 assistance in the statement, verifier and write-up. No independent human review.",
+  "open_questions": [
+    {
+      "question": "Can the scalar pre-wrapper equivalence be kernel-checked beside factor_iff_pre?",
+      "why_it_matters": "Labels.lean still concludes only R' = R. A kernel proof would match the trust level of that theorem for the phase freedom.",
+      "first_step": "Add the lambda hypothesis in a successor of Labels.lean and extend PrintAxioms, without editing the frozen file.",
+      "blocked_by": "No Lean/Mathlib 4.21.0 toolchain in this environment."
+    },
+    {
+      "question": "Does the same scalar statement hold for one cold (E = 0) literal pair?",
+      "why_it_matters": "The three certified pairs are non-cold, so cold ends keep (N) and the wrapper scale as assumptions.",
+      "first_step": "Bind one cold (N) circuit with this package's gate semantics.",
+      "blocked_by": "Exact.lean has no cold literal pair."
+    }
+  ]
+}

research/hpe-pre-wrapper-phase/VERIFY.json

@@ -0,0 +1,31 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/hyperplane-end-lean/HyperplaneEnd/Exact.lean",
+    "research/hyperplane-end-lean/HyperplaneEnd/Labels.lean"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Equational replay of the phase-sharp pre-wrapper lemma and exact Z[i] binding on the three certified pairs, including phase, reject and width controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py",
+        "--self-test"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Failure control: a phase-shifted shipped pre-wrapper, with ports kept consistent, must fail the lambda=1 clause."
+    }
+  ]
+}