diff --git a/Physlib.lean b/Physlib.lean
index fcc24ff3c..f5730df15 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -67,6 +67,10 @@ public import Physlib.FluidDynamics.NavierStokes.Momentum
 public import Physlib.Mathematics.Calculus.AdjFDeriv
 public import Physlib.Mathematics.Calculus.Divergence
 public import Physlib.Mathematics.Calculus.ParametricIntegration
+public import Physlib.Mathematics.Calculus.Wirtinger.Basic
+public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
+public import Physlib.Mathematics.Calculus.Wirtinger.Multivariable
+public import Physlib.Mathematics.Calculus.Wirtinger.UpperHalfPlane
 public import Physlib.Mathematics.DataStructures.FourTree.Basic
 public import Physlib.Mathematics.DataStructures.FourTree.UniqueMap
 public import Physlib.Mathematics.DataStructures.Matrix.LieTrace
@@ -165,6 +169,11 @@ public import Physlib.Particles.SuperSymmetry.MSSMNu.AnomalyCancellation.OrthogY
 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.N1.Derivative
+public import Physlib.Particles.SuperSymmetry.N1.KahlerMetric
+public import Physlib.Particles.SuperSymmetry.N1.KahlerPotential
+public import Physlib.Particles.SuperSymmetry.N1.LogKahlerHn
+public import Physlib.Particles.SuperSymmetry.N1.SuperPotential
 public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.AllowsTerm
 public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Basic
 public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Completions
diff --git a/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean b/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
new file mode 100644
index 000000000..24260e3c5
--- /dev/null
+++ b/Physlib/Mathematics/Calculus/Wirtinger/Basic.lean
@@ -0,0 +1,143 @@
+/-
+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.Analysis.Calculus.FDeriv.Comp
+public import Mathlib.Analysis.Calculus.FDeriv.Linear
+public import Mathlib.Analysis.Complex.Basic
+
+/-!
+
+# Wirtinger calculus
+
+## Notation
+
+* The differentiation direction is a *subscript*: `∂_v f` and `∂̄_v f` are the holomorphic and
+  anti-holomorphic Wirtinger derivatives of `f` in direction `v`, splitting the total real
+  derivative `d_v f` (straight `d` for the total, `∂`/`∂̄` for the parts).
+* A `/∂` fraction differentiates with respect to a *variable*, not a direction: a real
+  coordinate `∂f/∂x`, or the argument of a one-variable function in the chain rule, `∂g/∂f`,
+  `∂g/∂f̄` (outer `g : ℂ → ℂ`, inner `f : V → ℂ`).
+* `f̄` is the pointwise conjugate `p ↦ conj (f p)`.
+
+## i. Overview
+
+The **Wirtinger calculus** differentiates complex functions `f` that need not
+be holomorphic, treating a variable and its conjugate as independent and
+replacing the complex derivative with a pair:
+
+- `∂_v f`  (`dWirtingerDir`), the holomorphic part along `v`;
+- `∂̄_v f` (`dWirtingerAntiDir`), the anti-holomorphic part along `v`,
+
+obtained by splitting the real derivative of `f` along `v` into its
+`ℂ`-linear and conjugate-linear parts. The split detects holomorphy:
+`∂̄_v f = 0` ⟺ Cauchy–Riemann holds along `v`, and then `∂_v f` is the ordinary
+complex derivative. The guiding example is a Kähler potential `K(φ, φ̄)`:
+real, non-holomorphic, no complex derivative, yet `∂K/∂φ` and `∂K/∂φ̄` are
+exactly what physics uses.
+
+The folder has three layers:
+
+- `Wirtinger.Basic` (this file), two algebraic lemmas feeding the calculus:
+  `realLinear_apply_eq_wirtinger` (the real-linear Wirtinger split) and
+  `fderiv_star_eq` (differentiation commutes with conjugation). Mathlib has
+  `fderiv ℂ` and `fderiv ℝ` but no Wirtinger pair, which is built on `fderiv ℝ`.
+- `Wirtinger.Multivariable`, the foundation: directional operators
+  `∂_v`, `∂̄_v` on `f : V → ℂ` for arbitrary `v : V`, with linearity,
+  Leibniz, chain rule, conjugations, holomorphic collapse, and **Schwarz's
+  theorem** `∂_v ∂̄_w f = ∂̄_w ∂_v f` (reduced to Mathlib's
+  `ContDiffAt.isSymmSndFDerivAt`). The directional form is forced by
+  Schwarz, which relates two *distinct* directions.
+- `Wirtinger.Coordinate`, the coordinate specialization to `V = ℂⁿ`
+  (spelled `ι → ℂ`, `n = |ι|`) along `v = Pi.single I 1`. Packages
+  `dWirtingerCoord`, `dWirtingerAntiCoord`, the projection/conjugation CLMs
+  (`coordProjCLM`, `conjCoordCLM`, `conjCLM`), the Pi-domain
+  `restrictScalars` bridge, and the coordinate forms of every result from
+  `Multivariable`, including Schwarz `∂_I ∂_J̄ f = ∂_J̄ ∂_I f`.
+
+The anti-holomorphic variable is written with `star`, matching Mathlib's
+`StarRing ℂ`.
+
+## ii. Key results
+
+- `Physlib.Wirtinger.realLinear_apply_eq_wirtinger` : the real-linear Wirtinger
+    decomposition `L w = a * w + b * star w` of any `L : ℂ →L[ℝ] ℂ`, the
+    key algebraic identity behind the Wirtinger chain rule.
+- `Physlib.Wirtinger.fderiv_star_eq` : the real derivative of a pointwise
+    conjugate `p ↦ star (f p)` is `conjCLE` composed with `fderiv ℝ f`.
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace Physlib.Wirtinger
+
+/-!
+
+## A. The real-linear Wirtinger decomposition
+
+Any real-linear map `ℂ →L[ℝ] ℂ` splits into a holomorphic and an
+anti-holomorphic part, with the Wirtinger coefficients as weights. Together
+with the derivative of a pointwise conjugate (`fderiv_star_eq`), this is the
+algebraic input to the chain rules. Both sit here, *below* the foundation, so
+the multivariable calculus can consume them directly.
+
+-/
+
+/-- Split a real-linear map `ℂ → ℂ` into its Wirtinger components. Any
+real-linear `L : ℂ →L[ℝ] ℂ` splits into a holomorphic and an anti-holomorphic part
+with the Wirtinger coefficients `a = ½(L 1 - i * L i)`, `b = ½(L 1 + i * L i)` as
+weights:
+
+  `L w = a * w + b * star w`.
+
+This is purely algebraic: `L` is an arbitrary real-linear map, no derivative
+involved. Its use is the Wirtinger chain rule (`dWirtingerDir_comp`, §D in
+`Multivariable`), where the weights of the outer differential `L = fderiv ℝ g (f u)`
+are the coefficients `∂g/∂f`, `∂g/∂f̄`. -/
+lemma realLinear_apply_eq_wirtinger (L : ℂ →L[ℝ] ℂ) (w : ℂ) :
+    L w =
+      ((1 / 2 : ℂ) * (L 1 - Complex.I * L Complex.I)) * w
+        + ((1 / 2 : ℂ) * (L 1 + Complex.I * L Complex.I)) * star w := by
+  calc
+    L w = L ((w.re : ℝ) • (1 : ℂ) + (w.im : ℝ) • Complex.I) := by
+              congr 1; apply Complex.ext <;> simp
+    _ = (w.re : ℝ) • L 1 + (w.im : ℝ) • L Complex.I := by
+          rw [map_add, map_smul, map_smul]
+    _ = ((1 / 2 : ℂ) * (L 1 - Complex.I * L Complex.I)) * w
+          + ((1 / 2 : ℂ) * (L 1 + Complex.I * L Complex.I)) * star w := by
+      apply Complex.ext <;>
+        simp [Complex.add_re, Complex.add_im, Complex.sub_re, Complex.sub_im,
+          Complex.mul_re, Complex.mul_im, Complex.conj_re, Complex.conj_im,
+          Complex.I_re, Complex.I_im] <;>
+        ring
+
+/-- Differentiation commutes with conjugation: the real Fréchet derivative of the
+pointwise conjugate `p ↦ star (f p)` is `conjCLE` (conjugation on `ℂ`) composed with
+`fderiv ℝ f u`; in physicists' notation, `d f̄ = conj(d f)`. Conjugation is `ℝ`-linear,
+so it slides through the real derivative unchanged, whereas it does *not* commute with
+the holomorphic Wirtinger derivative `∂_v`. The `star` conjugates the *output* `f p`,
+so this is not a derivative in a conjugate variable.
+
+This is the analytic core of the downstream conjugation lemmas
+(`dWirtingerDir_star_comp` and variants in `Multivariable`): distributed over the
+Wirtinger split of `fderiv ℝ f u` (`realLinear_apply_eq_wirtinger`), the outer `conjCLE`
+conjugates the two coefficients and swaps the holomorphic and anti-holomorphic parts. -/
+lemma fderiv_star_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+    {f : E → ℂ} {u : E} (hf : DifferentiableAt ℝ f u) :
+    fderiv ℝ (fun p : E => star (f p)) u =
+      Complex.conjCLE.toContinuousLinearMap.comp (fderiv ℝ f u) := by
+  rw [show (fun p : E => star (f p)) = Complex.conjCLE.toContinuousLinearMap ∘ f from rfl,
+    fderiv_comp u Complex.conjCLE.toContinuousLinearMap.differentiableAt hf,
+    ContinuousLinearMap.fderiv]
+
+end Physlib.Wirtinger
+
+end
+
+end
diff --git a/Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean b/Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean
new file mode 100644
index 000000000..55682b0be
--- /dev/null
+++ b/Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean
@@ -0,0 +1,776 @@
+/-
+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 Physlib.Mathematics.Calculus.Wirtinger.Multivariable
+public import Mathlib.Analysis.Calculus.FDeriv.Pi
+public import Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
+public import Mathlib.Data.Fintype.Defs
+
+/-!
+
+# Wirtinger calculus in a complex coordinate basis
+
+## i. Overview
+
+This module is the **coordinate specialization** of `Wirtinger.Multivariable` to
+`V = ℂ^n` (spelled `ι → ℂ`, `n = |ι|` for a `Fintype` index `ι`), with the
+direction `d` fixed to the I-th standard basis vector `Pi.single I 1`:
+
+  `∂f/∂z^I  := ∂f/∂d`   along `d = Pi.single I 1`   (`dWirtingerCoord`)
+  `∂f/∂z̄^I := ∂f/∂d̄`  along `d = Pi.single I 1`   (`dWirtingerAntiCoord`)
+
+These are the partial Wirtinger derivatives w.r.t. coordinate `I` with the
+others fixed — the form physics uses, and the form the N=1 SUSY layer consumes
+downstream (with `ι` its chiral index type). The `I = J` Kronecker behaviour
+`∂z^J/∂z^I = δ_IJ`, `∂z̄^J/∂z̄^I = δ_IJ`, `∂z^J/∂z̄^I = ∂z̄^J/∂z^I = 0`
+holds.
+
+The file packages:
+
+- the **coordinate operators** `dWirtingerCoord`, `dWirtingerAntiCoord` and
+  their real-Fréchet unfolding (§A);
+- the **projection / conjugation CLMs** `coordProjCLM`, `conjCoordCLM`,
+  `conjCLM`, with `conjCLM` conjugate-`ℂ`-linear (`conjCLM_smul_I`);
+- the **`ℝ`/`ℂ` `restrictScalars` bridges**: `hasFDerivAt_restrictScalarsℝℂ` for a
+  holomorphic outer `g : ℂ → ℂ`, and the Pi-domain bridge (§B) for the `(ι → ℂ)`
+  domain — both pay the codomain `IsScalarTower ℝ ℂ ℂ` diamond once, the latter
+  packaged so its projections keep `restrictScalars` out of every lemma type;
+- the **coordinate forms** of every result from `Multivariable`:
+  pointwise additivity, scalar compatibility, the Leibniz product rule,
+  finite-sum rule,
+  conjugation lemmas, the holomorphic / anti-holomorphic collapse, the
+  outer-function chain rules, and coordinate-difference helpers for
+  `z^J − z̄^J` (§C–E);
+- **Schwarz's theorem** for the coordinate operators (§F):
+
+      `∂_I ∂_J̄ f = ∂_J̄ ∂_I f`     (`dWirtingerCoord_dWirtingerAntiCoord_comm`)
+
+  the keystone of Kähler-metric hermiticity: with `K` real,
+  `g_{IJ̄} = ∂_I ∂_J̄ K` and `star (g_{JĪ}) = ∂_J̄ ∂_I K`, so hermiticity
+  *is* this commutation.
+
+Hypothesis-bearing rules are stated **pointwise** (at `u`, with
+`DifferentiableAt`) — the weakest form, suitable for functions differentiable
+only on a proper subdomain (e.g. a slit-domain log Kähler potential); a
+consumer wanting a function-level equation `funext`s locally. The
+hypothesis-free constant and coordinate facts are stated as function
+equalities.
+
+## ii. Key results
+
+- `Physlib.Wirtinger.dWirtingerCoord` / `dWirtingerAntiCoord` : the
+    coordinate Wirtinger operators, definitionally the directional operators
+    along `Pi.single I 1`.
+- `Physlib.Wirtinger.coordProjCLM` / `conjCoordCLM` / `conjCLM` : the
+    coordinate projection, the conjugated coordinate, and pointwise
+    conjugation as `ℝ`-linear CLMs; `conjCLM` is conjugate-`ℂ`-linear
+    (`conjCLM_smul_I`).
+- `Physlib.Wirtinger.hasFDerivAt_restrictScalarsℝℂ` : restrict a complex 1-D
+    Fréchet derivative on `ℂ → ℂ` to `ℝ`-scalars — the codomain bridge feeding a
+    holomorphic outer `g : ℂ → ℂ` into the chain rules.
+- `Physlib.Wirtinger.differentiableAt_real_of_complex` /
+    `fderivReal_apply_eq_complex` : the `ℝ`/`ℂ` `restrictScalars` Pi-domain
+    bridge, projected so no lemma type carries `restrictScalars`.
+- `Physlib.Wirtinger.dWirtingerCoord_coordProj` /
+    `dWirtingerAntiCoord_coordProj` / `dWirtingerCoord_conjCoord` /
+    `dWirtingerAntiCoord_conjCoord` : the four Kronecker coordinate values
+    `∂z^J/∂z^I = δ_IJ`, `∂z̄^J/∂z̄^I = δ_IJ`, `∂z^J/∂z̄^I = ∂z̄^J/∂z^I = 0`.
+- `Physlib.Wirtinger.dWirtingerCoord_eq_complex_fderiv` /
+    `dWirtingerAntiCoord_eq_zero_of_holomorphic` : holomorphic collapse for
+    the coordinate operators (with anti-holomorphic duals).
+- `Physlib.Wirtinger.dWirtingerCoord_comp_apply` /
+    `dWirtingerCoord_comp_holomorphic_apply` (and their anti-holomorphic duals): the
+    two-term Wirtinger chain rule for an outer `g : ℂ → ℂ`, collapsing to
+    the single-term `deriv g · ∂_I f` for holomorphic `g`.
+- `Physlib.Wirtinger.dWirtingerCoord_coordDiff` /
+    `dWirtingerAntiCoord_coordDiff` : Wirtinger derivatives of the
+    coordinate difference `z^J − z̄^J`.
+- `Physlib.Wirtinger.dWirtingerCoord_dWirtingerAntiCoord_comm` : Schwarz's
+    theorem for the coordinate operators, `∂_I ∂_J̄ f = ∂_J̄ ∂_I f` on
+    `C²` `f`.
+
+## iii. Table of contents
+
+- A. The coordinate Wirtinger operators
+- B. The Pi-domain `restrictScalars` bridge
+- C. Properties of `dWirtingerCoord`
+- D. Properties of `dWirtingerAntiCoord`
+- E. Wirtinger chain rules for an outer function
+- F. Schwarz's theorem for the coordinate operators
+
+-/
+
+@[expose] public section
+noncomputable section
+
+namespace Physlib.Wirtinger
+
+variable {ι : Type*}
+
+/-- Restrict a complex 1-D Fréchet derivative on `ℂ → ℂ` to `ℝ`-scalars: the
+codomain half of the `ℝ`/`ℂ` `restrictScalars` bridge, used to feed a holomorphic
+outer function `g : ℂ → ℂ` into the real-derivative chain rules (§E). -/
+lemma hasFDerivAt_restrictScalarsℝℂ {f : ℂ → ℂ} {f' : ℂ →L[ℂ] ℂ}
+    {z : ℂ} (hf : HasFDerivAt f f' z) :
+    HasFDerivAt f (f'.restrictScalars ℝ) z :=
+  -- The `@`-application is required: the shorthand `hf.restrictScalars ℝ` fails with
+  -- `failed to synthesize IsScalarTower ℝ ℂ ℂ`. There are two routes to `SMul ℝ ℂ`,
+  -- via `Algebra ℝ ℂ` and via `NormedSpace ℝ ℂ`; `restrictScalars` demands the
+  -- `NormedSpace` spelling while `IsScalarTower.right` supplies the `Algebra` one.
+  -- They are defeq but not syntactically equal, and instance search matches only
+  -- shallowly, so it fails; passing `IsScalarTower.right` positionally via `@` routes
+  -- the slot through unification, which sees the defeq and succeeds.
+  @HasFDerivAt.restrictScalars ℝ _ ℂ _ _
+    ℂ _ _ _ (IsScalarTower.right : IsScalarTower ℝ ℂ ℂ)
+    ℂ _ _ _ (IsScalarTower.right : IsScalarTower ℝ ℂ ℂ)
+    _ _ _ hf
+
+/-- The I-th coordinate `z^I = u I` as an ℝ-linear CLM on `ι → ℂ`. -/
+def coordProjCLM (I : ι) : (ι → ℂ) →L[ℝ] ℂ := ContinuousLinearMap.proj (R := ℝ) I
+
+@[simp] lemma coordProjCLM_apply (I : ι) (u : ι → ℂ) : coordProjCLM I u = u I := rfl
+
+/-- The conjugated I-th coordinate `z̄^I = star (u I)` as an ℝ-linear CLM (not ℂ-linear). -/
+def conjCoordCLM (I : ι) : (ι → ℂ) →L[ℝ] ℂ :=
+  Complex.conjCLE.toContinuousLinearMap.comp (coordProjCLM I)
+
+@[simp] lemma conjCoordCLM_apply (I : ι) (u : ι → ℂ) : conjCoordCLM I u = star (u I) := rfl
+
+/-- Pointwise conjugation of a point of `ι → ℂ`, as a plain function. -/
+def conjConfig (u : ι → ℂ) : ι → ℂ := fun I => star (u I)
+
+@[simp] lemma conjConfig_apply (u : ι → ℂ) (I : ι) : conjConfig u I = star (u I) := rfl
+
+/-- Pointwise conjugation bundled as an ℝ-linear CLM (conjugate-ℂ-linear). -/
+def conjCLM : (ι → ℂ) →L[ℝ] (ι → ℂ) :=
+  ContinuousLinearMap.pi (fun I => conjCoordCLM I)
+
+@[simp] lemma conjCLM_apply (u : ι → ℂ) : conjCLM u = conjConfig u := rfl
+
+/-- `conjCLM` is conjugate-ℂ-linear: `conj (i·d) = -(i · conj d)`. -/
+lemma conjCLM_smul_I (d : ι → ℂ) :
+    conjCLM (Complex.I • d) = -(Complex.I • conjCLM (ι := ι) d) := by
+  funext I
+  simp only [conjCLM_apply, conjConfig_apply, Pi.smul_apply, Pi.neg_apply,
+    smul_eq_mul, star_mul', Complex.star_def, Complex.conj_I]
+  ring
+
+/-!
+
+## A. The coordinate Wirtinger operators
+
+The two coordinate Wirtinger operators are the directional Wirtinger derivatives
+of `Wirtinger.Multivariable` along the I-th coordinate direction `Pi.single I 1`:
+
+  dWirtingerCoord f I    = (1/2) · (∂_x − i · ∂_y) f
+  dWirtingerAntiCoord f I = (1/2) · (∂_x + i · ∂_y) f
+
+where `∂_x` and `∂_y` are the real Fréchet derivatives of `f` along the slot-I
+real and imaginary coordinate directions `Pi.single I 1` and
+`Pi.single I Complex.I` (the latter is `Complex.I • Pi.single I 1`). The sign on
+the imaginary-direction term is the only difference, making the two operators
+dual on (anti)holomorphic functions (§C, §D).
+
+-/
+
+variable [Fintype ι] [DecidableEq ι]
+
+/-- Holomorphic Wirtinger derivative along the I-th coordinate of `ι → ℂ`. -/
+def dWirtingerCoord (f : (ι → ℂ) → ℂ) (I : ι) : (ι → ℂ) → ℂ :=
+  fun u => dWirtingerDir f (Pi.single I 1) u
+
+/-- Anti-holomorphic Wirtinger derivative along the I-th coordinate of `ι → ℂ`. -/
+def dWirtingerAntiCoord (f : (ι → ℂ) → ℂ) (I : ι) : (ι → ℂ) → ℂ :=
+  fun u => dWirtingerAntiDir f (Pi.single I 1) u
+
+omit [Fintype ι] in
+/-- `c • Pi.single I 1 = Pi.single I c`: in particular the imaginary coordinate
+direction `Pi.single I i` is `i` times the real one. -/
+private lemma smul_single_one (I : ι) (c : ℂ) :
+    c • (Pi.single I 1 : (ι → ℂ)) = Pi.single I c := by
+  rw [← Pi.single_smul', smul_eq_mul, mul_one]
+
+/-- The coordinate operators are the directional Wirtinger derivatives along the
+coordinate direction `Pi.single I 1` (definitional). -/
+lemma dWirtingerCoord_eq_dWirtingerDir (f : (ι → ℂ) → ℂ) (I : ι)
+    (u : (ι → ℂ)) :
+    dWirtingerCoord f I u = dWirtingerDir f (Pi.single I 1) u := rfl
+
+/-- The anti-holomorphic coordinate operator is the anti-holomorphic directional Wirtinger
+derivative along `Pi.single I 1` (definitional). -/
+lemma dWirtingerAntiCoord_eq_dWirtingerAntiDir (f : (ι → ℂ) → ℂ)
+    (I : ι)
+    (u : (ι → ℂ)) :
+    dWirtingerAntiCoord f I u = dWirtingerAntiDir f (Pi.single I 1) u := rfl
+
+/-- Real-Fréchet form of `dWirtingerCoord`:
+`dWirtingerCoord f I u = (1/2)(∂_x − i · ∂_y) f`,
+the derivatives along the slot-I real and imaginary coordinate directions.
+Unconditional — the directional definition makes it definitional
+(`Complex.I • Pi.single I 1 = Pi.single I Complex.I`); no differentiability
+hypothesis is needed. -/
+lemma dWirtingerCoord_apply {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (I : ι) :
+    dWirtingerCoord f I u = (1 / 2 : ℂ) * (fderiv ℝ f u (Pi.single I 1)
+      - Complex.I * fderiv ℝ f u (Pi.single I Complex.I)) := by
+  simp only [dWirtingerCoord, dWirtingerDir, smul_single_one]
+
+/-- Real-Fréchet form of `dWirtingerAntiCoord`; mirror of `dWirtingerCoord_apply` with the
+sign flip on the imaginary-direction term. Unconditional, as for `dWirtingerCoord_apply`. -/
+lemma dWirtingerAntiCoord_apply {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (I : ι) :
+    dWirtingerAntiCoord f I u = (1 / 2 : ℂ) * (fderiv ℝ f u (Pi.single I 1)
+      + Complex.I * fderiv ℝ f u (Pi.single I Complex.I)) := by
+  simp only [dWirtingerAntiCoord, dWirtingerAntiDir, smul_single_one]
+
+/-!
+
+## B. The Pi-domain restrictScalars bridge
+
+The holomorphic collapse needs `ℂ`-linearity of the *real* Fréchet derivative,
+which on the `ι → ℂ` domain meets the `ℝ`/`ℂ` `restrictScalars` diamond. The
+private bridge `differentiableAt_real_and_fderiv_eq` pays the `@`-application
+ceremony once, with clean conclusions (no `restrictScalars` in any lemma type).
+
+-/
+
+omit [DecidableEq ι] in
+/-- The `ℝ`/`ℂ` `restrictScalars` bridge on the `ι → ℂ` domain, paid once and
+packaged so that `restrictScalars` stays out of every lemma *type*: stating it in
+a type re-triggers the codomain `IsScalarTower ℝ ℂ ℂ` module diamond (see
+`hasFDerivAt_restrictScalarsℝℂ`), and only a `have`-inferred occurrence is diamond-free. The
+`@`-application ceremony lives here; `differentiableAt_real_of_complex` and
+`fderivReal_apply_eq_complex` project out its two halves. -/
+private lemma differentiableAt_real_and_fderiv_eq {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (hf : DifferentiableAt ℂ f u) :
+    DifferentiableAt ℝ f u ∧ ∀ d, fderiv ℝ f u d = fderiv ℂ f u d := by
+  have hfr := @HasFDerivAt.restrictScalars ℝ _ ℂ _ _
+    ((ι → ℂ)) _ _ _
+      (inferInstance : IsScalarTower ℝ ℂ ((ι → ℂ)))
+    ℂ _ _ _ (IsScalarTower.right : IsScalarTower ℝ ℂ ℂ) _ _ _ hf.hasFDerivAt
+  exact ⟨hfr.differentiableAt,
+    fun d => by simp only [hfr.fderiv, ContinuousLinearMap.coe_restrictScalars']⟩
+
+omit [DecidableEq ι] in
+/-- A `ℂ`-differentiable function on `(ι → ℂ)` is
+`ℝ`-differentiable. -/
+lemma differentiableAt_real_of_complex {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (hf : DifferentiableAt ℂ f u) :
+    DifferentiableAt ℝ f u :=
+  (differentiableAt_real_and_fderiv_eq hf).1
+
+omit [DecidableEq ι] in
+/-- The real Fréchet derivative of a holomorphic function equals its complex one,
+pointwise — the single rewrite the collapse-family lemmas consume. -/
+lemma fderivReal_apply_eq_complex {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (hf : DifferentiableAt ℂ f u)
+    (d : (ι → ℂ)) :
+    fderiv ℝ f u d = fderiv ℂ f u d :=
+  (differentiableAt_real_and_fderiv_eq hf).2 d
+
+omit [DecidableEq ι] in
+/-- The real derivative of a holomorphic function is `ℂ`-linear along every
+direction — the hypothesis the foundation collapse `dWirtingerDir_eq_of_clinear`
+consumes, produced at the `ι → ℂ` domain through the bridge. -/
+private lemma clinear_of_holomorphic {f : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (hf : DifferentiableAt ℂ f u)
+    (d : (ι → ℂ)) :
+    fderiv ℝ f u (Complex.I • d) = Complex.I • fderiv ℝ f u d := by
+  rw [fderivReal_apply_eq_complex hf (Complex.I • d), fderivReal_apply_eq_complex hf d, map_smul]
+
+omit [Fintype ι] in
+/-- `conjConfig` fixes the real coordinate direction `Pi.single I 1` (since `star 1 = 1`). -/
+private lemma conjConfig_single_one (I : ι) :
+    conjConfig (Pi.single I (1 : ℂ)) = Pi.single I 1 := by
+  funext J
+  rw [conjConfig_apply]
+  rcases eq_or_ne J I with h | h
+  · subst h; rw [Pi.single_eq_same]; exact star_one ℂ
+  · rw [Pi.single_eq_of_ne h]; exact star_zero ℂ
+
+omit [DecidableEq ι] [Fintype ι] in
+/-- The real Fréchet derivative of the J-th coordinate projection `v ↦ v J`. -/
+private lemma fderiv_coordProj (J : ι) (u d : (ι → ℂ)) :
+    fderiv ℝ (fun v : (ι → ℂ) => v J) u d = d J := by
+  have h : HasFDerivAt (fun v : (ι → ℂ) => v J)
+      (coordProjCLM J) u :=
+    (coordProjCLM J).hasFDerivAt
+  rw [h.fderiv, coordProjCLM_apply]
+
+/-!
+
+## C. Properties of `dWirtingerCoord`
+
+Each rule is the `d = Pi.single I 1` specialisation of its `Wirtinger`
+foundation analogue. Rules carrying a differentiability hypothesis are stated
+**pointwise** (at `u`, hypothesis `DifferentiableAt`) — the weakest form, and the
+one to reach for on a function differentiable only on a proper domain (e.g. the
+`Hⁿ` log Kähler potential, regular only on its slit domain); a consumer wanting
+a function-level equation `funext`s locally. The hypothesis-free constant and
+coordinate facts are stated as function equalities — the constant and
+holomorphic-coordinate ones (`dWirtingerCoord_const`, `dWirtingerCoord_coordProj`) `@[simp]`.
+
+-/
+
+section
+
+variable {f g : (ι → ℂ) → ℂ}
+
+/-- `dWirtingerCoord` is local: functions agreeing on a neighbourhood of `u` have equal
+holomorphic Wirtinger derivative at `u`. -/
+lemma dWirtingerCoord_congr_of_eventuallyEq_apply {f₁ f₂ : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (h : f₁ =ᶠ[nhds u] f₂) (I : ι) :
+    dWirtingerCoord f₁ I u = dWirtingerCoord f₂ I u :=
+  dWirtingerDir_congr_of_eventuallyEq h (Pi.single I 1)
+
+/-- Constants have zero coordinate derivative. -/
+@[simp] lemma dWirtingerCoord_const (c : ℂ) (I : ι) :
+    dWirtingerCoord (fun _ : (ι → ℂ) => c) I = 0 := by
+  funext u; exact dWirtingerDir_const c (Pi.single I 1) u
+
+/-- The zero function has zero coordinate derivative. -/
+@[simp] lemma dWirtingerCoord_zero (I : ι) :
+    dWirtingerCoord (0 : (ι → ℂ) → ℂ) I = 0 :=
+  dWirtingerCoord_const 0 I
+
+/-- Pointwise negation rule for the holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerCoord_neg_apply {u : (ι → ℂ)} (I : ι) :
+    dWirtingerCoord (fun v => -(f v)) I u = -(dWirtingerCoord f I u) :=
+  dWirtingerDir_neg f (Pi.single I 1) u
+
+/-- `∂z^J / ∂z^I = δ_IJ`. -/
+@[simp] lemma dWirtingerCoord_coordProj (I J : ι) :
+    dWirtingerCoord (fun u : (ι → ℂ) => u J) I =
+      fun _ => if I = J then 1 else 0 := by
+  funext u
+  rw [dWirtingerCoord_apply I, fderiv_coordProj, fderiv_coordProj]
+  by_cases h : I = J
+  · subst h; rw [Pi.single_eq_same, Pi.single_eq_same, if_pos rfl, Complex.I_mul_I]; ring
+  · rw [Pi.single_eq_of_ne (Ne.symm h), Pi.single_eq_of_ne (Ne.symm h), if_neg h,
+      mul_zero, sub_zero, mul_zero]
+
+/-- Pointwise additivity of the holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerCoord_add_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (hg : DifferentiableAt ℝ g u) (I : ι) :
+    dWirtingerCoord (f + g) I u = dWirtingerCoord f I u + dWirtingerCoord g I u :=
+  dWirtingerDir_add hf hg (Pi.single I 1)
+
+/-- Pointwise compatibility with complex scalar multiplication at `u`. -/
+lemma dWirtingerCoord_smul_apply {u : (ι → ℂ)}
+    (c : ℂ) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerCoord (c • f) I u = c • dWirtingerCoord f I u :=
+  dWirtingerDir_smul c hf (Pi.single I 1)
+
+/-- Pointwise Leibniz rule for the holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerCoord_mul_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (hg : DifferentiableAt ℝ g u) (I : ι) :
+    dWirtingerCoord (f * g) I u =
+      dWirtingerCoord f I u * g u + f u * dWirtingerCoord g I u :=
+  dWirtingerDir_mul hf hg (Pi.single I 1)
+
+/-- Pointwise finite-sum rule for holomorphic coordinate derivatives at `u`. -/
+lemma dWirtingerCoord_fun_sum_apply {α : Type*} {s : Finset α}
+    {F : α → (ι → ℂ) → ℂ} {u : (ι → ℂ)}
+    (hF : ∀ a ∈ s, DifferentiableAt ℝ (F a) u) (I : ι) :
+    dWirtingerCoord (fun v => ∑ a ∈ s, F a v) I u =
+      ∑ a ∈ s, dWirtingerCoord (F a) I u :=
+  dWirtingerDir_fun_sum hF (Pi.single I 1)
+
+/-- For a holomorphic function, `dWirtingerCoord` is the complex Fréchet derivative in
+the corresponding coordinate direction. -/
+lemma dWirtingerCoord_eq_complex_fderiv_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℂ f u) (I : ι) :
+    dWirtingerCoord f I u = fderiv ℂ f u (Pi.single I 1) := by
+  show dWirtingerDir f (Pi.single I 1) u = fderiv ℂ f u (Pi.single I 1)
+  rw [dWirtingerDir_eq_of_clinear (clinear_of_holomorphic hf _), fderivReal_apply_eq_complex hf]
+
+/-- Global version of `dWirtingerCoord_eq_complex_fderiv_apply`. -/
+lemma dWirtingerCoord_eq_complex_fderiv (hf : Differentiable ℂ f) (I : ι) :
+    dWirtingerCoord f I = fun u => fderiv ℂ f u (Pi.single I 1) := by
+  funext u; exact dWirtingerCoord_eq_complex_fderiv_apply (hf u) I
+
+/-- An antiholomorphic function — a ℂ-differentiable `g` precomposed with
+`conjConfig` — has zero holomorphic Wirtinger derivative at `u`. -/
+lemma dWirtingerCoord_eq_zero_of_antiHolomorphic_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℂ g (conjConfig u)) (I : ι) :
+    dWirtingerCoord (fun v : (ι → ℂ) => g (conjConfig v)) I u = 0 := by
+  have hgr : DifferentiableAt ℝ g (conjCLM u) := by
+    rw [conjCLM_apply]; exact differentiableAt_real_of_complex hg
+  show dWirtingerDir (fun v : (ι → ℂ) => g (conjConfig v))
+      (Pi.single I 1) u = 0
+  rw [show (fun v : (ι → ℂ) => g (conjConfig v))
+      = fun v => g (conjCLM v) from by funext v; rw [conjCLM_apply],
+    dWirtingerDir_comp_conjLinear conjCLM_smul_I hgr]
+  simp only [conjCLM_apply]
+  exact dWirtingerAntiDir_eq_zero_of_clinear (clinear_of_holomorphic hg _)
+
+/-- Antiholomorphic functions have zero holomorphic Wirtinger derivative. -/
+lemma dWirtingerCoord_eq_zero_of_antiHolomorphic (hg : Differentiable ℂ g) (I : ι) :
+    dWirtingerCoord (fun u : (ι → ℂ) => g (conjConfig u)) I = 0 := by
+  funext u; exact dWirtingerCoord_eq_zero_of_antiHolomorphic_apply (hg (conjConfig u)) I
+
+end
+
+/-!
+
+## D. Properties of `dWirtingerAntiCoord`
+
+`dWirtingerAntiCoord` mirrors `dWirtingerCoord` with `z` and `z̄` swapped. The two anti-coordinate
+values `∂z̄^J/∂z^I` (`dWirtingerCoord_conjCoord`) and `∂z̄^J/∂z̄^I`
+(`dWirtingerAntiCoord_conjCoord`) are collected here — one for each operator — since
+both are conjugates of the §C holomorphic-coordinate values (`z̄^J = star z^J`), read
+off through `dWirtingerDir` / `dWirtingerAntiDir_star_comp`.
+
+-/
+
+section
+
+variable {f g : (ι → ℂ) → ℂ}
+
+/-- `dWirtingerAntiCoord` is local. -/
+lemma dWirtingerAntiCoord_congr_of_eventuallyEq_apply {f₁ f₂ : (ι → ℂ) → ℂ}
+    {u : (ι → ℂ)} (h : f₁ =ᶠ[nhds u] f₂) (I : ι) :
+    dWirtingerAntiCoord f₁ I u = dWirtingerAntiCoord f₂ I u :=
+  dWirtingerAntiDir_congr_of_eventuallyEq h (Pi.single I 1)
+
+/-- Constants have zero anti-holomorphic coordinate derivative. -/
+@[simp] lemma dWirtingerAntiCoord_const (c : ℂ) (I : ι) :
+    dWirtingerAntiCoord (fun _ : (ι → ℂ) => c) I = 0 := by
+  funext u; exact dWirtingerAntiDir_const c (Pi.single I 1) u
+
+/-- The zero function has zero anti-holomorphic coordinate derivative. -/
+@[simp] lemma dWirtingerAntiCoord_zero (I : ι) :
+    dWirtingerAntiCoord (0 : (ι → ℂ) → ℂ) I = 0 :=
+  dWirtingerAntiCoord_const 0 I
+
+/-- Pointwise negation rule for the anti-holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerAntiCoord_neg_apply {u : (ι → ℂ)} (I : ι) :
+    dWirtingerAntiCoord (fun v => -(f v)) I u = -(dWirtingerAntiCoord f I u) :=
+  dWirtingerAntiDir_neg f (Pi.single I 1) u
+
+/-- `∂z^J / ∂z̄^I = 0`. -/
+@[simp] lemma dWirtingerAntiCoord_coordProj (I J : ι) :
+    dWirtingerAntiCoord (fun u : (ι → ℂ) => u J) I = 0 := by
+  funext u
+  simp only [Pi.zero_apply]
+  rw [dWirtingerAntiCoord_apply I, fderiv_coordProj, fderiv_coordProj]
+  by_cases h : I = J
+  · subst h; rw [Pi.single_eq_same, Pi.single_eq_same, Complex.I_mul_I]; ring
+  · rw [Pi.single_eq_of_ne (Ne.symm h), Pi.single_eq_of_ne (Ne.symm h),
+      mul_zero, add_zero, mul_zero]
+
+/-- `∂z̄^J / ∂z^I = 0`. The conjugate of `dWirtingerAntiCoord_coordProj` (`z̄^J = star z^J`),
+read off through `dWirtingerDir_star_comp` rather than recomputed. -/
+lemma dWirtingerCoord_conjCoord (I J : ι) :
+    dWirtingerCoord (fun u : (ι → ℂ) => conjConfig u J) I = 0 := by
+  funext u
+  have hd : DifferentiableAt ℝ (fun w : (ι → ℂ) => w J) u :=
+    (coordProjCLM J).differentiableAt
+  change dWirtingerDir (fun v => star ((fun w : (ι → ℂ) => w J) v))
+      (Pi.single I 1) u = 0
+  rw [dWirtingerDir_star_comp hd (Pi.single I 1), ← dWirtingerAntiCoord_eq_dWirtingerAntiDir,
+    dWirtingerAntiCoord_coordProj, Pi.zero_apply, star_zero]
+
+/-- `∂z̄^J / ∂z̄^I = δ_IJ`. The conjugate of `dWirtingerCoord_coordProj`, read off through
+`dWirtingerAntiDir_star_comp` rather than recomputed. -/
+lemma dWirtingerAntiCoord_conjCoord (I J : ι) :
+    dWirtingerAntiCoord (fun u : (ι → ℂ) => conjConfig u J) I =
+      fun _ => if I = J then 1 else 0 := by
+  funext u
+  have hd : DifferentiableAt ℝ (fun w : (ι → ℂ) => w J) u :=
+    (coordProjCLM J).differentiableAt
+  change dWirtingerAntiDir (fun v => star ((fun w : (ι → ℂ) => w J) v))
+      (Pi.single I 1) u = if I = J then 1 else 0
+  rw [dWirtingerAntiDir_star_comp hd (Pi.single I 1), ← dWirtingerCoord_eq_dWirtingerDir,
+    dWirtingerCoord_coordProj]
+  simp only [apply_ite (star : ℂ → ℂ), star_one, star_zero]
+
+/-- Pointwise additivity of the anti-holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerAntiCoord_add_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (hg : DifferentiableAt ℝ g u) (I : ι) :
+    dWirtingerAntiCoord (f + g) I u = dWirtingerAntiCoord f I u + dWirtingerAntiCoord g I u :=
+  dWirtingerAntiDir_add hf hg (Pi.single I 1)
+
+/-- Pointwise compatibility with complex scalar multiplication at `u`. -/
+lemma dWirtingerAntiCoord_smul_apply {u : (ι → ℂ)}
+    (c : ℂ) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerAntiCoord (c • f) I u = c • dWirtingerAntiCoord f I u :=
+  dWirtingerAntiDir_smul c hf (Pi.single I 1)
+
+/-- Pointwise Leibniz rule for the anti-holomorphic coordinate derivative at `u`. -/
+lemma dWirtingerAntiCoord_mul_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (hg : DifferentiableAt ℝ g u) (I : ι) :
+    dWirtingerAntiCoord (f * g) I u =
+      dWirtingerAntiCoord f I u * g u + f u * dWirtingerAntiCoord g I u :=
+  dWirtingerAntiDir_mul hf hg (Pi.single I 1)
+
+/-- Pointwise finite-sum rule for anti-holomorphic coordinate derivatives at `u`. -/
+lemma dWirtingerAntiCoord_fun_sum_apply {α : Type*} {s : Finset α}
+    {F : α → (ι → ℂ) → ℂ} {u : (ι → ℂ)}
+    (hF : ∀ a ∈ s, DifferentiableAt ℝ (F a) u) (I : ι) :
+    dWirtingerAntiCoord (fun v => ∑ a ∈ s, F a v) I u =
+      ∑ a ∈ s, dWirtingerAntiCoord (F a) I u :=
+  dWirtingerAntiDir_fun_sum hF (Pi.single I 1)
+
+/-!
+
+### Coordinate-difference Wirtinger derivatives
+
+The Wirtinger derivatives of the coordinate difference `z^J − z̄^J`. This
+expression is the imaginary part of a coordinate up to a factor of
+`i`: `z^J − z̄^J = 2 i Im(u^J)`, so any function built from `Im` of the
+coordinates eventually differentiates against it. Collecting the four lemmas
+here saves every such consumer from re-running the same additivity chain by hand
+— `{dWirtingerCoord,dWirtingerAntiCoord}_add_apply`, the pointwise
+`{dWirtingerCoord,dWirtingerAntiCoord}_neg_apply`, and the §C/§D coordinate values
+(`dWirtingerCoord_coordProj` / `dWirtingerCoord_conjCoord` and their anti-holomorphic duals).
+
+-/
+
+omit [DecidableEq ι] in
+/-- The coordinate-difference function `v ↦ z^J − z̄^J` is real-differentiable:
+the difference of the coordinate CLMs `coordProjCLM J` and `conjCoordCLM J`. -/
+lemma differentiable_coordDiff (J : ι) :
+    Differentiable ℝ (fun v : (ι → ℂ) => v J - conjConfig v J) :=
+  (coordProjCLM J).differentiable.sub (conjCoordCLM J).differentiable
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- The coordinate difference `z^J − z̄^J` as a sum of the holomorphic coordinate
+and the negated conjugate coordinate — the form on which the `dWirtingerCoord` /
+`dWirtingerAntiCoord` additivity rules apply. -/
+private lemma coordDiff_eq_add_neg (J : ι) :
+    (fun v : (ι → ℂ) => v J - conjConfig v J)
+      = (fun v => v J) + (fun v => -(conjConfig v J)) := by
+  funext v; simp [sub_eq_add_neg]
+
+/-- `∂(z^J − z̄^J) / ∂z^I = δ_IJ`, from `∂z^J/∂z^I = δ_IJ` and
+`∂z̄^J/∂z^I = 0`. -/
+lemma dWirtingerCoord_coordDiff (I J : ι) :
+    dWirtingerCoord (fun v : (ι → ℂ) => v J - conjConfig v J) I
+      = fun _ => if I = J then 1 else 0 := by
+  funext u
+  have hchi : DifferentiableAt ℝ (fun v : (ι → ℂ) => v J) u :=
+    (coordProjCLM J).differentiableAt
+  have hneganti : DifferentiableAt ℝ
+      (fun v : (ι → ℂ) => -(conjConfig v J)) u :=
+    (conjCoordCLM J).differentiableAt.neg
+  rw [coordDiff_eq_add_neg, dWirtingerCoord_add_apply hchi hneganti I, dWirtingerCoord_neg_apply I,
+    dWirtingerCoord_coordProj, dWirtingerCoord_conjCoord]
+  simp
+
+/-- `∂(z^J − z̄^J) / ∂z̄^I = −δ_IJ`, from `∂z^J/∂z̄^I = 0` and
+`∂z̄^J/∂z̄^I = δ_IJ`. -/
+lemma dWirtingerAntiCoord_coordDiff (I J : ι) :
+    dWirtingerAntiCoord (fun v : (ι → ℂ) => v J - conjConfig v J) I
+      = fun _ => if I = J then -1 else 0 := by
+  funext u
+  have hchi : DifferentiableAt ℝ (fun v : (ι → ℂ) => v J) u :=
+    (coordProjCLM J).differentiableAt
+  have hneganti : DifferentiableAt ℝ
+      (fun v : (ι → ℂ) => -(conjConfig v J)) u :=
+    (conjCoordCLM J).differentiableAt.neg
+  rw [coordDiff_eq_add_neg, dWirtingerAntiCoord_add_apply hchi hneganti I,
+    dWirtingerAntiCoord_neg_apply I, dWirtingerAntiCoord_coordProj, dWirtingerAntiCoord_conjCoord]
+  by_cases h : I = J <;> simp [h]
+
+/-- For an antiholomorphic function the anti-holomorphic Wirtinger derivative equals
+the complex Fréchet derivative of `g` at `conjConfig u` along the slot-I real
+coordinate direction. Dual of `dWirtingerCoord_eq_complex_fderiv_apply`. -/
+lemma dWirtingerAntiCoord_eq_complex_fderiv_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℂ g (conjConfig u)) (I : ι) :
+    dWirtingerAntiCoord (fun v : (ι → ℂ) => g (conjConfig v)) I u =
+      fderiv ℂ g (conjConfig u) (Pi.single I 1) := by
+  have hgr : DifferentiableAt ℝ g (conjCLM u) := by
+    rw [conjCLM_apply]; exact differentiableAt_real_of_complex hg
+  show dWirtingerAntiDir (fun v : (ι → ℂ) => g (conjConfig v))
+      (Pi.single I 1) u = fderiv ℂ g (conjConfig u) (Pi.single I 1)
+  rw [show (fun v : (ι → ℂ) => g (conjConfig v))
+      = fun v => g (conjCLM v) from by funext v; rw [conjCLM_apply],
+    dWirtingerAntiDir_comp_conjLinear conjCLM_smul_I hgr]
+  simp only [conjCLM_apply, conjConfig_single_one]
+  rw [dWirtingerDir_eq_of_clinear (clinear_of_holomorphic hg _), fderivReal_apply_eq_complex hg]
+
+/-- Global version of `dWirtingerAntiCoord_eq_complex_fderiv_apply`. -/
+lemma dWirtingerAntiCoord_eq_complex_fderiv (hg : Differentiable ℂ g) (I : ι) :
+    dWirtingerAntiCoord (fun u : (ι → ℂ) => g (conjConfig u)) I =
+      fun u => fderiv ℂ g (conjConfig u) (Pi.single I 1) := by
+  funext u; exact dWirtingerAntiCoord_eq_complex_fderiv_apply (hg (conjConfig u)) I
+
+/-- Holomorphic functions have zero anti-holomorphic coordinate derivative. -/
+lemma dWirtingerAntiCoord_eq_zero_of_holomorphic_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℂ f u) (I : ι) :
+    dWirtingerAntiCoord f I u = 0 := by
+  show dWirtingerAntiDir f (Pi.single I 1) u = 0
+  exact dWirtingerAntiDir_eq_zero_of_clinear (clinear_of_holomorphic hf _)
+
+/-- Global version of `dWirtingerAntiCoord_eq_zero_of_holomorphic_apply`. -/
+lemma dWirtingerAntiCoord_eq_zero_of_holomorphic (hf : Differentiable ℂ f) (I : ι) :
+    dWirtingerAntiCoord f I = 0 := by
+  funext u; exact dWirtingerAntiCoord_eq_zero_of_holomorphic_apply (hf u) I
+
+end
+
+/-!
+
+## E. Wirtinger chain rules for an outer function
+
+The Wirtinger chain rules for the coordinate operators composed with a complex outer
+function `g : ℂ → ℂ`, each the `d = Pi.single I 1` case of the foundation chain
+rule. The outer `g` enters only through its directional derivatives
+`dWirtingerDir g 1` / `dWirtingerAntiDir g 1`.
+
+Those two numbers are the holomorphic and anti-holomorphic parts of `g`'s real Fréchet
+derivative: every real-linear map `ℂ → ℂ` decomposes uniquely as
+`h ↦ a · h + b · star h`, and at `z = f u` (the image of `u` under the inner
+function, where the chain rule evaluates `g`'s derivatives) the pair `(a, b)` is
+exactly `(dWirtingerDir g 1 z, dWirtingerAntiDir g 1 z)`. The universal two-term
+chain rule is this decomposition substituted into the real chain rule. For
+holomorphic `g` the anti-holomorphic part vanishes and the holomorphic part collapses to
+`deriv g z`, turning the universal form into the single-term rule
+`deriv g (f u) · ∂_I f(u)`.
+
+-/
+
+/-- The real Fréchet derivative of a holomorphic outer `g : ℂ → ℂ` is `ℝ`-linear
+multiplication by `deriv g z`. -/
+private lemma outerHolo_fderiv_restrictScalars {g : ℂ → ℂ} {z : ℂ}
+    (hg : DifferentiableAt ℂ g z) :
+    fderiv ℝ g z =
+      (ContinuousLinearMap.toSpanSingleton ℂ (deriv g z)).restrictScalars ℝ :=
+  (hasFDerivAt_restrictScalarsℝℂ hg.hasDerivAt.hasFDerivAt).fderiv
+
+/-- The real derivative of a holomorphic outer `g` is `ℂ`-linear along every
+direction — the hypothesis the foundation collapse consumes at `V = ℂ`. -/
+private lemma outerHolo_clinear {g : ℂ → ℂ} {z : ℂ}
+    (hg : DifferentiableAt ℂ g z) (d : ℂ) :
+    fderiv ℝ g z (Complex.I • d) = Complex.I • fderiv ℝ g z d := by
+  rw [outerHolo_fderiv_restrictScalars hg]
+  simp only [ContinuousLinearMap.coe_restrictScalars',
+    ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul]
+  ring
+
+/-- On a holomorphic outer `g`, the holomorphic directional derivative along `1`
+collapses to the ordinary complex derivative `deriv g`. -/
+private lemma dWirtingerDir_one_eq_deriv {g : ℂ → ℂ} {z : ℂ}
+    (hg : DifferentiableAt ℂ g z) :
+    dWirtingerDir g 1 z = deriv g z := by
+  rw [dWirtingerDir_eq_of_clinear (outerHolo_clinear hg 1), outerHolo_fderiv_restrictScalars hg]
+  simp only [ContinuousLinearMap.coe_restrictScalars',
+    ContinuousLinearMap.toSpanSingleton_apply, one_smul]
+
+/-- On a holomorphic outer `g`, the anti-holomorphic directional derivative along `1`
+vanishes. -/
+private lemma dWirtingerAntiDir_one_eq_zero {g : ℂ → ℂ} {z : ℂ}
+    (hg : DifferentiableAt ℂ g z) :
+    dWirtingerAntiDir g 1 z = 0 :=
+  dWirtingerAntiDir_eq_zero_of_clinear (outerHolo_clinear hg 1)
+
+section
+
+variable {g : ℂ → ℂ} {f : (ι → ℂ) → ℂ}
+
+/-- Full pointwise chain rule for a real-differentiable outer function. -/
+lemma dWirtingerCoord_comp_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℝ g (f u)) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerCoord (fun v => g (f v)) I u =
+      dWirtingerDir g 1 (f u) * dWirtingerCoord f I u
+        + dWirtingerAntiDir g 1 (f u) *
+          dWirtingerCoord (fun v : (ι → ℂ) => star (f v)) I u :=
+  dWirtingerDir_comp hg hf (Pi.single I 1)
+
+/-- Pointwise chain rule for a holomorphic outer function. -/
+lemma dWirtingerCoord_comp_holomorphic_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℂ g (f u)) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerCoord (fun v => g (f v)) I u =
+      deriv g (f u) * dWirtingerCoord f I u := by
+  rw [dWirtingerCoord_comp_apply
+      (Physlib.Wirtinger.hasFDerivAt_restrictScalarsℝℂ hg.hasFDerivAt).differentiableAt hf I,
+    dWirtingerDir_one_eq_deriv hg, dWirtingerAntiDir_one_eq_zero hg, zero_mul, add_zero]
+
+/-- Conjugating the inner expression: `∂(f̄)/∂z^I = conj (∂f/∂z̄^I)`. -/
+lemma dWirtingerCoord_star_comp_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerCoord (fun v : (ι → ℂ) => star (f v)) I u =
+      star (dWirtingerAntiCoord f I u) :=
+  dWirtingerDir_star_comp hf (Pi.single I 1)
+
+/-- Full pointwise chain rule for a real-differentiable outer function,
+anti-holomorphic version. -/
+lemma dWirtingerAntiCoord_comp_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℝ g (f u)) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerAntiCoord (fun v => g (f v)) I u =
+      dWirtingerDir g 1 (f u) * dWirtingerAntiCoord f I u
+        + dWirtingerAntiDir g 1 (f u) *
+          dWirtingerAntiCoord (fun v : (ι → ℂ) => star (f v)) I u :=
+  dWirtingerAntiDir_comp hg hf (Pi.single I 1)
+
+/-- Pointwise chain rule for a holomorphic outer function, anti-holomorphic version. -/
+lemma dWirtingerAntiCoord_comp_holomorphic_apply {u : (ι → ℂ)}
+    (hg : DifferentiableAt ℂ g (f u)) (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerAntiCoord (fun v => g (f v)) I u =
+      deriv g (f u) * dWirtingerAntiCoord f I u := by
+  rw [dWirtingerAntiCoord_comp_apply
+      (Physlib.Wirtinger.hasFDerivAt_restrictScalarsℝℂ hg.hasFDerivAt).differentiableAt hf I,
+    dWirtingerDir_one_eq_deriv hg, dWirtingerAntiDir_one_eq_zero hg, zero_mul, add_zero]
+
+/-- Conjugating the inner expression: `∂(f̄)/∂z̄^I = conj (∂f/∂z^I)`. -/
+lemma dWirtingerAntiCoord_star_comp_apply {u : (ι → ℂ)}
+    (hf : DifferentiableAt ℝ f u) (I : ι) :
+    dWirtingerAntiCoord (fun v : (ι → ℂ) => star (f v)) I u =
+      star (dWirtingerCoord f I u) :=
+  dWirtingerAntiDir_star_comp hf (Pi.single I 1)
+
+end
+
+/-!
+
+## F. Schwarz's theorem for the coordinate operators
+
+The headline second-order results, immediate specialisations of the
+multivariable theory along the coordinate directions `Pi.single I 1`:
+differentiability of a first coordinate Wirtinger derivative, and **Schwarz's
+theorem** for the mixed second derivative on a `C²` function,
+
+  `∂_I ∂_J̄ f = ∂_J̄ ∂_I f`     (`dWirtingerCoord_dWirtingerAntiCoord_comm`)
+
+This commutativity is the keystone of Kähler-metric hermiticity: with `K` real,
+`g_{IJ̄} = ∂_I ∂_J̄ K` and `star (g_{JĪ}) = ∂_J̄ ∂_I K`, so hermiticity is
+exactly this commutation.
+
+-/
+
+section
+
+variable {f : (ι → ℂ) → ℂ} {u : (ι → ℂ)}
+
+/-- On a `C²` function the holomorphic coordinate Wirtinger derivative is itself
+real-differentiable — the `d = Pi.single I 1` case of
+`differentiableAt_dWirtingerDir`. -/
+lemma differentiableAt_dWirtingerCoord (hf2 : ContDiffAt ℝ 2 f u) (I : ι) :
+    DifferentiableAt ℝ (fun v => dWirtingerCoord f I v) u :=
+  differentiableAt_dWirtingerDir hf2 (Pi.single I 1)
+
+/-- On a `C²` function the anti-holomorphic coordinate Wirtinger derivative is itself
+real-differentiable; dual of `differentiableAt_dWirtingerCoord`. -/
+lemma differentiableAt_dWirtingerAntiCoord (hf2 : ContDiffAt ℝ 2 f u) (J : ι) :
+    DifferentiableAt ℝ (fun v => dWirtingerAntiCoord f J v) u :=
+  differentiableAt_dWirtingerAntiDir hf2 (Pi.single J 1)
+
+/-- **Schwarz's theorem** for the coordinate Wirtinger operators: on a `C²` function the
+holomorphic and anti-holomorphic derivatives commute, `∂_I ∂_J̄ f = ∂_J̄ ∂_I f`. The
+`d = Pi.single I 1`, `e = Pi.single J 1` case of the general
+`dWirtingerDir_dWirtingerAntiDir_comm`. -/
+theorem dWirtingerCoord_dWirtingerAntiCoord_comm (hf2 : ContDiffAt ℝ 2 f u) (I J : ι) :
+    dWirtingerCoord (fun v => dWirtingerAntiCoord f J v) I u
+      = dWirtingerAntiCoord (fun v => dWirtingerCoord f I v) J u :=
+  dWirtingerDir_dWirtingerAntiDir_comm hf2 (Pi.single I 1) (Pi.single J 1)
+
+end
+
+end Physlib.Wirtinger
+end
+end
diff --git a/Physlib/Mathematics/Calculus/Wirtinger/Multivariable.lean b/Physlib/Mathematics/Calculus/Wirtinger/Multivariable.lean
new file mode 100644
index 000000000..1a8e1bbd6
--- /dev/null
+++ b/Physlib/Mathematics/Calculus/Wirtinger/Multivariable.lean
@@ -0,0 +1,724 @@
+/-
+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 Physlib.Mathematics.Calculus.Wirtinger.Basic
+public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+
+/-!
+
+# Multivariable Wirtinger calculus and Schwarz's theorem
+
+## Notation
+
+How the operators read is fixed in `Wirtinger.Basic`: the direction is a *subscript* (total
+real derivative `d_v f`, holomorphic and anti-holomorphic Wirtinger parts `∂_v f`, `∂̄_v f`),
+a `/∂` fraction differentiates with respect to a *variable* (`∂g/∂f`), and `f̄` is the
+pointwise conjugate. For iterated derivatives (§I) the operators compose, `∂_v ∂̄_w f`.
+
+* `v`, `w` are directions in `V`.
+* `u : V` is the *fixed* base point a derivative is evaluated at — the implicit point in the
+  subscript notation.
+* `p : V` is the *bound* base-point variable when a derivative is repackaged as a function of
+  position: the inner field of an iterated operator (`fun p => dWirtingerAntiDir f w p`, §I),
+  or the composite in the chain rule (`fun p => g (f p)`, §D).
+
+Base points (`u`, `p`) and directions (`v`, `w`) all live in `V`: a vector space is its own
+tangent space, so a displacement from a point is again an element of `V` (`u + t·v`).
+
+## i. Overview
+
+This module is the **foundation** of physlib's Wirtinger calculus. It defines the
+**directional Wirtinger derivatives** of `f : V → ℂ` on a complex vector space `V`, along a
+direction `v : V` (a complex number when `V = ℂ`, a vector in general):
+
+  `∂_v f  = (1/2)(d_v f − i·d_{i·v} f)`     (`dWirtingerDir`)
+  `∂̄_v f = (1/2)(d_v f + i·d_{i·v} f)`     (`dWirtingerAntiDir`)
+
+Here `d_v f = fderiv ℝ f u v` is the real Fréchet derivative along `v`, the limit
+`lim_{t→0} (f(u + t·v) − f(u)) / t` over real `t`; so "real" names the scalar `t`, not the
+direction `v`, and over all `v` these limits form the `ℝ`-linear map `fderiv ℝ f u : V → ℂ`.
+The second direction `i·v` is `v` turned 90° by the complex structure on `V`, so `(v, i·v)`
+is an orthogonal frame in `v`'s own (arbitrary) direction, a rotated and rescaled copy of the
+axes `(1, i)`. For `V = ℂ` one may take `v = 1`, giving `d_v f = ∂f/∂x` and
+`d_{i·v} f = ∂f/∂y`; writing `z = x + i y` and `z̄ = x − i y`, the formulas recover the
+classical `∂f/∂z = (1/2)(∂_x − i ∂_y)f` and `∂f/∂z̄ = (1/2)(∂_x + i ∂_y)f`.
+
+The two operators measure the failure of `ℂ`-linearity. The real derivative always commutes
+with real scaling and addition; `ℂ`-linearity asks in addition that it commute with `i`, that
+is `d_{i·v} f = i·d_v f`. The gap `d_{i·v} f − i·d_v f` to that condition is exactly
+`−2i·∂̄_v f`, so `∂̄_v f` is the obstruction to `ℂ`-linearity and vanishes precisely when `f`
+is holomorphic. Equivalently, the operators split the real derivative into its holomorphic and
+anti-holomorphic parts, the directional form of the Dolbeault decomposition `d = ∂ + ∂̄`,
+which sum back to
+
+  `d_v f = ∂_v f + ∂̄_v f`.
+
+This is the coordinate-free form of treating `z` and `z̄` as independent (the `V = ℂ` case
+above). When `f` is holomorphic the anti-holomorphic half vanishes and `∂_v f` is the ordinary
+complex derivative (§F). Everything rests on `fderiv ℝ` and `Wirtinger.Basic`, with no lower
+Wirtinger layer.
+
+On these operators the module builds the **full directional calculus**:
+
+* real-linearity, the Leibniz rule, and the finite-sum rule (§B);
+* the inner-field conjugation lemmas, swapping the two operators (§C);
+* the two-term Wirtinger chain rule for an outer `g : ℂ → ℂ` (§D);
+* domain conjugation: precomposing with a conjugate-linear map swaps the two
+  operators (§E);
+* the holomorphic / anti-holomorphic collapse, keyed on `ℂ`-linearity or
+  conjugate-linearity of the real derivative along `v` (§F);
+* differentiability and locality of the operators on a `C²` field (§H).
+
+The capstone (§I) is **Schwarz's theorem** in Wirtinger form. On a `C²` field the
+holomorphic and anti-holomorphic derivatives in any two directions commute:
+
+  `∂_v ∂̄_w f = ∂̄_w ∂_v f`     (`dWirtingerDir_dWirtingerAntiDir_comm`)
+
+It is no new analytic fact: it reduces to the symmetry of the second real Fréchet
+derivative (`ContDiffAt.isSymmSndFDerivAt`), carried out via the `weightedDirDeriv` bridge
+of §G.
+
+## ii. Key results
+
+- `Physlib.Wirtinger.dWirtingerDir` / `dWirtingerAntiDir` : directional Wirtinger
+    derivatives of `f : V → ℂ` along `v`.
+- `Physlib.Wirtinger.dWirtingerDir_add` / `dWirtingerDir_smul` /
+    `dWirtingerDir_mul` / `dWirtingerDir_fun_sum` : real-linearity, the Leibniz
+    rule, and the finite-sum rule (each with an anti-holomorphic dual).
+- `Physlib.Wirtinger.dWirtingerDir_star_comp` / `dWirtingerAntiDir_star_comp` :
+    conjugating the inner field swaps the holomorphic and anti-holomorphic operators.
+- `Physlib.Wirtinger.dWirtingerDir_comp` / `dWirtingerAntiDir_comp` : the two-term
+    Wirtinger chain rule for an outer `g : ℂ → ℂ`.
+- `Physlib.Wirtinger.dWirtingerDir_comp_conjLinear` /
+    `dWirtingerAntiDir_comp_conjLinear` : precomposing with a conjugate-`ℂ`-linear
+    map swaps the two operators (with the base point and direction transported
+    through the map).
+- `Physlib.Wirtinger.dWirtingerDir_eq_of_clinear` /
+    `dWirtingerAntiDir_eq_zero_of_clinear` : the holomorphic collapse, keyed on
+    `ℂ`-linearity of the real derivative along the direction (each with a
+    conjugate-`ℂ`-linear dual).
+- `Physlib.Wirtinger.differentiableAt_dWirtingerDir` /
+    `differentiableAt_dWirtingerAntiDir` : the directional derivative of a `C²`
+    field is itself real-differentiable.
+- `Physlib.Wirtinger.dWirtingerDir_congr_of_eventuallyEq` /
+    `dWirtingerAntiDir_congr_of_eventuallyEq` : the directional derivative depends
+    only on the field near the point.
+- `Physlib.Wirtinger.dWirtingerDir_dWirtingerAntiDir_comm` : Schwarz's theorem,
+    `∂_v ∂̄_w f = ∂̄_w ∂_v f` for a `C²` `f`.
+
+## iii. Table of contents
+
+- A. The directional Wirtinger operators
+- B. Real-linearity and the Leibniz rule
+- C. Conjugation
+- D. The Wirtinger chain rule
+- E. Domain conjugation
+- F. The holomorphic collapse
+- G. The second-derivative bridge
+- H. Differentiability and locality
+- I. Schwarz's theorem
+
+## iv. References
+
+- Kreutz-Delgado, *The Complex Gradient Operator and the CR-Calculus*,
+  arXiv:0906.4835 — directional/multivariable formulation and two-term chain
+  rule (§D); second-order theory behind §G–I.
+- Mortini & Rupp, *The Clairaut–Schwarz Theorem for Mixed Wirtinger
+  Derivatives*, Bull. Iranian Math. Soc. 48 (2022), 2643–2647 — the mixed
+  holomorphic/anti-holomorphic symmetry of §I under the same `C²` hypothesis,
+  with the same reduction to real Schwarz used here.
+- Koor, Qiu, Kwek & Rebentrost, *A short tutorial on Wirtinger Calculus with
+  applications in quantum information*, arXiv:2312.04858 — companion
+  exposition of the scalar single/multivariable calculus and sign conventions.
+- *Complex differential form*, Wikipedia (section "The Dolbeault operators") — the
+  `d = ∂ + ∂̄` splitting and the `∂`/`∂̄` notation this module's operators are named after.
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace Physlib.Wirtinger
+
+variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedSpace ℂ V]
+  {f : V → ℂ} {u : V}
+
+/-!
+
+## A. The directional Wirtinger operators
+
+The two directional operators repackage the real Fréchet derivative of `f` along
+`v` and `i·v` into a holomorphic part `∂_v f` and an anti-holomorphic part `∂̄_v f`,
+the combinations `(1/2)(d_v f ∓ i·d_{i·v} f)`. Both are `ℂ`-valued and depend on the
+base point `u`.
+
+-/
+
+/-- The holomorphic directional Wirtinger derivative `∂_v f = (1/2)(d_v f − i·d_{i·v} f)`
+of `f : V → ℂ` along the direction vector `v : V`. -/
+def dWirtingerDir (f : V → ℂ) (v : V) (u : V) : ℂ :=
+  (1 / 2 : ℂ) * (fderiv ℝ f u v - Complex.I * fderiv ℝ f u (Complex.I • v))
+
+/-- The anti-holomorphic directional Wirtinger derivative
+`∂̄_v f = (1/2)(d_v f + i·d_{i·v} f)` of `f : V → ℂ` along the direction vector `v : V`. -/
+def dWirtingerAntiDir (f : V → ℂ) (v : V) (u : V) : ℂ :=
+  (1 / 2 : ℂ) * (fderiv ℝ f u v + Complex.I * fderiv ℝ f u (Complex.I • v))
+
+/-- Definitional unfolding of `dWirtingerDir`, used to expand the outer operator
+of a composition without touching the inner one. -/
+lemma dWirtingerDir_apply (g : V → ℂ) (v u : V) :
+    dWirtingerDir g v u
+      = (1 / 2 : ℂ) * (fderiv ℝ g u v - Complex.I * fderiv ℝ g u (Complex.I • v)) :=
+  rfl
+
+/-- Definitional unfolding of `dWirtingerAntiDir`. -/
+lemma dWirtingerAntiDir_apply (g : V → ℂ) (v u : V) :
+    dWirtingerAntiDir g v u
+      = (1 / 2 : ℂ) * (fderiv ℝ g u v + Complex.I * fderiv ℝ g u (Complex.I • v)) :=
+  rfl
+
+/-!
+
+## B. Real-linearity and the Leibniz rule
+
+The directional operators are built from `fderiv ℝ`, so they inherit its
+vanishing on constants, additivity, negation, complex-scalar compatibility, the
+finite-sum rule, and — through the Fréchet product rule — a Wirtinger Leibniz
+rule.
+
+-/
+
+/-- Constants have zero holomorphic directional Wirtinger derivative, `∂_v c = 0`. -/
+@[simp] lemma dWirtingerDir_const (c : ℂ) (v u : V) :
+    dWirtingerDir (fun _ : V => c) v u = 0 := by
+  simp [dWirtingerDir, fderiv_const_apply]
+
+/-- Constants have zero anti-holomorphic directional Wirtinger derivative, `∂̄_v c = 0`. -/
+@[simp] lemma dWirtingerAntiDir_const (c : ℂ) (v u : V) :
+    dWirtingerAntiDir (fun _ : V => c) v u = 0 := by
+  simp [dWirtingerAntiDir, fderiv_const_apply]
+
+/-- `dWirtingerDir` of a negated function, `∂_v(−g) = −∂_v g`. Holds with no
+differentiability hypothesis, since `fderiv` of a negation is unconditional. -/
+@[simp] lemma dWirtingerDir_neg (g : V → ℂ) (v u : V) :
+    dWirtingerDir (fun p => -(g p)) v u = -(dWirtingerDir g v u) := by
+  simp only [dWirtingerDir, fderiv_fun_neg, ContinuousLinearMap.neg_apply]; ring
+
+/-- `dWirtingerAntiDir` of a negated function, `∂̄_v(−g) = −∂̄_v g`. -/
+@[simp] lemma dWirtingerAntiDir_neg (g : V → ℂ) (v u : V) :
+    dWirtingerAntiDir (fun p => -(g p)) v u = -(dWirtingerAntiDir g v u) := by
+  simp only [dWirtingerAntiDir, fderiv_fun_neg, ContinuousLinearMap.neg_apply]; ring
+
+/-- Additivity of `dWirtingerDir`, `∂_v(g + h) = ∂_v g + ∂_v h`. -/
+lemma dWirtingerDir_add {g h : V → ℂ} (hg : DifferentiableAt ℝ g u)
+    (hh : DifferentiableAt ℝ h u) (v : V) :
+    dWirtingerDir (g + h) v u = dWirtingerDir g v u + dWirtingerDir h v u := by
+  simp only [dWirtingerDir, fderiv_add hg hh, ContinuousLinearMap.add_apply]; ring
+
+/-- Additivity of `dWirtingerAntiDir`, `∂̄_v(g + h) = ∂̄_v g + ∂̄_v h`. -/
+lemma dWirtingerAntiDir_add {g h : V → ℂ} (hg : DifferentiableAt ℝ g u)
+    (hh : DifferentiableAt ℝ h u) (v : V) :
+    dWirtingerAntiDir (g + h) v u = dWirtingerAntiDir g v u + dWirtingerAntiDir h v u := by
+  simp only [dWirtingerAntiDir, fderiv_add hg hh, ContinuousLinearMap.add_apply]; ring
+
+/-- Compatibility of `dWirtingerDir` with complex scalar multiplication,
+`∂_v(c·g) = c·∂_v g`. -/
+lemma dWirtingerDir_smul (c : ℂ) {g : V → ℂ} (hg : DifferentiableAt ℝ g u) (v : V) :
+    dWirtingerDir (c • g) v u = c • dWirtingerDir g v u := by
+  simp only [dWirtingerDir, fderiv_const_smul hg c, ContinuousLinearMap.smul_apply,
+    smul_eq_mul]; ring
+
+/-- Compatibility of `dWirtingerAntiDir` with complex scalar multiplication,
+`∂̄_v(c·g) = c·∂̄_v g`. -/
+lemma dWirtingerAntiDir_smul (c : ℂ) {g : V → ℂ} (hg : DifferentiableAt ℝ g u) (v : V) :
+    dWirtingerAntiDir (c • g) v u = c • dWirtingerAntiDir g v u := by
+  simp only [dWirtingerAntiDir, fderiv_const_smul hg c, ContinuousLinearMap.smul_apply,
+    smul_eq_mul]; ring
+
+omit [NormedSpace ℂ V] in
+/-- The real Fréchet derivative of a product, evaluated at a tangent `v`. -/
+private lemma fderiv_mul_apply {g h : V → ℂ} (hg : DifferentiableAt ℝ g u)
+    (hh : DifferentiableAt ℝ h u) (v : V) :
+    fderiv ℝ (g * h) u v = g u * fderiv ℝ h u v + h u * fderiv ℝ g u v := by
+  simpa using DFunLike.congr_fun (fderiv_mul hg hh) v
+
+/-- The Wirtinger Leibniz rule for `dWirtingerDir`,
+`∂_v(g·h) = ∂_v g·h + g·∂_v h`. -/
+lemma dWirtingerDir_mul {g h : V → ℂ} (hg : DifferentiableAt ℝ g u)
+    (hh : DifferentiableAt ℝ h u) (v : V) :
+    dWirtingerDir (g * h) v u = dWirtingerDir g v u * h u + g u * dWirtingerDir h v u := by
+  simp only [dWirtingerDir, fderiv_mul_apply hg hh]; ring
+
+/-- The Wirtinger Leibniz rule for `dWirtingerAntiDir`,
+`∂̄_v(g·h) = ∂̄_v g·h + g·∂̄_v h`. -/
+lemma dWirtingerAntiDir_mul {g h : V → ℂ} (hg : DifferentiableAt ℝ g u)
+    (hh : DifferentiableAt ℝ h u) (v : V) :
+    dWirtingerAntiDir (g * h) v u =
+      dWirtingerAntiDir g v u * h u + g u * dWirtingerAntiDir h v u := by
+  simp only [dWirtingerAntiDir, fderiv_mul_apply hg hh]; ring
+
+/-- Finite-sum rule for `dWirtingerDir`, `∂_v(∑ₐ Fₐ) = ∑ₐ ∂_v Fₐ`. -/
+lemma dWirtingerDir_fun_sum {α : Type*} {s : Finset α} {F : α → V → ℂ}
+    (hF : ∀ a ∈ s, DifferentiableAt ℝ (F a) u) (v : V) :
+    dWirtingerDir (fun p => ∑ a ∈ s, F a p) v u = ∑ a ∈ s, dWirtingerDir (F a) v u := by
+  simp only [dWirtingerDir, fderiv_fun_sum hF, ContinuousLinearMap.sum_apply]
+  rw [Finset.mul_sum, ← Finset.sum_sub_distrib, Finset.mul_sum]
+
+/-- Finite-sum rule for `dWirtingerAntiDir`, `∂̄_v(∑ₐ Fₐ) = ∑ₐ ∂̄_v Fₐ`. -/
+lemma dWirtingerAntiDir_fun_sum {α : Type*} {s : Finset α} {F : α → V → ℂ}
+    (hF : ∀ a ∈ s, DifferentiableAt ℝ (F a) u) (v : V) :
+    dWirtingerAntiDir (fun p => ∑ a ∈ s, F a p) v u = ∑ a ∈ s, dWirtingerAntiDir (F a) v u := by
+  simp only [dWirtingerAntiDir, fderiv_fun_sum hF, ContinuousLinearMap.sum_apply]
+  rw [Finset.mul_sum, ← Finset.sum_add_distrib, Finset.mul_sum]
+
+/-!
+
+## C. Conjugation
+
+Conjugating the inner field `f` swaps the two operators, up to an outer conjugation on the
+value (`fderiv_star_eq`):
+
+  `∂_v f̄ = conj (∂̄_v f)`,     `∂̄_v f̄ = conj (∂_v f)`.
+
+Each operator applied to the conjugate field `f̄` returns the *other* operator on `f`,
+conjugated — the bar exchanges holomorphic and anti-holomorphic dependence. Concretely, on
+`V = ℂ` take the holomorphic `f(z) = z`, with `∂_z z = 1`, `∂̄_z z = 0`:
+
+* `∂_v f̄ = conj (∂̄_v f)` reads `∂_z z̄ = conj 0 = 0` — the conjugate `z̄` has no
+  holomorphic part;
+* the dual `∂̄_v f̄ = conj (∂_v f)` reads `∂̄_z z̄ = conj 1 = 1` — all of `z̄`'s dependence
+  sits in the anti-holomorphic operator.
+
+The chain rule of §D builds on these to handle a conjugated inner argument.
+
+-/
+
+/-- Conjugating the function swaps the operators up to an outer conjugation:
+`∂_v f̄ = conj (∂̄_v f)`. -/
+lemma dWirtingerDir_star_comp (hf : DifferentiableAt ℝ f u) (v : V) :
+    dWirtingerDir (fun p => star (f p)) v u = star (dWirtingerAntiDir f v u) := by
+  simp only [dWirtingerDir, dWirtingerAntiDir]
+  rw [fderiv_star_eq hf]
+  simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
+    Complex.conjCLE_apply, Complex.star_def, map_mul, map_add, map_div₀, map_one,
+    map_ofNat, Complex.conj_I]
+  ring
+
+/-- Conjugating the function swaps the operators up to an outer conjugation:
+`∂̄_v f̄ = conj (∂_v f)`. Dual of `dWirtingerDir_star_comp`. -/
+lemma dWirtingerAntiDir_star_comp (hf : DifferentiableAt ℝ f u) (v : V) :
+    dWirtingerAntiDir (fun p => star (f p)) v u = star (dWirtingerDir f v u) := by
+  simp only [dWirtingerDir, dWirtingerAntiDir]
+  rw [fderiv_star_eq hf]
+  simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
+    Complex.conjCLE_apply, Complex.star_def, map_mul, map_sub, map_div₀, map_one,
+    map_ofNat, Complex.conj_I]
+  ring
+
+/-!
+
+## D. The Wirtinger chain rule
+
+Composing with an outer `g : ℂ → ℂ` gives a **two-term** chain rule:
+
+  `∂_v(g∘f) = (∂g/∂f)·∂_v f + (∂g/∂f̄)·∂_v f̄`.
+
+A non-holomorphic `g` depends on both its argument and its conjugate, so both channels
+contribute: the holomorphic `∂g/∂f` and the anti-holomorphic `∂g/∂f̄`, each times the
+matching inner derivative — two terms where the complex-analytic rule has one. The two
+coefficients come from `realLinear_apply_eq_wirtinger`: every `ℝ`-linear `L : ℂ → ℂ`
+splits as `L w = a·w + b·conj w`, and on the outer real derivative `L = fderiv ℝ g (f u)`
+that gives `a = ∂g/∂f`, `b = ∂g/∂f̄`. The proof applies this split to the outer factor and
+reuses the §C conjugation lemmas for the `∂_v f̄` term.
+
+-/
+
+/-- The two-term Wirtinger chain rule for `dWirtingerDir`, outer `g : ℂ → ℂ` and inner
+`f : V → ℂ`:
+
+  `∂_v(g∘f) = (∂g/∂f)·∂_v f + (∂g/∂f̄)·∂_v f̄`.
+
+`realLinear_apply_eq_wirtinger` splits the chain rule's outer `ℝ`-linear factor into the
+`∂g/∂f`, `∂g/∂f̄` coefficients, each multiplying its inner directional derivative `∂_v f`,
+`∂_v f̄`. -/
+lemma dWirtingerDir_comp {g : ℂ → ℂ} (hg : DifferentiableAt ℝ g (f u))
+    (hf : DifferentiableAt ℝ f u) (v : V) :
+    dWirtingerDir (fun p => g (f p)) v u =
+      dWirtingerDir g 1 (f u) * dWirtingerDir f v u
+        + dWirtingerAntiDir g 1 (f u) * dWirtingerDir (fun p => star (f p)) v u := by
+  simp only [dWirtingerDir, dWirtingerAntiDir, smul_eq_mul, mul_one]
+  rw [show (fun p => g (f p)) = g ∘ f from rfl, fderiv_comp u hg hf, fderiv_star_eq hf]
+  simp only [ContinuousLinearMap.comp_apply]
+  have hA := realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u v)
+  have hB := realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u (Complex.I • v))
+  rw [hA, hB]
+  simp only [ContinuousLinearEquiv.coe_coe, Complex.conjCLE_apply, Complex.star_def]
+  ring
+
+/-- The two-term Wirtinger chain rule for `dWirtingerAntiDir`, the anti-holomorphic dual of
+`dWirtingerDir_comp`:
+
+  `∂̄_v(g∘f) = (∂g/∂f)·∂̄_v f + (∂g/∂f̄)·∂̄_v f̄`.
+
+Same outer `∂g/∂f`, `∂g/∂f̄` coefficients, now each multiplying its anti-holomorphic inner
+derivative `∂̄_v f`, `∂̄_v f̄`; same proof as `dWirtingerDir_comp`. -/
+lemma dWirtingerAntiDir_comp {g : ℂ → ℂ} (hg : DifferentiableAt ℝ g (f u))
+    (hf : DifferentiableAt ℝ f u) (v : V) :
+    dWirtingerAntiDir (fun p => g (f p)) v u =
+      dWirtingerDir g 1 (f u) * dWirtingerAntiDir f v u
+        + dWirtingerAntiDir g 1 (f u) * dWirtingerAntiDir (fun p => star (f p)) v u := by
+  simp only [dWirtingerDir, dWirtingerAntiDir, smul_eq_mul, mul_one]
+  rw [show (fun p => g (f p)) = g ∘ f from rfl, fderiv_comp u hg hf, fderiv_star_eq hf]
+  simp only [ContinuousLinearMap.comp_apply]
+  have hA := realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u v)
+  have hB := realLinear_apply_eq_wirtinger (fderiv ℝ g (f u)) (fderiv ℝ f u (Complex.I • v))
+  rw [hA, hB]
+  simp only [ContinuousLinearEquiv.coe_coe, Complex.conjCLE_apply, Complex.star_def]
+  ring
+
+/-!
+
+## E. Domain conjugation
+
+The goal is to differentiate anti-holomorphic functions: a holomorphic `g` precomposed with
+conjugation of its input (the scalar case is `g(z̄)`, but the input is a general vector). So
+this section conjugates a function's *input*: precomposing `g` with a domain map
+`L : V → V'` (forming `g ∘ L`) swaps the two operators, whereas §C conjugated the output.
+The map `L` is **conjugate-`ℂ`-linear**: real-linear and continuous, but anti-commuting with
+`i`:
+
+  `L (i · x) = −(i · L x)`,
+
+the abstract form of `conj (i·x) = −i · conj x`. That sign flip swaps the two operators: in
+the holomorphic combination `(1/2)(d_v f − i·d_{i·v} f)` the `d_{i·v} f` term picks up the
+minus from `L`, turning it anti-holomorphic. So precomposition `g ∘ L` swaps `∂ ↔ ∂̄`, with
+`g`'s derivative taken at the mapped point `L u` in the mapped direction `L v`:
+
+  `∂_v(g ∘ L)`  at `u`  =  `∂̄_{L v} g`  at `L u`
+  `∂̄_v(g ∘ L)`  at `u`  =  `∂_{L v} g`  at `L u`
+
+(`dWirtingerDir_comp_conjLinear` and its dual `dWirtingerAntiDir_comp_conjLinear`).
+
+Concretely on `ℂ`, let `L : z ↦ z̄` and `g(z) = log(z)`, so `g ∘ L` is `z ↦ log(z̄)`. The
+theorem computes this composite's derivatives from the known derivative of `log`, swapping
+the operator. Its anti-holomorphic derivative is `log`'s ordinary derivative `1/z` at the
+mapped point `z̄`:
+
+  `∂̄_z log(z̄) = 1/z̄`,
+
+while its holomorphic derivative vanishes, `∂_z log(z̄) = 0`, because `log` is holomorphic.
+So `log(z̄)` is purely anti-holomorphic, with its dependence carried by `∂̄`.
+
+So precomposing with conjugation turns `∂` into `∂̄` and vice versa: a holomorphic `g(z̄)`
+has zero holomorphic derivative, and its anti-holomorphic derivative is just `g`'s ordinary
+complex derivative (§F, and the example above). The proof uses only `L`'s anti-commutation
+with `i`, so it holds over any complex `V`, `V'`.
+
+-/
+
+section DomainConjugation
+
+variable {V' : Type*} [NormedAddCommGroup V'] [NormedSpace ℝ V'] [NormedSpace ℂ V']
+
+omit [NormedSpace ℂ V] [NormedSpace ℂ V'] in
+/-- Chain rule for an inner continuous linear map `L`. Because the derivative of a linear
+map is the map itself, the real Fréchet derivative of `g ∘ L` at `u`, applied to `x`, equals
+the derivative of `g` at `L u` applied to `L x`. -/
+private lemma fderiv_comp_clm_apply {g : V' → ℂ} {L : V →L[ℝ] V'} {u : V}
+    (hg : DifferentiableAt ℝ g (L u)) (x : V) :
+    fderiv ℝ (fun p => g (L p)) u x = fderiv ℝ g (L u) (L x) := by
+  rw [show (fun p => g (L p)) = g ∘ (L : V → V') from rfl,
+    fderiv_comp u hg L.differentiableAt, ContinuousLinearMap.fderiv,
+    ContinuousLinearMap.comp_apply]
+
+/-- Domain conjugation swaps the operators: precomposing with a conjugate-`ℂ`-linear `L`
+turns the holomorphic derivative of `g ∘ L` at `u` into the anti-holomorphic derivative of
+`g` at the mapped point `L u`, in the mapped direction `L v`:
+`∂_v(g ∘ L)` at `u` equals `∂̄_{L v} g` at `L u`. -/
+lemma dWirtingerDir_comp_conjLinear {g : V' → ℂ} {L : V →L[ℝ] V'} {u : V}
+    (hL : ∀ x : V, L (Complex.I • x) = -(Complex.I • L x))
+    (hg : DifferentiableAt ℝ g (L u)) (v : V) :
+    dWirtingerDir (fun p => g (L p)) v u = dWirtingerAntiDir g (L v) (L u) := by
+  simp only [dWirtingerDir, dWirtingerAntiDir, fderiv_comp_clm_apply hg, hL, map_neg]; ring
+
+/-- Dual of `dWirtingerDir_comp_conjLinear`: the anti-holomorphic derivative of `g ∘ L` at
+`u` is the holomorphic derivative of `g` at the mapped point `L u`, in the mapped direction
+`L v`: `∂̄_v(g ∘ L)` at `u` equals `∂_{L v} g` at `L u`. -/
+lemma dWirtingerAntiDir_comp_conjLinear {g : V' → ℂ} {L : V →L[ℝ] V'} {u : V}
+    (hL : ∀ x : V, L (Complex.I • x) = -(Complex.I • L x))
+    (hg : DifferentiableAt ℝ g (L u)) (v : V) :
+    dWirtingerAntiDir (fun p => g (L p)) v u = dWirtingerDir g (L v) (L u) := by
+  simp only [dWirtingerDir, dWirtingerAntiDir, fderiv_comp_clm_apply hg, hL, map_neg]; ring
+
+end DomainConjugation
+
+/-!
+
+## F. The holomorphic collapse
+
+The two-operator split collapses to one exactly when `f` is holomorphic along `v`, i.e. its
+real derivative is `ℂ`-linear there (`d_{i·v} f = i·d_v f`, the Cauchy–Riemann condition):
+then `∂_v f` is the full real derivative `d_v f` and `∂̄_v f` vanishes. Dually, a
+conjugate-`ℂ`-linear derivative makes `∂_v f` vanish and `∂̄_v f` the full derivative.
+
+The lemmas take this `ℂ`-linearity condition directly as hypothesis, not holomorphy itself.
+The reason is a clean division of labor.
+
+**The domain-general collapse.** Given the identity `d_{i·v} f = i·d_v f`, the collapse is pure
+algebra: unfold `∂_v f = (1/2)(d_v f − i·d_{i·v} f)`, substitute the identity, and `∂_v f`
+reduces to `d_v f` while `∂̄_v f` cancels to `0`. No property of the domain `V` enters, so a
+single proof covers every complex `V`.
+
+**The domain-specific bridge.** Holomorphy is stated through the complex derivative
+`fderiv ℂ`, but the collapse is about the real derivative `fderiv ℝ`; the implication
+`f` holomorphic ⟹ `d_{i·v} f = i·d_v f` is the bridge between them. Relating the two
+derivatives is domain-specific, so each consumer establishes the bridge in its own setting,
+then applies the domain-general lemma above.
+
+-/
+
+/-- Holomorphic collapse: along a direction where the real derivative is `ℂ`-linear, the
+holomorphic derivative is the full real derivative, `∂_v f = d_v f`. -/
+lemma dWirtingerDir_eq_of_clinear {v : V}
+    (h : fderiv ℝ f u (Complex.I • v) = Complex.I • fderiv ℝ f u v) :
+    dWirtingerDir f v u = fderiv ℝ f u v := by
+  simp only [dWirtingerDir, h, smul_eq_mul]; rw [← mul_assoc, Complex.I_mul_I]; ring
+
+/-- Holomorphic collapse: the anti-holomorphic derivative vanishes along a direction
+of `ℂ`-linearity, `∂̄_v f = 0`. -/
+lemma dWirtingerAntiDir_eq_zero_of_clinear {v : V}
+    (h : fderiv ℝ f u (Complex.I • v) = Complex.I • fderiv ℝ f u v) :
+    dWirtingerAntiDir f v u = 0 := by
+  simp only [dWirtingerAntiDir, h, smul_eq_mul]; rw [← mul_assoc, Complex.I_mul_I]; ring
+
+/-- Anti-holomorphic collapse: a direction of conjugate-`ℂ`-linearity kills the
+holomorphic derivative, `∂_v f = 0`. -/
+lemma dWirtingerDir_eq_zero_of_antilinear {v : V}
+    (h : fderiv ℝ f u (Complex.I • v) = -(Complex.I • fderiv ℝ f u v)) :
+    dWirtingerDir f v u = 0 := by
+  simp only [dWirtingerDir, h, smul_eq_mul, mul_neg]; rw [← mul_assoc, Complex.I_mul_I]; ring
+
+/-- Anti-holomorphic collapse: the anti-holomorphic derivative is the full real
+derivative along a direction of conjugate-`ℂ`-linearity, `∂̄_v f = d_v f`. -/
+lemma dWirtingerAntiDir_eq_of_antilinear {v : V}
+    (h : fderiv ℝ f u (Complex.I • v) = -(Complex.I • fderiv ℝ f u v)) :
+    dWirtingerAntiDir f v u = fderiv ℝ f u v := by
+  simp only [dWirtingerAntiDir, h, smul_eq_mul, mul_neg]; rw [← mul_assoc, Complex.I_mul_I]; ring
+
+/-!
+
+## G. The second-derivative bridge
+
+Schwarz's theorem (§I) commutes two Wirtinger operators, so it differentiates a directional
+Wirtinger derivative a *second* time. This section bridges that second derivative to the
+second real Fréchet derivative `fderiv ℝ (fderiv ℝ f) u`, where mixed partials are already
+symmetric.
+
+Each directional operator is, definitionally, a combination `(1/2)(d_{b₁} f + c·d_{b₂} f)` of
+the real derivative along two directions (`c = −i` holomorphic with `b₂ = i·b₁`, `c = +i`
+anti-holomorphic). `weightedDirDeriv` records this as a function of the base point, with
+`b₁`, `b₂` left free: the directions stay fixed while the point `p` varies, turning the
+one-point derivative into a field `V → ℂ` that can itself be differentiated. Differentiating
+it once more sends each first derivative to `fderiv ℝ (fderiv ℝ f) u` on two slots.
+
+The two inner directions `b₁`, `b₂` are intrinsic: they are the pair a Wirtinger derivative
+already combines (`v` and `i·v`). The second differentiation, by contrast, is an ordinary
+Fréchet derivative along one new direction `a`, so the bridge lands directly on the plain
+second derivative `fderiv ℝ (fderiv ℝ f) u` in the outer slot `a` and inner slot `b₁`/`b₂`,
+whose slot symmetry (`ContDiffAt.isSymmSndFDerivAt`) drives Schwarz. The *outer* Wirtinger
+combination is rebuilt afterward by instantiating `a` at `v` and `i·v`.
+
+Because `weightedDirDeriv` and its bridge `fderiv_weightedDirDeriv` are generic in `c`, `b₁`,
+`b₂`, one lemma serves every second-order pairing. The four combinations (holomorphic or
+anti-holomorphic, twice) differ only in their coefficients and all reduce to
+`fderiv ℝ (fderiv ℝ f) u` on the directions `v`, `i·v`, `w`, `i·w`. §I discharges the mixed
+pairing that Kähler geometry needs; the others follow from the same bridge with a different
+`(c, b₁, b₂)`, then `ContDiffAt.isSymmSndFDerivAt` and `ring`.
+
+**Structure.**
+
+* `weightedDirDeriv` : the base-point field `p ↦ (1/2)(d_{b₁} f + c·d_{b₂} f)`, the shape
+  shared by both directional operators (`c = −i` or `+i`).
+* `differentiableAt_fderiv` : from `ContDiffAt ℝ 2 f`, the first derivative `fderiv ℝ f` is
+  itself differentiable at `u`, the regularity the rest of the section consumes.
+* `hasFDerivAt_fderiv_apply`, `hasFDerivAt_weightedDirDeriv` : the evaluation field
+  `p ↦ d_b f`, and hence `weightedDirDeriv`, is differentiable wherever `fderiv ℝ f` is.
+* `fderiv_weightedDirDeriv` : the bridge, sending a derivative of `weightedDirDeriv` along a
+  direction `a` to the second Fréchet derivative `fderiv ℝ (fderiv ℝ f) u` in the two slots.
+* `dWirtingerDir_eq_weightedDirDeriv`, `dWirtingerAntiDir_eq_weightedDirDeriv` : the operators
+  `∂_v f`, `∂̄_v f` are `weightedDirDeriv` at `(c, b₁, b₂) = (−i, v, i·v)` and `(i, w, i·w)`.
+* `fderiv_dWirtingerDir`, `fderiv_dWirtingerAntiDir` : specialize the bridge, so a second
+  derivative of `∂_v f`, `∂̄_v f` lands on `fderiv ℝ (fderiv ℝ f) u` in the two slots.
+
+-/
+
+/-- The combination `p ↦ (1/2)(d_{b₁} f + c·d_{b₂} f)` of the real Fréchet
+derivative of `f` along two directions. `dWirtingerDir f v` is this with
+`c = -i`, `b₁ = v`, `b₂ = i·v`; `dWirtingerAntiDir f v` with `c = i`. -/
+private def weightedDirDeriv (f : V → ℂ) (c : ℂ) (b₁ b₂ : V) : V → ℂ :=
+  fun p => (1 / 2 : ℂ) * (fderiv ℝ f p b₁ + c * fderiv ℝ f p b₂)
+
+omit [NormedSpace ℂ V] in
+/-- `f` is `C¹` in its first derivative, so `fderiv ℝ f` is differentiable at
+`u` — the regularity that makes a `weightedDirDeriv` (hence a directional derivative)
+differentiable. -/
+private lemma differentiableAt_fderiv (hf2 : ContDiffAt ℝ 2 f u) :
+    DifferentiableAt ℝ (fderiv ℝ f) u :=
+  (hf2.fderiv_right (m := 1) (by norm_num)).differentiableAt one_ne_zero
+
+omit [NormedSpace ℂ V] in
+/-- The field `p ↦ d_b f` is the evaluation map `· b` composed with `fderiv ℝ f`,
+so when `fderiv ℝ f` is differentiable its derivative is `fderiv ℝ (fderiv ℝ f) u`
+post-composed with that evaluation. -/
+private lemma hasFDerivAt_fderiv_apply (hf' : DifferentiableAt ℝ (fderiv ℝ f) u)
+    (b : V) :
+    HasFDerivAt (fun p => fderiv ℝ f p b)
+      ((ContinuousLinearMap.apply ℝ ℂ b).comp (fderiv ℝ (fderiv ℝ f) u)) u :=
+  (ContinuousLinearMap.apply ℝ ℂ b).hasFDerivAt.comp u hf'.hasFDerivAt
+
+omit [NormedSpace ℂ V] in
+/-- The `weightedDirDeriv` is differentiable wherever `fderiv ℝ f` is. -/
+private lemma hasFDerivAt_weightedDirDeriv (hf' : DifferentiableAt ℝ (fderiv ℝ f) u)
+    (c : ℂ) (b₁ b₂ : V) :
+    HasFDerivAt (weightedDirDeriv f c b₁ b₂)
+      ((1 / 2 : ℂ) • ((ContinuousLinearMap.apply ℝ ℂ b₁).comp (fderiv ℝ (fderiv ℝ f) u)
+        + c • (ContinuousLinearMap.apply ℝ ℂ b₂).comp (fderiv ℝ (fderiv ℝ f) u))) u :=
+  ((hasFDerivAt_fderiv_apply hf' b₁).add
+    ((hasFDerivAt_fderiv_apply hf' b₂).const_mul c)).const_mul (1 / 2)
+
+omit [NormedSpace ℂ V] in
+/-- The bridge: differentiating a `weightedDirDeriv` along a third direction `a`
+lands on the second real Fréchet derivative `fderiv ℝ (fderiv ℝ f) u a b` in the
+two slots. -/
+private lemma fderiv_weightedDirDeriv (hf' : DifferentiableAt ℝ (fderiv ℝ f) u)
+    (c : ℂ) (b₁ b₂ a : V) :
+    fderiv ℝ (weightedDirDeriv f c b₁ b₂) u a
+      = (1 / 2 : ℂ) * (fderiv ℝ (fderiv ℝ f) u a b₁
+          + c * fderiv ℝ (fderiv ℝ f) u a b₂) := by
+  rw [(hasFDerivAt_weightedDirDeriv hf' c b₁ b₂).fderiv]
+  simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
+    ContinuousLinearMap.coe_comp', Function.comp_apply, ContinuousLinearMap.apply_apply,
+    smul_eq_mul, mul_add]
+
+/-- A directional derivative is a `weightedDirDeriv`: anti-holomorphic with `c = i`. -/
+private lemma dWirtingerAntiDir_eq_weightedDirDeriv (w : V) :
+    (fun p => dWirtingerAntiDir f w p) = weightedDirDeriv f Complex.I w (Complex.I • w) :=
+  rfl
+
+/-- A directional derivative is a `weightedDirDeriv`: holomorphic with `c = -i`. -/
+private lemma dWirtingerDir_eq_weightedDirDeriv (v : V) :
+    (fun p => dWirtingerDir f v p) = weightedDirDeriv f (-Complex.I) v (Complex.I • v) := by
+  funext p; simp only [dWirtingerDir, weightedDirDeriv]; ring
+
+/-- Differentiating the anti-holomorphic directional derivative lands on the second
+real Fréchet derivative in the two slots. -/
+private lemma fderiv_dWirtingerAntiDir (hf' : DifferentiableAt ℝ (fderiv ℝ f) u)
+    (w a : V) :
+    fderiv ℝ (fun p => dWirtingerAntiDir f w p) u a
+      = (1 / 2 : ℂ) * (fderiv ℝ (fderiv ℝ f) u a w
+          + Complex.I * fderiv ℝ (fderiv ℝ f) u a (Complex.I • w)) := by
+  rw [dWirtingerAntiDir_eq_weightedDirDeriv, fderiv_weightedDirDeriv hf']
+
+/-- Differentiating the holomorphic directional derivative lands on the second real
+Fréchet derivative in the two slots. -/
+private lemma fderiv_dWirtingerDir (hf' : DifferentiableAt ℝ (fderiv ℝ f) u)
+    (v a : V) :
+    fderiv ℝ (fun p => dWirtingerDir f v p) u a
+      = (1 / 2 : ℂ) * (fderiv ℝ (fderiv ℝ f) u a v
+          - Complex.I * fderiv ℝ (fderiv ℝ f) u a (Complex.I • v)) := by
+  rw [dWirtingerDir_eq_weightedDirDeriv, fderiv_weightedDirDeriv hf']; ring
+
+/-!
+
+## H. Differentiability and locality
+
+Schwarz (§I) and the coordinate layer treat a directional derivative as a field in the base
+point `p`, and need two regularity facts about it. Both are public packagings of §G, consumed
+in `Coordinate.lean`.
+
+**Differentiability.** On a `C²` field the directional derivative `p ↦ ∂_v f` is itself
+real-differentiable (`differentiableAt_dWirtingerDir`): by §G it is a `weightedDirDeriv`, and
+`fderiv ℝ f` is differentiable for a `C²` `f`. Without this a Wirtinger derivative could not
+be differentiated a second time, as Schwarz (§I) does.
+
+**Locality.** The value `∂_v f` at `u` depends only on how `f` behaves near `u`, inherited
+from `fderiv ℝ f u`: the operator is built from it, and a Fréchet derivative is fixed by `f`
+on an arbitrarily small neighbourhood. So if `f₁` and `f₂` coincide on some neighbourhood of
+`u` (in Lean `f₁ =ᶠ[nhds u] f₂`, where `=ᶠ` is equality on a filter-large set and `[nhds u]`
+is the neighbourhood filter of `u`) they have the same directional derivative at `u`
+(`dWirtingerDir_congr_of_eventuallyEq`). This is what makes the operators usable on functions
+regular only on a restricted domain (the Kähler potentials, defined on a slit domain rather
+than all of `V`): the derivative at `u` needs only `f` near `u`, so a consumer may swap `f`
+for a locally-equal representative and rely on the local `C²`/holomorphy hypotheses
+(`ContDiffAt`, `DifferentiableAt`), which likewise depend only on `f` near `u`: their `...At`
+form asks for regularity only on a neighbourhood of `u`, which a restricted-domain function
+has at each point of its domain.
+
+-/
+
+/-- On a `C²` field the holomorphic directional derivative is itself
+real-differentiable. -/
+lemma differentiableAt_dWirtingerDir (hf2 : ContDiffAt ℝ 2 f u) (v : V) :
+    DifferentiableAt ℝ (fun p => dWirtingerDir f v p) u := by
+  rw [dWirtingerDir_eq_weightedDirDeriv]
+  exact (hasFDerivAt_weightedDirDeriv (differentiableAt_fderiv hf2) _ _ _).differentiableAt
+
+/-- On a `C²` field the anti-holomorphic directional derivative is itself
+real-differentiable. -/
+lemma differentiableAt_dWirtingerAntiDir (hf2 : ContDiffAt ℝ 2 f u) (w : V) :
+    DifferentiableAt ℝ (fun p => dWirtingerAntiDir f w p) u := by
+  rw [dWirtingerAntiDir_eq_weightedDirDeriv]
+  exact (hasFDerivAt_weightedDirDeriv (differentiableAt_fderiv hf2) _ _ _).differentiableAt
+
+/-- The holomorphic directional derivative depends only on the field near the point:
+fields agreeing on a neighbourhood have equal derivative. -/
+lemma dWirtingerDir_congr_of_eventuallyEq {f₁ f₂ : V → ℂ} {u : V}
+    (h : f₁ =ᶠ[nhds u] f₂) (v : V) :
+    dWirtingerDir f₁ v u = dWirtingerDir f₂ v u := by
+  simp only [dWirtingerDir, h.fderiv_eq]
+
+/-- The anti-holomorphic directional derivative depends only on the field near the
+point; dual of `dWirtingerDir_congr_of_eventuallyEq`. -/
+lemma dWirtingerAntiDir_congr_of_eventuallyEq {f₁ f₂ : V → ℂ} {u : V}
+    (h : f₁ =ᶠ[nhds u] f₂) (v : V) :
+    dWirtingerAntiDir f₁ v u = dWirtingerAntiDir f₂ v u := by
+  simp only [dWirtingerAntiDir, h.fderiv_eq]
+
+/-!
+
+## I. Schwarz's theorem
+
+-/
+
+/-- **Schwarz's theorem** for the directional Wirtinger operators: on a `C²` field `f` the
+holomorphic and anti-holomorphic directional derivatives commute in any two directions,
+`∂_v ∂̄_w f = ∂̄_w ∂_v f`.
+
+The commutation adds no analytic input. By the §G bridge each order expands into a real-linear
+combination of the second real Fréchet derivative `fderiv ℝ (fderiv ℝ f) u` on the four
+directions `v`, `i·v`, `w`, `i·w`. The two orders give the same combination up to transposing
+the two slots of that second derivative, and `ContDiffAt.isSymmSndFDerivAt`, the symmetry of
+ordinary mixed second partials, equates them. -/
+theorem dWirtingerDir_dWirtingerAntiDir_comm (hf2 : ContDiffAt ℝ 2 f u) (v w : V) :
+    dWirtingerDir (fun p => dWirtingerAntiDir f w p) v u
+      = dWirtingerAntiDir (fun p => dWirtingerDir f v p) w u := by
+  have hf' := differentiableAt_fderiv hf2
+  have hsymm : IsSymmSndFDerivAt ℝ f u := hf2.isSymmSndFDerivAt (by simp)
+  rw [dWirtingerDir_apply (fun p => dWirtingerAntiDir f w p) v u,
+    dWirtingerAntiDir_apply (fun p => dWirtingerDir f v p) w u,
+    fderiv_dWirtingerAntiDir hf', fderiv_dWirtingerAntiDir hf',
+    fderiv_dWirtingerDir hf', fderiv_dWirtingerDir hf',
+    hsymm.eq w v, hsymm.eq w (Complex.I • v),
+    hsymm.eq (Complex.I • w) v, hsymm.eq (Complex.I • w) (Complex.I • v)]
+  ring
+
+end Physlib.Wirtinger
+
+end
+
+end
diff --git a/Physlib/Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean b/Physlib/Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean
new file mode 100644
index 000000000..55dd5a71c
--- /dev/null
+++ b/Physlib/Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean
@@ -0,0 +1,340 @@
+/-
+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 Physlib.Mathematics.Calculus.Wirtinger.Coordinate
+public import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+
+/-!
+
+# Half-plane Wirtinger calculus on `ι → ℂ`
+
+Model-independent complex-analysis on the configuration space `ι → ℂ`, reusable by
+any logarithmic half-plane potential. The headline object is the real-linear
+coordinate argument `coordArgCLM a b I u = a·zᴵ + b·z̄ᴵ`, with Wirtinger
+derivatives `∂_J coordArg = a·δ_{JI}`, `∂̄_J coordArg = b·δ_{JI}` and the
+derivatives of `∑ log ∘ coordArg`. Under the realness condition `b = star a` it is
+the positive real `2 Re(a·zᴵ)` on the slit plane. Two instances:
+
+- `imArgCLM = coordArgCLM (−i) i` — the upper half-plane, `arg = 2 Im(zᴵ)`;
+- `reArgCLM = coordArgCLM 1 1` — the right half-plane, `arg = 2 Re(zᴵ)`.
+
+The open slit-set `{v | ∀ I, imArgCLM I v ∈ Complex.slitPlane}` (a product of
+upper half-planes) and its non-vanishing facts are recorded for the `imArgCLM`
+instance.
+
+This is the calculus layer: everything uses the raw `dWirtingerCoord` /
+`dWirtingerAntiCoord` operators, with no SUSY content.
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace Physlib.Wirtinger
+
+variable {ι : Type*} [Fintype ι] [DecidableEq ι]
+
+/-!
+
+## A. The general coordinate argument `coordArgCLM`
+
+-/
+
+/-- The inner real-linear map `imArgCLM I u = i (star (uᴵ) − uᴵ)`, the ℂ-valued
+projection onto `2 Im(uᴵ)`. Built from the coordinate CLMs `coordProjCLM I` and
+`conjCoordCLM I`; on the upper half-plane it is the positive real `2 Im(uᴵ)`. -/
+def imArgCLM (I : ι) : (ι → ℂ) →L[ℝ] ℂ :=
+  (-Complex.I) • (coordProjCLM I - conjCoordCLM I)
+
+/-- The general ℝ-linear coordinate argument `coordArgCLM a b I u = a·uᴵ + b·z̄ᴵ`.
+`imArgCLM` is the `(−i, i)` instance and `reArgCLM` the `(1, 1)` instance; the map
+is real-linear (the `z̄` term is conjugate-linear), hence a `→L[ℝ]`. -/
+def coordArgCLM (a b : ℂ) (I : ι) : (ι → ℂ) →L[ℝ] ℂ :=
+  a • coordProjCLM I + b • conjCoordCLM I
+
+omit [Fintype ι] [DecidableEq ι] in
+@[simp] lemma coordArgCLM_apply (a b : ℂ) (I : ι) (u : ι → ℂ) :
+    coordArgCLM a b I u = a * u I + b * star (u I) := by
+  simp only [coordArgCLM, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
+    coordProjCLM_apply, conjCoordCLM_apply, smul_eq_mul]
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- Under the realness condition `b = star a` the coordinate argument is a real:
+`coordArgCLM a (star a) I u = a·uᴵ + ā·z̄ᴵ = ↑(2 Re(a·uᴵ))`. Both instances satisfy
+it (`imArgCLM`: `star (−i) = i`; `reArgCLM`: `star 1 = 1`), making the argument a
+*positive* real on the slit plane — the hypothesis of the metric/positivity story. -/
+lemma coordArgCLM_eq_ofReal (a : ℂ) (I : ι) (u : ι → ℂ) :
+    coordArgCLM a (star a) I u = ((2 * (a * u I).re : ℝ) : ℂ) := by
+  simp only [coordArgCLM_apply, Complex.star_def]
+  apply Complex.ext <;>
+    simp only [Complex.add_re, Complex.add_im, Complex.mul_re, Complex.mul_im,
+      Complex.conj_re, Complex.conj_im, Complex.ofReal_re, Complex.ofReal_im] <;>
+    ring
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- `imArgCLM` is the `(−i, i)` instance of `coordArgCLM`. -/
+lemma imArgCLM_eq_coordArgCLM (I : ι) :
+    imArgCLM I = coordArgCLM (-Complex.I) Complex.I I := by
+  ext u
+  simp only [imArgCLM, coordArgCLM, ContinuousLinearMap.smul_apply,
+    ContinuousLinearMap.add_apply, ContinuousLinearMap.sub_apply,
+    coordProjCLM_apply, conjCoordCLM_apply, smul_eq_mul]
+  ring
+
+/-- Holomorphic Wirtinger derivative of the general argument: `∂_J (coordArg a b I) = a·δ_JI`. -/
+lemma dWirtingerCoord_coordArgCLM (a b : ℂ) (I J : ι) (u : ι → ℂ) :
+    dWirtingerCoord (fun v : ι → ℂ => coordArgCLM a b I v) J u = if J = I then a else 0 := by
+  have e : (fun v : ι → ℂ => coordArgCLM a b I v)
+      = ⇑(a • coordProjCLM I) + ⇑(b • conjCoordCLM I) := by
+    funext v
+    simp only [coordArgCLM, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
+      Pi.add_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply]
+  rw [e, dWirtingerCoord_add_apply (a • coordProjCLM I).differentiableAt
+        (b • conjCoordCLM I).differentiableAt J,
+      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_smul',
+      dWirtingerCoord_smul_apply a (coordProjCLM I).differentiableAt J,
+      dWirtingerCoord_smul_apply b (conjCoordCLM I).differentiableAt J]
+  have h1 : dWirtingerCoord (⇑(coordProjCLM I)) J u = if J = I then 1 else 0 :=
+    congrFun (dWirtingerCoord_coordProj J I) u
+  have h2 : dWirtingerCoord (⇑(conjCoordCLM I)) J u = 0 :=
+    congrFun (dWirtingerCoord_conjCoord J I) u
+  rw [h1, h2]
+  by_cases h : J = I <;> simp [h]
+
+/-- Anti-holomorphic Wirtinger derivative of the general argument: `∂̄_J coordArg = b·δ_JI`. -/
+lemma dWirtingerAntiCoord_coordArgCLM (a b : ℂ) (I J : ι) (u : ι → ℂ) :
+    dWirtingerAntiCoord (fun v : ι → ℂ => coordArgCLM a b I v) J u = if J = I then b else 0 := by
+  have e : (fun v : ι → ℂ => coordArgCLM a b I v)
+      = ⇑(a • coordProjCLM I) + ⇑(b • conjCoordCLM I) := by
+    funext v
+    simp only [coordArgCLM, ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,
+      Pi.add_apply, ContinuousLinearMap.coe_smul', Pi.smul_apply]
+  rw [e, dWirtingerAntiCoord_add_apply (a • coordProjCLM I).differentiableAt
+        (b • conjCoordCLM I).differentiableAt J,
+      ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_smul',
+      dWirtingerAntiCoord_smul_apply a (coordProjCLM I).differentiableAt J,
+      dWirtingerAntiCoord_smul_apply b (conjCoordCLM I).differentiableAt J]
+  have h1 : dWirtingerAntiCoord (⇑(coordProjCLM I)) J u = 0 :=
+    congrFun (dWirtingerAntiCoord_coordProj J I) u
+  have h2 : dWirtingerAntiCoord (⇑(conjCoordCLM I)) J u = if J = I then 1 else 0 :=
+    congrFun (dWirtingerAntiCoord_conjCoord J I) u
+  rw [h1, h2]
+  by_cases h : J = I <;> simp [h]
+
+omit [Fintype ι] [DecidableEq ι] in
+@[simp] lemma imArgCLM_apply (I : ι) (u : ι → ℂ) :
+    imArgCLM I u = Complex.I * (star (u I) - u I) := by
+  simp only [imArgCLM, ContinuousLinearMap.smul_apply, ContinuousLinearMap.sub_apply,
+    coordProjCLM_apply, conjCoordCLM_apply, smul_eq_mul]
+  ring
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- The inner map is the positive real `2 Im(uᴵ)`, viewed in ℂ:
+`imArgCLM I u = ↑(2 Im(uᴵ))`. -/
+lemma imArgCLM_eq_ofReal (I : ι) (u : ι → ℂ) :
+    imArgCLM I u = ((2 * (u I).im : ℝ) : ℂ) := by
+  rw [imArgCLM_apply, Complex.star_def]
+  apply Complex.ext <;>
+    simp only [Complex.mul_re, Complex.mul_im, Complex.sub_re, Complex.sub_im,
+      Complex.conj_re, Complex.conj_im, Complex.I_re, Complex.I_im, Complex.ofReal_re,
+      Complex.ofReal_im] <;>
+    ring
+
+/-!
+
+## B. The slit set and the upper half-plane
+
+-/
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- On the slit plane the inner argument is a *positive* real: membership of
+`imArgCLM I u = ↑(2 Im(uᴵ))` forces `0 < Im(uᴵ)`, i.e. `uᴵ` lies in the upper
+half-plane. -/
+lemma im_pos_of_mem_slitPlane {I : ι} {u : ι → ℂ}
+    (h : imArgCLM I u ∈ Complex.slitPlane) : 0 < (u I).im := by
+  rw [imArgCLM_eq_ofReal] at h
+  have := Complex.ofReal_mem_slitPlane.1 h
+  linarith
+
+omit [DecidableEq ι] in
+/-- The set of configurations on which every inner argument `imArgCLM I v` lies in
+the slit plane is open: a finite intersection of preimages of the open set
+`Complex.slitPlane` under the continuous CLMs `imArgCLM I`. -/
+lemma isOpen_slitSet :
+    IsOpen {v : ι → ℂ | ∀ I, imArgCLM I v ∈ Complex.slitPlane} := by
+  rw [Set.setOf_forall]
+  exact isOpen_iInter_of_finite fun I =>
+    (imArgCLM I).continuous.isOpen_preimage _ Complex.isOpen_slitPlane
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- Non-vanishing of `z − z̄` on the upper half-plane, via slit-plane membership of
+the inner map: `uᴶ − star (uᴶ) ≠ 0`. -/
+lemma sub_star_ne_zero {u : ι → ℂ} {J : ι}
+    (h : imArgCLM J u ∈ Complex.slitPlane) : u J - star (u J) ≠ 0 := fun hzero =>
+  Complex.slitPlane_ne_zero h <| by
+    rw [imArgCLM_apply, ← neg_sub, hzero, neg_zero, mul_zero]
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- Mirror of `sub_star_ne_zero` with the subtraction reversed: `star (zᴶ) − zᴶ ≠ 0`
+on the slit plane — the orientation `field_simp` needs. -/
+lemma star_sub_ne_zero {u : ι → ℂ} {J : ι}
+    (h : imArgCLM J u ∈ Complex.slitPlane) : star (u J) - u J ≠ 0 := by
+  rw [← neg_sub]; exact neg_ne_zero.mpr (sub_star_ne_zero h)
+
+/-!
+
+## C. Wirtinger derivatives of `∑ log ∘ coordArgCLM`
+
+-/
+
+omit [DecidableEq ι] in
+/-- Every summand `Complex.log ∘ coordArgCLM a b I` is real-differentiable at `u`
+once its inner argument lies in the slit plane. -/
+private lemma differentiableAt_log_coordArgCLM {a b : ℂ} {u : ι → ℂ}
+    (h : ∀ I, coordArgCLM a b I u ∈ Complex.slitPlane) (I : ι) :
+    DifferentiableAt ℝ (fun v : ι → ℂ => Complex.log (coordArgCLM a b I v)) u :=
+  ((hasFDerivAt_restrictScalarsℝℂ (Complex.hasDerivAt_log (h I)).hasFDerivAt).comp u
+    (coordArgCLM a b I).hasFDerivAt).differentiableAt
+
+/-- Closed form of the holomorphic Wirtinger derivative of a single log summand:
+`(coordArgCLM a b I u)⁻¹ · (a · δ_{JI})`. -/
+private lemma dWirtingerCoord_log_comp_coordArgCLM {a b : ℂ} {u : ι → ℂ}
+    (h : ∀ I, coordArgCLM a b I u ∈ Complex.slitPlane) (I J : ι) :
+    dWirtingerCoord (fun v : ι → ℂ => Complex.log (coordArgCLM a b I v)) J u =
+      (coordArgCLM a b I u)⁻¹ * (if J = I then a else 0) := by
+  rw [dWirtingerCoord_comp_holomorphic_apply (Complex.differentiableAt_log (h I))
+    (coordArgCLM a b I).hasFDerivAt.differentiableAt J, dWirtingerCoord_coordArgCLM,
+    (Complex.hasDerivAt_log (h I)).deriv]
+
+/-- Holomorphic Wirtinger derivative of the summed log argument: collapses to
+`(coordArgCLM a b J u)⁻¹ · a`. -/
+lemma dWirtingerCoord_sum_log_comp_coordArgCLM {a b : ℂ} {u : ι → ℂ}
+    (h : ∀ I, coordArgCLM a b I u ∈ Complex.slitPlane) (J : ι) :
+    dWirtingerCoord (fun v : ι → ℂ => ∑ I, Complex.log (coordArgCLM a b I v)) J u =
+      (coordArgCLM a b J u)⁻¹ * a := by
+  have hsum :
+      dWirtingerCoord (fun v : ι → ℂ => ∑ I, Complex.log (coordArgCLM a b I v)) J u =
+        ∑ I, dWirtingerCoord (fun v : ι → ℂ => Complex.log (coordArgCLM a b I v)) J u := by
+    simpa using dWirtingerCoord_fun_sum_apply (s := Finset.univ)
+      (F := fun I v => Complex.log (coordArgCLM a b I v))
+      (fun I _ => differentiableAt_log_coordArgCLM h I) J
+  rw [hsum]
+  simp_rw [dWirtingerCoord_log_comp_coordArgCLM h]
+  rw [Finset.sum_eq_single J
+    (fun I _ hI => by rw [if_neg (Ne.symm hI)]; ring)
+    (fun hJ => absurd (Finset.mem_univ J) hJ), if_pos rfl]
+
+/-- Closed form of the anti-holomorphic Wirtinger derivative of a single log
+summand: `(coordArgCLM a b I u)⁻¹ · (b · δ_{JI})`. -/
+private lemma dWirtingerAntiCoord_log_comp_coordArgCLM {a b : ℂ} {u : ι → ℂ}
+    (h : ∀ I, coordArgCLM a b I u ∈ Complex.slitPlane) (I J : ι) :
+    dWirtingerAntiCoord (fun v : ι → ℂ => Complex.log (coordArgCLM a b I v)) J u =
+      (coordArgCLM a b I u)⁻¹ * (if J = I then b else 0) := by
+  rw [dWirtingerAntiCoord_comp_holomorphic_apply (Complex.differentiableAt_log (h I))
+    (coordArgCLM a b I).hasFDerivAt.differentiableAt J, dWirtingerAntiCoord_coordArgCLM,
+    (Complex.hasDerivAt_log (h I)).deriv]
+
+/-- Anti-holomorphic Wirtinger derivative of the summed log argument: collapses to
+`(coordArgCLM a b J u)⁻¹ · b`. -/
+lemma dWirtingerAntiCoord_sum_log_comp_coordArgCLM {a b : ℂ} {u : ι → ℂ}
+    (h : ∀ I, coordArgCLM a b I u ∈ Complex.slitPlane) (J : ι) :
+    dWirtingerAntiCoord (fun v : ι → ℂ => ∑ I, Complex.log (coordArgCLM a b I v)) J u =
+      (coordArgCLM a b J u)⁻¹ * b := by
+  have hsum :
+      dWirtingerAntiCoord (fun v : ι → ℂ => ∑ I, Complex.log (coordArgCLM a b I v)) J u =
+        ∑ I, dWirtingerAntiCoord (fun v : ι → ℂ => Complex.log (coordArgCLM a b I v)) J u := by
+    simpa using dWirtingerAntiCoord_fun_sum_apply (s := Finset.univ)
+      (F := fun I v => Complex.log (coordArgCLM a b I v))
+      (fun I _ => differentiableAt_log_coordArgCLM h I) J
+  rw [hsum]
+  simp_rw [dWirtingerAntiCoord_log_comp_coordArgCLM h]
+  rw [Finset.sum_eq_single J
+    (fun I _ hI => by rw [if_neg (Ne.symm hI)]; ring)
+    (fun hJ => absurd (Finset.mem_univ J) hJ), if_pos rfl]
+
+/-!
+
+## D. The upper half-plane instance `imArgCLM = coordArgCLM (−i) i`
+
+-/
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- Slit-plane membership transports between `imArgCLM` and its `coordArgCLM`
+form, the bridge through which the `imArgCLM` log-chain lemmas reduce to the
+general ones. -/
+private lemma mem_slitPlane_coordArgCLM_of_imArgCLM {u : ι → ℂ}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (I : ι) :
+    coordArgCLM (-Complex.I) Complex.I I u ∈ Complex.slitPlane := by
+  rw [← imArgCLM_eq_coordArgCLM]; exact h I
+
+/-- Holomorphic Wirtinger derivative of the summed log argument on `H^n`: the
+`(−i, i)` instance of `dWirtingerCoord_sum_log_comp_coordArgCLM`. -/
+lemma dWirtingerCoord_sum_log_comp_imArgCLM {u : ι → ℂ}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (J : ι) :
+    dWirtingerCoord (fun v : ι → ℂ => ∑ I, Complex.log (imArgCLM I v)) J u =
+      (imArgCLM J u)⁻¹ * (-Complex.I) := by
+  simp_rw [imArgCLM_eq_coordArgCLM]
+  exact dWirtingerCoord_sum_log_comp_coordArgCLM (mem_slitPlane_coordArgCLM_of_imArgCLM h) J
+
+/-- Anti-holomorphic Wirtinger derivative of the summed log argument on `H^n`: the
+`(−i, i)` instance of `dWirtingerAntiCoord_sum_log_comp_coordArgCLM`. -/
+lemma dWirtingerAntiCoord_sum_log_comp_imArgCLM {u : ι → ℂ}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (J : ι) :
+    dWirtingerAntiCoord (fun v : ι → ℂ => ∑ I, Complex.log (imArgCLM I v)) J u =
+      (imArgCLM J u)⁻¹ * Complex.I := by
+  simp_rw [imArgCLM_eq_coordArgCLM]
+  exact dWirtingerAntiCoord_sum_log_comp_coordArgCLM (mem_slitPlane_coordArgCLM_of_imArgCLM h) J
+
+/-!
+
+## E. The right half-plane instance `reArgCLM = coordArgCLM 1 1`
+
+-/
+
+/-- The right-half-plane coordinate argument `reArgCLM I u = uᴵ + z̄ᴵ = 2 Re(uᴵ)`,
+the `(1, 1)` instance of `coordArgCLM`; on the right half-plane it is the positive
+real `2 Re(uᴵ)`, the no-scale modulus combination `T + T̄`. -/
+def reArgCLM (I : ι) : (ι → ℂ) →L[ℝ] ℂ := coordArgCLM 1 1 I
+
+omit [Fintype ι] [DecidableEq ι] in
+@[simp] lemma reArgCLM_apply (I : ι) (u : ι → ℂ) :
+    reArgCLM I u = u I + star (u I) := by
+  simp only [reArgCLM, coordArgCLM_apply, one_mul]
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- The right-half-plane argument is the positive real `2 Re(uᴵ)`, viewed in ℂ. -/
+lemma reArgCLM_eq_ofReal (I : ι) (u : ι → ℂ) :
+    reArgCLM I u = ((2 * (u I).re : ℝ) : ℂ) := by
+  have h : reArgCLM I u = coordArgCLM (1 : ℂ) (star (1 : ℂ)) I u := by rw [reArgCLM, star_one]
+  rw [h, coordArgCLM_eq_ofReal, one_mul]
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- On the open right half-plane the argument lies in the slit plane: `0 < Re(uᴵ)`
+forces `reArgCLM I u = ↑(2 Re uᴵ)` to be a positive real. -/
+lemma reArgCLM_mem_slitPlane {I : ι} {u : ι → ℂ} (h : 0 < (u I).re) :
+    reArgCLM I u ∈ Complex.slitPlane := by
+  rw [reArgCLM_eq_ofReal]
+  exact Complex.ofReal_mem_slitPlane.2 (by linarith)
+
+/-- Holomorphic Wirtinger derivative of the right-half-plane argument:
+`∂_J reArg = δ_{JI}` (the `(1, 1)` instance of `dWirtingerCoord_coordArgCLM`). -/
+lemma dWirtingerCoord_reArgCLM (I J : ι) (u : ι → ℂ) :
+    dWirtingerCoord (fun v : ι → ℂ => reArgCLM I v) J u = if J = I then 1 else 0 := by
+  simpa only [reArgCLM] using dWirtingerCoord_coordArgCLM 1 1 I J u
+
+/-- Anti-holomorphic Wirtinger derivative of the right-half-plane argument:
+`∂̄_J reArg = δ_{JI}` (the `(1, 1)` instance of `dWirtingerAntiCoord_coordArgCLM`). -/
+lemma dWirtingerAntiCoord_reArgCLM (I J : ι) (u : ι → ℂ) :
+    dWirtingerAntiCoord (fun v : ι → ℂ => reArgCLM I v) J u = if J = I then 1 else 0 := by
+  simpa only [reArgCLM] using dWirtingerAntiCoord_coordArgCLM 1 1 I J u
+
+end Physlib.Wirtinger
+
+end
+
+end
diff --git a/Physlib/Particles/SuperSymmetry/N1/Derivative.lean b/Physlib/Particles/SuperSymmetry/N1/Derivative.lean
new file mode 100644
index 000000000..0e83b6e9e
--- /dev/null
+++ b/Physlib/Particles/SuperSymmetry/N1/Derivative.lean
@@ -0,0 +1,83 @@
+/-
+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 Physlib.Particles.SuperSymmetry.N1.Basic
+public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
+
+/-!
+
+# SUSY N=1 chiral sector — the scalar derivatives
+
+## i. Overview
+
+The chiral and anti-chiral derivatives `∂_I` / `∂_J̄` of the N=1 chiral sector,
+as the `Model` methods `M.dChiralScalar` / `M.dAntiChiralScalar` — thin wrappers
+over the coordinate Wirtinger calculus of
+`Mathematics/Calculus/Wirtinger/Coordinate.lean`. They bind each index type of
+the `Model` to a differentiation *direction*, so **a barred derivative is taken
+with respect to the anti-chiral field, never the chiral one**:
+
+* `M.dChiralScalar` (chiral index `I : C`) — the holomorphic `∂/∂z^I`, w.r.t. the
+  chiral configuration; the model `M` is inert here (the chiral slot needs no
+  relabel), taken only for a uniform call shape;
+* `M.dAntiChiralScalar` (barred index `J̄ : A`) — the anti-holomorphic `∂/∂z̄^J̄`,
+  w.r.t. the anti-chiral configuration; it also bundles the `A → C` relabel
+  (`equiv.symm`) the barred index needs.
+
+The `C`/`A` index types keep the two from being confused; proofs `rw` to
+`dWirtingerCoord` / `dWirtingerAntiCoord` to use the Wirtinger calculus.
+
+## ii. Key results
+
+- `SUSY.N1.Model.dChiralScalar` / `SUSY.N1.Model.dAntiChiralScalar` : the chiral /
+    anti-chiral derivatives `∂_I` / `∂_J̄` (written `M.dChiralScalar` /
+    `M.dAntiChiralScalar`), wrapping `dWirtingerCoord` / `dWirtingerAntiCoord`.
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace SUSY.N1
+
+open Physlib.Wirtinger
+
+variable {C : Type*} [Fintype C] [DecidableEq C]
+variable {A : Type*} [Fintype A]
+
+namespace Model
+
+/-- The chiral derivative `∂_I` along a chiral index `I : C`, written
+`M.dChiralScalar f I`: differentiation w.r.t. the chiral configuration — the
+holomorphic Wirtinger derivative `∂/∂z^I`. The model `M` plays no role for the
+chiral slot (only `dAntiChiralScalar` needs `equiv`); it is taken so the chiral
+and anti-chiral derivatives share the uniform `M.dChiralScalar` /
+`M.dAntiChiralScalar` call shape. -/
+@[nolint unusedArguments]
+abbrev dChiralScalar (_M : Model C A) (f : ChiralScalarConfiguration C → ℂ) (I : C) :
+    ChiralScalarConfiguration C → ℂ :=
+  dWirtingerCoord f I
+
+/-- The anti-chiral derivative `∂_J̄` along a barred index `J̄ : A`, written
+`M.dAntiChiralScalar f J̄`: the anti-holomorphic Wirtinger derivative `∂/∂z̄^J̄`.
+
+It differentiates a function of the *single* chiral configuration `C → ℂ`; there
+is no `A`-indexed configuration to differentiate (no doubling — see `Basic.lean`).
+`A` contributes only the barred index `Jbar`, which `M`'s `equiv.symm` relabels to
+its chiral coordinate before the underlying operator acts. -/
+abbrev dAntiChiralScalar (M : Model C A) (f : ChiralScalarConfiguration C → ℂ) (Jbar : A) :
+    ChiralScalarConfiguration C → ℂ :=
+  dWirtingerAntiCoord f (M.equiv.symm Jbar)
+
+end Model
+
+end SUSY.N1
+
+end
+
+end
diff --git a/Physlib/Particles/SuperSymmetry/N1/KahlerMetric.lean b/Physlib/Particles/SuperSymmetry/N1/KahlerMetric.lean
new file mode 100644
index 000000000..3c69ffcd9
--- /dev/null
+++ b/Physlib/Particles/SuperSymmetry/N1/KahlerMetric.lean
@@ -0,0 +1,129 @@
+/-
+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 Physlib.Particles.SuperSymmetry.N1.KahlerPotential
+public import Physlib.Particles.SuperSymmetry.N1.Derivative
+
+/-!
+
+# N=1 SUSY — the abstract Kähler metric
+
+## i. Overview
+
+The Kähler metric is the geometric object that turns a Kähler potential into a
+field-space metric: a hermitian pairing on the tangent space of chiral scalar
+field space, locally given by the mixed second Wirtinger derivative of `K`.
+Once `K` is fixed (any `KahlerPotential`), the metric is determined,
+
+  `g_{IJ̄}(u) = ∂_I ∂_J̄ K`     (`KahlerPotential.metric`)
+
+— a chiral derivative of an anti-chiral one. This file takes the metric on
+*any* `KahlerPotential` and proves the one structural property that holds for
+all of them: **hermiticity**,
+
+  `star (g_{IJ̄}) = g_{JĪ}`     (`KahlerPotential.metric_hermitian`)
+
+on the regular domain. The proof is the promised payoff of the design: reality
+of `K` — automatic because its codomain is `ℝ`, packaged as
+`star ∘ K.lift = K.lift` — turns the conjugation into `∂_J̄ ∂_I K` via the
+conjugation lemmas of `Mathematics/Calculus/Wirtinger/Coordinate.lean`,
+and **Schwarz's theorem** (`dWirtingerCoord_dWirtingerAntiCoord_comm`) commutes that back to
+`∂_I ∂_J̄ K`. The `C²` regularity carried by `KahlerPotential` is exactly what
+both steps consume.
+
+The canonical consumer is the concrete `Hⁿ` log potential of
+`Particles/SuperSymmetry/N1/LogKahlerHn.lean`: its `kahlerMetric` is defined as `K.metric` of that
+very `KahlerPotential`, and the Poincaré metric is the closed form of this
+abstract `g_{IJ̄}` at that instance.
+
+## ii. Key results
+
+- `SUSY.N1.KahlerPotential.metric` : the Kähler metric `g_{IJ̄} = ∂_I ∂_J̄ K`.
+- `SUSY.N1.KahlerPotential.metric_hermitian` : hermiticity
+    `star (g_{IJ̄}) = g_{JĪ}` on the domain.
+
+## iii. Table of contents
+
+- A. The Kähler metric
+- B. Hermiticity
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace SUSY.N1
+
+open Physlib.Wirtinger
+
+namespace KahlerPotential
+
+variable {C : Type*} [Fintype C] [DecidableEq C]
+
+/-!
+
+## A. The Kähler metric
+
+The metric is the mixed second Wirtinger derivative of the ℂ-lift, `∂_I ∂_J̄ K`
+— a chiral derivative of an anti-chiral one, both drawn from the operators of
+`Mathematics/Calculus/Wirtinger/Coordinate.lean`. It mirrors the concrete `kahlerMetric` of
+`Particles/SuperSymmetry/N1/LogKahlerHn.lean`, but is taken on an arbitrary `KahlerPotential`; the
+concrete `H^n` potential of `Particles/SuperSymmetry/N1/LogKahlerHn.lean` is one instance
+(`kahlerMetric := K.metric`).
+
+-/
+
+variable {A : Type*} [Fintype A]
+
+/-- The Kähler metric `g_{IJ̄}(u) = ∂_I ∂_J̄ K` of an abstract Kähler potential:
+`M.dChiralScalar` (holomorphic slot `I : C`) of `M.dAntiChiralScalar`
+(barred slot `J̄ : A`), on the ℂ-lift. -/
+def metric (K : KahlerPotential C) (M : Model C A)
+    (I : C) (Jbar : A) (u : ChiralScalarConfiguration C) : ℂ :=
+  M.dChiralScalar (fun v => M.dAntiChiralScalar K.lift Jbar v) I u
+
+/-!
+
+## B. Hermiticity
+
+-/
+
+/-- **Hermiticity** of the Kähler metric: `star (g_{IJ̄}) = g_{JĪ}` at any point of
+the regular domain, slots swapped via `equiv`. Reality of `K` (free from the `ℝ`
+codomain, packaged as `star ∘ K.lift = K.lift`) turns the conjugate of `∂_I ∂_J̄ K`
+into `∂_J̄ ∂_I K`, which Schwarz's theorem `dWirtingerCoord_dWirtingerAntiCoord_comm`
+commutes back. `hu` supplies the `C²` regularity. -/
+theorem metric_hermitian (K : KahlerPotential C) (M : Model C A)
+    {u : ChiralScalarConfiguration C} (hu : u ∈ K.domain)
+    (I : C) (Jbar : A) :
+    star (K.metric M I Jbar u) = K.metric M (M.equiv.symm Jbar) (M.equiv I) u := by
+  have hg2 : ContDiffAt ℝ 2 K.lift u := K.contDiffAt_of_mem hu
+  have hinner : DifferentiableAt ℝ
+      (fun v => dWirtingerAntiCoord K.lift (M.equiv.symm Jbar) v) u :=
+    differentiableAt_dWirtingerAntiCoord hg2 (M.equiv.symm Jbar)
+  -- Near `u`, conjugating the anti-chiral derivative of `K` gives its chiral
+  -- derivative (reality of `K` via `star_lift` + the conjugation lemma).
+  have heq_chiral : (fun v => star (dWirtingerAntiCoord K.lift (M.equiv.symm Jbar) v))
+      =ᶠ[nhds u] (fun v => dWirtingerCoord K.lift (M.equiv.symm Jbar) v) := by
+    filter_upwards [K.domain_open.mem_nhds hu] with v hv
+    rw [← dWirtingerCoord_star_comp_apply (K.differentiableAt_of_mem hv) (M.equiv.symm Jbar),
+      K.star_lift]
+  show star (dWirtingerCoord (fun v => dWirtingerAntiCoord K.lift (M.equiv.symm Jbar) v) I u)
+      = dWirtingerCoord
+          (fun v => dWirtingerAntiCoord K.lift (M.equiv.symm (M.equiv I)) v) (M.equiv.symm Jbar) u
+  rw [M.equiv.symm_apply_apply, ← dWirtingerAntiCoord_star_comp_apply hinner I,
+    dWirtingerAntiCoord_congr_of_eventuallyEq_apply heq_chiral I]
+  exact (dWirtingerCoord_dWirtingerAntiCoord_comm hg2 (M.equiv.symm Jbar) I).symm
+
+end KahlerPotential
+
+end SUSY.N1
+
+end
+
+end
diff --git a/Physlib/Particles/SuperSymmetry/N1/KahlerPotential.lean b/Physlib/Particles/SuperSymmetry/N1/KahlerPotential.lean
new file mode 100644
index 000000000..d5806f02e
--- /dev/null
+++ b/Physlib/Particles/SuperSymmetry/N1/KahlerPotential.lean
@@ -0,0 +1,166 @@
+/-
+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 Physlib.Particles.SuperSymmetry.N1.Basic
+public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
+public import Mathlib.Analysis.Calculus.ContDiff.Basic
+
+/-!
+
+# N=1 SUSY — the abstract Kähler potential
+
+## i. Overview
+
+This module introduces the abstract `KahlerPotential` data of an N=1 model: a
+real-valued function `K` of the chiral scalars, twice continuously
+differentiable on an open domain. It is the abstraction-first counterpart of
+the concrete `Hⁿ` log potential in `Particles/SuperSymmetry/N1/LogKahlerHn.lean`.
+
+The codomain is `ℝ`, not `ℂ`: a Kähler potential is a physical real
+observable, so reality is enforced by the type rather than a separate `IsReal`
+predicate. The Wirtinger operators of `Mathematics/Calculus/Wirtinger/Coordinate.lean`
+act on `ℂ`-valued
+functions, so derivatives are taken on the ℂ-lift
+`fun u => ((K u : ℝ) : ℂ)`, whose regularity follows from that of `K` via the
+continuous ℝ-linear map `Complex.ofRealCLM` (`contDiffOn_lift`). The payoff is
+reality of the lift, `star ∘ K.lift = K.lift` (`star_lift`) — the keystone of
+Kähler-metric hermiticity in `Particles/SuperSymmetry/N1/KahlerMetric.lean`.
+
+The regularity is `C²` on the domain: the mixed second derivative `∂_I ∂_J̄ K`
+and the Schwarz step behind its hermiticity both need the first derivative to be
+differentiable in turn, which `C²` supplies (`differentiableAt_of_mem` is the
+weaker first-order fact the hermiticity proof also uses).
+
+## ii. Key results
+
+All regularity is over `ℝ` (i.e. `ContDiffOn ℝ`, `DifferentiableAt ℝ`): a
+real-valued `K` cannot be `ℂ`-differentiable except as a constant, and the
+Wirtinger operators of `Mathematics/Calculus/Wirtinger/Coordinate.lean` are built
+on `fderiv ℝ` anyway.
+
+- `SUSY.N1.KahlerPotential` : the abstract Kähler-potential structure
+    (real-valued, `ℝ`-`C²` on an open domain).
+- `SUSY.N1.KahlerPotential.lift` : the ℂ-lift fed to the Wirtinger operators
+    (the chiral derivative `∂_I K` is then `dWirtingerCoord K.lift I`).
+- `SUSY.N1.KahlerPotential.contDiffOn_lift` : the lift inherits the potential's
+    `ℝ`-`C²` regularity, via `Complex.ofRealCLM`.
+- `SUSY.N1.KahlerPotential.contDiffAt_of_mem` / `differentiableAt_of_mem` :
+    `ℝ`-`C²` / `ℝ`-differentiability of the lift at a point of the domain.
+
+## iii. Table of contents
+
+- A. The Kähler potential structure
+- B. The ℂ-lift
+- C. Regularity accessors
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace SUSY.N1
+
+variable {C : Type*} [Fintype C]
+
+/-!
+
+## A. The Kähler potential structure
+
+A `KahlerPotential` is a real function `toFun` of the chiral scalars, defined
+with second-order regularity on an open `domain`. Globally-smooth potentials
+take `domain := Set.univ`; partial-domain ones (such as the `Hⁿ` log
+potential, smooth only on the slit locus) take a proper open subset.
+
+-/
+
+/-- The abstract Kähler potential of an N=1 model: a real-valued function of
+the chiral scalars, with `ContDiffOn ℝ 2` regularity on an open domain.
+Reality is by construction from the `ℝ` codomain; derivatives are taken on the
+ℂ-lift `fun u => ((toFun u : ℝ) : ℂ)`. -/
+structure KahlerPotential (C : Type*) [Fintype C] where
+  /-- The (real) Kähler potential as a function of the chiral scalars. -/
+  toFun : ChiralScalarConfiguration C → ℝ
+  /-- The open set on which the potential is regular. -/
+  domain : Set (ChiralScalarConfiguration C)
+  /-- The domain is open. -/
+  domain_open : IsOpen domain
+  /-- The (real) potential is twice continuously real-differentiable on the
+  domain. The ℂ-lift's regularity is derived (`contDiffOn_lift`). -/
+  contDiffOn : ContDiffOn ℝ 2 toFun domain
+
+namespace KahlerPotential
+
+/-- Write `K u` for `K.toFun u`. -/
+instance : CoeFun (KahlerPotential C)
+    (fun _ => ChiralScalarConfiguration C → ℝ) where
+  coe := toFun
+
+/-!
+
+## B. The ℂ-lift
+
+The Wirtinger operators of `Mathematics/Calculus/Wirtinger/Coordinate.lean` act on
+`ℂ`-valued functions, so
+the real potential is fed to them through its ℂ-lift `K.lift`; the chiral
+derivative `∂_I K` is then simply `dWirtingerCoord K.lift I`.
+
+-/
+
+/-- The ℂ-lift of the real Kähler potential: the `ℂ`-valued function the Wirtinger
+operators consume. -/
+def lift (K : KahlerPotential C) : ChiralScalarConfiguration C → ℂ :=
+  fun u => ((K.toFun u : ℝ) : ℂ)
+
+@[simp] lemma lift_apply (K : KahlerPotential C)
+    (u : ChiralScalarConfiguration C) :
+    K.lift u = ((K.toFun u : ℝ) : ℂ) := rfl
+
+/-- Reality of the potential: conjugating the ℂ-lift is the identity. This is the
+payoff of the `ℝ` codomain — the conjugation lemmas of
+`Mathematics/Calculus/Wirtinger/Coordinate.lean` use it
+to turn `∂_J̄` of `K` into `∂_I`, the key step in Kähler-metric hermiticity. -/
+lemma star_lift (K : KahlerPotential C) : (fun v => star (K.lift v)) = K.lift := by
+  funext v; simp [lift_apply]
+
+/-!
+
+## C. Regularity accessors
+
+The real `contDiffOn` field is transported to the ℂ-lift (`Complex.ofRealCLM`
+is a continuous ℝ-linear map) and unpacked into the differentiability facts the
+Wirtinger layer consumes. This milestone needs only first-order
+differentiability of the lift at a domain point.
+
+-/
+
+/-- Regularity transported to the ℂ-lift: `Complex.ofRealCLM` is a continuous
+ℝ-linear map, so `ContDiffOn` of the real potential gives `ContDiffOn` of the
+lift. -/
+lemma contDiffOn_lift (K : KahlerPotential C) :
+    ContDiffOn ℝ 2 K.lift K.domain :=
+  K.contDiffOn.continuousLinearMap_comp Complex.ofRealCLM
+
+/-- The ℂ-lift is `C²` at any point of the (open) domain. -/
+lemma contDiffAt_of_mem (K : KahlerPotential C)
+    {u : ChiralScalarConfiguration C} (hu : u ∈ K.domain) : ContDiffAt ℝ 2 K.lift u :=
+  K.contDiffOn_lift.contDiffAt (K.domain_open.mem_nhds hu)
+
+/-- The ℂ-lift is real-differentiable at any point of the (open) domain — the
+first-order regularity the hermiticity proof consumes. -/
+lemma differentiableAt_of_mem (K : KahlerPotential C)
+    {u : ChiralScalarConfiguration C} (hu : u ∈ K.domain) :
+    DifferentiableAt ℝ K.lift u :=
+  (K.contDiffAt_of_mem hu).differentiableAt two_ne_zero
+
+end KahlerPotential
+
+end SUSY.N1
+
+end
+
+end
diff --git a/Physlib/Particles/SuperSymmetry/N1/LogKahlerHn.lean b/Physlib/Particles/SuperSymmetry/N1/LogKahlerHn.lean
new file mode 100644
index 000000000..79007828d
--- /dev/null
+++ b/Physlib/Particles/SuperSymmetry/N1/LogKahlerHn.lean
@@ -0,0 +1,255 @@
+/-
+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 Physlib.Particles.SuperSymmetry.N1.KahlerMetric
+public import Physlib.Mathematics.Calculus.Wirtinger.UpperHalfPlane
+public import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
+
+/-!
+
+# SUSY N=1 — the multi-field log Kähler potential on `H^n`
+
+## i. Overview
+
+The multi-field upper-half-plane log Kähler potential
+
+  `K(u) = -∑_I log(2 Im u^I)`
+
+on the chiral scalars indexed by `C`, as the concrete
+`KahlerPotential C` instance of the
+abstract machinery in `Particles/SuperSymmetry/N1/KahlerPotential.lean` and
+`Particles/SuperSymmetry/N1/KahlerMetric.lean`. The moduli space `H^n` sits inside
+`ChiralScalarConfiguration C` through the slit-set of
+`Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean`
+(the open set on which every `imArgCLM I` lies in `Complex.slitPlane`); on
+it `2 Im u^I > 0`, so each `log` is real and the leading minus sign yields
+a positive-definite Kähler metric.
+
+`K` is genuinely real, so it lives in the `ℝ`-codomain `KahlerPotential`;
+the Wirtinger operators act on its ℂ-lift `K.lift`. In chiral coordinates
+the equivalent complex form `K = -∑_I log(i (φ̄^I − φ^I))` is the one in
+which the closed forms proved here — `∂K/∂φ^J = -1/(φ^J − φ̄^J)`,
+`∂K/∂φ̄^J = 1/(φ^J − φ̄^J)`, and the diagonal Poincaré metric
+`g_{IJ̄} = -δ_{IJ}/(φ^I − φ̄^I)²` — fall out cleanly. Hermiticity is not
+re-proven: it is the `K`-instance of the abstract
+`KahlerPotential.metric_hermitian`.
+
+## ii. Key results
+
+- `SUSY.N1.K` : the multi-field log Kähler potential, as a `KahlerPotential C`.
+- `SUSY.N1.dChiralScalar_K`, `SUSY.N1.dAntiChiralScalar_K` :
+    closed-form chiral / anti-chiral derivatives of `K.lift`.
+- `SUSY.N1.kahlerMetric` : the Kähler metric `g_{IJ̄}(u) = ∂²K / (∂φ^I ∂φ̄^J)`,
+    defined as the abstract `K.metric`.
+- `SUSY.N1.kahlerMetric_apply` : closed-form diagonal Poincaré
+    metric `g_{IJ̄}(u) = -δ_{IJ} / (z^I − z̄^I)²`, i.e. the Poincaré metric
+    `δ_{IJ} / (2 Im z^I)²` (positive-definite on `H^n`, though positivity is
+    not formalised here).
+- `SUSY.N1.kahlerMetric_hermitian` : hermiticity `star (g_{IJ̄}) = g_{JĪ}`,
+    the concrete instance of `KahlerPotential.metric_hermitian`.
+
+## iii. Table of contents
+
+- A. The log Kähler potential as a `KahlerPotential`
+- B. The chain rule for `log ∘ imArgCLM`
+- C. Closed-form Wirtinger derivatives of `K`
+- D. The Kähler metric and its hermiticity
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace SUSY.N1
+
+open Physlib.Wirtinger
+
+variable {C : Type*} [Fintype C] [DecidableEq C]
+
+/-!
+
+## A. The log Kähler potential as a `KahlerPotential`
+
+The `H^n` log potential `-∑_I log(2 Im u^I)` is a genuine real observable, so it
+is packaged as a `KahlerPotential C` on the open slit-set of
+`Mathematics/Calculus/Wirtinger/UpperHalfPlane.lean`. Its ℂ-lift `K.lift` is what the Wirtinger
+operators consume; on the domain it equals the complex form
+`-∑_I log(imArgCLM I ·)` (via `Complex.ofReal_log` on the positive reals),
+the bridge `K_lift_eq` through which §C evaluates the derivatives.
+
+-/
+
+/-- The multi-field upper-half-plane log Kähler potential as a `KahlerPotential`:
+the real observable `K(u) = -∑_I log(2 Im u^I)`, regular on the open slit-set
+realising `H^n` as moduli space. Reality is by construction from the `ℝ`
+codomain; the Wirtinger operators consume the ℂ-lift `K.lift`. -/
+def K : KahlerPotential C where
+  toFun := fun u => -∑ I, Real.log (2 * (u I).im)
+  domain := {v | ∀ I, imArgCLM I v ∈ Complex.slitPlane}
+  domain_open := isOpen_slitSet
+  contDiffOn := by
+    have hsmooth : ∀ I : C,
+        ContDiff ℝ 2 (fun v : ChiralScalarConfiguration C => 2 * (v I).im) :=
+      fun I => contDiff_const.mul ((Complex.imCLM.comp (coordProjCLM I)).contDiff)
+    intro u hu
+    have hne : ∀ I : C, (2 * (u I).im : ℝ) ≠ 0 := fun I => by
+      have := im_pos_of_mem_slitPlane (hu I)
+      have hpos : (0 : ℝ) < 2 * (u I).im := by linarith
+      exact hpos.ne'
+    exact (ContDiffAt.sum fun I _ => (hsmooth I).contDiffAt.log (hne I)).neg.contDiffWithinAt
+
+omit [DecidableEq C] in
+/-- On the slit domain the ℂ-lift of `K` is the familiar complex log form
+`-∑_I log(imArgCLM I u)`: the inner argument `imArgCLM I u = ↑(2 Im u^I)` is a
+positive real, so `Complex.log ↑r = ↑(Real.log r)` (`Complex.ofReal_log`). -/
+private lemma K_lift_eq {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) :
+    (K : KahlerPotential C).lift u = -∑ I, Complex.log (imArgCLM I u) := by
+  have hcast : (K : KahlerPotential C).lift u
+      = ((-∑ I, Real.log (2 * (u I).im) : ℝ) : ℂ) := rfl
+  rw [hcast]
+  push_cast
+  refine congrArg Neg.neg (Finset.sum_congr rfl fun I _ => ?_)
+  have hpos : (0 : ℝ) < 2 * (u I).im := by linarith [im_pos_of_mem_slitPlane (h I)]
+  rw [Complex.ofReal_log hpos.le, ← imArgCLM_eq_ofReal]
+
+omit [DecidableEq C] in
+/-- Near any slit-domain point the ℂ-lift of `K` agrees with the complex log
+form, so the Wirtinger derivatives may be taken on the latter inside the
+calculus. -/
+private lemma K_lift_eventuallyEq {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) :
+    (K : KahlerPotential C).lift =ᶠ[nhds u]
+      (fun v => -∑ I, Complex.log (imArgCLM I v)) := by
+  filter_upwards [isOpen_slitSet.mem_nhds h] with v hv
+  exact K_lift_eq hv
+
+/-!
+
+## C. Closed-form Wirtinger derivatives of `K`
+
+Applying the holomorphic-outer chain rule to each summand of the complex log
+form (which the lift equals near a domain point, `K_lift_eq`) yields the
+closed-form expressions `∂K/∂φ^J = -1/(z^J − z̄^J)` and
+`∂K/∂φ̄^J = 1/(z^J − z̄^J)`.
+
+-/
+
+/-- The conjugation model for the single-type `Hⁿ` example: chiral and anti-chiral
+indices coincide, so `equiv` is the identity. -/
+def model : Model C C := ⟨Equiv.refl _⟩
+
+/-- Closed form of the chiral derivative `∂_J K = -1 / (z^J - z̄^J)` of the
+multi-field upper-half-plane log Kähler potential. Near `u` the lift equals
+`-∑_I log(imArgCLM I ·)`; `∂_J` passes the negation, the sum collapses to its
+diagonal term, and the slit-plane non-vanishing facts close the algebra. -/
+theorem dChiralScalar_K {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (J : C) :
+    model.dChiralScalar (K : KahlerPotential C).lift J u = -(1 / (u J - conjConfig u J)) := by
+  show dWirtingerCoord (K : KahlerPotential C).lift J u = -(1 / (u J - conjConfig u J))
+  have _ : u J - star (u J) ≠ 0 := sub_star_ne_zero (h J)
+  have _ : star (u J) - u J ≠ 0 := star_sub_ne_zero (h J)
+  rw [dWirtingerCoord_congr_of_eventuallyEq_apply (K_lift_eventuallyEq h) J,
+    dWirtingerCoord_neg_apply,
+    dWirtingerCoord_sum_log_comp_imArgCLM h J, imArgCLM_apply]
+  simp only [conjConfig_apply]
+  field_simp
+  ring
+
+/-- Closed form of the anti-chiral derivative `∂_J̄ K = 1 / (z^J - z̄^J)` of the
+multi-field upper-half-plane log Kähler potential (barred index via the identity
+`model`). Mirror of `dChiralScalar_K`. -/
+theorem dAntiChiralScalar_K {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (J : C) :
+    model.dAntiChiralScalar (K : KahlerPotential C).lift J u =
+      1 / (u J - conjConfig u J) := by
+  simp only [Model.dAntiChiralScalar, model, Equiv.refl_symm, Equiv.coe_refl, id_eq]
+  have _ : u J - star (u J) ≠ 0 := sub_star_ne_zero (h J)
+  have _ : star (u J) - u J ≠ 0 := star_sub_ne_zero (h J)
+  rw [dWirtingerAntiCoord_congr_of_eventuallyEq_apply (K_lift_eventuallyEq h) J,
+    dWirtingerAntiCoord_neg_apply,
+    dWirtingerAntiCoord_sum_log_comp_imArgCLM h J, imArgCLM_apply]
+  simp only [conjConfig_apply]
+  field_simp
+  ring
+
+/-!
+
+## D. The Kähler metric and its hermiticity
+
+The mixed second Wirtinger derivative `g_{IJ̄}(u) = ∂²K/(∂φ^I ∂φ̄^J)`
+is the Kähler metric, here the abstract `K.metric` of the `KahlerPotential`
+`K`. Its closed form on `H^n` is the diagonal Poincaré-metric
+`-δ_{IJ} / (z^I − z̄^I)²`, the positive-definite metric
+`δ_{IJ} / (2 Im z^I)²`. Hermiticity is the `K`-instance of
+`KahlerPotential.metric_hermitian`.
+
+-/
+
+/-- On a neighbourhood of any point where the slit-plane hypothesis holds,
+`dWirtingerAntiCoord K.lift J` agrees with its closed form `(φ^J − φ̄^J)⁻¹`. Feeds
+`dWirtingerCoord_congr_of_eventuallyEq_apply` in `kahlerMetric_apply`, letting the second
+Wirtinger derivative be taken on the closed form inside the calculus. -/
+private lemma dWirtingerAntiCoord_K_eventuallyEq {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (J : C) :
+    (fun v : ChiralScalarConfiguration C =>
+        dWirtingerAntiCoord (K : KahlerPotential C).lift J v) =ᶠ[nhds u]
+      (fun v => (v J - conjConfig v J)⁻¹) := by
+  filter_upwards [isOpen_slitSet.mem_nhds h] with v hv
+  rw [show dWirtingerAntiCoord (K : KahlerPotential C).lift J v
+        = model.dAntiChiralScalar (K : KahlerPotential C).lift J v from rfl,
+    dAntiChiralScalar_K hv J, one_div]
+
+/-- The Kähler metric `g_{IJ̄}(u) = ∂²K / (∂φ^I ∂φ̄^J)` of the multi-field
+upper-half-plane log Kähler potential — the abstract `K.metric` at the identity
+`model`. -/
+def kahlerMetric (I J : C) (u : ChiralScalarConfiguration C) : ℂ :=
+  (K : KahlerPotential C).metric model I J u
+
+/-- Closed form of the Kähler metric on `H^n`: diagonal Poincaré-metric on
+each factor, `g_{IJ̄}(u) = -δ_{IJ} / (z^I − z̄^I)²`. Since `z^I − z̄^I = 2i Im z^I`,
+this is the Poincaré metric `δ_{IJ} / (2 Im z^I)²`, positive-definite on `H^n`
+(positivity is not formalised here). -/
+theorem kahlerMetric_apply {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (I J : C) :
+    kahlerMetric I J u =
+      if I = J then -(1 / (u I - conjConfig u I) ^ 2) else 0 := by
+  have hw : u J - conjConfig u J ≠ 0 := by
+    have := sub_star_ne_zero (h J)
+    rwa [conjConfig_apply]
+  have hcomp : dWirtingerCoord (fun v : ChiralScalarConfiguration C =>
+        (v J - conjConfig v J)⁻¹) I u
+      = deriv (fun w : ℂ => w⁻¹) (u J - conjConfig u J)
+        * dWirtingerCoord (fun v : ChiralScalarConfiguration C =>
+            v J - conjConfig v J) I u :=
+    dWirtingerCoord_comp_holomorphic_apply (differentiableAt_inv hw)
+      (differentiable_coordDiff J u) I
+  simp only [kahlerMetric, KahlerPotential.metric, Model.dChiralScalar, Model.dAntiChiralScalar,
+    model, Equiv.refl_symm, Equiv.coe_refl, id_eq]
+  rw [dWirtingerCoord_congr_of_eventuallyEq_apply (dWirtingerAntiCoord_K_eventuallyEq h J) I, hcomp,
+    (hasDerivAt_inv hw).deriv, dWirtingerCoord_coordDiff]
+  by_cases hIJ : I = J
+  · subst hIJ; simp
+  · simp [hIJ]
+
+/-- **Hermiticity** of the `H^n` Kähler metric: `star (g_{IJ̄}) = g_{JĪ}` on the
+slit domain. Not re-proven here — it is the `K`-instance of the abstract
+`KahlerPotential.metric_hermitian`, whose proof is reality of `K` (free from the
+`ℝ` codomain) plus Schwarz's theorem. -/
+theorem kahlerMetric_hermitian {u : ChiralScalarConfiguration C}
+    (h : ∀ I, imArgCLM I u ∈ Complex.slitPlane) (I J : C) :
+    star (kahlerMetric I J u) = kahlerMetric J I u := by
+  have h2 := (K : KahlerPotential C).metric_hermitian model h I J
+  simpa only [kahlerMetric, model, Equiv.refl_symm, Equiv.coe_refl, id_eq] using h2
+
+end SUSY.N1
+
+end
+
+end
diff --git a/Physlib/Particles/SuperSymmetry/N1/SuperPotential.lean b/Physlib/Particles/SuperSymmetry/N1/SuperPotential.lean
new file mode 100644
index 000000000..4f81bea9c
--- /dev/null
+++ b/Physlib/Particles/SuperSymmetry/N1/SuperPotential.lean
@@ -0,0 +1,144 @@
+/-
+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 Physlib.Particles.SuperSymmetry.N1.Derivative
+public import Physlib.Mathematics.Calculus.Wirtinger.Coordinate
+
+/-!
+
+# N=1 SUSY — the abstract superpotential
+
+## i. Overview
+
+The abstract `SuperPotential` data of an N=1 model: a globally holomorphic
+`ℂ`-valued function `W` of the chiral scalars. No domain, no reality
+condition — `W` is genuinely complex and entire.
+
+The chiral derivative `∂_I W` is just `dWirtingerCoord W I`: `dWirtingerCoord` collapses to
+the complex Fréchet derivative on holomorphic functions
+(`dWirtingerCoord_eq_complex_fderiv` in `Mathematics/Calculus/Wirtinger/Coordinate.lean`).
+
+### The conjugate superpotential
+
+`W.bar u := star (W u)` — the anti-chiral superpotential `W̄`, anti-holomorphic
+in the chiral coordinate per the standard N=1 convention. Bundled
+anti-holomorphicity: `bar_antiHolomorphic`.
+
+## ii. Key results
+
+- `SUSY.N1.SuperPotential` : the abstract superpotential structure.
+- `SUSY.N1.SuperPotential.bar` : the conjugate superpotential `W̄ = star ∘ W`,
+    a bare anti-holomorphic function of the chiral coordinate.
+- `SUSY.N1.SuperPotential.bar_antiHolomorphic` : anti-holomorphicity of `W̄`.
+- `SUSY.N1.SuperPotential.bar_dChiralScalar` : `∂_I W̄ = 0`.
+- `SUSY.N1.SuperPotential.bar_dAntiChiralScalar_apply` : `∂_J̄ W̄ = star (∂_J W)`.
+
+## iii. Table of contents
+
+- A. The superpotential structure
+- B. The conjugate superpotential
+
+-/
+
+@[expose] public section
+
+noncomputable section
+
+namespace SUSY.N1
+
+variable {C : Type*} [Fintype C]
+
+/-!
+
+## A. The superpotential structure
+
+A `SuperPotential` is a globally holomorphic `ℂ`-valued function of the chiral
+scalars. Holomorphy is `Differentiable ℂ`, the full physical content; there is
+no domain (the abstraction takes superpotentials to be entire) and no reality
+condition (the superpotential is genuinely complex).
+
+-/
+
+/-- The abstract chiral superpotential `W : ChiralScalarConfiguration C → ℂ` of an N=1
+model, with bundled global holomorphicity. No domain field (`W` is entire) and
+no reality field (`W` is genuinely complex); the conjugate `W̄` is the
+anti-chiral counterpart `bar` defined below. -/
+structure SuperPotential (C : Type*) [Fintype C] where
+  /-- The underlying function `W : ChiralScalarConfiguration C → ℂ`. -/
+  toFun : ChiralScalarConfiguration C → ℂ
+  /-- Global holomorphicity of `W`: `Differentiable ℂ` on all of
+  `ChiralScalarConfiguration C` (no domain restriction). -/
+  holomorphic : Differentiable ℂ toFun
+
+namespace SuperPotential
+
+/-- Coerce `W : SuperPotential C` to its underlying function: `W u = W.toFun u`. -/
+instance : CoeFun (SuperPotential C)
+    (fun _ => ChiralScalarConfiguration C → ℂ) where
+  coe := toFun
+
+/-!
+
+## B. The conjugate superpotential
+
+-/
+
+/-- The anti-chiral superpotential `W̄(u) := star (W u)`, anti-holomorphic in
+the chiral coordinate `u` per the standard N=1 convention `W̄(Φ̄) = star(W(Φ))`.
+Returned as a bare function — `W̄` is not a `SuperPotential` because the
+structure bundles holomorphicity, which `W̄` does not have. Anti-holomorphicity
+is captured by `bar_antiHolomorphic`. -/
+def bar (W : SuperPotential C) : ChiralScalarConfiguration C → ℂ :=
+  fun u => star (W u)
+
+/-- Simp-normal form of `W.bar`: `W̄(u) = star (W u)`. -/
+@[simp] lemma bar_apply (W : SuperPotential C)
+    (u : ChiralScalarConfiguration C) :
+    W.bar u = star (W u) := rfl
+
+/-- Antiholomorphicity of `W̄`: `star ∘ W.bar = W.toFun` by `star_star`, so
+`star ∘ W.bar` inherits `ℂ`-differentiability from `W.holomorphic`. The
+derivative content is spelled out by `bar_dChiralScalar` (`∂_I W̄ = 0`) and
+`bar_dAntiChiralScalar_apply` (`∂_J̄ W̄ = star (∂_J W)`). -/
+lemma bar_antiHolomorphic (W : SuperPotential C) :
+    Differentiable ℂ (star ∘ W.bar) := by
+  simpa [Function.comp_def, star_star] using W.holomorphic
+
+open Physlib.Wirtinger
+
+variable [DecidableEq C] {A : Type*} [Fintype A]
+
+/-- The chiral derivative of the conjugate superpotential vanishes, `∂_I W̄ = 0`:
+`W̄` is anti-holomorphic. Not `@[simp]`: its LHS head is the reducible `M.dChiralScalar`
+wrapper (unfolding to `dWirtingerCoord`), so it is not in simp-normal form — matching
+the convention that the conjugation lemmas of `Wirtinger/Coordinate.lean` aren't `@[simp]`. -/
+lemma bar_dChiralScalar (W : SuperPotential C) (M : Model C A) (I : C) :
+    M.dChiralScalar (W.bar) I = 0 := by
+  funext u
+  show dWirtingerCoord (fun v => star (W v)) I u = 0
+  rw [dWirtingerCoord_star_comp_apply (differentiableAt_real_of_complex (W.holomorphic u)) I,
+    dWirtingerAntiCoord_eq_zero_of_holomorphic_apply (W.holomorphic u) I, star_zero]
+
+/-- The anti-chiral derivative of the conjugate superpotential is the conjugate of
+the chiral derivative of `W`, `∂_J̄ W̄ = star (∂_J W)` (dotted index `J̄ : A`) — the
+literal `∂_ī W̄` the F-term contraction consumes. Pointwise (`_apply`), not
+`@[simp]`; proved by unfolding the wrappers and applying `dWirtingerAntiCoord_star_comp_apply`. -/
+lemma bar_dAntiChiralScalar_apply (W : SuperPotential C) (M : Model C A)
+    (Jbar : A) (u : ChiralScalarConfiguration C) :
+    M.dAntiChiralScalar (W.bar) Jbar u = star (M.dChiralScalar W (M.equiv.symm Jbar) u) := by
+  show dWirtingerAntiCoord (fun v => star (W v)) (M.equiv.symm Jbar) u
+      = star (dWirtingerCoord W (M.equiv.symm Jbar) u)
+  exact dWirtingerAntiCoord_star_comp_apply (differentiableAt_real_of_complex (W.holomorphic u))
+    (M.equiv.symm Jbar)
+
+end SuperPotential
+
+end SUSY.N1
+
+end
+
+end