Add paper_tuft_sm_lagrangian Lean modules and build target

Hqiv/Algebra/CliffordCl06SixDimension.lean

@@ -0,0 +1,121 @@
+import Hqiv.Algebra.CliffordSixImaginaryScaffold
+import Mathlib.Algebra.DirectSum.Module
+import Mathlib.Data.Nat.Choose.Sum
+import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
+import Mathlib.LinearAlgebra.Dimension.Finite
+import Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
+import Mathlib.LinearAlgebra.ExteriorPower.Basis
+import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+import Mathlib.Order.Extension.Well
+import Mathlib.Order.SupIndep
+
+/-!
+# Real dimension of abstract `Cl(0,6)` (`CliffordCl06Six`)
+
+Over `ℝ`, `2` is invertible, so `CliffordAlgebra.equivExterior` identifies **any** Clifford
+algebra on a finite free module with the exterior algebra on the same module **as a real vector
+space**.  For `M = ℝ⁶`, `⋀[ℝ]^k M` has dimension `Nat.choose 6 k`, hence total dimension
+`∑_{k=0}^6 \binom{6}{k} = 2^6 = 64`.
+
+This is the algebraic backbone for Furey-style **minimal left ideal** counting: once a faithful
+`8`-dimensional real representation is packaged, minimal ideals have real dimension `8`; that
+layer is *not* proved here (it needs an explicit simple-algebra certificate, e.g. a chosen
+`Mat₈(ℝ)` model), but the ambient `Cl(0,6)` dimension `64` is unconditional in this file.
+-/
+
+namespace Hqiv.Algebra
+
+open scoped DirectSum
+
+open DirectSum Submodule Module Finset CompleteLattice
+
+abbrev Cl06Carrier : Type := Fin 6 → ℝ
+
+abbrev ExtCl06 := ExteriorAlgebra ℝ Cl06Carrier
+
+/-- The `Fin 7`-indexed exterior grading pieces `⋀^k ℝ⁶` for `k = 0,…,6`. -/
+def extPowGraded (i : Fin 7) : Submodule ℝ ExtCl06 :=
+  ⋀[ℝ]^(i.val : ℕ) Cl06Carrier
+
+noncomputable instance extPowGraded_moduleFinite (i : Fin 7) :
+    Module.Finite ℝ (extPowGraded i) := by
+  let b := Module.Free.chooseBasis ℝ Cl06Carrier
+  letI : LinearOrder (Module.Free.ChooseBasisIndex ℝ Cl06Carrier) :=
+    IsWellFounded.wellOrderExtension emptyWf.rel
+  simpa [extPowGraded, ExteriorAlgebra.exteriorPower] using
+    Module.Finite.of_basis (b.exteriorPower (i.val : ℕ))
+
+lemma extPowGraded_eq_exteriorPower (i : Fin 7) :
+    extPowGraded i = ExteriorAlgebra.exteriorPower ℝ (i.val : ℕ) Cl06Carrier :=
+  rfl
+
+lemma exteriorPower_nat_succ_bot (n : ℕ) (hn : 6 < n) :
+    ExteriorAlgebra.exteriorPower ℝ n Cl06Carrier = ⊥ :=
+  Submodule.finrank_eq_zero.1 <| by
+    have hf : finrank ℝ Cl06Carrier = 6 := by rw [Module.finrank_pi, Fintype.card_fin]
+    rw [exteriorPower.finrank_eq (R := ℝ) (M := Cl06Carrier), hf, Nat.choose_eq_zero_of_lt hn]
+
+lemma iSup_extPowGraded_eq_iSup_nat :
+    (⨆ i : Fin 7, extPowGraded i) = ⨆ n : ℕ, (⋀[ℝ]^n Cl06Carrier : Submodule ℝ ExtCl06) := by
+  refine le_antisymm (iSup_le fun i => ?_) (iSup_le fun n => ?_)
+  · exact le_iSup _ (i.val : ℕ)
+  · by_cases hn : n ≤ 6
+    · let i : Fin 7 := ⟨n, Nat.lt_succ_iff.mpr hn⟩
+      exact le_iSup (fun j : Fin 7 => extPowGraded j) i
+    · push_neg at hn
+      rw [exteriorPower_nat_succ_bot n hn]
+      exact bot_le
+
+lemma iSup_nat_exterior_pow_eq_top :
+    (⨆ n : ℕ, (⋀[ℝ]^n Cl06Carrier : Submodule ℝ ExtCl06)) = ⊤ := by
+  let 𝒜 : ℕ → Submodule ℝ ExtCl06 := fun n => ⋀[ℝ]^n Cl06Carrier
+  haveI : DirectSum.Decomposition 𝒜 :=
+    inferInstanceAs (DirectSum.Decomposition 𝒜)
+  exact IsInternal.submodule_iSup_eq_top (DirectSum.Decomposition.isInternal 𝒜)
+
+lemma iSup_extPowGraded_eq_top : (⨆ i : Fin 7, extPowGraded i) = ⊤ := by
+  rw [iSup_extPowGraded_eq_iSup_nat, iSup_nat_exterior_pow_eq_top]
+
+lemma iSupIndep_extPowGraded : iSupIndep extPowGraded := by
+  let 𝒜 : ℕ → Submodule ℝ ExtCl06 := fun n => ⋀[ℝ]^n Cl06Carrier
+  haveI : DirectSum.Decomposition 𝒜 :=
+    inferInstanceAs (DirectSum.Decomposition 𝒜)
+  exact iSupIndep.comp (IsInternal.submodule_iSupIndep (DirectSum.Decomposition.isInternal 𝒜))
+    Fin.val_injective
+
+lemma isInternal_extPowGraded : IsInternal extPowGraded :=
+  (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top extPowGraded).mpr
+    ⟨iSupIndep_extPowGraded, iSup_extPowGraded_eq_top⟩
+
+noncomputable def extPowDecomposeLinearEquiv : ExtCl06 ≃ₗ[ℝ] ⨁ i : Fin 7, extPowGraded i :=
+  (LinearEquiv.ofBijective (DirectSum.coeLinearMap extPowGraded) isInternal_extPowGraded).symm
+
+lemma finrank_extPowGraded (i : Fin 7) :
+    finrank ℝ (extPowGraded i) = Nat.choose 6 i.val := by
+  rw [extPowGraded_eq_exteriorPower, exteriorPower.finrank_eq (R := ℝ) (M := Cl06Carrier),
+    Module.finrank_pi, Fintype.card_fin]
+
+noncomputable def extGradingBasis :
+    Basis (Σ i : Fin 7, Module.Free.ChooseBasisIndex ℝ (extPowGraded i)) ℝ ExtCl06 :=
+  IsInternal.collectedBasis isInternal_extPowGraded fun i =>
+    Module.Free.chooseBasis ℝ (extPowGraded i)
+
+lemma finrank_extCl06 : finrank ℝ ExtCl06 = 64 := by
+  classical
+  rw [Module.finrank_eq_card_basis extGradingBasis, Fintype.card_sigma]
+  simp_rw [← Module.finrank_eq_card_chooseBasisIndex ℝ (extPowGraded _), finrank_extPowGraded]
+  simp +decide
+
+noncomputable instance invertibleTwoReal : Invertible (2 : ℝ) :=
+  invertibleOfNonzero (two_ne_zero : (2 : ℝ) ≠ 0)
+
+noncomputable def cliffordCl06SixLinearEquivExterior :
+    CliffordCl06Six ≃ₗ[ℝ] ExtCl06 :=
+  haveI := invertibleTwoReal
+  CliffordAlgebra.equivExterior quadFormCl06Six
+
+theorem cliffordCl06Six_finrank : finrank ℝ CliffordCl06Six = 64 := by
+  haveI := invertibleTwoReal
+  rw [LinearEquiv.finrank_eq cliffordCl06SixLinearEquivExterior, finrank_extCl06]
+
+end Hqiv.Algebra

Hqiv/Algebra/CliffordCl06SixIdeal.lean

@@ -0,0 +1,69 @@
+import Hqiv.Algebra.CliffordCl06SixDimension
+import Hqiv.Algebra.CliffordMinimalIdeal
+
+/-!
+# Left ideals and idempotents in abstract `Cl(0,6)` (`CliffordCl06Six`)
+
+`CliffordCl06Six` is a **64**-dimensional real algebra (`Hqiv.Algebra.cliffordCl06Six_finrank`).  This
+file records the basic **ring-theoretic** packaging used in Furey-style discussions:
+
+* **Left ideals** as `Submodule CliffordCl06Six CliffordCl06Six` (scalar action `r • x = r * x`).
+* The **principal** left ideal generated by `1` is the whole algebra (`leftIdealGenerated_one_eq_top`).
+* **Existence** of a nontrivial idempotent (`1`).
+* **Unital ideals:** `cliffordCl06Six_leftIdeal_eq_top_of_one_mem` — any left ideal containing `1` is `⊤`.
+* **Minimal `⊤` (conditional):** `cliffordCl06Six_top_isMinimalLeftIdeal` — if `CliffordCl06Six` is a simple
+  left module over itself, then `⊤` is `IsMinimalLeftIdeal` (same pattern as `Cl(1) ≅ ℂ`).
+
+What is **not** proved here (and remains representation-theoretic) is a Mathlib certificate that
+`CliffordCl06Six` is abstractly isomorphic to `Mat₈(ℝ)` and hence that nonzero primitive idempotents
+generate **8**-dimensional minimal left ideals — that step is exactly where a faithful `8`-dimensional
+real spinor representation must enter (compare `Hqiv.Algebra.OctonionSpinorCarrier`, the bridge
+file `Hqiv.Algebra.CliffordCl06SixSpinorBridge`, and the **conditional** surjectivity layer
+`Hqiv.Algebra.CliffordCl06SixStandardSpinorMatLiftSurjective`).
+-/
+
+namespace Hqiv.Algebra
+
+open Submodule
+
+abbrev CliffordLeftIdeal := Submodule CliffordCl06Six CliffordCl06Six
+
+/-- Left ideal generated by `e : CliffordCl06Six` (all left multiples `a * e`). -/
+noncomputable def cliffordCl06SixLeftIdealGenerated (e : CliffordCl06Six) : CliffordLeftIdeal :=
+  span CliffordCl06Six (Set.range fun a : CliffordCl06Six => a * e)
+
+theorem mem_cliffordCl06SixLeftIdealGenerated {e x : CliffordCl06Six} :
+    x ∈ cliffordCl06SixLeftIdealGenerated e ↔
+      x ∈ span CliffordCl06Six (Set.range fun a : CliffordCl06Six => a * e) :=
+  Iff.rfl
+
+theorem cliffordCl06SixLeftIdealGenerated_one_eq_top :
+    cliffordCl06SixLeftIdealGenerated (1 : CliffordCl06Six) = ⊤ := by
+  refine eq_top_iff.mpr fun x _ => ?_
+  simp only [cliffordCl06SixLeftIdealGenerated]
+  exact Submodule.subset_span (show x ∈ Set.range (· * (1 : CliffordCl06Six)) from ⟨x, mul_one x⟩)
+
+theorem exists_nonzero_idempotent_cliffordCl06Six :
+    ∃ e : CliffordCl06Six, e * e = e ∧ e ≠ 0 :=
+  ⟨1, mul_one _, one_ne_zero⟩
+
+theorem cliffordCl06SixLeftIdealGenerated_le_top (e : CliffordCl06Six) :
+    cliffordCl06SixLeftIdealGenerated e ≤ ⊤ :=
+  le_top
+
+/-- Any left ideal containing `1` is the whole algebra (`r • 1 = r` for `r : CliffordCl06Six`). -/
+theorem cliffordCl06Six_leftIdeal_eq_top_of_one_mem {I : CliffordLeftIdeal}
+    (h : (1 : CliffordCl06Six) ∈ I) : I = ⊤ := by
+  rw [Submodule.eq_top_iff']
+  intro x
+  simpa only [smul_eq_mul, mul_one] using Submodule.smul_mem I x h
+
+/-- If `CliffordCl06Six` is simple as a left module over itself, then `⊤` is a minimal nonzero
+left ideal (same pattern as `cliffordOneDim_top_isMinimalLeftIdeal` for the division ring `Cl(1)`).
+-/
+theorem cliffordCl06Six_top_isMinimalLeftIdeal
+    [IsSimpleModule CliffordCl06Six CliffordCl06Six] [Nontrivial CliffordCl06Six] :
+    IsMinimalLeftIdeal (⊤ : CliffordLeftIdeal) :=
+  IsMinimalLeftIdeal.top_of_isSimpleModule (R := CliffordCl06Six)
+
+end Hqiv.Algebra

Hqiv/Algebra/CliffordCl06SixSpinorGammaMatInt.lean

@@ -0,0 +1,74 @@
+import Hqiv.Algebra.CliffordCl06SixStandardSpinorRho
+import Mathlib.Algebra.Algebra.Defs
+import Mathlib.Data.Fintype.Basic
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.Matrix.Basic
+import Mathlib.LinearAlgebra.Matrix.Notation
+
+/-!
+# Integer (`ℤ`) spinor `γ` matrices and `γ`-monomials
+
+Mirror of `CliffordCl06SixStandardSpinorRho` at coefficients in `ℤ`, using the same triple
+Kronecker bitmask layout.  Casting into `ℝ` commutes with Kronecker product and with the six fixed
+blocks, so the `ℝ` model used by `cl06SpinorGammaMat` is exactly `Matrix.map (algebraMap ℤ ℝ)` of
+this layer.
+-/
+
+namespace Hqiv.Algebra
+
+open Matrix Finset
+
+/-- Same mask convention as `cl06SpinorGammaMaskFinset` in `CliffordCl06SixStandardSpinorMatLiftSurjective`. -/
+def cl06SpinorGammaMaskFinset (m : Fin 64) : Finset (Fin 6) :=
+  univ.filter fun i : Fin 6 => (m.val >>> i.val) % 2 = 1
+
+/-! ## `2 × 2` blocks over `ℤ` -/
+
+def spinorIxZ : Matrix (Fin 2) (Fin 2) ℤ := !![1, 0; 0, 1]
+def spinorXZ : Matrix (Fin 2) (Fin 2) ℤ := !![0, 1; 1, 0]
+def spinorZZ : Matrix (Fin 2) (Fin 2) ℤ := !![1, 0; 0, -1]
+def spinorAZ : Matrix (Fin 2) (Fin 2) ℤ := !![0, 1; -1, 0]
+
+def spinorKron3Z (A B C : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 8) (Fin 8) ℤ :=
+  fun i j =>
+    A (fin8Lo i) (fin8Lo j) * B (fin8Mid i) (fin8Mid j) * C (fin8Hi i) (fin8Hi j)
+
+def cl06SpinorGammaMatZ : Fin 6 → Matrix (Fin 8) (Fin 8) ℤ
+  | ⟨0, _⟩ => spinorKron3Z spinorAZ spinorIxZ spinorXZ
+  | ⟨1, _⟩ => spinorKron3Z spinorAZ spinorIxZ spinorZZ
+  | ⟨2, _⟩ => spinorKron3Z spinorAZ spinorAZ spinorAZ
+  | ⟨3, _⟩ => spinorKron3Z spinorIxZ spinorXZ spinorAZ
+  | ⟨4, _⟩ => spinorKron3Z spinorIxZ spinorZZ spinorAZ
+  | ⟨5, _⟩ => spinorKron3Z spinorXZ spinorAZ spinorIxZ
+
+def spinorGammaMonomialMatZ (m : Fin 64) : Matrix (Fin 8) (Fin 8) ℤ :=
+  (cl06SpinorGammaMaskFinset m).sort (· ≤ ·)|>.foldl
+    (fun A i => A * cl06SpinorGammaMatZ i) (1 : Matrix (Fin 8) (Fin 8) ℤ)
+
+/-! ## Cast lemmas (`algebraMap ℤ ℝ`) -/
+
+theorem spinorKron3Z_map (A B C : Matrix (Fin 2) (Fin 2) ℤ) :
+    (spinorKron3Z A B C).map (algebraMap ℤ ℝ) =
+      spinorKron3 (A.map (algebraMap ℤ ℝ)) (B.map (algebraMap ℤ ℝ)) (C.map (algebraMap ℤ ℝ)) := by
+  ext i j
+  simp only [spinorKron3Z, spinorKron3, Matrix.map_apply, map_mul]
+
+theorem spinorIxZ_map : spinorIxZ.map (algebraMap ℤ ℝ) = spinorIx := by
+  ext i j; fin_cases i <;> fin_cases j <;> simp [spinorIxZ, spinorIx, Matrix.map_apply, map_one, map_zero]
+
+theorem spinorXZ_map : spinorXZ.map (algebraMap ℤ ℝ) = spinorX := by
+  ext i j; fin_cases i <;> fin_cases j <;> simp [spinorXZ, spinorX, Matrix.map_apply, map_one, map_zero]
+
+theorem spinorZZ_map : spinorZZ.map (algebraMap ℤ ℝ) = spinorZ := by
+  ext i j; fin_cases i <;> fin_cases j <;> simp [spinorZZ, spinorZ, Matrix.map_apply, map_one, map_zero, map_neg]
+
+theorem spinorAZ_map : spinorAZ.map (algebraMap ℤ ℝ) = spinorA := by
+  ext i j; fin_cases i <;> fin_cases j <;> simp [spinorAZ, spinorA, Matrix.map_apply, map_one, map_zero, map_neg]
+
+theorem cl06SpinorGammaMatZ_map (k : Fin 6) :
+    (cl06SpinorGammaMatZ k).map (algebraMap ℤ ℝ) = cl06SpinorGammaMat k := by
+  fin_cases k <;>
+    (simp only [cl06SpinorGammaMatZ, cl06SpinorGammaMat]; rw [spinorKron3Z_map]; simp only
+      [spinorAZ_map, spinorIxZ_map, spinorXZ_map, spinorZZ_map])
+
+end Hqiv.Algebra