feat(SUSY/N1): add chiral scalar configuration space and coordinate CLMs

[pariandrea]

Motivation

This is the foundational layer of a formalization of the N=1 chiral scalar sector
in Physlib. The broader goal is to build the Wirtinger differential calculus on
complex field space — the ∂/∂φ^I and ∂/∂φ̄^I operators that underpin
supersymmetric and Kähler geometry — and ultimately a worked Kähler-geometry
application (the log Kähler potential on H^n and its metric).

Following review feedback on the larger branch, that work is being split into
reviewable pieces. This PR contributes only the basic data layer: the labels, the
configuration space, and the coordinate maps that everything downstream is built on.
It is fully self-contained over Mathlib, so it can be reviewed and merged
independently of the calculus that will follow.

What this adds

Physlib/SUSY/N1/Basic.lean:

• ChiralIndex — the label data of the chiral sector reduces to a single n : ℕ, the number of complex scalars. Chiral and anti-chiral indices share the one label
  set Fin n; in the scalar sector the bar is the identity, so no separate pairing is
  carried as data.
• ChiralScalarValue n = Fin n → ℂ — the physical scalar configuration space,
  carrying exactly 2n real degrees of freedom. Declared as an abbrev so Mathlib's
  α → ℂ calculus lemmas apply by unification.
• ChiralScalarValue.antiChiral — the anti-chiral view as the derived
  pointwise complex conjugate, not an independent input. Every φ̄ formula factors
  through this, keeping the configuration space physical and the 2n count honest.
• chiralCoordCLM I / antiChiralCoordCLM I — the per-coordinate projections
  z^I = u I and z̄^I = star (u I) as continuous ℝ-linear maps. Both are continuous
  and real-linear, but only chiralCoordCLM is ℂ-linear — antiChiralCoordCLM factors
  through conjugation and must live at the →L[ℝ] level.

[jstoobysmith]

I have two questions about this definition:

1. I think ChiralIndex might be the wrong name here, as an element of ChiralIndex is the number of chiral fields, whilst I think a chiral index is really an element of Fin n.
2. what stops you generalizing this to an arbitary Fintype, rather than Fin n?

I wonder if something like the following is better (I think discussed before):

structure Model (ChiralIndexingType : Type) [Fintype ChiralIndexingType] 
    (AntiChiralIndexingType : Type) [Fintype AntiChiralIndexingType] where
   equiv : ChiralIndexingType ≃ AntiChiralIndexingType

[pariandrea]

Adopted your suggestion: Model is now exactly that two-type structure.
The index types are arbitrary Type* with [Fintype …] now (not Fin n), and the
ChiralIndex name is gone. In the client files I write the two types as the shorter C /
A to keep signatures within the 100-col limit, with
a one-line note in the overview bridging the descriptive names to C / A.

[jstoobysmith]

I think ChiralScalarConfiguration would be a better name. Maybe add to the doc-string something like:
The term of this type gives a value to each of the chiral scalar fields.

[jstoobysmith]

I think you likely also need a type AntiChiralScalarConfiguration

[pariandrea]

Changed the name to ChiralScalarConfiguration as suggested.

I did not add an independent A → ℂ configuration as I think it's the wrong choice. The physical identities would then hold only where the anti-chiral field is the conjugate of the chiral one, so every theorem would carry 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 A is left as an index type only. We still keep distinct index
types to enforce the correct contraction rules, but there is a single field
configuration, avoiding a fictitious doubling of the physical DOF.

[jstoobysmith]

Should be able to lift this to a CLM.

[pariandrea]

CLM.lean is gone. Those CLMs aren't SUSY-specific, they're general operations on a
finite-index complex coordinate space C → ℂ — so rather than fold them into the SUSY
Basic.lean I moved them down into the Wirtinger calculus, where anything on C → ℂ
can reuse them:

• Basic.lean — the ℝ/ℂ scalar-restriction bridge plus the coordinate-basis CLMs and
  conjugation.
• Multivariable.lean — the directional Wirtinger derivatives and their full calculus
  (Leibniz, chain rule, conjugation, holomorphic collapse), capped by Schwarz's
  theorem.
• Coordinate.lean — the coordinate operators dWirtingerCoord /
  dWirtingerCoordBar, the projection/conjugation CLMs (coordProjCLM, conjCoordCLM,
  conjCLM), and coordinate Schwarz.
• UpperHalfPlane.lean — reusable upper-half-plane lemmas.

The full Wirtinger calculus can be seen in the larger PR #1107.

[doxtor6]

We already have Physlib.Particles.SuperSymmetry, maybe we should put it there? Also if it is about Wirtinger calculus, maybe we should put this PR in Physlib.Mathematics

[pariandrea]

Wirtinger calculus agreed, it's general complex analysis with no SUSY content, so in
the larger PR #1107 it already lives under Physlib/Mathematics/Calculus/Wirtinger/. (This PR is just the bite-sized Basic.lean split out of #1107.)

SUSY placement is a good point. The existing Physlib/Particles/SuperSymmetry/ is MSSM
anomaly cancellation (MSSMNu/) and SU(5)+U(1) charge spectra (SU5/). The work in #1107 is the other side of SUSY: the continuous scalar-sector geometry (Kähler potential and metric, holomorphic superpotential). It could probably be moved in N1/ subfolder.

[jstoobysmith]

I would change this to the following. It means you end up carrying around 'unused' variables, but I think it will help with the overall consistency.

namespace Model 

set_option linter.unusedVariables false in
/-- The chiral scalar configuration: an assignment of complex values to each
chiral label. An `abbrev` so unification applies Mathlib's `α → ℂ` calculus
lemmas directly. -/
@[nolint unusedArguments]
abbrev ChiralScalarConfiguration {ChiralIndexingType} (M : Model ChiralIndexingType) := ChiralIndexingType → ℂ

end Model

[pariandrea]

Thanks for the suggestion. I tried but it did not turn out easy to do.

ChiralScalarConfiguration is really just C → ℂ, so it only depends on the index type, not on a whole Model. Making it a Model method means the KahlerPotential/SuperPotential structures have to carry a model term they never use, and for concrete examples Lean then can't infer the index type on its own.

The concrete example is in the larger PR:

def K : KahlerPotential C -- current
def K : KahlerPotential model -- C hidden in model → Lean can't find it

I think this would be resolved by manual type annotations all over the place to compensate.
It is entirely possible that I am implementing the change naively and there is a cleaner way.

So I'd keep it as it is currently, and use the M. dot-notation for the operations that genuinely use the model (dChiralScalar, dAntiChiralScalar, metric). I am open to suggestions and happy to revisit this.

[jstoobysmith]

This looks good to me now. I think placing it in ./Particles/Supersymmetry might be better though (or at least making sure we have only one folder for SUSY - whether that is moving the stuff there or here).

[pariandrea]

I'll move the new code under Particles/SuperSymmetry/ rather than reorganize the existing SU5/MSSMNu files. Is Particles/SuperSymmetry/N1/ the correct path?

[jstoobysmith]

Yes please! After this - I think we're all good to go.

[doxtor6]

It looks good to me too.

[jstoobysmith]

Approved - will merge when linters pass. Many thanks.