IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondScratch

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
   2
   3/-! # Gap2JDiamondScratch
   4
   5Scratchpad used while debugging kernel reduction for `Fin` numeral goals during
   6the C15 J-diamond lattice work. No load-bearing theorems live here; the four small
   7kernel witnesses below are kept as compiling exhibits and nothing imports them. The
   8lesson is banked as `L-qg-fin-literal-show-first` in QG memory.
   9
  10Findings, kept as compiling witnesses:
  11
  12* `decide` and the `OfNat` simprocs do not unfold non-literal `Fin` bounds
  13  (projections such as `K.nV`, `K.nE`). Writing `({2} : Finset (Fin
  14  twoEdgeComplex.nV))` fails `OfNat` synthesis outright, and `fin_cases` over
  15  `Fin K.nE` leaves residuals `⟨2, ⋯⟩ = 2` that `simp` and `try decide` cannot
  16  close (they became silent `sorryAx` in the main module before the fix).
  17* The fix: `show` the definitionally-equal literal form first, then
  18  `ext` + `fin_cases` + `simp` closes every case. -/
  19
  20namespace IndisputableMonolith
  21namespace Gravity
  22namespace SevenGaps
  23namespace Gap2JDiamondScratch
  24
  25open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
  26
  27variable {B : ℕ}
  28
  29structure SC4 (K : BoundedComplex B) where
  30  verts : Finset (Fin K.nV)
  31  edges : Finset (Fin K.nE)
  32
  33def teLeft : SC4 twoEdgeComplex where
  34  verts := ({0, 1} : Finset (Fin 4))
  35  edges := ({0} : Finset (Fin 2))
  36
  37def teRight : SC4 twoEdgeComplex where
  38  verts := ({2, 3} : Finset (Fin 4))
  39  edges := ({1} : Finset (Fin 2))
  40
  41-- projections with a non-literal bound: this one simp can still close
  42theorem teInterEmpty : teLeft.verts ∩ teRight.verts = ∅ := by
  43  ext v
  44  fin_cases v <;> simp [teLeft, teRight]
  45
  46-- the working pattern for the case simp cannot: `show` the literal form first
  47theorem teInter2 : teLeft.verts ∩ teRight.verts =
  48    (({0, 1} : Finset (Fin 4)) ∩ ({2, 3} : Finset (Fin 4))) := rfl
  49
  50theorem inter4literal : (({0, 1, 2} : Finset (Fin 4)) ∩ ({2, 3} : Finset (Fin 4))) = {2} := by
  51  ext v
  52  fin_cases v <;> simp
  53
  54-- a Fin 4 numeral equality `decide` closes when the bound is literal
  55theorem fin4decide : (⟨2, by decide⟩ : Fin 4) = 2 := by decide
  56
  57end Gap2JDiamondScratch
  58end SevenGaps
  59end Gravity
  60end IndisputableMonolith
  61