From f93f31135be05165903a20cd80685cfd3e7f8a0b Mon Sep 17 00:00:00 2001
From: ywz65 <154373401+ywz65@users.noreply.github.com>
Date: Thu, 15 Oct 2026 08:38:09 -0700
Subject: [PATCH 1/2] Formalize four-channel factorization to C5 pivot bridge

---
 .../Algebra.lean                              |  64 +++++++++
 .../LEAN-CHECK.json                           |  68 +++++++++
 .../paired-plane-four-channel-lean/Pivot.lean | 103 ++++++++++++++
 .../paired-plane-four-channel-lean/README.md  | 105 ++++++++++++++
 .../SOURCES.json                              |  29 ++++
 .../paired-plane-four-channel-lean/Schur.lean | 134 ++++++++++++++++++
 .../paired-plane-four-channel-lean/TASK.json  |  99 +++++++++++++
 .../VERIFY.json                               |  20 +++
 .../check_lean.py                             |  96 +++++++++++++
 .../paired-plane-four-channel-lean/verify.py  |  58 ++++++++
 10 files changed, 776 insertions(+)
 create mode 100644 research/paired-plane-four-channel-lean/Algebra.lean
 create mode 100644 research/paired-plane-four-channel-lean/LEAN-CHECK.json
 create mode 100644 research/paired-plane-four-channel-lean/Pivot.lean
 create mode 100644 research/paired-plane-four-channel-lean/README.md
 create mode 100644 research/paired-plane-four-channel-lean/SOURCES.json
 create mode 100644 research/paired-plane-four-channel-lean/Schur.lean
 create mode 100644 research/paired-plane-four-channel-lean/TASK.json
 create mode 100644 research/paired-plane-four-channel-lean/VERIFY.json
 create mode 100644 research/paired-plane-four-channel-lean/check_lean.py
 create mode 100644 research/paired-plane-four-channel-lean/verify.py

diff --git a/research/paired-plane-four-channel-lean/Algebra.lean b/research/paired-plane-four-channel-lean/Algebra.lean
new file mode 100644
index 0000000000..28cc01e705
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/Algebra.lean
@@ -0,0 +1,64 @@
+import Std
+set_option maxRecDepth 100000
+set_option maxHeartbeats 40000000
+namespace Four
+open Lean.Grind
+structure M (K : Type) where
+  e00 : K
+  e01 : K
+  e02 : K
+  e03 : K
+  e10 : K
+  e11 : K
+  e12 : K
+  e13 : K
+  e20 : K
+  e21 : K
+  e22 : K
+  e23 : K
+  e30 : K
+  e31 : K
+  e32 : K
+  e33 : K
+variable {K : Type} [CommRing K]
+def mul (a b : M K) : M K := ⟨a.e00*b.e00+a.e01*b.e10+a.e02*b.e20+a.e03*b.e30, a.e00*b.e01+a.e01*b.e11+a.e02*b.e21+a.e03*b.e31, a.e00*b.e02+a.e01*b.e12+a.e02*b.e22+a.e03*b.e32, a.e00*b.e03+a.e01*b.e13+a.e02*b.e23+a.e03*b.e33, a.e10*b.e00+a.e11*b.e10+a.e12*b.e20+a.e13*b.e30, a.e10*b.e01+a.e11*b.e11+a.e12*b.e21+a.e13*b.e31, a.e10*b.e02+a.e11*b.e12+a.e12*b.e22+a.e13*b.e32, a.e10*b.e03+a.e11*b.e13+a.e12*b.e23+a.e13*b.e33, a.e20*b.e00+a.e21*b.e10+a.e22*b.e20+a.e23*b.e30, a.e20*b.e01+a.e21*b.e11+a.e22*b.e21+a.e23*b.e31, a.e20*b.e02+a.e21*b.e12+a.e22*b.e22+a.e23*b.e32, a.e20*b.e03+a.e21*b.e13+a.e22*b.e23+a.e23*b.e33, a.e30*b.e00+a.e31*b.e10+a.e32*b.e20+a.e33*b.e30, a.e30*b.e01+a.e31*b.e11+a.e32*b.e21+a.e33*b.e31, a.e30*b.e02+a.e31*b.e12+a.e32*b.e22+a.e33*b.e32, a.e30*b.e03+a.e31*b.e13+a.e32*b.e23+a.e33*b.e33⟩
+def one : M K := ⟨1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1⟩
+def scale (c : K) (a : M K) : M K := ⟨c*a.e00, c*a.e01, c*a.e02, c*a.e03, c*a.e10, c*a.e11, c*a.e12, c*a.e13, c*a.e20, c*a.e21, c*a.e22, c*a.e23, c*a.e30, c*a.e31, c*a.e32, c*a.e33⟩
+def det (a : M K) : K := a.e00*a.e11*a.e22*a.e33 - a.e00*a.e11*a.e23*a.e32 - a.e00*a.e12*a.e21*a.e33 + a.e00*a.e12*a.e23*a.e31 + a.e00*a.e13*a.e21*a.e32 - a.e00*a.e13*a.e22*a.e31 - a.e01*a.e10*a.e22*a.e33 + a.e01*a.e10*a.e23*a.e32 + a.e01*a.e12*a.e20*a.e33 - a.e01*a.e12*a.e23*a.e30 - a.e01*a.e13*a.e20*a.e32 + a.e01*a.e13*a.e22*a.e30 + a.e02*a.e10*a.e21*a.e33 - a.e02*a.e10*a.e23*a.e31 - a.e02*a.e11*a.e20*a.e33 + a.e02*a.e11*a.e23*a.e30 + a.e02*a.e13*a.e20*a.e31 - a.e02*a.e13*a.e21*a.e30 - a.e03*a.e10*a.e21*a.e32 + a.e03*a.e10*a.e22*a.e31 + a.e03*a.e11*a.e20*a.e32 - a.e03*a.e11*a.e22*a.e30 - a.e03*a.e12*a.e20*a.e31 + a.e03*a.e12*a.e21*a.e30
+def adj (a : M K) : M K := ⟨(a.e11*a.e22*a.e33 - a.e11*a.e23*a.e32 - a.e12*a.e21*a.e33 + a.e12*a.e23*a.e31 + a.e13*a.e21*a.e32 - a.e13*a.e22*a.e31), -(a.e01*a.e22*a.e33 - a.e01*a.e23*a.e32 - a.e02*a.e21*a.e33 + a.e02*a.e23*a.e31 + a.e03*a.e21*a.e32 - a.e03*a.e22*a.e31), (a.e01*a.e12*a.e33 - a.e01*a.e13*a.e32 - a.e02*a.e11*a.e33 + a.e02*a.e13*a.e31 + a.e03*a.e11*a.e32 - a.e03*a.e12*a.e31), -(a.e01*a.e12*a.e23 - a.e01*a.e13*a.e22 - a.e02*a.e11*a.e23 + a.e02*a.e13*a.e21 + a.e03*a.e11*a.e22 - a.e03*a.e12*a.e21), -(a.e10*a.e22*a.e33 - a.e10*a.e23*a.e32 - a.e12*a.e20*a.e33 + a.e12*a.e23*a.e30 + a.e13*a.e20*a.e32 - a.e13*a.e22*a.e30), (a.e00*a.e22*a.e33 - a.e00*a.e23*a.e32 - a.e02*a.e20*a.e33 + a.e02*a.e23*a.e30 + a.e03*a.e20*a.e32 - a.e03*a.e22*a.e30), -(a.e00*a.e12*a.e33 - a.e00*a.e13*a.e32 - a.e02*a.e10*a.e33 + a.e02*a.e13*a.e30 + a.e03*a.e10*a.e32 - a.e03*a.e12*a.e30), (a.e00*a.e12*a.e23 - a.e00*a.e13*a.e22 - a.e02*a.e10*a.e23 + a.e02*a.e13*a.e20 + a.e03*a.e10*a.e22 - a.e03*a.e12*a.e20), (a.e10*a.e21*a.e33 - a.e10*a.e23*a.e31 - a.e11*a.e20*a.e33 + a.e11*a.e23*a.e30 + a.e13*a.e20*a.e31 - a.e13*a.e21*a.e30), -(a.e00*a.e21*a.e33 - a.e00*a.e23*a.e31 - a.e01*a.e20*a.e33 + a.e01*a.e23*a.e30 + a.e03*a.e20*a.e31 - a.e03*a.e21*a.e30), (a.e00*a.e11*a.e33 - a.e00*a.e13*a.e31 - a.e01*a.e10*a.e33 + a.e01*a.e13*a.e30 + a.e03*a.e10*a.e31 - a.e03*a.e11*a.e30), -(a.e00*a.e11*a.e23 - a.e00*a.e13*a.e21 - a.e01*a.e10*a.e23 + a.e01*a.e13*a.e20 + a.e03*a.e10*a.e21 - a.e03*a.e11*a.e20), -(a.e10*a.e21*a.e32 - a.e10*a.e22*a.e31 - a.e11*a.e20*a.e32 + a.e11*a.e22*a.e30 + a.e12*a.e20*a.e31 - a.e12*a.e21*a.e30), (a.e00*a.e21*a.e32 - a.e00*a.e22*a.e31 - a.e01*a.e20*a.e32 + a.e01*a.e22*a.e30 + a.e02*a.e20*a.e31 - a.e02*a.e21*a.e30), -(a.e00*a.e11*a.e32 - a.e00*a.e12*a.e31 - a.e01*a.e10*a.e32 + a.e01*a.e12*a.e30 + a.e02*a.e10*a.e31 - a.e02*a.e11*a.e30), (a.e00*a.e11*a.e22 - a.e00*a.e12*a.e21 - a.e01*a.e10*a.e22 + a.e01*a.e12*a.e20 + a.e02*a.e10*a.e21 - a.e02*a.e11*a.e20)⟩
+theorem mul_assoc (a b c : M K) : mul (mul a b) c = mul a (mul b c) := by
+  cases a; cases b; cases c
+  simp only [mul, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem mul_one (a : M K) : mul a one = a := by
+  cases a
+  simp only [mul, one, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem one_mul (a : M K) : mul one a = a := by
+  cases a
+  simp only [mul, one, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem scale_mul (t : K) (a b : M K) : mul (scale t a) b = scale t (mul a b) := by
+  cases a; cases b
+  simp only [mul, scale, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem scale_scale (t u : K) (a : M K) : scale t (scale u a) = scale (t*u) a := by
+  cases a
+  simp only [scale, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem scale_one (a : M K) : scale 1 a = a := by
+  cases a
+  simp only [scale, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem adj_left (a : M K) : mul (adj a) a = scale (det a) one := by
+  cases a
+  simp only [adj, mul, det, scale, one, M.mk.injEq]
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> grind
+theorem det_one : det (one : M K) = 1 := by simp only [det, one]; grind
+theorem det_mul (a b : M K) : det (mul a b) = det a * det b := by
+  cases a; cases b
+  simp only [det, mul]
+  grind
+end Four
+#print axioms Four.det_mul
+#print axioms Four.adj_left
diff --git a/research/paired-plane-four-channel-lean/LEAN-CHECK.json b/research/paired-plane-four-channel-lean/LEAN-CHECK.json
new file mode 100644
index 0000000000..bd9a568601
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/LEAN-CHECK.json
@@ -0,0 +1,68 @@
+{
+  "status": "PASS_FOUR_CHANNEL_LEAN",
+  "version": "Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
+  "source_sha256": {
+    "Algebra.lean": "d908ace095ef1d025d4a1fed5009e00b6c489ed96654ea5ddaa700b3cc543724",
+    "Schur.lean": "0e714c6f64ac8895080959babb8595ba7bdb391e43a2cee6be51d81690f56db0",
+    "Pivot.lean": "0899c8021cdf7d2aed120ad36fc1f20ad59ff30f2db45d20eae17f711bfbd2fc"
+  },
+  "theorem_axioms": {
+    "Four.det_mul": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "Four.adj_left": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "PairedC5.reverse_inverse": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "PairedC5.no_four_pivot": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "PairedC5.relaxed_diagonal": [
+      "propext"
+    ],
+    "PairedC5.relaxed_remaining_zeros": [
+      "propext"
+    ],
+    "PairedC5.relaxed_four_pivot": [
+      "propext"
+    ],
+    "PairedC5.relaxed_missing_edge": [
+      "propext"
+    ],
+    "Four.reverse_inverse": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "Pivot.factor_to_pivot": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "Pivot.no_four_channels": [
+      "Classical.choice",
+      "Quot.sound",
+      "propext"
+    ],
+    "Pivot.relaxed_through_four": [
+      "propext"
+    ]
+  },
+  "rejected_mutations": [
+    "reverse_inverse_wrong_conclusion",
+    "pivot_nonzero_cross_block",
+    "remove_ring_nontriviality",
+    "relaxed_factor_zero_channels"
+  ],
+  "scope": "Four-channel factorization implies normalized pivot; no strict C5 fitting factorization. Ordinary rank and selected-mask embedding remain external."
+}
diff --git a/research/paired-plane-four-channel-lean/Pivot.lean b/research/paired-plane-four-channel-lean/Pivot.lean
new file mode 100644
index 0000000000..66f7a4d6b3
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/Pivot.lean
@@ -0,0 +1,103 @@
+import Algebra
+import Schur
+
+namespace Four
+open Lean.Grind
+variable {K : Type} [CommRing K]
+
+theorem reverse_inverse (a b : M K) (h : mul a b = one) : mul b a = one := by
+  have hu : det b * det a = 1 := by
+    have hd := congrArg det h
+    rw [det_mul, det_one] at hd
+    grind
+  have hs : scale (det a) b = adj a := by
+    calc
+      scale (det a) b = mul (scale (det a) one) b := by rw [scale_mul, one_mul]
+      _ = mul (mul (adj a) a) b := by rw [adj_left]
+      _ = mul (adj a) (mul a b) := mul_assoc _ _ _
+      _ = adj a := by rw [h, mul_one]
+  have hb : b = scale (det b) (adj a) := by
+    calc
+      b = scale (det b * det a) b := by rw [hu, scale_one]
+      _ = scale (det b) (scale (det a) b) := (scale_scale _ _ _).symm
+      _ = scale (det b) (adj a) := by rw [hs]
+  calc
+    mul b a = mul (scale (det b) (adj a)) a := by rw [← hb]
+    _ = scale (det b) (mul (adj a) a) := scale_mul _ _ _
+    _ = scale (det b) (scale (det a) one) := by rw [adj_left]
+    _ = one := by rw [scale_scale, hu, scale_one]
+
+theorem sandwich (x q p y : M K) (h : mul q p = one) :
+    mul (mul x q) (mul p y) = mul x y := by
+  calc
+    mul (mul x q) (mul p y) = mul x (mul q (mul p y)) := mul_assoc _ _ _
+    _ = mul x (mul (mul q p) y) := by rw [mul_assoc]
+    _ = mul x y := by rw [h, one_mul]
+end Four
+
+namespace Pivot
+open Lean.Grind
+open PairedC5
+variable {K : Type} [CommRing K]
+
+def blocks (a b c d : Mat2 K) : Four.M K :=
+  ⟨a.a, a.b, b.a, b.b, a.c, a.d, b.c, b.d,
+   c.a, c.b, d.a, d.b, c.c, c.d, d.c, d.d⟩
+def upper (a : Four.M K) : Mat2 K := ⟨a.e00,a.e01,a.e10,a.e11⟩
+
+omit [CommRing K] in
+@[simp] theorem upper_blocks (a b c d : Mat2 K) : upper (blocks a b c d) = a := by
+  cases a; rfl
+
+theorem blocks_mul (a b c d e f g h : Mat2 K) :
+    Four.mul (blocks a b c d) (blocks e f g h) =
+      blocks (add (mul a e) (mul b g)) (add (mul a f) (mul b h))
+             (add (mul c e) (mul d g)) (add (mul c f) (mul d h)) := by
+  cases a; cases b; cases c; cases d; cases e; cases f; cases g; cases h
+  simp only [Four.mul, blocks, mul, add, Four.M.mk.injEq]
+  refine ⟨?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_,?_⟩ <;> grind
+
+def ThroughFour (m : BlockMatrix K) (u v : Fin 5 → Fin 2 → Mat2 K) : Prop :=
+  ∀ i j, m i j = add (mul (u i 0) (v j 0)) (mul (u i 1) (v j 1))
+
+theorem factor_to_pivot (m : BlockMatrix K) (u v : Fin 5 → Fin 2 → Mat2 K)
+    (hf : ThroughFour m u v)
+    (h00 : m 0 0 = one) (h22 : m 2 2 = one)
+    (h02 : m 0 2 = zero) (h20 : m 2 0 = zero) : FourPivot m := by
+  let p := blocks (u 0 0) (u 0 1) (u 2 0) (u 2 1)
+  let q := blocks (v 0 0) (v 2 0) (v 0 1) (v 2 1)
+  have hpq : Four.mul p q = Four.one := by
+    dsimp [p,q]
+    rw [blocks_mul, ← hf 0 0, ← hf 0 2, ← hf 2 0, ← hf 2 2]
+    rw [h00,h02,h20,h22]
+    rfl
+  have hqp := Four.reverse_inverse p q hpq
+  intro i j
+  have hx := Four.sandwich (blocks (u i 0) (u i 1) zero zero)
+      q p (blocks (v j 0) zero (v j 1) zero) hqp
+  dsimp [p,q] at hx
+  rw [blocks_mul, blocks_mul, blocks_mul, blocks_mul] at hx
+  have he := congrArg upper hx
+  simp only [upper_blocks, mul_zero, zero_mul, add_zero] at he
+  rw [← hf i 0, ← hf i 2, ← hf 0 j, ← hf 2 j, ← hf i j] at he
+  exact he.symm
+
+theorem no_four_channels (hne : (0 : K) ≠ 1) (m : BlockMatrix K)
+    (u v : Fin 5 → Fin 2 → Mat2 K) (hfit : Fits m) (hf : ThroughFour m u v) : False := by
+  have hz02 : m 0 2 = zero := hfit.2 0 2 (by unfold Far; decide)
+  have hz20 : m 2 0 = zero := hfit.2 2 0 (by unfold Far; decide)
+  exact no_four_pivot hne m hfit (factor_to_pivot m u v hf (hfit.1 0) (hfit.1 2) hz02 hz20)
+
+/-- Four explicit scalar channels do realize the predecessor's one-edge-relaxed mask. -/
+def relaxedFactor (i : Fin 5) (k : Fin 2) : Mat2 Int :=
+  if (group i && k.val == 0) || (!group i && k.val == 1) then one else zero
+
+theorem relaxed_through_four : ThroughFour relaxed relaxedFactor relaxedFactor := by
+  unfold ThroughFour
+  decide
+end Pivot
+
+#print axioms Four.reverse_inverse
+#print axioms Pivot.factor_to_pivot
+#print axioms Pivot.no_four_channels
+#print axioms Pivot.relaxed_through_four
diff --git a/research/paired-plane-four-channel-lean/README.md b/research/paired-plane-four-channel-lean/README.md
new file mode 100644
index 0000000000..1ec5f68230
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/README.md
@@ -0,0 +1,105 @@
+# Four scalar channels imply the normalized C5 pivot equation
+
+This package closes the **factorization-to-pivot** gap left explicit in
+[PR2525](https://github.com/CrocSwap/integer-mult-bounds/pull/2525).
+For a nontrivial commutative coefficient ring, a five-by-five matrix of
+two-by-two blocks with identity diagonal and the C5 forbidden zeros cannot
+factor through four scalar channels. The coefficients and free blocks may be
+asymmetric. The result is checked by Lean 4.34.1 using only its standard
+axioms; no Mathlib installation is required.
+
+It does not formalize the library statement that ordinary field rank at most
+four supplies such a factorization, the source JSON interpretation, or the
+full rank49 theorem. These remain separate interfaces. There is no new rank
+optimum, physical COPY bill, supplier or exponent claim.
+
+## Formal statement and proof boundary
+
+`Pivot.ThroughFour m u v` states the literal factorization
+
+```text
+m[i,j] = u[i,0] v[j,0] + u[i,1] v[j,1],
+```
+
+where each entry is a two-by-two scalar matrix. Thus `u` and `v` are a general
+10-by-4 and 4-by-10 factorization, with no restriction to diagonal or commuting
+blocks. `Pivot.factor_to_pivot` assumes only this factorization and
+`m[0,0]=m[2,2]=I_2`, `m[0,2]=m[2,0]=0`. It derives
+
+```text
+m[i,j] = m[i,0] m[0,j] + m[i,2] m[2,j].
+```
+
+The proof stacks the selected factor rows into `p` and columns into `q`.
+The four pivot equations give `pq=I_4`. `Four.reverse_inverse` derives
+`qp=I_4` over a commutative ring by determinant and adjugate identities.
+Associativity then gives the displayed normalized equation. `Algebra.lean`
+proves the required four-by-four scalar polynomial identities; scalar
+commutativity is used there, not commutativity of two-by-two blocks.
+
+`Pivot.no_four_channels` applies the unchanged predecessor
+`PairedC5.no_four_pivot`. Its hypothesis is now an arbitrary four-channel
+factorization, rather than the normalized pivot equation itself.
+`Pivot.relaxed_through_four` gives explicit integer factors for the
+predecessor's one-edge-relaxed example. Its only forbidden pair violations
+are the B-D pair documented in PR2525, so the full zero pattern matters.
+
+The mathematical rank consequence over a field follows externally from the
+usual rank-factorization theorem (padding with zero channels if necessary).
+The new Lean theorem does not use that library theorem and does not redefine
+ordinary matrix rank as `ThroughFour`.
+
+## Reproduce
+
+From the repository root, with Lean4.34.1 and Python3.10+:
+
+```sh
+python3 -I -B research/paired-plane-four-channel-lean/check_lean.py --lean /path/to/lean
+python3.12 scripts/research_package.py --package research/paired-plane-four-channel-lean
+```
+
+The first command performs a fresh isolated module build, prints all twelve
+theorem axiom inventories, and rejects four actual altered Lean programs:
+wrong reverse-inverse conclusion, a nonzero pivot cross block, omitted ring
+nontriviality, and a broken relaxed factor. The polynomial build may take
+several minutes; its bound is900 seconds, with120 seconds for each later
+module or mutation. Temporary compiled modules are not used as submitted
+evidence. `--out NEW_FILE` saves a receipt and refuses an existing path.
+
+The registered Python replay checks the **recorded** Lean receipt against the
+three exact source files and unchanged predecessor bytes, then rejects four
+receipt/source corruptions. It does not invoke Lean. `LEAN-CHECK.json` records
+the actual local kernel run; it is not a hosted-CI claim. The positive relaxed
+factor is also kernel checked. Separate AI review checked factor orientation,
+ring hypotheses and the remaining rank boundary; no human review is claimed.
+
+## Sources and credit
+
+`Schur.lean` is byte-for-byte PR2525 at
+`ed86bcbe8f728e5412a6ef8f1910bac38f073f51`, with Git blob and SHA256 in
+`SOURCES.json`. That work (ywz65 with OpenAI Codex assistance) formalized the
+normalized C5 obstruction and externally bound it to the selected mask.
+PR2484 by thakrarsagar supplied the scalar minrank49 construction and C5/I44
+certificate; Cinna Davis supplied the paired-plane matching and Adam Gall
+the scalar permission contract. This package claims only the missing formal
+factorization normalization, not priority for those results. PR2541's
+all-block-size written rank theorem is complementary and already covers the
+mathematical rank bound more generally.
+
+The picker assigned `complex-rank-shape-decoder`, priority revision4, nonce
+`5daa35e3a3b51d84040a502049bb18ef`. The prescribed ceiling replay and lever
+screen passed as orientation. The scope is explicitly **changed**: this is
+a formal lower-bound interface handoff, not a new per-call profile clearing
+the card's5% gate. Exact card, base, overlap, claim and next questions are in
+`TASK.json`. Prepared for ywz65 with substantial OpenAI Codex assistance in
+proof construction, checking and writing. Apache-2.0.
+
+## Open next questions
+
+Connect a maintained field matrix-rank definition to `ThroughFour` with exact
+row and column indexing, then formally embed the source-bound C5 and isolated
+I44 block. That would close the remaining ordinary-rank and source-interface
+gaps for the fixed scalar instance. The first step is a rank-factorization
+adapter; the blocker here is the absence of a matrix-rank library and formal
+source parser, not a missing normalized-pivot hypothesis. No native cost
+conclusion follows from closing those formal interfaces alone.
diff --git a/research/paired-plane-four-channel-lean/SOURCES.json b/research/paired-plane-four-channel-lean/SOURCES.json
new file mode 100644
index 0000000000..0a5fc25931
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/SOURCES.json
@@ -0,0 +1,29 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 2525,
+      "head": "ed86bcbe8f728e5412a6ef8f1910bac38f073f51",
+      "path": "research/paired-plane-c5-schur-lean/Schur.lean",
+      "local_file": "Schur.lean",
+      "sha256": "0e714c6f64ac8895080959babb8595ba7bdb391e43a2cee6be51d81690f56db0",
+      "git_blob": "569563457a25517e38f3c0e96864dc222b97c75e",
+      "credit": "ywz65 with OpenAI Codex assistance; Apache-2.0; unchanged normalized C5 obstruction and relaxed witness."
+    }
+  ]
+}
diff --git a/research/paired-plane-four-channel-lean/Schur.lean b/research/paired-plane-four-channel-lean/Schur.lean
new file mode 100644
index 0000000000..569563457a
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/Schur.lean
@@ -0,0 +1,134 @@
+/- Apache-2.0. Prepared for ywz65 with substantial OpenAI Codex assistance.
+   Formal Schur interface from thakrarsagar/PR2484's C5 proof.
+   This file does not define matrix rank or formalize the rank-to-pivot bridge. -/
+import Std
+
+namespace PairedC5
+open Lean.Grind
+
+structure Mat2 (K : Type) where
+  a : K
+  b : K
+  c : K
+  d : K
+  deriving DecidableEq
+
+variable {K : Type} [CommRing K]
+
+def mul (x y : Mat2 K) : Mat2 K :=
+  ⟨x.a*y.a+x.b*y.c, x.a*y.b+x.b*y.d,
+   x.c*y.a+x.d*y.c, x.c*y.b+x.d*y.d⟩
+def one : Mat2 K := ⟨1,0,0,1⟩
+def zero : Mat2 K := ⟨0,0,0,0⟩
+def add (x y : Mat2 K) : Mat2 K := ⟨x.a+y.a,x.b+y.b,x.c+y.c,x.d+y.d⟩
+
+theorem mul_assoc (x y z : Mat2 K) : mul (mul x y) z = mul x (mul y z) := by
+  cases x; cases y; cases z
+  simp only [mul, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem mul_one (x : Mat2 K) : mul x one = x := by
+  cases x
+  simp only [mul, one, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem one_mul (x : Mat2 K) : mul one x = x := by
+  cases x
+  simp only [mul, one, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem mul_zero (x : Mat2 K) : mul x zero = zero := by
+  cases x
+  simp only [mul, zero, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem zero_mul (x : Mat2 K) : mul zero x = zero := by
+  cases x
+  simp only [mul, zero, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem add_zero (x : Mat2 K) : add x zero = x := by
+  cases x
+  simp only [add, zero, Mat2.mk.injEq]
+  grind
+
+@[simp] theorem zero_add (x : Mat2 K) : add zero x = x := by
+  cases x
+  simp only [add, zero, Mat2.mk.injEq]
+  grind
+
+/-- The square-block step cannot be replaced by rectangular one-sided inversion. -/
+theorem reverse_inverse (x y : Mat2 K) (h : mul x y = one) : mul y x = one := by
+  cases x; cases y
+  simp only [mul, one, Mat2.mk.injEq] at h ⊢
+  grind
+
+theorem cancel_right_zero (x y z : Mat2 K)
+    (hinv : mul x y = one) (hzero : mul z y = zero) : z = zero := by
+  have rev := reverse_inverse x y hinv
+  calc
+    z = mul z (mul y x) := by rw [rev, mul_one]
+    _ = mul (mul z y) x := (mul_assoc z y x).symm
+    _ = zero := by rw [hzero, zero_mul]
+
+abbrev BlockMatrix (K : Type) := Fin 5 → Fin 5 → Mat2 K
+
+/-- Non-neighbouring planes of the orthogonality C5 have forced zero blocks. -/
+def Far (i j : Fin 5) : Prop := (i.val+2)%5 = j.val ∨ (j.val+2)%5 = i.val
+
+def Fits (m : BlockMatrix K) : Prop :=
+  (∀ i, m i i = one) ∧ (∀ i j, Far i j → m i j = zero)
+
+/-- Schur factorization through the four scalar pivot ports in planes 0 and 2. -/
+def FourPivot (m : BlockMatrix K) : Prop :=
+  ∀ i j, m i j = add (mul (m i 0) (m 0 j)) (mul (m i 2) (m 2 j))
+
+/-- Exact formalized proposition: no fitting C5 matrix has the normalized
+    four-pivot factorization. Ordinary matrix rank is not a hypothesis here. -/
+theorem no_four_pivot (hne : (0 : K) ≠ 1) (m : BlockMatrix K)
+    (hfit : Fits m) (hf : FourPivot m) : False := by
+  rcases hfit with ⟨hd, hz⟩
+  have h30 : m 3 0 = zero := hz 3 0 (by unfold Far; decide)
+  have h03 : m 0 3 = zero := hz 0 3 (by unfold Far; decide)
+  have h42 : m 4 2 = zero := hz 4 2 (by unfold Far; decide)
+  have h24 : m 2 4 = zero := hz 2 4 (by unfold Far; decide)
+  have h13 : m 1 3 = zero := hz 1 3 (by unfold Far; decide)
+  have h14 : m 1 4 = zero := hz 1 4 (by unfold Far; decide)
+  have d : mul (m 3 2) (m 2 3) = one := by
+    simpa [h30, hd 3] using (hf 3 3).symm
+  have e : mul (m 4 0) (m 0 4) = one := by
+    simpa [h42, hd 4] using (hf 4 4).symm
+  have bd : mul (m 1 2) (m 2 3) = zero := by
+    simpa [h13, h03] using (hf 1 3).symm
+  have be : mul (m 1 0) (m 0 4) = zero := by
+    simpa [h14, h24] using (hf 1 4).symm
+  have bc : m 1 2 = zero := cancel_right_zero _ _ _ d bd
+  have ba : m 1 0 = zero := cancel_right_zero _ _ _ e be
+  have contradiction : (one : Mat2 K) = zero := by
+    simpa [hd 1, ba, bc] using hf 1 1
+  have scalar : (1 : K) = 0 := congrArg Mat2.a contradiction
+  exact hne scalar.symm
+
+/-- Concrete integer witness after freeing the B-D pair. Planes A,E share
+    two coordinates; B,C,D share the other two. -/
+def group (i : Fin 5) : Bool := i.val == 0 || i.val == 4
+
+def relaxed : BlockMatrix Int := fun i j => if group i == group j then one else zero
+
+theorem relaxed_diagonal : ∀ i, relaxed i i = one := by decide
+
+theorem relaxed_remaining_zeros : ∀ i j, Far i j →
+    ¬ ((i = 1 ∧ j = 3) ∨ (i = 3 ∧ j = 1)) → relaxed i j = zero := by unfold Far; decide
+
+theorem relaxed_four_pivot : FourPivot relaxed := by unfold FourPivot; decide
+
+theorem relaxed_missing_edge : relaxed 1 3 = one ∧ relaxed 1 3 ≠ zero := by decide
+
+end PairedC5
+
+#print axioms PairedC5.reverse_inverse
+#print axioms PairedC5.no_four_pivot
+#print axioms PairedC5.relaxed_diagonal
+#print axioms PairedC5.relaxed_remaining_zeros
+#print axioms PairedC5.relaxed_four_pivot
+#print axioms PairedC5.relaxed_missing_edge
diff --git a/research/paired-plane-four-channel-lean/TASK.json b/research/paired-plane-four-channel-lean/TASK.json
new file mode 100644
index 0000000000..53068e9edd
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/TASK.json
@@ -0,0 +1,99 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Kernel-check that arbitrary four-scalar-channel factorization implies the C5 normalized pivot equation; deduce strict fitting impossibility over nontrivial commutative rings.",
+  "scope_change_reason": "The assigned child-rank profile search is replaced by the explicit PR2525 missing factorization-to-pivot handoff. This result does not meet or claim the card 5percent profile improvement gate.",
+  "bottleneck_link": "Separates algebraic query dimension from native pricing and closes a formal normalization premise behind the fixed-mask49-channel lower bound.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after exact Lean build, standard-axiom inventory, real proof mutations, relaxed factor, pinned predecessor, separate review and scoped submission.",
+  "outcome": "completed",
+  "evidence": "Algebra.lean; unchanged Schur.lean; Pivot.lean; fresh Lean4.34.1 receipt with12theorems and4 rejected mutations.",
+  "author": "ywz65",
+  "ai_assistance": "Substantial OpenAI Codex assistance for proof, checking and writing; separate AI proof review, no independent human review.",
+  "open_questions": [
+    {
+      "question": "Can a maintained field matrix-rank definition provide ThroughFour, then embed the pinned C5/I44 source?",
+      "why_it_matters": "Closes the ordinary-rank and source interfaces for a full formal fixed-mask rank49 lower bound.",
+      "first_step": "Prove a rank-factorization adapter with explicit row and column indices.",
+      "blocked_by": "No matrix-rank library or formal source parser is used here."
+    }
+  ],
+  "selection": {
+    "nonce": "5daa35e3a3b51d84040a502049bb18ef",
+    "track": "complex-mechanisms",
+    "scope_key": "cad3ba853d7f324f16fa"
+  },
+  "freshness": {
+    "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "priority_revision": 4,
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/2525#issuecomment-6195368693",
+    "first_step": "complex-local-word-ceiling verifier and levers positive controls passed",
+    "separate_review": "research_c checked algebra orientation, ring hypotheses, arbitrary factorization and remaining ordinary-rank boundary; no actionable issue.",
+    "submission_overlap": {
+      "open_prs": {
+        "fetched_at": "2026-10-15T15:35:57.911482+00:00",
+        "complete_pagination": true,
+        "records": 786
+      },
+      "discussions": {
+        "fetched_at": "2026-10-15T15:22:22.047084+00:00",
+        "complete_pagination": true,
+        "records": 1239
+      }
+    },
+    "warnings": [
+      "discussions: refresh failed; using old data if available: gh: API rate limit already exceeded for user ID 154373401.\n"
+    ],
+    "submission_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+    "source_head_recheck": "PR2525 remains ed86bcbe8f728e5412a6ef8f1910bac38f073f51; REST comments read before submission"
+  }
+}
diff --git a/research/paired-plane-four-channel-lean/VERIFY.json b/research/paired-plane-four-channel-lean/VERIFY.json
new file mode 100644
index 0000000000..a342dcd268
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/VERIFY.json
@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Exact recorded kernel receipt source/axiom/control bindings and4rejected source/receipt faults; not a fresh Lean run."
+    }
+  ]
+}
diff --git a/research/paired-plane-four-channel-lean/check_lean.py b/research/paired-plane-four-channel-lean/check_lean.py
new file mode 100644
index 0000000000..86a05e6ff0
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/check_lean.py
@@ -0,0 +1,96 @@
+#!/usr/bin/env python3
+"""Fresh isolated Lean 4.34.1 build; explicit axiom inventory and controls.
+Prepared for ywz65 with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+import argparse
+from hashlib import sha256
+import json
+import os
+from pathlib import Path
+import re
+import subprocess
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+SOURCES = ('Algebra.lean', 'Schur.lean', 'Pivot.lean')
+NAMES = {'Four.det_mul', 'Four.adj_left', 'Four.reverse_inverse',
+         'PairedC5.reverse_inverse', 'PairedC5.no_four_pivot',
+         'PairedC5.relaxed_diagonal', 'PairedC5.relaxed_remaining_zeros',
+         'PairedC5.relaxed_four_pivot', 'PairedC5.relaxed_missing_edge',
+         'Pivot.factor_to_pivot', 'Pivot.no_four_channels',
+         'Pivot.relaxed_through_four'}
+CONTROLS = {
+    'reverse_inverse_wrong_conclusion':
+        ('(h : mul a b = one) : mul b a = one', '(h : mul a b = one) : mul b a = scale 0 one'),
+    'pivot_nonzero_cross_block':
+        ('(h02 : m 0 2 = zero)', '(h02 : m 0 2 = one)'),
+    'remove_ring_nontriviality':
+        ('(hne : (0 : K) ≠ 1)', '(hne : True)'),
+    'relaxed_factor_zero_channels':
+        ('if (group i && k.val == 0)', 'if (group i && k.val == 9)'),
+}
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('--lean', required=True, type=Path)
+    parser.add_argument('--out', type=Path)
+    args = parser.parse_args()
+    lean = args.lean.resolve()
+    version = subprocess.check_output([str(lean), '--version'], text=True).strip()
+    need('version 4.34.1,' in version, 'Lean4.34.1 required')
+    raw = {name: (HERE/name).read_bytes() for name in SOURCES}
+    with tempfile.TemporaryDirectory(prefix='four-channel-lean-') as tmp:
+        work = Path(tmp)
+        for name, data in raw.items():
+            (work/name).write_bytes(data)
+        # A private module directory prevents accidentally using an old .olean.
+        env = dict(os.environ, LEAN_PATH=str(work))
+
+        def run(name, compile_module=False):
+            command = [str(lean), '-j1']
+            if compile_module:
+                command += ['-o', str(work/(Path(name).stem+'.olean'))]
+            return subprocess.run(command+[str(work/name)], cwd=work, env=env,
+                                  capture_output=True, text=True, encoding='utf-8',
+                                  timeout=900 if name == 'Algebra.lean' else 120)
+
+        output = ''
+        for name in SOURCES:
+            result = run(name, compile_module=True)
+            need(result.returncode == 0, result.stdout+result.stderr)
+            output += result.stdout
+        reports = re.findall(r"'([^']+)' depends on axioms: \[([^\]]*)\]", output)
+        need(len(reports) == len(NAMES) and {n for n, _ in reports} == NAMES,
+             'exact theorem inventory missing or duplicated')
+        axioms = {}
+        for name, report in reports:
+            values = sorted(v.strip() for v in report.split(',') if v.strip())
+            need(set(values) <= {'propext', 'Classical.choice', 'Quot.sound'},
+                 'unsupported axiom: '+name)
+            axioms[name] = values
+        source = raw['Pivot.lean'].decode('utf-8')
+        for label, (old, new) in CONTROLS.items():
+            need(source.count(old) == 1, 'mutation target: '+label)
+            (work/'Mutation.lean').write_text(source.replace(old, new), encoding='utf-8', newline='\n')
+            bad = run('Mutation.lean')
+            need(bad.returncode != 0 and 'error:' in bad.stdout,
+                 'mutation did not fail compilation: '+label)
+    receipt = {'status': 'PASS_FOUR_CHANNEL_LEAN', 'version': version,
+               'source_sha256': {name: sha256(data).hexdigest() for name, data in raw.items()},
+               'theorem_axioms': axioms, 'rejected_mutations': list(CONTROLS),
+               'scope': 'Four-channel factorization implies normalized pivot; no strict C5 fitting factorization. Ordinary rank and selected-mask embedding remain external.'}
+    if args.out:
+        with args.out.open('x', encoding='utf-8') as stream:
+            json.dump(receipt, stream, indent=2)
+            stream.write('\n')
+    print(json.dumps(receipt))
+
+
+if __name__ == '__main__':
+    main()
diff --git a/research/paired-plane-four-channel-lean/verify.py b/research/paired-plane-four-channel-lean/verify.py
new file mode 100644
index 0000000000..c8894cdad4
--- /dev/null
+++ b/research/paired-plane-four-channel-lean/verify.py
@@ -0,0 +1,58 @@
+#!/usr/bin/env python3
+"""Validate the source-bound recorded Lean run; this does not execute Lean.
+Prepared for ywz65 with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from copy import deepcopy
+from hashlib import sha256
+import importlib.util
+import json
+from pathlib import Path
+
+HERE = Path(__file__).resolve().parent
+spec = importlib.util.spec_from_file_location('four_channel_check', HERE/'check_lean.py')
+checker = importlib.util.module_from_spec(spec)
+spec.loader.exec_module(checker)
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def validate(receipt, sources):
+    need(receipt['status'] == 'PASS_FOUR_CHANNEL_LEAN', 'recorded status')
+    need('version 4.34.1,' in receipt['version'], 'recorded toolchain')
+    need(receipt['source_sha256'] == {n: sha256(b).hexdigest() for n,b in sources.items()}, 'formal source binding')
+    need(set(receipt['theorem_axioms']) == checker.NAMES, 'theorem inventory')
+    need(all(isinstance(v,list) and len(v) == len(set(v)) and
+             set(v) <= {'propext','Classical.choice','Quot.sound'}
+             for v in receipt['theorem_axioms'].values()), 'axiom inventory')
+    need(receipt['rejected_mutations'] == list(checker.CONTROLS), 'control inventory')
+
+
+def main():
+    receipt = json.loads((HERE/'LEAN-CHECK.json').read_text(encoding='utf-8'))
+    sources = {name:(HERE/name).read_bytes() for name in checker.SOURCES}
+    predecessor = json.loads((HERE/'SOURCES.json').read_text(encoding='utf-8'))['predecessors'][0]
+    need(sha256(sources['Schur.lean']).hexdigest() == predecessor['sha256'], 'exact predecessor bytes')
+    validate(receipt,sources)
+    cases=[]
+    altered = dict(sources, **{'Pivot.lean':sources['Pivot.lean']+b'\n'})
+    cases.append(('formal source drift',receipt,altered))
+    bad=deepcopy(receipt); bad['theorem_axioms']['Pivot.factor_to_pivot']=['sorryAx']
+    cases.append(('untrusted axiom',bad,sources))
+    bad=deepcopy(receipt); del bad['theorem_axioms']['Pivot.no_four_channels']
+    cases.append(('missing theorem',bad,sources))
+    bad=deepcopy(receipt); bad['rejected_mutations']=bad['rejected_mutations'][:-1]
+    cases.append(('missing kernel control',bad,sources))
+    for label,bad,raw in cases:
+        try:
+            validate(bad,raw)
+        except ValueError:
+            continue
+        raise ValueError('accepted control: '+label)
+    print('PASS_FOUR_CHANNEL_RECORDED_BINDING theorems=12 receipt_controls=4; not a fresh Lean run')
+
+
+if __name__ == '__main__':
+    main()

From 07c57449e0d0fdd442bfdae31e087afe14b38c9a Mon Sep 17 00:00:00 2001
From: ywz65 <154373401+ywz65@users.noreply.github.com>
Date: Thu, 15 Oct 2026 08:46:04 -0700
Subject: [PATCH 2/2] Bind formal receipt to Git-normalized source bytes

---
 research/paired-plane-four-channel-lean/LEAN-CHECK.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/research/paired-plane-four-channel-lean/LEAN-CHECK.json b/research/paired-plane-four-channel-lean/LEAN-CHECK.json
index bd9a568601..557d9bf364 100644
--- a/research/paired-plane-four-channel-lean/LEAN-CHECK.json
+++ b/research/paired-plane-four-channel-lean/LEAN-CHECK.json
@@ -2,7 +2,7 @@
   "status": "PASS_FOUR_CHANNEL_LEAN",
   "version": "Lean (version 4.34.1, x86_64-w64-windows-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)",
   "source_sha256": {
-    "Algebra.lean": "d908ace095ef1d025d4a1fed5009e00b6c489ed96654ea5ddaa700b3cc543724",
+    "Algebra.lean": "d29175cb7239901a648e1feba51b0db71dbbb08e5c490d708df4884d8f631236",
     "Schur.lean": "0e714c6f64ac8895080959babb8595ba7bdb391e43a2cee6be51d81690f56db0",
     "Pivot.lean": "0899c8021cdf7d2aed120ad36fc1f20ad59ff30f2db45d20eae17f711bfbd2fc"
   },