Lean migration: Phase 3 (Unit, Prod, AboveBelow lattices)

- Spa.Lattice.Unit: PUnit fixed height 0 (lattice lifted from mathlib)
- Spa.Lattice.Prod: chain unzip + FixedHeight (h1+h2) on products
  (componentwise lattice lifted from mathlib's Prod.instLattice)
- Spa.Lattice.AboveBelow: flat lattice via Lattice.mk' (mirrors the Agda
  semilattices+absorption construction), boundedness via rank into Nat,
  Plain x ↦ plainFixedHeight x, height 2

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

lean/Spa/Lattice/Prod.lean

@@ -0,0 +1,113 @@
+/-
+Port of `Lattice/Prod.agda`.
+
+The component-wise lattice structure on `α × β` is lifted into mathlib
+(`Prod.instLattice`), as is decidability of equality. What remains custom is
+the fixed-height content:
+
+  unzip                      ↦ LTSeries.exists_unzip
+  a,∙-Monotonic/∙,b-Monotonic ↦ Prod.mk_lt_mk_iff_right/left (strict mono of
+                                the two injections, used to map the chains)
+  fixedHeight (h₁ + h₂)      ↦ FixedHeight.prod
+  isFiniteHeightLattice      ↦ instance FiniteHeightLattice (α × β)
+-/
+import Spa.Lattice
+
+namespace Spa
+
+section Unzip
+
+variable {α β : Type*} [PartialOrder α] [PartialOrder β]
+
+/-- Agda: `unzip` — a chain in the product splits into chains of the
+components whose lengths sum to at least the original length. -/
+theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
+    ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+      c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+      c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+      c.length ≤ c₁.length + c₂.length := by
+  suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
+      ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+        c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+        c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+        c.length ≤ c₁.length + c₂.length from H c.length c rfl
+  intro n
+  induction n with
+  | zero =>
+    intro c hn
+    refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
+      rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
+    · have hlast : Fin.last c.length = 0 := by ext; simp [hn]
+      simp [RelSeries.last, RelSeries.head, hlast]
+  | succ n ih =>
+    intro c hn
+    have h0 : c.length ≠ 0 := by omega
+    obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
+      ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
+    rw [RelSeries.last_tail] at hl₁ hl₂
+    rw [RelSeries.head_tail] at hh₁ hh₂
+    rw [RelSeries.tail_length] at hlen
+    have hstep : c.head < c 1 := by
+      have h := c.step ⟨0, by omega⟩
+      have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
+        ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
+      rwa [h1] at h
+    obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
+    rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
+      rcases eq_or_lt_of_le hle2 with heq2 | hlt2
+    · exact absurd (Prod.ext heq1 heq2) hstep.ne
+    · refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        hh₂.trans heq2.symm, hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+
+end Unzip
+
+section FixedHeight
+
+variable {α β : Type*} [Lattice α] [Lattice β]
+
+/-- Agda: `Lattice/Prod.agda`'s `fixedHeight` — the product of lattices of
+heights `h₁` and `h₂` has height `h₁ + h₂`. The longest chain climbs the first
+component (at `⊥₂`), then the second component (at `⊤₁`). -/
+def FixedHeight.prod {h₁ h₂ : ℕ} (fhA : FixedHeight α h₁) (fhB : FixedHeight β h₂) :
+    FixedHeight (α × β) (h₁ + h₂) where
+  bot := (fhA.bot, fhB.bot)
+  top := (fhA.top, fhB.top)
+  longestChain :=
+    RelSeries.smash
+      (fhA.longestChain.map (fun a => (a, fhB.bot))
+        (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
+      (fhB.longestChain.map (fun b => (fhA.top, b))
+        (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
+      (by simp [fhA.last_longestChain, fhB.head_longestChain])
+  head_longestChain := by simp [fhA.head_longestChain]
+  last_longestChain := by simp [fhB.last_longestChain]
+  length_longestChain := by
+    simp [fhA.length_longestChain, fhB.length_longestChain]
+  bounded := fun c => by
+    obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
+    have h₁ := fhA.bounded c₁
+    have h₂ := fhB.bounded c₂
+    omega
+
+/-- Agda: `Lattice/Prod.agda`'s `isFiniteHeightLattice`/`finiteHeightLattice`. -/
+instance [IA : FiniteHeightLattice α] [IB : FiniteHeightLattice β] :
+    FiniteHeightLattice (α × β) where
+  height := IA.height + IB.height
+  fixedHeight := IA.fixedHeight.prod IB.fixedHeight
+
+end FixedHeight
+
+end Spa