[Lean] Prove unitary prefix bounds on the existing Lemma G semantics

.github/workflows/unitary-prefix-norm.yml

@@ -0,0 +1,43 @@
+name: Verify unitary prefix norm lemmas
+
+on:
+  pull_request:
+    paths:
+      - 'research/lean-unitary-prefix-norm/**'
+      - 'research/e8-lemma-g-lean/LemmaG/Stream.lean'
+      - 'research/e8-lemma-g-lean/PROOF.md'
+      - 'research/e8-lemma-g-lean/lake-manifest.json'
+      - 'research/e8-lemma-g-lean/lean-toolchain'
+      - 'research/hyperplane-end-lean/PROOF.md'
+      - '.github/workflows/unitary-prefix-norm.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  lean-prefix-norm:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
+        with:
+          python-version: '3.12'
+      - name: Check source bindings and guard tests
+        run: |
+          python3 -I -B research/lean-unitary-prefix-norm/verify.py --source-only
+          python3 -I -B research/lean-unitary-prefix-norm/test_verifier.py
+      - name: Install pinned elan bootstrap
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Build fresh proofs and audit all theorem axioms
+        run: |
+          python3 -I -B research/lean-unitary-prefix-norm/verify.py --work "$RUNNER_TEMP/unitary-prefix-norm"
+          cat "$RUNNER_TEMP/unitary-prefix-norm/AXIOMS.log"
+          git diff --exit-code

research/lean-unitary-prefix-norm/AXIOMS.json

@@ -0,0 +1,166 @@
+{
+  "PrefixNorm.Examples.asymmetric_preserves_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.backward_bits_if": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_endpoint": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_not_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.eight_not_norm_preserving": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.forward_bits_if": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_cancellation_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_prefix_bound": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.half_store_overshoot": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_endpoint": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.phases_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.recipe_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_not_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_bits": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_sq": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_uniform": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.inverse_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.recipesExact_take": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_bits": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_sq": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_uniform": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.supported_certificate": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.supported_prefix": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.weighted_prefix": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.weighted_row": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.wellLabelled_take": [
+    "Quot.sound",
+    "propext"
+  ]
+}

research/lean-unitary-prefix-norm/OVERLAP.json

@@ -0,0 +1,112 @@
+{
+  "schema_version": 1,
+  "status": "bounded overlap evidence, not a novelty certificate",
+  "base_commit": "bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c",
+  "refreshed_main": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "refresh_delta": "Only historical reconciliation92 evidence/ledger changes; selected record, guidance, catalogue and all five live proof inputs unchanged.",
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1291",
+  "entry": {
+    "searched_at": "2026-10-13T21:46:15.108970+00:00",
+    "terms": [
+      "prefix norm",
+      "signed prefix",
+      "unitary",
+      "formal interface"
+    ],
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-13T21:46:07.137936+00:00",
+        "complete_pagination": true,
+        "records": 860
+      },
+      "discussions": {
+        "fetched_at": "2026-10-13T21:46:15.079923+00:00",
+        "complete_pagination": true,
+        "records": 32
+      }
+    },
+    "local_records": 325,
+    "warnings": []
+  },
+  "pre_submission": {
+    "searched_at": "2026-10-13T22:18:53.601924+00:00",
+    "terms": [
+      "prefix norm",
+      "signed prefix",
+      "unitary",
+      "formal interface"
+    ],
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-13T22:18:44.696720+00:00",
+        "complete_pagination": true,
+        "records": 800
+      },
+      "discussions": {
+        "fetched_at": "2026-10-13T22:18:53.568634+00:00",
+        "complete_pagination": true,
+        "records": 51
+      }
+    },
+    "local_records": 327,
+    "warnings": []
+  },
+  "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.",
+  "nearest_work": [
+    {
+      "number": 1282,
+      "title": "Research audit: signed prefixes give 18/21-bit local bounds for selected PR1094",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1282",
+      "head": "851e5232f7c9e105fb6e8f3a7be7a070e7524012",
+      "updated_at": "2026-10-13T21:44:02Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Explicit predecessor and formalization handoff: written unitary norm argument plus selected finite row/Horner replay. This package formalizes the quantified implication on the existing Lean semantics and deliberately leaves the concrete row certificate external."
+    },
+    {
+      "number": 821,
+      "title": "Research audit: 286-to-160-bit prefix estimate for pinned #626 (no new kappa)",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/821",
+      "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8",
+      "updated_at": "2026-10-13T06:25:21Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Written replica-level norm estimate for historical PR626; different precision layer and no Lean prefix-norm theorem. Its retained local envelope is not recomputed here."
+    },
+    {
+      "number": 1086,
+      "title": "Formalize source-bound CK cleanup-prefix scalar reordering in Lean",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1086",
+      "head": "89a2dac3e8f84703110e00a231079c96fa4a9dd3",
+      "updated_at": "2026-10-13T17:51:15Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Lean scalar cleanup reordering with source-bound historical finite instance; no norm-preservation or component-store theorem."
+    },
+    {
+      "number": 1295,
+      "title": "Conditional precision audit: commuting intervals lower PR1054's rounded-word budget",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1295",
+      "head": "3a6773708f0d73f7dbee164f4c6e7658b0b41509",
+      "updated_at": "2026-10-13T21:55:39Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Concurrent conditional rounded dirty-word precision substitution using commuting intervals; different recursion and no proof-assistant formalization."
+    },
+    {
+      "number": 1294,
+      "title": "Independent verification: universal dirty phase identities with four explicit invariants",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1294",
+      "head": "03025ca1d51091a9525203000e77dacccfa6a70d",
+      "updated_at": "2026-10-13T21:52:52Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Concurrent universal noncommutative phase identities for the dirty-word interval argument; different algebraic obligations and explicitly not a proof-assistant formalization."
+    }
+  ],
+  "existing_formal_source": {
+    "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+    "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8",
+    "distinction": "Imports the original conjugation theorem and event semantics unchanged; adds normed-space and partial-store corollaries. HPE PROOF.md supplies orientation, not an additional imported Lean axiom."
+  }
+}