From 580e44dca3083b554352fb776d8a4b8d60bdf9c7 Mon Sep 17 00:00:00 2001
From: ValentinBredemestre <valentin.bredemestre@agileeo.com>
Date: Sat, 17 Jan 2026 22:51:09 +0200
Subject: [PATCH] Introduce Z-prime charge assignments for Standard Model
 fermions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Introduce the key data structure for Z′-models over the Standard Model:
integer charge assignments for the chiral SM fermions with n families.

This provides a lightweight foundation for the Z′ API (issue #880), on which
family symmetries, anomaly cancellation conditions, and equivalence relations
will be built in subsequent work.
---
 .../StandardModel/ZPrime/Charges.lean         | 46 +++++++++++++++++++
 1 file changed, 46 insertions(+)
 create mode 100644 PhysLean/Particles/StandardModel/ZPrime/Charges.lean

diff --git a/PhysLean/Particles/StandardModel/ZPrime/Charges.lean b/PhysLean/Particles/StandardModel/ZPrime/Charges.lean
new file mode 100644
index 00000000..789b14f3
--- /dev/null
+++ b/PhysLean/Particles/StandardModel/ZPrime/Charges.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import Mathlib.Data.Int.Basic
+import Mathlib.Data.Fin.Basic
+/-!
+
+# Z-prime charges for the Standard Model
+
+This file introduces the key data structure for Z′-models over the Standard Model:
+the assignment of **integer** charges to the (chiral) SM fermions with `n` families.
+
+We model the SM fermions (without RHN) as `5` species (Q, U, D, L, E) each carrying
+`n` family copies. Thus a charge assignment is a function `Fin 5 → Fin n → ℤ`.
+
+This file is intentionally lightweight: it provides the underlying data structure and
+basic projections. Further API components (family permutations, potential-term charges,
+anomaly cancellation conditions, quotients by scaling/hypercharge) are developed in
+subsequent files/PRs.
+-/
+
+/-- Integer Z′-charges for the `n`-family Standard Model fermions (without RHN). -/
+abbrev SMZPrimeCharges (n : ℕ) : Type := Fin 5 → Fin n → ℤ
+
+namespace SMZPrimeCharges
+
+variable {n : ℕ}
+
+/-- The Q charges as a map `Fin n → ℤ`. -/
+abbrev Q (χ : SMZPrimeCharges n) : Fin n → ℤ := χ 0
+
+/-- The U charges as a map `Fin n → ℤ`. -/
+abbrev U (χ : SMZPrimeCharges n) : Fin n → ℤ := χ 1
+
+/-- The D charges as a map `Fin n → ℤ`. -/
+abbrev D (χ : SMZPrimeCharges n) : Fin n → ℤ := χ 2
+
+/-- The L charges as a map `Fin n → ℤ`. -/
+abbrev L (χ : SMZPrimeCharges n) : Fin n → ℤ := χ 3
+
+/-- The E charges as a map `Fin n → ℤ`. -/
+abbrev E (χ : SMZPrimeCharges n) : Fin n → ℤ := χ 4
+
+end SMZPrimeCharges