From 6404adb824fdf9c6a3300fcf44d66e18e76c8c96 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Sat, 24 Oct 2026 16:43:33 +0000 Subject: [PATCH] Reduce Erdos97ConvexOctagon peak compiler memory --- .../CoveragePairRowIndexMaskSoundness.lean | 61 ++++++++- .../CoverageSearchRowChoiceSoundness.lean | 122 +++++++++++++++++- 2 files changed, 180 insertions(+), 3 deletions(-) diff --git a/LeanPool/Erdos97ConvexOctagon/CoveragePairRowIndexMaskSoundness.lean b/LeanPool/Erdos97ConvexOctagon/CoveragePairRowIndexMaskSoundness.lean index 95138ac447..60bd504c88 100644 --- a/LeanPool/Erdos97ConvexOctagon/CoveragePairRowIndexMaskSoundness.lean +++ b/LeanPool/Erdos97ConvexOctagon/CoveragePairRowIndexMaskSoundness.lean @@ -18,6 +18,55 @@ import Mathlib.Tactic.NormNum.GCD namespace Erdos97Octagon.RawIncidence +-- Bound each kernel reduction cache to one centre of the finite table. +private theorem pairRowIndexMasks_bit_centre_0 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 0 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 0 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_1 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 1 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 1 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_2 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 2 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 2 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_3 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 3 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 3 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_4 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 4 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 4 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_5 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 5 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 5 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_6 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 6 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 6 rowIndex).pairMask pairIndex.val := by + decide +kernel + +private theorem pairRowIndexMasks_bit_centre_7 : + ∀ (pairIndex : Fin 64) (rowIndex : Fin 35), + bitSetB ((pairRowIndexMasks.getD 7 #[]).getD pairIndex.val 0) rowIndex.val = + bitSetB (searchRowChoiceAt 7 rowIndex).pairMask pairIndex.val := by + decide +kernel + /-- The transposed pair table records exactly which row choices contain each pair bit. -/ theorem pairRowIndexMasks_bit (centre : Vertex) (pairIndex : Fin 64) (rowIndex : Fin 35) : @@ -25,6 +74,16 @@ theorem pairRowIndexMasks_bit rowIndex.val = bitSetB (searchRowChoiceAt centre rowIndex).pairMask pairIndex.val := by revert centre pairIndex rowIndex - decide +kernel + as_aux_lemma => + intro centre + fin_cases centre + · exact pairRowIndexMasks_bit_centre_0 + · exact pairRowIndexMasks_bit_centre_1 + · exact pairRowIndexMasks_bit_centre_2 + · exact pairRowIndexMasks_bit_centre_3 + · exact pairRowIndexMasks_bit_centre_4 + · exact pairRowIndexMasks_bit_centre_5 + · exact pairRowIndexMasks_bit_centre_6 + · exact pairRowIndexMasks_bit_centre_7 end Erdos97Octagon.RawIncidence diff --git a/LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean b/LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean index e710039c66..f981bcda5c 100644 --- a/LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean +++ b/LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean @@ -44,13 +44,72 @@ theorem searchRowChoiceAt_mem (centre : Vertex) (index : Fin 35) : rw [hequal] exact Array.getElem_mem hindex +-- Check each centre separately to keep the kernel reduction caches bounded. +private theorem searchRowChoices_complete_centre_0 : + (rowOptions 0).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 0 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_1 : + (rowOptions 1).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 1 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_2 : + (rowOptions 2).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 2 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_3 : + (rowOptions 3).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 3 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_4 : + (rowOptions 4).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 4 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_5 : + (rowOptions 5).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 5 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_6 : + (rowOptions 6).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 6 index).rowMask) := by + decide +kernel + +private theorem searchRowChoices_complete_centre_7 : + (rowOptions 7).reverse = + List.ofFn (fun index : Fin 35 => + packedRow (searchRowChoiceAt 7 index).rowMask) := by + decide +kernel + /-- The generated table is the complete legal-row enumeration, in search order. -/ theorem searchRowChoices_complete (centre : Vertex) : (rowOptions centre).reverse = List.ofFn (fun index : Fin 35 => packedRow (searchRowChoiceAt centre index).rowMask) := by revert centre - decide +kernel + as_aux_lemma => + intro centre + fin_cases centre + · exact searchRowChoices_complete_centre_0 + · exact searchRowChoices_complete_centre_1 + · exact searchRowChoices_complete_centre_2 + · exact searchRowChoices_complete_centre_3 + · exact searchRowChoices_complete_centre_4 + · exact searchRowChoices_complete_centre_5 + · exact searchRowChoices_complete_centre_6 + · exact searchRowChoices_complete_centre_7 /-- Every mathematical incidence row occurs at one lightweight search index. -/ theorem exists_searchRowChoiceIndex (Q : OctagonIncidence) (centre : Vertex) : @@ -63,12 +122,71 @@ theorem exists_searchRowChoiceIndex (Q : OctagonIncidence) (centre : Vertex) : obtain ⟨index, hrow⟩ := hrow exact ⟨index, hrow.symm⟩ +-- Reuse the same bounded checks for the independently generated pair masks. +private theorem searchRowChoiceAt_pairMask_centre_0 (index : Fin 35) : + (searchRowChoiceAt 0 index).pairMask = + rowPairMask (searchRowChoiceAt 0 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_1 (index : Fin 35) : + (searchRowChoiceAt 1 index).pairMask = + rowPairMask (searchRowChoiceAt 1 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_2 (index : Fin 35) : + (searchRowChoiceAt 2 index).pairMask = + rowPairMask (searchRowChoiceAt 2 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_3 (index : Fin 35) : + (searchRowChoiceAt 3 index).pairMask = + rowPairMask (searchRowChoiceAt 3 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_4 (index : Fin 35) : + (searchRowChoiceAt 4 index).pairMask = + rowPairMask (searchRowChoiceAt 4 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_5 (index : Fin 35) : + (searchRowChoiceAt 5 index).pairMask = + rowPairMask (searchRowChoiceAt 5 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_6 (index : Fin 35) : + (searchRowChoiceAt 6 index).pairMask = + rowPairMask (searchRowChoiceAt 6 index).rowMask := by + revert index + decide +kernel + +private theorem searchRowChoiceAt_pairMask_centre_7 (index : Fin 35) : + (searchRowChoiceAt 7 index).pairMask = + rowPairMask (searchRowChoiceAt 7 index).rowMask := by + revert index + decide +kernel + /-- Every stored unordered-pair mask is exactly computed from its row mask. -/ theorem searchRowChoiceAt_pairMask (centre : Vertex) (index : Fin 35) : (searchRowChoiceAt centre index).pairMask = rowPairMask (searchRowChoiceAt centre index).rowMask := by revert centre index - decide +kernel + as_aux_lemma => + intro centre + fin_cases centre + · exact searchRowChoiceAt_pairMask_centre_0 + · exact searchRowChoiceAt_pairMask_centre_1 + · exact searchRowChoiceAt_pairMask_centre_2 + · exact searchRowChoiceAt_pairMask_centre_3 + · exact searchRowChoiceAt_pairMask_centre_4 + · exact searchRowChoiceAt_pairMask_centre_5 + · exact searchRowChoiceAt_pairMask_centre_6 + · exact searchRowChoiceAt_pairMask_centre_7 /-- The centre-two row table uses exactly the public fixed-branch ordering. -/ theorem searchRowChoiceAt_two_mask (index : Fin 35) :