Reduce BrillNoetherGraphs certificate replay memory

LeanPool/BrillNoetherGraphs/Imports.lean

@@ -226,6 +226,7 @@ public import LeanPool.BrillNoetherGraphs.LowGenus
 public import LeanPool.BrillNoetherGraphs.LowGenus.AtanasovRanganathanExistence
 public import LeanPool.BrillNoetherGraphs.LowGenus.AtanasovRanganathanProgram
 public import LeanPool.BrillNoetherGraphs.LowGenus.ClosedConstructionTail
+public import LeanPool.BrillNoetherGraphs.LowGenus.CompactCellTreeLookup
 public import LeanPool.BrillNoetherGraphs.LowGenus.ConfigurationBananaDoubleChip
 public import LeanPool.BrillNoetherGraphs.LowGenus.ConfigurationBananaTail
 public import LeanPool.BrillNoetherGraphs.LowGenus.ConfigurationChippedTriangle
@@ -357,6 +358,7 @@ public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.AcyclicOrientati
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.BlockSlopeRounding
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.BrillNoetherRank
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.CanonicalSlackPair
+public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.ChunkedLookup
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.CommonOffsetRounding
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.ConvexIntegerRounding
 public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.Duality

LeanPool/BrillNoetherGraphs/LowGenus/CompactCellTreeLookup.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2026 Nathan Pflueger and OpenAI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathan Pflueger, OpenAI
+-/
+module
+
+public import LeanPool.BrillNoetherGraphs.LowGenus.GenusFiveClosedCover
+
+/-!
+# Equivalent receipt lookups for compact cover replay
+
+The generated row proofs keep their original tables and checker statements. Their private
+`_chunked` lemmas replay the same trees with a size-checked block lookup, skipping complete
+receipt blocks rather than repeatedly traversing a concatenated prefix.
+
+The original proofs transfer these results through `checkLookup_eq_check`. Their `as_aux_lemma`
+wrappers also preserve the names and types of the original kernel-check auxiliary declarations.
+-/
+
+@[expose] public section
+
+open Utilities Utilities.Certificate
+
+namespace AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree
+
+/-- Decode receipt indices through a supplied lookup function. -/
+def decodeLookup {p : ℕ}
+    (forms : List (ExplicitPotential.AffineForm p))
+    (lookupReceipt : ℕ → Certificate.AffineCover.FarkasData) : CompactCellTree → CellTree p
+  | .cell index indices => .cell index (indices.map lookupReceipt)
+  | .absurd index => .absurd (lookupReceipt index)
+  | .split index nonnegative negative =>
+      .split (forms.getD index 0)
+        (decodeLookup forms lookupReceipt nonnegative)
+        (decodeLookup forms lookupReceipt negative)
+
+/-- List lookup recovers the original compact-tree decoder. -/
+theorem decodeLookup_getD {p : ℕ} (tree : CompactCellTree)
+    (forms : List (ExplicitPotential.AffineForm p))
+    (receipts : List Certificate.AffineCover.FarkasData) :
+    decodeLookup forms (fun index => receipts.getD index { terms := [] }) tree =
+      tree.decode forms receipts := by
+  induction tree with
+  | cell index indices => rfl
+  | absurd index => rfl
+  | split index nonnegative negative ihNonnegative ihNegative =>
+      simp only [decodeLookup, decode, ihNonnegative, ihNegative]
+
+/-- Replay a compact tree using an extensionally equivalent receipt lookup. -/
+def checkLookup {n p : ℕ} {core : ExplicitPotential.Core n p}
+    (tree : CompactCellTree) (forms : List (ExplicitPotential.AffineForm p))
+    (lookupReceipt : ℕ → Certificate.AffineCover.FarkasData)
+    (cells : List (CoordinateCell core))
+    (active : List (ExplicitPotential.AffineForm p)) : Bool :=
+  (decodeLookup forms lookupReceipt tree).check cells active
+
+/-- Changing the lookup implementation preserves every original replay result. -/
+theorem checkLookup_eq_check {n p : ℕ} {core : ExplicitPotential.Core n p}
+    (tree : CompactCellTree) (forms : List (ExplicitPotential.AffineForm p))
+    (receipts : List Certificate.AffineCover.FarkasData)
+    (lookupReceipt : ℕ → Certificate.AffineCover.FarkasData)
+    (hLookup : ∀ index, lookupReceipt index = receipts.getD index { terms := [] })
+    (cells : List (CoordinateCell core))
+    (active : List (ExplicitPotential.AffineForm p)) :
+    checkLookup tree forms lookupReceipt cells active = tree.check forms receipts cells active := by
+  have hFunctions : lookupReceipt = fun index => receipts.getD index { terms := [] } :=
+    funext hLookup
+  rw [checkLookup, hFunctions, decodeLookup_getD]
+  rfl
+end AtanasovRanganathan.GenusFiveClosedCover.CompactCellTree

LeanPool/BrillNoetherGraphs/LowGenus/GenusFiveRow03CoverReceipts.lean

@@ -6,6 +6,7 @@ Authors: Nathan Pflueger
 module
 
 public import LeanPool.BrillNoetherGraphs.Utilities.Subdivision.AffineCover
+public import LeanPool.BrillNoetherGraphs.Utilities.Foundations.ChunkedLookup
 
 /-!
 # Sparse Farkas receipts for the row-03 closed cover
@@ -1769,4 +1770,34 @@ def farkasReceipts : List Certificate.AffineCover.FarkasData :=
   farkasReceipts0 ++ farkasReceipts1 ++ farkasReceipts2 ++ farkasReceipts3 ++ farkasReceipts4 ++
   farkasReceipts5 ++ farkasReceipts6
 
+/-- Existing receipt blocks with their checked sizes, avoiding repeated prefix traversal. -/
+def farkasReceiptChunks : List (ℕ × List Certificate.AffineCover.FarkasData) :=
+  [(128, farkasReceipts0),
+   (128, farkasReceipts1),
+   (128, farkasReceipts2),
+   (128, farkasReceipts3),
+   (128, farkasReceipts4),
+   (128, farkasReceipts5),
+   (28, farkasReceipts6)]
+
+private theorem farkasReceiptChunks_sizes :
+    ∀ chunk ∈ farkasReceiptChunks, chunk.1 = chunk.2.length := by
+  intro chunk hMem
+  simp only [farkasReceiptChunks, List.mem_cons, List.not_mem_nil, or_false] at hMem
+  rcases hMem with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
+
+/-- Block lookup keeps the original table, order, and out-of-range default. -/
+def farkasReceiptLookup (index : ℕ) : Certificate.AffineCover.FarkasData :=
+  List.lookupChunks farkasReceiptChunks index { terms := [] }
+
+theorem farkasReceiptLookup_eq_getD (index : ℕ) :
+    farkasReceiptLookup index = farkasReceipts.getD index { terms := [] } := by
+  have hTable : farkasReceiptChunks.flatMap Prod.snd = farkasReceipts := by
+    simp only [farkasReceiptChunks, List.flatMap_cons, List.flatMap_nil, List.append_nil,
+      List.append_assoc, farkasReceipts]
+  have hLookup := List.lookupChunks_eq_getD_flatMap farkasReceiptChunks
+    farkasReceiptChunks_sizes index { terms := [] }
+  rw [hTable] at hLookup
+  exact hLookup
+
 end AtanasovRanganathan.GenusFiveRow03FixedCover