Prove four-channel factorization implies the C5 pivot equation

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

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": "d29175cb7239901a648e1feba51b0db71dbbb08e5c490d708df4884d8f631236",
+    "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."
+}

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

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.

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