V-01 complex calculus: ccontr, cpdC, cdir, cmat, rcontr

-- Generated by scripts/release05/gen_platform_tree.py (ATLAS-RELEASE-05) by skeleton subtraction from Atlas/EinsteinMaxwell/NP/Basic.lean
-- definition bundle: kept ExactVacuumAtlas.EinsteinMaxwell.NP.ccontr, ExactVacuumAtlas.EinsteinMaxwell.NP.cdir, ExactVacuumAtlas.EinsteinMaxwell.NP.cmat, ExactVacuumAtlas.EinsteinMaxwell.NP.cpdC, ExactVacuumAtlas.EinsteinMaxwell.NP.rcontr
import Mathlib
import Definitions.Def_Atlas_Core_Basic
import Definitions.Def_Atlas_EinsteinMaxwell_Basic
/-! # Complex contractions and complex-valued coordinate derivatives (ATLAS-V-01)

B3 local layer, registered in `mission/PHYSICS_BOUNDARY.md` §K. Dimension-generic (`Fin n`, total dimension `n`).

* `rcontr T x u v = Σ_{μ,ν} T_{μν}(x) u^μ v^ν` — real bilinear contraction of a real covariant rank-2 field
  (`Metric n` or `TwoForm n`; both are `Fin n → Fin n → Pt n → ℝ`).
* `ccontr T x u v = Σ_{μ,ν} (T_{μν}(x) : ℂ) u^μ v^ν` — its **complex-bilinear** extension to complex vectors. This
  is the contraction used for null frames (no complex conjugation anywhere).
* `hcontr T x u v = Σ (T_{μν}(x) : ℂ) conj(u^μ) v^ν` — the Hermitian (sesquilinear) form. It is **not** used by the
  frame theory; it exists only for the negative control `Atlas.EinsteinMaxwell.NP.Control`.
* `cpdC i f x` — derivative of the real one-variable slice `u ↦ f (x with xᵢ := u)` of a complex-valued function of
  the **real** coordinates (Mathlib `deriv` over `ℝ` with values in `ℂ`); same slice convention as the registered
  `pd` (A1). No holomorphy is assumed or used.
* `cdir Z f x = Σ_μ Z^μ cpdC μ f x` — derivative along a complex coordinate vector `Z`: the complex-linear
  combination of the real coordinate derivatives.

Bridges proved here: `ccontr` of real vectors is the cast of `rcontr`; `ccontr` is complex-bilinear; `cpdC` of a
cast real function is the cast of `pd` (unconditionally); for a slice-differentiable `f`,
`cpdC f = pd (Re f) + i pd (Im f)`; `cdir` with real components on a real function is the cast of the real
directional derivative; the matrix form `(Eᵀ G E)_{AB} = ccontr g (E·A) (E·B)`. -/

open Complex
open scoped ComplexConjugate Matrix ContDiff

namespace ExactVacuumAtlas.EinsteinMaxwell.NP

/-- Real bilinear contraction `Σ_{μ,ν} T_{μν}(x) u^μ v^ν`. -/
noncomputable def rcontr {n : ℕ} (T : Fin n → Fin n → Pt n → ℝ) (x : Pt n) (u v : Fin n → ℝ) : ℝ :=
  ∑ μ, ∑ ν, T μ ν x * u μ * v ν

/-- Complex-bilinear contraction `Σ_{μ,ν} T_{μν}(x) u^μ v^ν` of complex vectors (no conjugation). -/
noncomputable def ccontr {n : ℕ} (T : Fin n → Fin n → Pt n → ℝ) (x : Pt n) (u v : Fin n → ℂ) : ℂ :=
  ∑ μ, ∑ ν, (T μ ν x : ℂ) * u μ * v ν

/-- Complex-valued slice derivative `∂ᵢ f (x)` of `f : ℝⁿ → ℂ` (real variable, complex values). -/
noncomputable def cpdC {n : ℕ} (i : Fin n) (f : Pt n → ℂ) (x : Pt n) : ℂ :=
  deriv (fun u : ℝ => f (Function.update x i u)) (x i)

/-- Derivative along a complex coordinate vector: `Z(f) = Σ_μ Z^μ ∂_μ f`. -/
noncomputable def cdir {n : ℕ} (Z : Fin n → ℂ) (f : Pt n → ℂ) (x : Pt n) : ℂ :=
  ∑ μ, Z μ * cpdC μ f x

/-- The complexification of a real field matrix at `x`. -/
noncomputable def cmat {n : ℕ} (T : Fin n → Fin n → Pt n → ℝ) (x : Pt n) : Matrix (Fin n) (Fin n) ℂ :=
  (metricMatrix T x).map (fun t : ℝ => (t : ℂ))

variable {n : ℕ}

/-! ### Contractions -/

/-! ### Complex-valued coordinate derivatives -/

/-! ### `cpdC` and `cdir` are genuine derivatives -/

end ExactVacuumAtlas.EinsteinMaxwell.NP

• Endorsed by Shuze Chen · Oct 24, 2026

  Confirmed by the moderator at approval.

• Endorsed by He Wang · Oct 24, 2026

  Confirmed by the mission captain (proposal self-audit).