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

[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

[jstoobysmith]

Should be able to lift this to a CLM.

[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