From e05179c39a54b197b4a660d6949266bdeefaa2bc Mon Sep 17 00:00:00 2001
From: ywz65 <154373401+ywz65@users.noreply.github.com>
Date: Thu, 15 Oct 2026 11:34:22 -0700
Subject: [PATCH] Formalize split residual retractions and additive conjugation

---
 research/lean-split-residual/README.md        | 140 +++++++++++++
 research/lean-split-residual/RESULT.json      |   8 +
 research/lean-split-residual/SOURCES.json     |  24 +++
 .../lean-split-residual/SplitResidual.lean    | 119 +++++++++++
 research/lean-split-residual/TASK.json        |  83 ++++++++
 research/lean-split-residual/VERIFY.json      |  33 +++
 research/lean-split-residual/test_cli.py      |  48 +++++
 research/lean-split-residual/verify.py        | 192 ++++++++++++++++++
 8 files changed, 647 insertions(+)
 create mode 100644 research/lean-split-residual/README.md
 create mode 100644 research/lean-split-residual/RESULT.json
 create mode 100644 research/lean-split-residual/SOURCES.json
 create mode 100644 research/lean-split-residual/SplitResidual.lean
 create mode 100644 research/lean-split-residual/TASK.json
 create mode 100644 research/lean-split-residual/VERIFY.json
 create mode 100644 research/lean-split-residual/test_cli.py
 create mode 100644 research/lean-split-residual/verify.py

diff --git a/research/lean-split-residual/README.md b/research/lean-split-residual/README.md
new file mode 100644
index 0000000000..35df8f6f10
--- /dev/null
+++ b/research/lean-split-residual/README.md
@@ -0,0 +1,140 @@
+# Kernel-checked split residual interface for selected BIT
+
+Jose Manuel's [PR2195](https://github.com/CrocSwap/integer-mult-bounds/pull/2195)
+proves the selected BIT local-ring integration conditionally on completed
+callees. Section 1 supplies an explicit split-rank factorization instead of
+inferring rank from trace modulo the prime. This package kernel-checks that
+algebraic implication and its conjugation behavior. The mathematical
+factorization retains PR2195 credit; the contribution is the formal boundary,
+not a new supplier or exponent.
+
+## Exact proposition
+
+Let A and M be additive commutative groups, represented by Lean's IntModule
+class. Let B:A->M, V:M->A and C:M->M preserve zero, addition and negation.
+Assume V(B(a))=a for every a. Put P=BV and define
+
+    D(x,y) = (x-Px+P(Cy), C(Px)+y-C(P(Cy))),
+    F(z) = D(z)-z,
+    U(a) = (-B(a), C(B(a))),
+    W(x,y) = V(x)-V(C(y)),
+    L(x,y) = -V(x),     R(a) = (B(a),0).
+
+SplitResidual.lean proves F=UW, LU=id and WR=id. It also proves that the
+image of F is exactly the image of U, and U is injective. Every residual
+image element therefore has a unique A coordinate. P is idempotent.
+With the additional hypothesis C(C(x))=x, D is involutory.
+
+For an invertible additive change of coordinates T, the formalized
+residual-conjugation identity is
+
+    T D T^-1 - id = T (D-id) T^-1.
+
+Transformed factors TU and WT^-1 have retractions LT^-1 and TR. This
+includes weight/chart changes once their additive bijections are supplied.
+No orthogonality or transpose-as-inverse assumption is used. The factorization
+and retractions do not require C^2=id; only D-involution uses that premise.
+No field, characteristic, trace or diagonalizability hypothesis enters the proof.
+
+## Formal/source correspondence
+
+| Lean roots | Exact meaning and assumptions |
+|---|---|
+| map_sub, factorization | Distribute the explicit additive maps through the residual |
+| left_inverse, right_inverse | The displayed retractions, using VB=id |
+| projection_idempotent | P=BV is idempotent |
+| image_iff, lifted_injective | Residual image is a uniquely coordinatized copy of A |
+| involution | D^2=id, additionally using C^2=id |
+| conjugate_factorization, conjugate_left_inverse, conjugate_right_inverse | Factorization and retractions survive an explicit two-sided bijection |
+| conjugate_residual | Actual conjugated operation minus identity equals conjugated residual, requiring subtraction preservation |
+| integer_example, integer_split_example | Concrete signed-swap instance over integers |
+
+For the source matrices take A=R^r and M=R^m over R=Z/q^w, B,V from the
+split image/kernel basis, and C the reversal. Source section 1 states VB=I
+and F=[-B;CB][V,-VC]. The formal formula is precisely this block formula
+evaluated on a pair, not a renamed conclusion supplied as a hypothesis.
+
+**Remaining external obligations:** construction and authentication of concrete
+B,V,C; their module instances and scalar linearity; the determinant-unit lift
+from residue-field bases; and a formal dimension/rank theorem. The kernel
+proves retractions and image correspondence, not a library assertion
+rank(F)=r. Mathematically, R-linear B,V,C and A=R^r identify the residual
+image with that free module. Finite fixtures corroborate this specialization
+without binding every selected frame in Lean.
+
+The selected word, profile, completed callees, physical hosting, row allocation,
+tape/precision and outer analytic transfer remain separate. Their assumptions
+are unchanged.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+    python3.12 scripts/research_package.py --package research/lean-split-residual
+    python3.12 -I -O -B research/lean-split-residual/verify.py --lean /absolute/path/to/lean
+
+Use Lean 4.34.1. The explicit --lean command recompiles all source in a fresh
+temporary directory with warnings treated as errors, then queries all fourteen
+roots and rejects axioms outside propext, Classical.choice and Quot.sound.
+It never accepts a saved compiler log as evidence. Four material theorem
+mutations must fail compilation. A genuinely compiled declaration depending
+on an injected axiom must be rejected by the audit.
+
+The registered Python hook runs finite fixtures and export controls.
+**It does not run Lean automatically.** The explicit live command was run
+during development on Windows with Lean 4.34.1 and CPython 3.12.14.
+RESULT.json binds the Lean source SHA-256, also reported by live verification.
+
+Default verification is read-only; --write explicitly replaces RESULT.json.
+Git-free exports need this package and the declared PROOF.md input at their
+repository-relative paths. The generic runner additionally audits historical
+task/source provenance.
+
+## Evidence and controls
+
+The 252 exact modular matrix cases cover m=1..6, every positive r<=m,
+three basis charts, primes 3/5 and widths 1/2. They check VB=I, P^2=P,
+F=UW, LU=I, WR=I, D^2=I, residue ranks and conjugated identities.
+**42 cases have positive rank but zero trace modulo the prime.**
+Unit-pivot inversion and separate residue-field elimination use exact integers.
+
+Five controls cover a missing lift sign, absent retraction premise,
+transpose-as-inverse, absent C-involution premise, and the rank-zero boundary.
+The last is a positive identity boundary, not a rejected counterexample.
+The four live Lean mutations change/remove the lift sign, VB hypothesis,
+right section and C^2 hypothesis. Git-free CLI tests reject source and
+Lean-byte corruption and Boolean/float receipt substitutions, and verify
+read-only success. All Python checks remain active under -O.
+
+The source's 636 frames and 531 residuals are not rerun here. These small-ring
+controls do not replace its geometry checks. No selected cold replay, hosted
+CI, human review, Mathlib matrix theorem or full multiplication theorem is claimed.
+
+## Provenance and overlap
+
+Scientific base 21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7, priority 5;
+picker nonce dba52022fd62ead90880b092efd7d755. The prescribed binding baseline
+passed. SOURCES.json pins the exact retained source proof, catalogue and
+selected record. Original PR2195 head:
+3a1cf78a1ba6322129e42d80c50d21765524d612, Jose Manuel (jmbarrancoml).
+
+The card was narrowed to this boundary after reading the already formal HPE
+wrapper/label proofs. Local Lean and merged notes, open PRs and targeted
+REST queries showed no exact existing kernel treatment. TASK.json records
+coverage limits, including the stale Discussion snapshot; no search proves
+novelty or exhausts diffs. Claim: PR2195 comment 6199233287.
+
+Retain PR2195's credits to alephnan PR1627, eumemic PR490/source527,
+DreamingOfClouds PR589 and the selected construction lineage. The small live
+axiom-audit pattern follows our PR2618 verifier; no new audit framework is
+claimed. Prepared for ywz65 with substantial OpenAI Codex assistance.
+Apache-2.0.
+
+## Open next questions
+
+1. Bind one actual selected rank-divisible-by-prime frame to the kernel.
+   Begin with finite-ring B,V,C literals and VB=I; concrete representation
+   and authenticated translation remain missing.
+2. Connect the image correspondence to a free-module dimension API and
+   formalize the determinant-unit basis lift. The rank-library bridge
+   remains external to the present proof.
diff --git a/research/lean-split-residual/RESULT.json b/research/lean-split-residual/RESULT.json
new file mode 100644
index 0000000000..ec4fa8115b
--- /dev/null
+++ b/research/lean-split-residual/RESULT.json
@@ -0,0 +1,8 @@
+{
+  "status": "PASS_SPLIT_RESIDUAL_CONTROLS",
+  "formal_sha256": "bb1beefee02cdf17004df49ffa75fe043e9057b896e21b9074b28e26b0d60177",
+  "ring_cases": 252,
+  "positive_trace_zero_cases": 42,
+  "conjugated_cases": 252,
+  "controls": 5
+}
diff --git a/research/lean-split-residual/SOURCES.json b/research/lean-split-residual/SOURCES.json
new file mode 100644
index 0000000000..920775f32d
--- /dev/null
+++ b/research/lean-split-residual/SOURCES.json
@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7",
+  "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/selected-bit-local-ring-sweeps/PROOF.md",
+      "usage": "input",
+      "git_blob": "4330de85dd9862ed15d84ab917887d249753df99",
+      "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7"
+    }
+  ]
+}
diff --git a/research/lean-split-residual/SplitResidual.lean b/research/lean-split-residual/SplitResidual.lean
new file mode 100644
index 0000000000..5aa90554a5
--- /dev/null
+++ b/research/lean-split-residual/SplitResidual.lean
@@ -0,0 +1,119 @@
+import Std
+set_option maxHeartbeats 4000000
+namespace SplitResidual
+open Lean.Grind
+variable {A M : Type} [IntModule A] [IntModule M]
+
+structure AddMap (X Y : Type) [IntModule X] [IntModule Y] where
+  apply : X → Y
+  zero : apply 0 = 0
+  add : ∀ x y, apply (x+y) = apply x + apply y
+  neg : ∀ x, apply (-x) = -apply x
+
+theorem map_sub (f : AddMap A M) (x y : A) :
+    f.apply (x-y) = f.apply x - f.apply y := by
+  simp only [AddCommGroup.sub_eq_add_neg, f.add, f.neg]
+
+def proj (B : AddMap A M) (V : AddMap M A) (x : M) := B.apply (V.apply x)
+def lifted (B : AddMap A M) (C : AddMap M M) (a : A) : M × M :=
+  (-B.apply a, C.apply (B.apply a))
+def lowered (V : AddMap M A) (C : AddMap M M) (z : M × M) : A :=
+  V.apply z.1 - V.apply (C.apply z.2)
+def undoLift (V : AddMap M A) (z : M × M) : A := -V.apply z.1
+def embed (B : AddMap A M) (a : A) : M × M := (B.apply a, 0)
+def d (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) : M × M :=
+  (z.1 - proj B V z.1 + proj B V (C.apply z.2),
+   C.apply (proj B V z.1) + z.2 - C.apply (proj B V (C.apply z.2)))
+def residual (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) : M × M :=
+  ((d B V C z).1-z.1, (d B V C z).2-z.2)
+
+theorem factorization (B : AddMap A M) (V : AddMap M A) (C : AddMap M M) (z : M × M) :
+    residual B V C z = lifted B C (lowered V C z) := by
+  apply Prod.ext
+  · simp only [residual,d,proj,lifted,lowered,map_sub]
+    grind
+  · simp only [residual,d,proj,lifted,lowered,map_sub]
+    grind
+
+theorem left_inverse (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (a : A) :
+    undoLift V (lifted B C a) = a := by
+  simp only [undoLift,lifted,V.neg,hVB]
+  grind
+
+theorem right_inverse (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (a : A) :
+    lowered V C (embed B a) = a := by
+  simp only [lowered,embed,C.zero,V.zero,hVB]
+  grind
+
+theorem projection_idempotent (B : AddMap A M) (V : AddMap M A)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (x : M) :
+    proj B V (proj B V x) = proj B V x := by
+  simp only [proj,hVB]
+
+theorem image_iff (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) (z : M × M) :
+    (∃ x, residual B V C x = z) ↔ (∃ a, lifted B C a = z) := by
+  constructor
+  · rintro ⟨x,hx⟩
+    exact ⟨lowered V C x, (factorization B V C x).symm.trans hx⟩
+  · rintro ⟨a,ha⟩
+    refine ⟨embed B a, ?_⟩
+    rw [factorization,right_inverse B V C hVB,ha]
+
+theorem lifted_injective (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a) {a b : A}
+    (h : lifted B C a = lifted B C b) : a = b := by
+  have h' := congrArg (undoLift V) h
+  simpa only [left_inverse B V C hVB] using h'
+theorem involution (B : AddMap A M) (V : AddMap M A) (C : AddMap M M)
+    (hVB : ∀ a, V.apply (B.apply a) = a)
+    (hCC : ∀ x, C.apply (C.apply x) = x) (z : M × M) :
+    d B V C (d B V C z) = z := by
+  apply Prod.ext <;>
+    simp only [d,proj,map_sub,B.add,V.add,C.add,hVB,hCC] <;> grind
+
+structure Bijection (X : Type) where
+  forward : X → X
+  backward : X → X
+  back_forward : ∀ x, backward (forward x) = x
+  forward_back : ∀ x, forward (backward x) = x
+
+theorem conjugate_factorization {X Y : Type} (F : X → X) (U : Y → X)
+    (W : X → Y) (h : ∀ x, F x = U (W x)) (T : Bijection X) (x : X) :
+    T.forward (F (T.backward x)) = T.forward (U (W (T.backward x))) := by
+  rw [h]
+
+theorem conjugate_left_inverse {X Y : Type} (U : Y → X) (L : X → Y)
+    (h : ∀ y, L (U y) = y) (T : Bijection X) (y : Y) :
+    L (T.backward (T.forward (U y))) = y := by
+  rw [T.back_forward,h]
+
+theorem conjugate_right_inverse {X Y : Type} (W : X → Y) (R : Y → X)
+    (h : ∀ y, W (R y) = y) (T : Bijection X) (y : Y) :
+    W (T.backward (T.forward (R y))) = y := by
+  rw [T.back_forward,h]
+
+theorem conjugate_residual {X : Type} [IntModule X] (F : X → X)
+    (T : Bijection X) (hsub : ∀ x y, T.forward (x-y) = T.forward x - T.forward y)
+    (x : X) :
+    T.forward (F (T.backward x)) - x =
+      T.forward (F (T.backward x) - T.backward x) := by
+  rw [hsub,T.forward_back]
+
+def intIdentity : AddMap Int Int := ⟨id, rfl, by intros; rfl, by intros; rfl⟩
+def intNegative : AddMap Int Int := ⟨fun x => -x, by decide,
+  by intros; grind, by intros; rfl⟩
+
+theorem integer_example (x y : Int) :
+    d intIdentity intIdentity intNegative (x,y) = (-y,-x) := by
+  apply Prod.ext <;> simp only [d,proj,intIdentity,intNegative,id] <;> grind
+
+theorem integer_split_example (a : Int) :
+    undoLift intIdentity (lifted intIdentity intNegative a) = a ∧
+    lowered intIdentity intNegative (embed intIdentity a) = a := by
+  constructor
+  · exact left_inverse intIdentity intIdentity intNegative (fun _ => rfl) a
+  · exact right_inverse intIdentity intIdentity intNegative (fun _ => rfl) a
+end SplitResidual
diff --git a/research/lean-split-residual/TASK.json b/research/lean-split-residual/TASK.json
new file mode 100644
index 0000000000..e5233be205
--- /dev/null
+++ b/research/lean-split-residual/TASK.json
@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 5,
+  "base_commit": "21ec98bfd2e9f27810a8718d95d9b5d19a5df7d7",
+  "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": "Kernel-check PR2195 section1's split residual factorization, explicit retractions and image correspondence, involution, and additive conjugation invariance.",
+  "scope_change_reason": "HPE wrappers already have proofs; the newer selected BIT local-ring argument states this split residual bridge only in prose and finite checks. The factorization remains credited, not a new mathematical theorem.",
+  "bottleneck_link": "Makes the ring-safe width argument inspectable without trace-as-rank, retaining concrete free-basis construction and supplier cost as external obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Formalize this factorization interface, run live kernel/axiom/mutation controls and exact ring fixtures, then stop.",
+  "outcome": "completed",
+  "evidence": "SplitResidual.lean, README.md, RESULT.json, verify.py --lean live audit and test_cli.py Git-free controls.",
+  "author": "ywz65",
+  "ai_assistance": "Substantial OpenAI Codex assistance in formalization, testing, source and overlap analysis, and writing.",
+  "open_questions": [
+    {
+      "question": "Can selected finite image/kernel bases become kernel-checked instances of these retractions?",
+      "why_it_matters": "The abstract proof does not authenticate or construct the selected 636 frame bases.",
+      "first_step": "Bind one rank-divisible-by-prime frame's B,V,C and verify VB=I in a concrete finite-ring module.",
+      "blocked_by": "A concrete representation and source-to-kernel translation."
+    },
+    {
+      "question": "Can the free-module rank conclusion and lifted local-ring basis construction be formalized?",
+      "why_it_matters": "This proves retractions and image correspondence, not a library dimension theorem.",
+      "first_step": "Connect lifted_injective and image_iff to a free-module dimension API.",
+      "blocked_by": "A compatible algebra library and formal invertibility of the chosen image/kernel basis."
+    }
+  ],
+  "nonce": "dba52022fd62ead90880b092efd7d755",
+  "source_credit": {
+    "pr": 2195,
+    "head": "3a1cf78a1ba6322129e42d80c50d21765524d612",
+    "author": "Jose Manuel (jmbarrancoml)",
+    "path": "research/selected-bit-local-ring-sweeps/PROOF.md",
+    "section": "1"
+  },
+  "overlap": {
+    "open_prs": "767 records, complete snapshot 2026-10-15T18:06:42Z",
+    "discussions": "1239 records, complete snapshot 2026-10-15T15:22:22Z; stale at submission",
+    "additional": "Local Lean/source/merged-note search and targeted REST 2195/Lean, split-rank/Lean and residual-factorization/Lean queries; no exhaustive code-diff search."
+  },
+  "upstream_checkpoint": {
+    "commit": "ab4fcd39c74effa88d464ed1d80ec832f6020e51",
+    "guidance": "unchanged; fast-forwarded before publication; scientific pins21ec98 retained"
+  }
+}
diff --git a/research/lean-split-residual/VERIFY.json b/research/lean-split-residual/VERIFY.json
new file mode 100644
index 0000000000..d4b7904d9c
--- /dev/null
+++ b/research/lean-split-residual/VERIFY.json
@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/selected-bit-local-ring-sweeps/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticated source/formal bytes and 252 exact local-ring factorization/retraction/conjugation fixtures including 42 positive ranks with zero residue trace. Does not run Lean; explicit --lean documented."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/test_cli.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Git-free read-only replay, source corruption, typed receipts and formal-source drift."
+    }
+  ]
+}
diff --git a/research/lean-split-residual/test_cli.py b/research/lean-split-residual/test_cli.py
new file mode 100644
index 0000000000..2f64328bff
--- /dev/null
+++ b/research/lean-split-residual/test_cli.py
@@ -0,0 +1,48 @@
+"""Read-only minimal-export checks for the public finite verifier."""
+import hashlib,json,shutil,subprocess,sys,tempfile,unittest
+from pathlib import Path
+P=Path(__file__).resolve().parent
+R=P.parent.parent
+
+class CliTests(unittest.TestCase):
+    def setUp(self):
+        self.tmp=tempfile.TemporaryDirectory(prefix="split-residual-export-")
+        self.root=Path(self.tmp.name);self.package=self.root/P.relative_to(R)
+        shutil.copytree(P,self.package)
+        for item in json.loads((P/"SOURCES.json").read_bytes())["files"]:
+            if item["usage"]=="input":
+                dest=self.root/item["path"];dest.parent.mkdir(parents=True,exist_ok=True)
+                shutil.copyfile(R/item["path"],dest)
+        self.addCleanup(self.tmp.cleanup)
+    def call(self):
+        return subprocess.run([sys.executable,"-I","-O","-B",str(self.package/"verify.py")],
+                              cwd=self.root,text=True,capture_output=True,timeout=60)
+    def inventory(self):
+        return {str(x.relative_to(self.root)):hashlib.sha256(x.read_bytes()).hexdigest()
+                for x in self.root.rglob("*") if x.is_file()}
+    def test_readonly_export(self):
+        before=self.inventory();result=self.call()
+        self.assertEqual(result.returncode,0,result.stderr)
+        self.assertEqual(self.inventory(),before)
+        self.assertIn("PASS_SPLIT_RESIDUAL_CONTROLS",result.stdout)
+    def test_changed_source(self):
+        source=self.root/"research/selected-bit-local-ring-sweeps/PROOF.md"
+        source.write_bytes(source.read_bytes()+b"\nchanged\n")
+        result=self.call()
+        self.assertNotEqual(result.returncode,0)
+        self.assertIn("source hash mismatch",result.stderr)
+    def test_typed_receipt(self):
+        path=self.package/"RESULT.json";original=json.loads(path.read_bytes())
+        for bad in (True,float(original["ring_cases"])):
+            path.write_text(json.dumps(dict(original,ring_cases=bad)),encoding="utf-8")
+            result=self.call()
+            self.assertNotEqual(result.returncode,0)
+            self.assertIn("receipt mismatch",result.stderr)
+    def test_changed_formal_bytes(self):
+        source=self.package/"SplitResidual.lean"
+        source.write_bytes(source.read_bytes()+b"\n-- changed\n")
+        result=self.call()
+        self.assertNotEqual(result.returncode,0)
+        self.assertIn("receipt mismatch",result.stderr)
+
+if __name__=="__main__":unittest.main()
diff --git a/research/lean-split-residual/verify.py b/research/lean-split-residual/verify.py
new file mode 100644
index 0000000000..fa63edfe3e
--- /dev/null
+++ b/research/lean-split-residual/verify.py
@@ -0,0 +1,192 @@
+"""Finite ring controls; --lean additionally recompiles and audits the live kernel proof."""
+import argparse,hashlib,json,os,re,shutil,subprocess,tempfile
+from pathlib import Path
+P=Path(__file__).resolve().parent
+R=P.parent.parent
+ROOTS=("map_sub","factorization","left_inverse","right_inverse","projection_idempotent",
+       "image_iff","lifted_injective","involution","conjugate_factorization",
+       "conjugate_left_inverse","conjugate_right_inverse","conjugate_residual",
+       "integer_example","integer_split_example")
+
+def need(ok,message):
+    if not ok:raise ValueError(message)
+def canonical(x):return json.dumps(x,sort_keys=True,separators=(",",":"),allow_nan=False)
+def sha(x):return hashlib.sha256(x).hexdigest()
+def sources():
+    for item in json.loads((P/"SOURCES.json").read_bytes())["files"]:
+        if item["usage"]=="input":
+            raw=(R/item["path"]).read_bytes()
+            need(sha(raw)==item["sha256"],"source hash mismatch")
+            need(hashlib.sha1(b"blob "+str(len(raw)).encode()+b"\0"+raw).hexdigest()==item["git_blob"],"source blob mismatch")
+
+def ident(n):return [[int(i==j) for j in range(n)] for i in range(n)]
+def transpose(a):return [list(x) for x in zip(*a)]
+def add(a,b,q):return [[(x+y)%q for x,y in zip(ar,br)] for ar,br in zip(a,b)]
+def neg(a,q):return [[-x%q for x in row] for row in a]
+def sub(a,b,q):return add(a,neg(b,q),q)
+def mul(a,b,q):
+    return [[sum(x*y for x,y in zip(row,col))%q for col in zip(*b)] for row in a]
+def block(a,b,c,d):return [x+y for x,y in zip(a,b)]+[x+y for x,y in zip(c,d)]
+
+def inverse(a,q):
+    n=len(a);t=[row[:]+ir for row,ir in zip(a,ident(n))]
+    import math
+    for j in range(n):
+        pivot=next((i for i in range(j,n) if math.gcd(t[i][j],q)==1),None)
+        need(pivot is not None,"nonunit matrix pivot")
+        t[j],t[pivot]=t[pivot],t[j]
+        u=pow(t[j][j],-1,q);t[j]=[x*u%q for x in t[j]]
+        for i in range(n):
+            if i!=j:
+                c=t[i][j];t[i]=[(x-c*y)%q for x,y in zip(t[i],t[j])]
+    need([row[:n] for row in t]==ident(n),"inverse elimination")
+    return [row[n:] for row in t]
+
+def chart(n,q,variant):
+    a=ident(n)
+    if n>1:
+        for k in range(2*n+variant):
+            i=k%n;j=(i+1+(variant%(n-1)))%n
+            if i==j:j=(i+1)%n
+            a[i]=[(x+(k+1)*y)%q for x,y in zip(a[i],a[j])]
+        a=a[1:]+a[:1]
+    a[0]=[2*x%q for x in a[0]]
+    return a
+
+def rank_mod(a,p):
+    t=[[x%p for x in row] for row in a];r=0
+    for j in range(len(t[0])):
+        pivot=next((i for i in range(r,len(t)) if t[i][j]),None)
+        if pivot is None:continue
+        t[r],t[pivot]=t[pivot],t[r]
+        u=pow(t[r][j],-1,p);t[r]=[x*u%p for x in t[r]]
+        for i in range(len(t)):
+            if i!=r:
+                c=t[i][j];t[i]=[(x-c*y)%p for x,y in zip(t[i],t[r])]
+        r+=1
+    return r
+
+def finite():
+    sources()
+    counts=dict(ring_cases=0,positive_trace_zero_cases=0,conjugated_cases=0,controls=0)
+    for p in (3,5):
+        for w in (1,2):
+            q=p**w
+            for n in range(1,7):
+                c=[row[::-1] for row in ident(n)]
+                for r in range(1,n+1): # rank zero is separately an identity control
+                    for variant in range(3):
+                        t=chart(n,q,variant);ti=inverse(t,q)
+                        b=[row[:r] for row in t];v=ti[:r]
+                        pr=mul(b,v,q)
+                        need(mul(v,b,q)==ident(r),"basis retraction")
+                        need(mul(pr,pr,q)==pr,"projector premise")
+                        pc=mul(pr,c,q);cp=mul(c,pr,q)
+                        d=block(sub(ident(n),pr,q),pc,cp,sub(ident(n),mul(cp,c,q),q))
+                        u=neg(b,q)+mul(c,b,q)
+                        ww=[a+z for a,z in zip(v,neg(mul(v,c,q),q))]
+                        ll=[a+[0]*n for a in neg(v,q)]
+                        rr=b+[[0]*r for _ in range(n)]
+                        f=sub(d,ident(2*n),q)
+                        need(mul(u,ww,q)==f,"residual factorization")
+                        need(mul(ll,u,q)==ident(r),"left retraction")
+                        need(mul(ww,rr,q)==ident(r),"right retraction")
+                        need(mul(d,d,q)==ident(2*n),"address involution")
+                        need(rank_mod(f,p)==r,"residual residue rank")
+                        need(rank_mod(pr,p)==r,"projector residue rank")
+                        if r%p==0:
+                            need(sum(pr[i][i] for i in range(n))%p==0,"trace-zero fixture")
+                            counts["positive_trace_zero_cases"]+=1
+                        s=chart(2*n,q,variant);si=inverse(s,q)
+                        dc=mul(mul(s,d,q),si,q)
+                        uc=mul(s,u,q);wc=mul(ww,si,q)
+                        lc=mul(ll,si,q);rc=mul(s,rr,q)
+                        need(mul(uc,wc,q)==sub(dc,ident(2*n),q),"conjugated residual")
+                        need(mul(lc,uc,q)==ident(r) and mul(wc,rc,q)==ident(r),"conjugated retractions")
+                        counts["ring_cases"]+=1;counts["conjugated_cases"]+=1
+    q=9;b=[[1],[0]];v=[[1,0]];c=[[0,1],[1,0]]
+    u=neg(b,q)+mul(c,b,q);ww=[v[0]+neg(mul(v,c,q),q)[0]]
+    ll=[[-1%q,0,0,0]]
+    need(mul(ll,b+mul(c,b,q),q)!=[[1]],"missing negative sign not exposed")
+    counts["controls"]+=1
+    badv=[[3,0]]
+    need(mul(badv,b,q)!=[[1]],"missing VB identity not exposed")
+    counts["controls"]+=1
+    s=chart(4,q,2);si=inverse(s,q)
+    need(mul(s,transpose(s),q)!=ident(4),"transpose alias fixture")
+    need(mul(mul(ll,transpose(s),q),mul(s,u,q),q)!=[[1]],"transpose-as-inverse not exposed")
+    counts["controls"]+=1
+    badc=[[2,0],[0,2]]
+    need(mul(badc,badc,q)!=ident(2),"C involution fixture")
+    bad_d=block([[0,0],[0,0]],badc,badc,[[0,0],[0,0]])
+    need(mul(bad_d,bad_d,q)!=ident(4),"missing C involution not exposed")
+    counts["controls"]+=1
+    need(sub(ident(4),ident(4),q)==[[0]*4 for _ in range(4)],"rank-zero residual")
+    counts["controls"]+=1
+    return {"status":"PASS_SPLIT_RESIDUAL_CONTROLS","formal_sha256":sha((P/"SplitResidual.lean").read_bytes()),**counts}
+
+def audit(output):
+    expected={"SplitResidual."+n for n in ROOTS}
+    pattern=re.compile(r"^'([^']+)' (?:depends on axioms:\s*\[([^]]*)\]|does not depend on any axioms)\s*$",re.M)
+    found={}
+    for m in pattern.finditer(output):
+        name,body=m.groups()
+        need(name in expected and name not in found,"unexpected/duplicate axiom root")
+        axioms=[] if body is None else [x.strip() for x in body.split(",")]
+        need(set(axioms)<={"propext","Classical.choice","Quot.sound"},"forbidden axiom")
+        found[name]=sorted(axioms)
+    need(set(found)==expected,"missing axiom roots")
+    need(not pattern.sub("",output).strip(),"unexpected audit output")
+    return found
+
+def live_lean(executable):
+    lean=shutil.which(executable);need(lean,"Lean unavailable")
+    version=subprocess.check_output([lean,"--version"],text=True,encoding="utf-8").strip()
+    need("version 4.34.1" in version,"tested compiler is Lean4.34.1")
+    formal=(P/"SplitResidual.lean").read_bytes()
+    with tempfile.TemporaryDirectory(prefix="split-residual-") as temp:
+        directory=Path(temp);env=os.environ.copy();env["LEAN_PATH"]=str(directory)
+        def run(name,compile=False):
+            cmd=[lean,"-j1","-DwarningAsError=true",name]
+            if compile:cmd+=["-o",name.replace(".lean",".olean")]
+            return subprocess.run(cmd,cwd=directory,env=env,text=True,encoding="utf-8",capture_output=True,timeout=120)
+        (directory/"SplitResidual.lean").write_bytes(formal)
+        result=run("SplitResidual.lean",True)
+        need(result.returncode==0,"kernel compilation failed\n"+result.stdout+result.stderr)
+        query="import SplitResidual\n"+"".join("#print axioms SplitResidual."+n+"\n" for n in ROOTS)
+        (directory/"Audit.lean").write_bytes(query.encode())
+        result=run("Audit.lean")
+        need(result.returncode==0 and not result.stderr.strip(),"axiom command failed")
+        axioms=audit(result.stdout)
+        mutations=(
+          ("wrong_lift_sign","(-B.apply a, C.apply (B.apply a))","(B.apply a, C.apply (B.apply a))"),
+          ("omit_retraction","(hVB : ∀ a, V.apply (B.apply a) = a)","(hVB : True)"),
+          ("wrong_right_section","(B.apply a, 0)","(0, B.apply a)"),
+          ("omit_involution","(hCC : ∀ x, C.apply (C.apply x) = x)","(hCC : True)"))
+        for name,old,new in mutations:
+            need(old.encode() in formal,"mutation missing")
+            (directory/"Mutation.lean").write_bytes(formal.replace(old.encode(),new.encode(),1))
+            result=run("Mutation.lean")
+            need(result.returncode!=0 and "error" in result.stdout.lower(),"mutated theorem accepted: "+name)
+        bad="import Std\naxiom injected : False\n"
+        bad+="theorem SplitResidual."+ROOTS[0]+" : False := injected\n"
+        bad+="".join("theorem SplitResidual."+n+" : True := by trivial\n" for n in ROOTS[1:])
+        bad+="".join("#print axioms SplitResidual."+n+"\n" for n in ROOTS)
+        (directory/"BadAudit.lean").write_bytes(bad.encode());result=run("BadAudit.lean")
+        need(result.returncode==0,"axiom rejection control failed to compile")
+        try:audit(result.stdout)
+        except ValueError:pass
+        else:raise ValueError("forbidden axiom accepted")
+    return {"version":version,"roots":len(ROOTS),"axioms":axioms,"rejected_mutations":[m[0] for m in mutations],"formal_sha256":sha(formal)}
+
+def main():
+    parser=argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--write",action="store_true")
+    parser.add_argument("--lean")
+    args=parser.parse_args()
+    result=finite()
+    if args.write:(P/"RESULT.json").write_text(json.dumps(result,indent=2)+"\n",encoding="utf-8",newline="\n")
+    else:need(canonical(result)==canonical(json.loads((P/"RESULT.json").read_bytes())),"receipt mismatch")
+    if args.lean:print("PASS_LIVE_LEAN "+canonical(live_lean(args.lean)))
+    print(canonical(result))
+if __name__=="__main__":main()