feat: Wirtinger calculus and N=1 SUSY scalar Wirtinger derivatives by pariandrea · Pull Request #1107 · leanprover-community/physlib

pariandrea · 2026-05-18T12:41:35Z

Summary

Adds a reusable Wirtinger calculus for ℂ → ℂ functions, and builds on it
the N=1 SUSY scalar Wirtinger derivatives ∂/∂φ^I and ∂/∂φ̄^I on the
chiral configuration space. The change is purely additive — 11 new files, no
existing code modified (aside from registering the modules in Physlib.lean).

What this adds

Physlib/Mathematics/Calculus/Wirtinger/ — a general 1-D Wirtinger calculus:

dWirtinger / dWirtingerBar, the operators (1/2)(∂_x ∓ i∂_y);
their collapse to the complex derivative on holomorphic functions and the
real-linear Wirtinger decomposition;
the differentiation rules — locality, real-linearity, the Leibniz rule, the
two-term chain rule, conjugation lemmas;
an outer-function derivative catalog (Complex.log, …).

Physlib/SUSY/N1/ — the N=1 scalar sector:

ChiralScalarValue n = Fin n → ℂ, the physical configuration space, with the
anti-chiral view as a derived conjugation;
dScalar / dScalarBar, the scalar Wirtinger operators, defined as the 1-D
operators applied through a coordinate slice;
their calculus — coordinate rules ∂φ^J/∂φ^I = δ_IJ, additivity, the Leibniz
rule, the holomorphic/antiholomorphic collapse, and the outer chain rules.

Worked example

SUSY/N1/Examples.lean computes, in closed form, the chiral and anti-chiral
Wirtinger derivatives of the multi-field upper-half-plane log Kähler potential
K = -∑_I log(i(z̄^I − z^I)), and from them the Kähler metric
g_{IJ̄} = -δ_{IJ}/(z^I − z̄^I)² — the Poincaré metric on Hⁿ.

…figuration space Introduces the basic data layer for the N=1 chiral SUSY sector. * `ChiralIndex` bundles a chiral label set, an anti-chiral label set, and the bar equivalence pairing each chiral field with its anti-chiral partner. Bar is data so non-trivial pairings are expressible. * `ChiralScalarValue` / `AntiChiralScalarValue` are the curried configuration spaces. * `WirtingerInput T := T.Chiral → ℂ` is the **physical configuration space**: n complex scalars carry 2n real DOF and that count is exactly what `WirtingerInput` encodes. The anti-chiral data is a derived view (`WirtingerInput.antiChiral`) computed via the bar map and complex conjugation, not a separate input. This rules out off-locus configurations by typing. * `ChiralIndex.starConfig` realizes complex conjugation on configurations. The Wirtinger calculus on top — `dHolo`, `dAntiHolo`, the symbolic algebra that lets users manipulate `∂/∂z` and `∂/∂z̄` as in physics — will land in `SUSY/N1/Deriv.lean` in a follow-up. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Close all eight sorries in `dScalar` and `dScalarBar` (coordinate Kronecker deltas, additivity, ℂ-scaling, Leibniz, holomorphic-reduction to the complex Fréchet derivative, and zero anti-derivative for holomorphic functions). * Add `WirtingerInput.instIsScalarTowerComplex` and three `fderiv` simp lemmas for coordinate, conjugated-coordinate, and anti-chiral projections. * Introduce a `private fderiv_real_apply_eq_complex` helper that factors the `DifferentiableAt.fderiv_restrictScalars` boilerplate shared by `eq_complex_fderiv_apply` and `eq_zero_of_differentiableAt_complex`. * Provide pointwise `add_apply`/`smul_apply`/`mul_apply` companions in both `dScalar` and `dScalarBar` namespaces; the global versions are thin `funext` wrappers over them. * Add `ChiralIndex.starConfig_apply` simp lemma symmetric to `WirtingerInput.antiChiral_apply`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Restructure the file-level and section docstrings of `SUSY/N1/Basic.lean` and `SUSY/N1/Deriv.lean` to follow the canonical physlib layout (`## i. Overview` / `## ii. Key results` / `## iii. Table of contents` / `## iv. References`, then `## A.`/`## B.`/... section blocks). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Introduces DerivChainRule.lean (one-field model T1, ℝ-linear coordinate CLMs zCLM/zbarCLM, real Fréchet derivative of Complex.log via restrictScalars) and DerivTest.lean (closed-form Wirtinger derivatives of the upper-half-plane log Kähler potential). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

ChiralIndex was a structure carrying separate Chiral/AntiChiral types plus a bar equivalence. In the scalar sector this generality was unused: the bar was always Equiv.refl. This commit replaces the structure with `abbrev ChiralIndex : Type := ℕ`, with `Fin n` as the single index set for both chiral and anti-chiral. dScalarBar now indexes directly on Fin n with no T.bar.symm translation. The chain-rule layer (zCLM, zbarCLM) is now polymorphic in n. The showcase computation lifts from H to H^n: K = ∑_I log(i(z^I − z̄^I)), with closed-form Wirtinger derivatives ∂K/∂φ^J = 1/(z^J − z̄^J) and ∂K/∂φ̄^J = -1/(z^J − z̄^J) for any n. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…tyle Restructure file-level docstrings of DerivChainRule.lean and DerivTest.lean to follow the canonical physlib layout (`## i. Overview` / `## ii. Key results` / `## iii. Table of contents` / `## iv. References`), and add prose paragraphs to each lettered section block in Basic.lean, Deriv.lean, DerivChainRule.lean, and DerivTest.lean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…e_complex Bundle pointwise complex conjugation as an ℝ-linear continuous endomorphism ChiralScalarValue.antiChiralCLM and use it to prove dScalar.eq_zero_of_antiHolomorphic: the chiral Wirtinger derivative kills any function of the form `g ∘ ·.antiChiral` for ℂ-differentiable g. Closes the symmetric API gap with dScalarBar.eq_zero_of_differentiable_complex. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…d files Promote bundled continuous linear maps to a single file `CLM.lean` holding `zCLM`, `zbarCLM`, and `antiChiralCLM` (with their `_apply` simp lemmas and bump-direction lemmas). `Deriv.lean` keeps the operator algebra and projection-fderiv simp lemmas, importing CLM for the antiholomorphic vanishing proof. Rename `DerivChainRule.lean` to `ChainRule.lean` and remove the per- coordinate CLMs from it; the file now contains only outer-function chain-rule helpers (currently the real Fréchet derivative of `Complex.log`). Rename `DerivTest.lean` to `Examples.lean` to reflect that it is the runnable showcase of concrete computations, not a unit test. Update imports throughout, including the root module `Physlib.lean`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

- Examples.lean: rename inner namespace `DerivTest` to `Examples` to match the file rename; fix the lake env command path; update the module docstring's bullet list and the section B prose's reference from `DerivChainRule` to `ChainRule`. - Deriv.lean: drop the now-stale phrase "trivial bar pairing baked into ChiralScalarValue" from the dScalarBar docstring (the bar field was removed when ChiralIndex became ℕ); remove the inline comment in fderiv_real_apply_eq_complex that duplicated the docstring. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Add `hasFDerivAt_real_inv` to ChainRule.lean (mirroring the existing `Complex.log` block — restrict scalars to ℝ on Mathlib's `hasDerivAt_inv`) and use it to prove the diagonal Poincaré-metric closed form `g_{IJ̄}(u) = δ_{IJ} / (z^I − z̄^I)²` for the multi-field upper-half-plane log Kähler potential. Definition `kahlerMetric I J u := dScalar (dScalarBar K J) I u` plus the closed-form theorem `kahlerMetric_apply`. Proof uses openness of the slit-set, EventuallyEq.fderiv_eq to swap `dScalarBar K J` for its closed form on a neighborhood, then chain rule via `hasFDerivAt_real_inv` and `HasFDerivAt.comp` on the inner CLM `zCLM J - zbarCLM J`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…lper Rename three @[simp] leaf lemmas to coordinate-aware names and add a section-A header explaining their role: fderiv_eval → fderiv_chiralCoord fderiv_starRingEnd_eval → fderiv_starRingEnd_chiralCoord fderiv_antiChiral → fderiv_antiChiralCoord The middle one keeps `starRingEnd` in both name and statement because that is `simp`'s normal form for `star` on `ℂ`; the docstring records this so future readers do not try to "fix" it. Convert the four coordinate-rule proofs (dScalar/dScalarBar × chiralCoord/antiChiralCoord) from `simp [...]` to explicit `simp only [...]` so the dependency on the renamed leaf lemmas is grep-able at each callsite while the leaves themselves remain globally `@[simp]`. Add a private `fderiv_mul_apply` helper local to this file. Both `dScalar.mul_apply` and `dScalarBar.mul_apply` previously inlined a `congrArg + simpa` bridge to evaluate `fderiv_mul`'s bundled-CLM equation at the two Wirtinger tangent vectors; sharing the bridge shrinks each proof from ~20 lines to 7. The helper is local because the same lemma lifted to `Physlib/Mathematics/` produces a `Mul` instance that `rw` cannot unify with the call site — same-file elaboration sidesteps the mismatch. Body uses `DFunLike.congr_fun`, the idiomatic Mathlib spelling. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Drop `@[simp]` from holomorphic/antiholomorphic vanishing lemmas (their `Differentiable ℂ` hypotheses are not auto-dischargeable). Replace the two `#check`s in Examples.lean with the conventional do-not-import disclaimer, and drop the redundant `noncomputable` on `kahlerMetric` already covered by the file's `noncomputable section`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…te docstrings Rename the coordinate CLMs to align with the rest of the SUSY/N1 layer's descriptive register: - `zCLM` → `chiralCoordCLM` - `zbarCLM` → `antiChiralCoordCLM` (`antiChiralCLM` already used the descriptive form and is unchanged.) Touches 41 call sites across CLM.lean, ChainRule.lean, and Examples.lean. Two body simplifications follow the rename: - `antiChiralCoordCLM` reuses `chiralCoordCLM I` instead of inlining `ContinuousLinearMap.proj`. - `antiChiralCLM` reuses `antiChiralCoordCLM` via `ContinuousLinearMap.pi`, replacing the inlined three-line builder. Two docstring rewrites: - Section i (Overview) frames `ChiralScalarValue n` as a product of slots, lists all three CLMs with explicit types, and answers "why isn't there a `chiralCLM`?" inline (the whole-space chiral map is the identity). - Section B drops "lifts" / "atoms" jargon, names the mechanism the sign flip drives (`dScalar` → `dScalarBar` after precomposition). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

§A code: - `fderiv_chiralCoord`: `change` uses `chiralCoordCLM J` instead of inlined `ContinuousLinearMap.proj`. - `fderiv_starRingEnd_chiralCoord`: drop the `let L := ...` builder and the explicit `rw [ContinuousLinearMap.fderiv L]`; rely on the `antiChiralCoordCLM J`-named CLM whose `_apply` is `@[simp]`. Proof body shrinks from four lines to two. §A docstrings: each lemma now names the disguised CLM it is and the simp surface form it covers. §B docstrings: - Section header opens with the tension (calculus consumes ℝ, holomorphic test functions ship in ℂ) and names the bridge mechanism (ℂ-linear ⟹ ℝ-linear). - Lemma docstring leads with the mathematical claim, then concisely explains why the proof is verbose (Mathlib's `IsScalarTower ℝ ℂ ℂ` instance policy). §C docstrings: - Section header lists both Wirtinger formulas explicitly and closes with the duality payoff (§D and §E). - `dScalar` / `dScalarBar` each give the explicit formula and the (anti)holomorphic behavior; cross-reference §D / §E. - `fderiv_mul_apply` leads with the rule statement, then explains why it lives locally. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…thlib Pi.single_smul' Extraction: - `differentiableAt_real_of_complex`: wraps `DifferentiableAt.restrictScalars` with the manual `IsScalarTower ℝ ℂ ℂ` instance (same workaround as `fderiv_real_apply_eq_complex`). - `pi_single_I_eq_smul`: `Pi.single I Complex.I = Complex.I • Pi.single I 1`, derived from Mathlib's `Pi.single_smul'` instead of an `ext + by_cases` proof. - `fderiv_complex_pi_single_I_apply`: ℂ-linearity of `fderiv ℂ f u` applied to the slot-I imaginary bump, proven by a three-step `rw` chain (`pi_single_I_eq_smul`, `ContinuousLinearMap.map_smul`, `smul_eq_mul`) — no bare `simp`. All three helpers live in §B alongside `fderiv_real_apply_eq_complex` as bridge infrastructure for the ℝ ↔ ℂ Fréchet conversion. Call-site cleanup: - `eq_complex_fderiv_apply`, `eq_zero_of_antiHolomorphic_apply`, `eq_zero_of_differentiableAt_complex`: replace inline `hsingle` + `hI` blocks with one-line `have hI := fderiv_complex_pi_single_I_apply f u I`. - `eq_zero_of_antiHolomorphic_apply`: replace inline `@`-prefix `restrictScalars` call with `differentiableAt_real_of_complex hg`. Style: - Four `unfold dScalar` / `unfold dScalarBar` calls become `simp only [dScalar]` / `simp only [dScalarBar]`, the modern Mathlib idiom for revealing a `def` body. Net: 39 insertions, 37 deletions; three new named helpers, three trimmed proof sites, one `@`-prefix dance localized to §B. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Pull the real-Fréchet chain rule for `v ↦ g v.antiChiral` out of `dScalar.eq_zero_of_antiHolomorphic_apply` into a standalone lemma `fderiv_real_comp_antiChiral`, sited next to `fderiv_mul_apply`. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Add `dScalarBar.eq_complex_fderiv_apply` / `eq_complex_fderiv`: on an antiholomorphic input, the anti-chiral Wirtinger derivative collapses to the complex Fréchet derivative of the inner function, completing the §D/§E (anti)holomorphic duality. Rename §E lemmas for namespace-symmetric naming with §D: eq_complex_fderiv_of_antiHolomorphic_apply → eq_complex_fderiv_apply eq_complex_fderiv_of_antiHolomorphic → eq_complex_fderiv eq_zero_of_differentiableAt_complex → eq_zero_of_holomorphic_apply eq_zero_of_differentiable_complex → eq_zero_of_holomorphic `dScalar.eq_complex_fderiv*` and `dScalarBar.eq_complex_fderiv*` now form the matched "collapses to ℂ-fderiv" diagonal; the two `eq_zero_of_*Holomorphic*` lemmas form the vanishing diagonal. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ternals Drop redundant `fderiv_starRingEnd_chiralCoord`; reprove `fderiv_antiChiralCoord` via its CLM, matching `fderiv_chiralCoord`. Extract `fderiv_real_pi_single_I_apply_of_complex` (the `∂_y = i·∂_x` fact) and collapse the four §D/§E vanishing/collapse proofs onto it. Mark §A/§B/§C scaffolding `private`, document the pointwise `_apply` lemmas, prefer `simp only`, and unify the delta-proof idiom. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

The file holds real Fréchet derivative facts for the outer holomorphic test functions (Complex.log, complex inversion), not a chain rule — the chain rule itself is applied downstream in Examples.lean. Rename to OuterDeriv.lean to pair with Deriv.lean and match the file's own outer/inner vocabulary; update the module title and all references. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

The @HasFDerivAt.restrictScalars boilerplate — an @-prefixed call manually supplying two non-global IsScalarTower ℝ ℂ ℂ instances — was duplicated verbatim across hasFDerivAt_real_log and hasFDerivAt_real_inv. Extract it into a single private helper hasFDerivAt_restrictScalarsℝℂ; both lemmas now delegate to it. Statements and docstrings unchanged. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…ead lemmas Extract hasFDerivAt_restrictScalarsℝℂ to localize the @-prefixed IsScalarTower.right workaround, and route both hasFDerivAt_real_log and hasFDerivAt_real_inv through it. Delete fderiv_real_log, differentiableAt_real_log, fderiv_real_inv and differentiableAt_real_inv: none were used anywhere, and each is a one-liner off the corresponding HasFDerivAt fact if ever needed. Tighten the module and section docstrings to match the surviving two lemmas. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Review-driven cleanup of the N=1 Wirtinger showcase: - Drop redundant Complex.Log / Complex.LogDeriv imports (re-exported transitively by OuterDeriv). - Replace two non-terminal bare `simp` calls (gCLM_pi_single_I, sub_zbar_pi_single_I) with explicit terminal rewrite chains; this also removes a roundabout intermediate `have`. - Use `ring` instead of `ring_nf` as the closer in dScalar_K / dScalarBar_K (`ring_nf` is a normalizer, not a closer). - Rename `gCLM` -> `logArgCLM` (and its derived lemmas): the old name carried no meaning; the new one names its role as the argument fed into `Complex.log` in each summand of K. - Consolidate the duplicated `Pi.single` bump algebra. Sections D and F independently re-derived how the coordinate difference acts on the real / imaginary bumps. Extract `coordDiff_pi_single_one` and `coordDiff_pi_single_I` into section B as the single source; D's logArgCLM_pi_single_* become thin `i`-scaled corollaries and F's sub_zbar_pi_single_* are deleted (they were the same fact). No statement changes; Examples.lean builds clean. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

antiChiral maps a configuration to a configuration, so annotate its codomain as ChiralScalarValue n rather than the raw Fin n → ℂ. Defeq, so no proof changes; aligns the signature with antiChiralCLM and removes a spurious input/output type asymmetry. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Add Physlib/Mathematics/Calculus/Wirtinger.lean: directional Wirtinger operators dWirtinger/dWirtingerBar on an arbitrary real normed domain, the 1-D ℂ→ℂ versions, and the general two-term chain rules plus their holomorphic-outer specializations. dScalar/dScalarBar are now thin specializations of Physlib.dWirtinger at the bump directions Pi.single I 1 and Pi.single I Complex.I. OuterDeriv collapses to a specialization layer exposing the chain rules in terms of dScalar/dScalarBar. Examples reworked to compute the Wirtinger derivatives of K directly via the holomorphic-outer chain rule, dropping the real-Fréchet detour (hasFDerivAt_K, fderiv_K_at_one, fderiv_K_at_I). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Apply the seven review findings on the general Wirtinger chain rule: - Move the 1-D ℂ→ℂ operators out of Mathlib's `Complex` namespace into `Physlib.Complex` (`dWirtinger`, `dWirtingerBar`). - Add holomorphic-collapse lemmas `Physlib.Complex.dWirtinger_apply_eq_deriv` and `dWirtingerBar_apply_eq_zero`. - Restate `comp_holomorphic_apply` to return the textbook form `deriv g (f u) * dWirtinger f …` and reprove it as a corollary of the two-term `comp_apply`, dropping the duplicated proof. Simplify the `Examples` summand proofs accordingly. - Add `dScalar_apply` / `dScalarBar_apply` unfold lemmas so the `Physlib.dWirtinger` wrapper no longer leaks into `Deriv` simp sets. - Add the conjugation bridge `Physlib.dWirtinger_star_comp` and the SUSY corollary `dScalar.star_comp`; exercise the two-term `comp_apply` on a non-holomorphic outer via an `example` in `Examples`. - Broaden the `Wirtinger.lean` module docstring to cover all of its contents. Full build passes; changed declarations use only standard axioms. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…decomposition - Extract `fderiv_star_eq` lemma to eliminate three identical `hconj` subproofs in `dWirtinger_star_comp`, `dWirtinger.comp_apply`, and `dWirtingerBar.comp_apply` - Add `dWirtingerBar_star_comp` (dual of `dWirtinger_star_comp`), derived from it via the involution `star ∘ star = id` - Promote `Physlib.Complex.realLinear_apply_eq_wirtinger` from `private` - Add `dScalarBar.star_comp` to OuterDeriv.lean, symmetric with `dScalar.star_comp` Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…te/ChainRule Wirtinger.lean becomes a barrel re-exporting four focused sub-files: - Wirtinger/Basic.lean — dWirtinger/dWirtingerBar defs + ℝ/ℂ bridge lemmas - Wirtinger/Complex.lean — one-variable ℂ→ℂ operators + Wirtinger decomposition - Wirtinger/Conjugate.lean — star/conjugation identities - Wirtinger/ChainRule.lean — chain rules + log/inv outer-function helpers Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

- Complex: extract `holo_fderiv_restrictScalars` private lemma shared by `dWirtinger_apply_eq_deriv` and `dWirtingerBar_apply_eq_zero`; replace `unfold` with `simp only`; rewrite `hw` in `realLinear_apply_eq_wirtinger` to match the smul form directly, replacing `rw [hw]; simp` with `congr_arg` - Conjugate: replace `change (conjCLE ∘ f)` in `fderiv_star_eq` with an inline `show ... = ... ∘ f from rfl` rewrite - ChainRule: remove 7-line `change` blocks and `let L/A/B` bindings from both `comp_apply` proofs; unfold via `simp only` and bridge lambda/composition mismatch with `show ... = g ∘ f from rfl`; replace dead second `simp` with targeted `coe_coe/conjCLE_apply/star_def` normalisation before `ring` Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

…n rules Remove the general directional `dWirtinger f dx dy : E → ℂ`; the sole Wirtinger operator is now `Physlib.dWirtinger : (ℂ → ℂ) → ℂ → ℂ`, promoted out of the `Physlib.Complex` namespace. SUSY `dScalar`/`dScalarBar` are defined directly via `fderiv` and their chain rules proved inline, removing the only downstream user of the general form and the overload confusion. Move `hasFDerivAt_real_log`/`hasFDerivAt_real_inv` into a new `OuterFunctions.lean`. Fold the one-lemma `Conjugate.lean` (`fderiv_star_eq`) into `Complex.lean`, drop the dead `fderiv_real_outer_apply_eq_complex`, and delete the now-empty `ChainRule.lean`. The module is 3 files: Basic (ℝ/ℂ bridge), Complex (operators + decomposition + conjugation), OuterFunctions. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

- Add module docstring to the Wirtinger aggregator (motivation, conventions, module layout). - Explain the explicit @-application in hasFDerivAt_restrictScalarsℝℂ. - Replace undefined D-notation in dWirtinger/dWirtingerBar docstrings with explicit fderiv expressions. - Qualify chain-rule references as downstream; backtick type names. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…nger Build out the Wirtinger module into a reusable calculus library and redefine the SUSY scalar operators on top of it, rather than as bespoke fderiv combinations. - Add Wirtinger/Rules.lean: full differentiation API for dWirtinger / dWirtingerBar (linearity, Leibniz, coordinate values, chain rule, conjugation swap). - Redefine SUSY.N1.dScalar / dScalarBar as Physlib.dWirtinger applied to the coordinate slice `fun t => f (Function.update u I t)`; re-derive the D/E properties as specializations via slice algebra. - dScalar_apply / dScalarBar_apply are now conditional on DifferentiableAt — the slice and Pi.single bump forms only agree where f is differentiable. - OuterDeriv chain rules now specialize dWirtinger_comp; relocate fderiv_neg_inv_clm_apply to Wirtinger/OuterFunctions.lean. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

The holomorphic-collapse proofs in SUSY/N1/Deriv.lean re-derived Cauchy–Riemann on the multivariate `fderiv`, duplicating work the Wirtinger library already does in 1-D. Wirtinger/Rules.lean: - add `dWirtinger_comp_star` / `dWirtingerBar_comp_star`: the holomorphic and anti-holomorphic derivatives of `w ↦ G(w̄)`. SUSY/N1/Deriv.lean: - add ℂ-slice infrastructure: `hasFDerivAt_slice_complex`, `differentiableAt_slice_complex`, `deriv_slice`, `slice_antiChiral`. - rewrite the four collapse lemmas (`dScalar`/`dScalarBar` `eq_complex_fderiv`, `eq_zero_of_holomorphic`, `eq_zero_of_antiHolomorphic`) to slice first, then invoke `dWirtinger_apply_eq_deriv` / `dWirtingerBar_apply_eq_zero` / `dWirtinger_comp_star`. - delete the §B Cauchy–Riemann block (`pi_single_I_eq_smul`, `fderiv_complex_pi_single_I_apply`, `fderiv_real_pi_single_I_apply_of_complex`), `fderiv_real_comp_antiChiral`, and the now-unused `instIsScalarTowerComplex`; renumber sections. Net -45 lines; full build passes, standard axioms only. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Clear residue from the slice-based refactor (b1101790, f27d4a4c): - Delete the dead `antiChiralCLM` endomorphism and its two bump lemmas from CLM.lean — the slice-based `eq_zero_of_antiHolomorphic` proof superseded them; nothing references them. - Fix OuterDeriv.lean §i overview: the chain rules delegate to the 1-D `dWirtinger_comp`/`dWirtingerBar_comp`, not `realLinear_apply_eq_wirtinger`. - Correct OuterFunctions.lean docstring: its only consumer is SUSY.N1.Examples, not the Wirtinger chain rules. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…r redundancy The worked Kähler example claimed the upper half-plane Hⁿ, but K = ∑log(i(u−ū)) made the slit-plane hypothesis satisfiable only on the lower half-plane and yielded a negative-definite metric. Redefine K = −∑log(i(ū−u)) so logArgCLM = 2·Im(u) > 0 on H, propagate the sign changes through the derivative/metric lemmas, and confirm the closed-form metric −δ/(zⁱ−z̄ⁱ)² is the positive-definite Poincaré metric. Also: - Remove dead §A coordinate-projection fderiv lemmas from Deriv.lean (unused since the 1-D Wirtinger refactor); drop the now-unneeded CLM import and renumber sections. - Add the missing negation API: dWirtinger_neg/dWirtingerBar_neg, slice_neg, dScalar.neg(_apply)/dScalarBar.neg(_apply). - Replace fderiv_neg_inv_clm_apply with fderiv_inv_clm_apply. - Docstring fixes: stale §F refs, §C title, Rules.lean missing overview and undocumented conjugation lemmas, empty References sections. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…ant _zero lemmas Section-intro prose in Rules.lean §A and Deriv.lean §C/§D listed the inherited calculus rules but omitted negation, added in the prior commit. Remove dWirtinger_zero / dWirtingerBar_zero: subsumed by the _const lemmas ((0 : ℂ→ℂ) is defeq fun _ => 0), never referenced by name, and the build confirms no simp call depended on them. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…port Narrow Deriv.lean to import Wirtinger.Rules instead of the full aggregator; this surfaced that Examples.lean consumed the OuterFunctions catalog only transitively, so it now imports Wirtinger.OuterFunctions explicitly. Reframe OuterFunctions.lean as a reusable, growth-oriented outer-function derivative catalog rather than example support. Fix stale module-layout descriptions in Wirtinger.lean and the §i list in OuterDeriv.lean, and correct the leaf-module wording in Examples.lean. Doc/import only — no proof or statement changes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…ules - Drop unused FDeriv.Add import from Wirtinger/OuterFunctions. - Drop five transitively-redundant FDeriv.* imports from SUSY/N1/Deriv, keeping only FDeriv.Pi. - List dWirtinger_const/dWirtingerBar_const in Rules' key results and §A. - List dScalar/dScalarBar.fun_sum_apply in Deriv's key results. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Replace the real-Fréchet bump route in the N=1 Kähler-potential examples with the abstract Wirtinger calculus: §C derives logArgCLM through chiralCoord/antiChiralCoord + ℝ-linearity, and §E computes the Kähler metric via comp_holomorphic_apply on the inv outer function. The bump formula dScalar_apply is now foundation-only, never used in examples. Add the locality machinery the second derivative needs: - dWirtinger_congr_of_eventuallyEq (Wirtinger/Rules.lean) — the 1-D reusable rule; - slice_eventuallyEq (Deriv.lean §A) — the slice preserves EventuallyEq; - dScalar.congr_of_eventuallyEq (Deriv.lean §C) — their composition. Drop the now-dead bump helpers coordDiff_pi_single_*, logArgCLM_pi_single_*. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

fderiv_inv_clm_apply and hasFDerivAt_real_inv were consumed only by the old bump-based kahlerMetric_apply, now rewritten to the abstract calculus. Remove both, the now-unused FDeriv.Comp import, and stale doc references. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…helpers dScalar_K / dScalarBar_K each inlined the full negation → sum → per-summand chain rule → diagonal collapse computation, making the theorems hard to follow. Lift each conceptual layer into a doc-commented helper: - star_sub_ne_zero, differentiableAt_log_logArgCLM: operator-independent facts, shared by both branches - dScalar_log_comp_logArgCLM / dScalarBar_log_comp_logArgCLM: per-summand closed form - dScalar_sum_log_comp_logArgCLM / dScalarBar_sum_log_comp_logArgCLM: derivative of the summed log argument, collapsed to the diagonal term dScalar_K / dScalarBar_K now read as factor → push → evaluate → algebra. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

…ar duals Rename pointwise SUSY Wirtinger lemmas to the `_apply` convention used by their siblings (`add_apply`, `comp_apply`, ...): - `dScalar.congr_of_eventuallyEq` -> `congr_of_eventuallyEq_apply` - `dScalar.star_comp` / `dScalarBar.star_comp` -> `star_comp_apply` Fill in the missing conjugate-operator duals: - add `Physlib.dWirtingerBar_congr_of_eventuallyEq` (only the `dWirtinger` locality lemma existed) - add `SUSY.N1.dScalarBar.congr_of_eventuallyEq_apply` Surface `dScalar_apply` / `dScalarBar_apply` in the Deriv.lean key-results list so the bump-form bridge is documented public API rather than apparent dead code. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Extract the byte-identical proofs of dWirtinger_comp / dWirtingerBar_comp into a single private dWirtinger_comp_aux conjunction; the public lemmas become .1 / .2 projections. Reword the garbled holo_fderiv_restrictScalars docstring. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

jstoobysmith

Looks good - some comments to help improve this.

jstoobysmith · 2026-05-18T13:34:52Z

+namespace Physlib
+
+/-- Restrict a complex 1-D Fréchet derivative on `ℂ → ℂ` to `ℝ`-scalars. -/
+lemma hasFDerivAt_restrictScalarsℝℂ {f : ℂ → ℂ} {f' : ℂ →L[ℂ] ℂ}


Is it not possible to use HasFDerivAt.restrictScalars directly somewhere?

It is not possible because the inference of the arguments does not work. They need to be provided manually.

jstoobysmith · 2026-05-18T13:35:15Z

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 The Physlib Contributors. All rights reserved.


The Physlib Contributors should be your name throughout.

jstoobysmith · 2026-05-18T13:36:44Z

+/-!
+
+# Wirtinger operators on `ℂ → ℂ` and the Wirtinger decomposition
+


Maybe a bit more detail on what the Wirtinger operators are.

Expanded the Overview section.

jstoobysmith · 2026-05-18T13:37:38Z

+
+/-- The real Fréchet derivative of `Complex.log` at a slit-plane point,
+packaged as a `HasFDerivAt` statement over `ℝ`. -/
+lemma hasFDerivAt_real_log {z : ℂ} (hz : z ∈ Complex.slitPlane) :


Is this necessary? I.e. could we use hasFDerivAt_restrictScalarsℝℂ directly?

It is not necessary. removed

jstoobysmith · 2026-05-18T13:38:33Z

Lemmas.lean would probably be a better title here.

jstoobysmith · 2026-05-18T13:40:32Z

+
+## i. Overview
+
+In this module we introduce the minimal label and configuration data for the


I think some additional context here would be nice e.g. what is missing, and how this fits into the big picture.

Expanded the overview

jstoobysmith · 2026-05-18T13:41:25Z

These can likely go in the Basic.lean file.

jstoobysmith · 2026-05-18T13:43:45Z

+
+-/
+
+namespace dScalar


This shouldn't be a namespace, similar elsewhere.

jstoobysmith · 2026-05-18T13:44:31Z

Would try and extract useful results from this into their own files.

the reusable lemmas moved into Kahler.lean/Deriv.lean. Examples.lean is now
a demo with only examples and #checks. This is a specific example of potential which shows that the infrastructure works. Expanding from here will help me understand what is actually reusable and what is specific to the calculation of a certain potential.

jstoobysmith · 2026-05-18T13:45:16Z

Could likely be merged with the Deriv file.

… feedback - Rename Wirtinger/Rules.lean to Lemmas.lean - Remove the Wirtinger.lean re-export aggregator; Physlib.lean imports the four leaf modules directly - Merge SUSY/N1/CLM.lean into SUSY/N1/Basic.lean - Merge SUSY/N1/OuterDeriv.lean into SUSY/N1/Deriv.lean - Flatten the dScalar / dScalarBar namespaces: lemmas are now dScalar_foo rather than dScalar.foo - Extract the H^n log Kähler potential and its Kähler metric into the new SUSY/N1/Kahler.lean; reduce Examples.lean to a runnable demo - Expand the Wirtinger-operator explanation in Complex.lean and the big-picture context in SUSY/N1/Basic.lean - Set copyright headers to the author's name Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Resolve the two `Style linters` CI failures on PR leanprover-community#1107: - check_file_imports: move the `SUSY.N1.*` import block to its sorted position (before `SpaceAndTime.*`) in `Physlib.lean`. - simpNF: drop `@[simp]` from `dWirtinger_star`, `dWirtingerBar_star`, `dScalar_antiChiralCoord`, and `dScalarBar_antiChiralCoord`. Their left-hand sides contain `star`/`antiChiral`, which simp normalises to `starRingEnd ℂ` before the lemma could fire, so they were never valid simp lemmas. All call sites use them explicitly via `rw`/`simp only`. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Note the `IsScalarTower ℝ ℂ ℂ` instance diamond (the `Algebra` vs `NormedSpace.complexToReal` route to `SMul ℝ ℂ`) behind `hasFDerivAt_restrictScalarsℝℂ`, with a commented-out `example` that reproduces the synthesis failure. Addresses PR leanprover-community#1107 review feedback. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

….lean `hasFDerivAt_real_log` was a one-line wrapper around `hasFDerivAt_restrictScalarsℝℂ`, used once and only for its differentiability corollary. Inline it at the call site in Kahler.lean and remove the now-empty OuterFunctions.lean. Addresses PR leanprover-community#1107 review feedback. Also expand the Wirtinger folder overview in Basic.lean (motivation, folder layout, conventions) — recovering content from the deleted Wirtinger.lean aggregator. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Relocate the Wirtinger declarations from the flat `Physlib` namespace into `Physlib.Wirtinger`, so generically-named lemmas (`fderiv_star_eq`, `realLinear_apply_eq_wirtinger`) no longer sit at top level and the namespace matches the `Wirtinger.{Basic,Complex,Lemmas}` module paths. Update all consumer references in SUSY/N1 and rewrap lines pushed past 100 chars. Also tighten the SUSY/N1/Basic.lean module/section docstrings (phrasing only). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Bring Wirtinger/Complex.lean onto the standard `i. Overview` / `ii. Key results` / `iii. Table of contents` scheme with lettered `A./B./C.` in-file section dividers, matching its sibling Wirtinger/Lemmas.lean and the SUSY/N1 modules. Fold the stray un-numbered `Scope and context` section of SUSY/N1/Basic.lean into the Overview so the numbered sequence is unbroken. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

pariandrea and others added 30 commits May 18, 2026 13:59

Add N=1 scalar Wirtinger derivatives

f26fb04

Add general SUSY Wirtinger chain rules

05a5aa0

pariandrea and others added 14 commits May 18, 2026 13:59

jstoobysmith reviewed May 18, 2026

View reviewed changes

pariandrea and others added 7 commits May 18, 2026 16:29

docs(Wirtinger): rename Complex.lean overview section heading

c2ac4ad

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

jstoobysmith self-assigned this May 20, 2026

		@@ -0,0 +1,116 @@
		/-
		Copyright (c) 2026 The Physlib Contributors. All rights reserved.

		/-!

		# Wirtinger operators on `ℂ → ℂ` and the Wirtinger decomposition


		## i. Overview

		In this module we introduce the minimal label and configuration data for the

Conversation

pariandrea commented May 18, 2026

Summary

What this adds

Worked example

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants