Flat closedness of the Fubini–Study fundamental form: dω = 0 on the tangent model

Category: 1-Mathlib-staging (CSD-free; differential forms on normed spaces).

The A4 residue brick (BACKLOG §A, recorded 2026-08-06 as formalisable): Mathlib's pin carries extDeriv on normed spaces (Analysis/Calculus/DifferentialForm/), so the closedness dω = 0 of the constant fundamental 2-form on the flat tangent model E is now a theorem, not prose. This module delivers:

• extDeriv_const / extDeriv_const_apply — the exterior derivative of ANY constant differential form vanishes (generic; the Mathlib-gap lemma);
• Kahler.fundamentalFormAlt : E [⋀^Fin 2]→L[ℝ] ℝ — the fundamental form ω u v = im ⟪u,v⟫ packaged as a continuous alternating 2-form (fundamentalFormAlt_apply ties it pointwise to Kahler.fundamentalForm);
• ★ Kahler.extDeriv_fundamentalFormAlt — d(x ↦ ω) = 0: the constant fundamental 2-form is closed in the flat exterior-derivative sense.

Honest scope

This is the flat statement, on the linear tangent model E = EuclideanSpace ℂ (Fin N) — the formalisable fragment of the manifold residual that KahlerOnticSetup.kahler_pointwise names (closedness dω = 0 and the top-power identity on ℂℙ^{N-1} itself; connectivity link L1, specs/connectivity-manifest.md). Forms on the quotient manifold ℂℙ^{N-1} remain outside Mathlib's API (its own DifferentialForm/Basic.lean TODO); nothing here claims manifold-level closedness, and the top-power volume identity is untouched. Follow-up tracked in specs/future-work.md (the W/EC ladders) and BACKLOG §A (A4).

Supporting API added en route (right-slot bilinearity of ω, the Cauchy–Schwarz bound |ω u v| ≤ ‖u‖‖v‖, the bundled fundamentalFormCLM): cross-linked from KahlerForm.lean's left-slot lemmas (fundamentalForm_add_left, fundamentalForm_real_smul_left, fundamentalForm_self, fundamentalForm_antisymm).

Generic: constant differential forms are closed

theorem extDeriv_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : E [⋀^Fin n]→L[𝕜] F) (x : E) : extDeriv (fun (x : E) => c) x = 0

The exterior derivative of a constant differential form vanishes (pointwise form). Mathlib-gap lemma: extDeriv is the alternatization of fderiv, and the derivative of a constant is 0.

theorem extDeriv_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : E [⋀^Fin n]→L[𝕜] F) : (extDeriv fun (x : E) => c) = 0

The exterior derivative of a constant differential form vanishes.

The fundamental form as a continuous alternating 2-form

theorem Kahler.fundamentalForm_add_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v v' : E) : fundamentalForm u (v + v') = fundamentalForm u v + fundamentalForm u v'

Right-slot additivity of the fundamental form (companion to fundamentalForm_add_left).

theorem Kahler.fundamentalForm_real_smul_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (r : ℝ) (u v : E) : fundamentalForm u (r • v) = r * fundamentalForm u v

Right-slot real homogeneity of the fundamental form (companion to fundamentalForm_real_smul_left).

theorem Kahler.abs_fundamentalForm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v : E) : |fundamentalForm u v| ≤ ‖u‖ * ‖v‖

Cauchy–Schwarz bound for the fundamental form: |ω u v| ≤ ‖u‖ * ‖v‖.

noncomputable def Kahler.fundamentalFormBilin {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →ₗ[ℝ] E →ₗ[ℝ] ℝ

The fundamental form as a bundled ℝ-bilinear map.

Equations

• Kahler.fundamentalFormBilin = LinearMap.mk₂ ℝ Kahler.fundamentalForm ⋯ ⋯ ⋯ ⋯

noncomputable def Kahler.fundamentalFormCLM {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E →L[ℝ] E →L[ℝ] ℝ

The fundamental form as a continuous ℝ-bilinear map (Cauchy–Schwarz gives the bound).

Equations

• Kahler.fundamentalFormCLM = Kahler.fundamentalFormBilin.mkContinuous₂ 1 ⋯

@[simp]

theorem Kahler.fundamentalFormCLM_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v : E) : (fundamentalFormCLM u) v = fundamentalForm u v

noncomputable def Kahler.fundamentalFormMulti {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E [×2]→L[ℝ] ℝ

The fundamental form as a continuous multilinear map on Fin 2 → E (uncurried through continuousMultilinearCurryFin1).

Equations

• Kahler.fundamentalFormMulti = ((continuousMultilinearCurryFin1 ℝ E ℝ).symm.toLinearIsometry.toContinuousLinearMap ∘SL Kahler.fundamentalFormCLM).uncurryLeft

@[simp]

theorem Kahler.fundamentalFormMulti_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (v : Fin 2 → E) : fundamentalFormMulti v = fundamentalForm (v 0) (v 1)

noncomputable def Kahler.fundamentalFormAlt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : E [⋀^Fin 2]→L[ℝ] ℝ

The fundamental 2-form: ω u v = im ⟪u,v⟫ as a continuous alternating 2-form on E (alternating by fundamentalForm_self).

Equations

• Kahler.fundamentalFormAlt = { toContinuousMultilinearMap := Kahler.fundamentalFormMulti, map_eq_zero_of_eq' := ⋯ }

@[simp]

theorem Kahler.fundamentalFormAlt_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (v : Fin 2 → E) : fundamentalFormAlt v = fundamentalForm (v 0) (v 1)

theorem Kahler.extDeriv_fundamentalFormAlt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (x : E) : extDeriv (fun (x : E) => fundamentalFormAlt) x = 0

★ Flat closedness of the fundamental form: dω = 0 (pointwise form). The constant differential 2-form x ↦ ω on the tangent model E is closed in the flat exterior-derivative sense. This discharges the formalisable fragment of the dω = 0 residual named by KahlerOnticSetup.kahler_pointwise (connectivity link L1); the manifold-level statement on ℂℙ^{N-1} stays open pending Mathlib manifold-form API.

theorem Kahler.extDeriv_fundamentalFormAlt_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : (extDeriv fun (x : E) => fundamentalFormAlt) = 0

★ Flat closedness of the fundamental form, function form: dω = 0.