Paper/thermodynamics arrow support

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/CliffordCl06SixStandardSpinorRho.lean

@@ -0,0 +1,138 @@
+import Hqiv.Algebra.CliffordCl06SixIdeal
+import Hqiv.Algebra.CliffordSixImaginaryScaffold
+import Hqiv.Algebra.OctonionSpinorCarrier
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Data.Fintype.BigOperators
+import Mathlib.Data.Matrix.Basic
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
+import Mathlib.LinearAlgebra.Finsupp.LinearCombination
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
+
+/-!
+# Standard real **8×8** spinor model for abstract `Cl(0,6)`
+
+Naive octonion **left** multiplication on `e₁,…,e₆` does **not** satisfy the mixed Clifford relations
+(`Hqiv.Algebra.OctonionLeftMulCliffordObstruction`).  Here we use the classical **alphabetic**
+`2×2` Kronecker construction (Toppan–Verbeek, arXiv:0903.0940, Eqs. (2)–(4)) to build six explicit
+`8×8` real matrices `γ₀,…,γ₅` with `γₖ² = -I₈` and `γₖ γₗ + γₗ γₖ = 0` for `k ≠ l`.
+
+For `Q(v) = -∑ₖ vₖ²` (`quadFormCl06Six`), any `M(v) = ∑ₖ vₖ γₖ` obeys `M(v)² = Q(v) · I₈`, hence
+`CliffordAlgebra.lift` yields
+
+`ρ_mat : CliffordCl06Six →ₐ[ℝ] Matrix (Fin 8) (Fin 8) ℝ`,
+
+and `algEquivMatrix'.symm` composes to
+
+`ρ : CliffordCl06Six →ₐ[ℝ] Module.End ℝ OctonionSpinorCarrier`.
+
+This is **not** the octonion left-mult lift; it is a concrete faithful `8`-dimensional real module for
+evaluating abstract ideals in `End(ℝ⁸)`.
+-/
+
+namespace Hqiv.Algebra
+
+open scoped BigOperators
+open Finset Matrix CliffordAlgebra Module QuadraticMap
+
+/-- The four `2×2` blocks `I, X, Z, A` from the alphabetic presentation. -/
+def spinorIx : Matrix (Fin 2) (Fin 2) ℝ := !![1, 0; 0, 1]
+def spinorX : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; 1, 0]
+def spinorZ : Matrix (Fin 2) (Fin 2) ℝ := !![1, 0; 0, -1]
+def spinorA : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; -1, 0]
+
+/-- Low / mid / high `Fin 2` digits of `i : Fin 8` (`8 = 2×2×2`, row-major). -/
+def fin8Lo (i : Fin 8) : Fin 2 :=
+  ⟨i.val % 2, Nat.mod_lt _ (by decide : 0 < 2)⟩
+
+def fin8Mid (i : Fin 8) : Fin 2 :=
+  ⟨(i.val / 2) % 2, Nat.mod_lt _ (by decide : 0 < 2)⟩
+
+def fin8Hi (i : Fin 8) : Fin 2 :=
+  ⟨i.val / 4, by omega⟩
+
+/-- Triple Kronecker product `A ⊗ B ⊗ C` (digit order matched to `numpy.kron`). -/
+noncomputable def spinorKron3 (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)
+
+/-- The six `γ` matrices, aligned with `cl06SixBasisVec 0,…,5`. -/
+noncomputable def cl06SpinorGammaMat : Fin 6 → Matrix (Fin 8) (Fin 8) ℝ
+  | ⟨0, _⟩ => spinorKron3 spinorA spinorIx spinorX
+  | ⟨1, _⟩ => spinorKron3 spinorA spinorIx spinorZ
+  | ⟨2, _⟩ => spinorKron3 spinorA spinorA spinorA
+  | ⟨3, _⟩ => spinorKron3 spinorIx spinorX spinorA
+  | ⟨4, _⟩ => spinorKron3 spinorIx spinorZ spinorA
+  | ⟨5, _⟩ => spinorKron3 spinorX spinorA spinorIx
+
+theorem quadFormCl06Six_apply (v : Fin 6 → ℝ) :
+    quadFormCl06Six v = -∑ i : Fin 6, v i * v i := by
+  classical
+  simp [quadFormCl06Six, weightedSumSquares_apply, Pi.smul_apply, smul_eq_mul, mul_assoc, neg_mul,
+    Finset.sum_neg_distrib]
+
+/-- `∑ₖ vₖ γₖ` as a linear map into matrices (Mathlib `Fintype.linearCombination`). -/
+noncomputable def cl06SpinorMatLin : (Fin 6 → ℝ) →ₗ[ℝ] Matrix (Fin 8) (Fin 8) ℝ :=
+  Fintype.linearCombination ℝ cl06SpinorGammaMat
+
+theorem cl06SixBasisVec_eq_piSingle (j : Fin 6) : cl06SixBasisVec j = Pi.single j (1 : ℝ) := by
+  funext k
+  by_cases h : k = j
+  · subst h
+    simp [cl06SixBasisVec, Pi.single_eq_same]
+  · simp [cl06SixBasisVec, h]
+
+set_option maxHeartbeats 800000 in
+theorem cl06SpinorMatLin_mul_self (v : Fin 6 → ℝ) :
+    cl06SpinorMatLin v * cl06SpinorMatLin v = (quadFormCl06Six v) • (1 : Matrix (Fin 8) (Fin 8) ℝ) := by
+  ext i j
+  simp_rw [Matrix.mul_apply, cl06SpinorMatLin, Fintype.linearCombination_apply, quadFormCl06Six_apply,
+    Matrix.smul_apply, Matrix.one_apply, smul_eq_mul]
+  fin_cases i <;> fin_cases j <;> (
+    simp [Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, cl06SpinorGammaMat, spinorKron3,
+      fin8Lo, fin8Mid, fin8Hi, spinorIx, spinorX, spinorZ, spinorA];
+    ring_nf)
+
+/-- Matrix algebra lift of `Cl(0,6)` for the standard spinor `γ` matrices. -/
+noncomputable def cl06StandardSpinorMatLift :
+    CliffordCl06Six →ₐ[ℝ] Matrix (Fin 8) (Fin 8) ℝ :=
+  CliffordAlgebra.lift quadFormCl06Six
+    ⟨cl06SpinorMatLin, fun w => by
+      rw [Algebra.algebraMap_eq_smul_one, cl06SpinorMatLin_mul_self]⟩
+
+/-- `Matrix (Fin 8) (Fin 8) ℝ ≃ₐ[ℝ] End(ℝ⁸)` for the standard basis. -/
+noncomputable abbrev cl06MatAlgEquiv : Matrix (Fin 8) (Fin 8) ℝ ≃ₐ[ℝ] Module.End ℝ OctonionSpinorCarrier :=
+  (algEquivMatrix' (R := ℝ) (n := Fin 8)).symm
+
+/-- Concrete spinor representation on `OctonionSpinorCarrier = Fin 8 → ℝ`. -/
+noncomputable def cl06StandardSpinorRho : CliffordCl06Six →ₐ[ℝ] Module.End ℝ OctonionSpinorCarrier :=
+  cl06MatAlgEquiv.toAlgHom.comp cl06StandardSpinorMatLift
+
+@[simp]
+theorem cl06StandardSpinorMatLift_ι (j : Fin 6) :
+    cl06StandardSpinorMatLift (CliffordAlgebra.ι quadFormCl06Six (cl06SixBasisVec j)) =
+      cl06SpinorGammaMat j := by
+  rw [cl06StandardSpinorMatLift, CliffordAlgebra.lift_ι_apply]
+  simp [cl06SpinorMatLin, cl06SixBasisVec_eq_piSingle, Fintype.linearCombination_apply_single,
+    one_smul]
+
+@[simp]
+theorem cl06StandardSpinorRho_ι (j : Fin 6) :
+    cl06StandardSpinorRho (CliffordAlgebra.ι quadFormCl06Six (cl06SixBasisVec j)) =
+      cl06MatAlgEquiv (cl06SpinorGammaMat j) := by
+  simp [cl06StandardSpinorRho, cl06StandardSpinorMatLift_ι]
+
+/-- Image of the full algebra under `ρ` (same as range of the underlying `ℝ`-linear map). -/
+noncomputable def cl06StandardSpinorRhoRange : Submodule ℝ (Module.End ℝ OctonionSpinorCarrier) :=
+  LinearMap.range cl06StandardSpinorRho.toLinearMap
+
+theorem cl06StandardSpinorRhoRange_finrank_le :
+    Module.finrank ℝ cl06StandardSpinorRhoRange ≤ 64 := by
+  have h := Submodule.finrank_le cl06StandardSpinorRhoRange
+  have hEnd : Module.finrank ℝ (Module.End ℝ OctonionSpinorCarrier) = 64 := by
+    simp [OctonionSpinorCarrier, Module.finrank_linearMap, Fintype.card_fin]
+  rw [hEnd] at h
+  exact h.trans (Nat.le_refl _)
+
+end Hqiv.Algebra