From 098aa757b37d163c9bd6387f295a35b2e43b2685 Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Wed, 3 Jun 2026 10:18:25 +0100 Subject: [PATCH 1/2] =?UTF-8?q?feat(SUSY/N1):=20chiral=20sector=20indexing?= =?UTF-8?q?=20data=20=E2=80=94=20Model=20and=20configuration=20type?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduces the standalone indexing data of the N=1 chiral scalar sector: * `Model` — two finite index types (chiral / anti-chiral) related by an equivalence `equiv`, kept distinct so the two slots of a contraction `g_{IJ̄}` cannot be confused. * `ChiralScalarConfiguration` — the physical scalar configuration space `C → ℂ`, the only field data (no-doubling: anti-chiral scalars are its conjugates). This is the foundational file of the larger N=1 SUSY / Wirtinger development; it depends only on Mathlib. Co-Authored-By: Claude Opus 4.8 --- Physlib.lean | 1 + Physlib/SUSY/N1/Basic.lean | 88 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 89 insertions(+) create mode 100644 Physlib/SUSY/N1/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 16253fd8d..29b920281 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -368,6 +368,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic public import Physlib.Relativity.Tensors.TensorSpecies.Basic public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.UnitTensor +public import Physlib.SUSY.N1.Basic public import Physlib.SpaceAndTime.Space.Basic public import Physlib.SpaceAndTime.Space.ConstantSliceDist public import Physlib.SpaceAndTime.Space.CrossProduct diff --git a/Physlib/SUSY/N1/Basic.lean b/Physlib/SUSY/N1/Basic.lean new file mode 100644 index 000000000..ac99a6aeb --- /dev/null +++ b/Physlib/SUSY/N1/Basic.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Andrea Pari. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrea Pari +-/ +module + +public import Mathlib.Data.Fintype.Defs +public import Mathlib.Analysis.Complex.Basic +public import Mathlib.Logic.Equiv.Basic + +/-! + +# SUSY N=1 chiral sector — basic indexing data + +## i. Overview + +The minimal label and configuration data for the N=1 chiral sector. + +A `Model` packages two finite index types — `ChiralIndexingType` (written `C` +below) indexing the chiral scalars and `AntiChiralIndexingType` (written `A`) +the anti-chiral (barred) slots — with an equivalence `equiv : C ≃ A`, kept +distinct so the two slots of a contraction `g_{IJ̄}` cannot be confused. The +physical configuration is `ChiralScalarConfiguration C = C → ℂ`, carrying +`2 · Fintype.card C` real degrees of freedom — the only field data; the +anti-chiral scalars are its complex conjugates, never an independent +configuration. + +Doubling — adding an independent `A → ℂ` configuration — is the wrong choice: +the physical identities would then hold only where anti-chiral is the conjugate +of chiral, so every theorem carries that subspace as a hypothesis (e.g. the +Kähler potential is real only there, making hermiticity of `g_{IJ̄}` +conditional). Building the conjugate in keeps them unconditional — `K` is real +by construction — and leaves `A` an index type only. + +This file carries only the index/configuration data; the chiral and anti-chiral +derivatives `∂_I` / `∂_J̄` (the `Model` methods `M.dChiralScalar` / +`M.dAntiChiralScalar`) are built on top of it in `Derivative.lean`. + +The files of this `SUSY/N1/` folder: + +* `Basic.lean` (this file) — the `Model` indexing data and the chiral + configuration type. +* `Derivative.lean` — the chiral / anti-chiral derivative wrappers + `M.dChiralScalar` / `M.dAntiChiralScalar` over the Wirtinger calculus. +* `SuperPotential.lean` — the abstract holomorphic superpotential `W` and its + conjugate `W̄`. +* `KahlerPotential.lean` — the abstract Kähler potential `K`. +* `KahlerMetric.lean` — the Kähler metric `g_{IJ̄} = ∂_I ∂_J̄ K` and its + hermiticity. +* `LogKahlerHn.lean` — worked example: the `Hⁿ` log Kähler potential (the + reusable upper-half-plane calculus lives in + `Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean`). + +## ii. Key results + +- `SUSY.N1.Model` : the indexing data of an N=1 sector — a chiral index type, + an anti-chiral (barred) index type, and an equivalence `equiv` between them. +- `SUSY.N1.ChiralScalarConfiguration` : the physical scalar configuration space + `C → ℂ`, where `C` is the finite type indexing the chiral scalars — the only + field data in the sector. + +-/ + +@[expose] public section + +noncomputable section + +namespace SUSY.N1 + +/-- The indexing data of an N=1 sector: a chiral index type `ChiralIndexingType`, +an anti-chiral (barred) index type `AntiChiralIndexingType`, and a bijection +`equiv` between them. -/ +structure Model (ChiralIndexingType : Type*) [Fintype ChiralIndexingType] + (AntiChiralIndexingType : Type*) [Fintype AntiChiralIndexingType] where + /-- The correspondence between chiral and anti-chiral (barred) labels. -/ + equiv : ChiralIndexingType ≃ AntiChiralIndexingType + +/-- The chiral scalar configuration: an assignment of complex values to each +chiral label. An `abbrev` so unification applies Mathlib's `α → ℂ` calculus +lemmas directly. -/ +abbrev ChiralScalarConfiguration (ChiralIndexingType : Type*) := ChiralIndexingType → ℂ + +end SUSY.N1 + +end + +end From c4da0c21e52bb1d58bfa86aee3ad5550ec768ddc Mon Sep 17 00:00:00 2001 From: Andrea Pari Date: Thu, 4 Jun 2026 12:59:28 +0100 Subject: [PATCH 2/2] refactor(SUSY/N1): move chiral sector to Particles/SuperSymmetry/N1 Consolidate the N=1 chiral sector under the existing Particles/SuperSymmetry/ tree instead of a parallel top-level SUSY/ folder, per review feedback on #1113. The internal SUSY.N1 namespace is unchanged; only the file path and root import move. Co-Authored-By: Claude Opus 4.8 --- Physlib.lean | 2 +- Physlib/{SUSY => Particles/SuperSymmetry}/N1/Basic.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename Physlib/{SUSY => Particles/SuperSymmetry}/N1/Basic.lean (98%) diff --git a/Physlib.lean b/Physlib.lean index 29b920281..8993e4d0f 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -164,6 +164,7 @@ public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY3B3.ToSols public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Permutations public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.Y3 +public import Physlib.Particles.SuperSymmetry.N1.Basic public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions @@ -368,7 +369,6 @@ public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic public import Physlib.Relativity.Tensors.TensorSpecies.Basic public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.UnitTensor -public import Physlib.SUSY.N1.Basic public import Physlib.SpaceAndTime.Space.Basic public import Physlib.SpaceAndTime.Space.ConstantSliceDist public import Physlib.SpaceAndTime.Space.CrossProduct diff --git a/Physlib/SUSY/N1/Basic.lean b/Physlib/Particles/SuperSymmetry/N1/Basic.lean similarity index 98% rename from Physlib/SUSY/N1/Basic.lean rename to Physlib/Particles/SuperSymmetry/N1/Basic.lean index ac99a6aeb..268e506d5 100644 --- a/Physlib/SUSY/N1/Basic.lean +++ b/Physlib/Particles/SuperSymmetry/N1/Basic.lean @@ -37,7 +37,7 @@ This file carries only the index/configuration data; the chiral and anti-chiral derivatives `∂_I` / `∂_J̄` (the `Model` methods `M.dChiralScalar` / `M.dAntiChiralScalar`) are built on top of it in `Derivative.lean`. -The files of this `SUSY/N1/` folder: +The files of this `Particles/SuperSymmetry/N1/` folder: * `Basic.lean` (this file) — the `Model` indexing data and the chiral configuration type.