The exponential chart exp(β + iω) on the real Mukai extension

exp(β + iω) = (1, β + iω, (β + iω)² / 2) has real and imaginary parts expRe and expIm. The computation that matters is three lines of pairing arithmetic:

⟪expRe, expRe⟫ = ⟪expIm, expIm⟫ = b ω ω,   ⟪expRe, expIm⟫ = 0,

so as soon as ω has positive square the pair spans a positive plane (isPositiveFrame_exp) — the chart lands in the period domain, and β is unconstrained. This is the distinguished family QuadraticForm/PositiveFrame.lean says is needed to name Bridgeland's component rather than an arbitrary half: take (expRe, expIm) as the reference pair.

Why this is charge construction and not extension algebra

The carrier is not defined here and neither is the frame API. RealExtension, realPairing and realForm — with the halving convention that makes ⟪δ, δ⟫ = -2 read unchanged — are owned by LinearAlgebra/Lattice/Mukai/RealForm.lean, and IsPositiveFrame, pairingDet and positiveFramesPlus are owned by LinearAlgebra/QuadraticForm/PositiveFrame.lean. Both stay where they are.

What this file adds is a choice: one distinguished positive frame out of the many the extension admits, singled out because a central charge is wanted. That choice is an input to Z(β,ω) and to nothing else in the extension algebra, which is why the cutover ledger's row 03 puts the chart with the numerical central-charge construction rather than with the quadratic extension.

Keeping it here is also what unblocks the split. RealForm.lean is upstream of the neutral charge root LinearAlgebra/BilinearForm/HodgeIndex.lean, whose transitive closure may contain neither stability conditions nor geometry, so the carrier cannot follow the chart; and Mukai.expCharge consumes the chart while CentralCharge/Quadratic.lean consumes expCharge, so the chart cannot land in Quadratic.lean either. A separate module below CentralCharge/ is the placement both constraints allow.

Per the ledger's first standing decision the namespace does not move: these are Mukai.expRe and Mukai.isPositiveFrame_exp at their new path, exactly as the immutable payloads in exe/RestateHistoricalNames.lean spell them.

V is an arbitrary real bilinear space; no geometry is asserted.

noncomputable def Mukai.expRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : RealExtension V

The real part of exp(β + iω).

Equations

• Mukai.expRe b β ω = (1, β, ((b β) β - (b ω) ω) / 2)

noncomputable def Mukai.expIm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : RealExtension V

The imaginary part of exp(β + iω).

Equations

• Mukai.expIm b β ω = (0, ω, (b β) ω)

@[simp]

theorem Mukai.realPairing_expRe_expRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : realPairing b (expRe b β ω) (expRe b β ω) = (b ω) ω

@[simp]

theorem Mukai.realPairing_expIm_expIm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : realPairing b (expIm b β ω) (expIm b β ω) = (b ω) ω

@[simp]

theorem Mukai.realPairing_expRe_expIm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : realPairing b (expRe b β ω) (expIm b β ω) = 0

@[simp]

theorem Mukai.realPairing_expIm_expRe {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) : realPairing b (expIm b β ω) (expRe b β ω) = 0

theorem Mukai.realForm_smul_add_smul {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (s t : ℝ) : (realForm b) (s • expRe b β ω + t • expIm b β ω) = (s ^ 2 + t ^ 2) * (b ω) ω / 2

The value of realForm on a combination of the two exponential vectors: the pair is orthogonal with equal square, so the form is a positive multiple of s ^ 2 + t ^ 2.

theorem Mukai.expRe_ne_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) : expRe b β ω ≠ 0

theorem Mukai.isPositiveFrame_exp {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) : PeriodDomain.IsPositiveFrame (realForm b) (expRe b β ω) (expIm b β ω)

The exponential chart lands in the period domain.

Only 0 < b ω ω is needed; β is unconstrained, and no signature hypothesis is used. The two vectors are orthogonal with equal positive square, so every nonzero combination has positive square, and they are independent because their rank coordinates are 1 and 0.

theorem Mukai.pairingDet_exp_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) : PeriodDomain.pairingDet (realForm b) (expRe b β ω) (expIm b β ω) (expRe b β ω) (expIm b β ω) = (b ω) ω ^ 2

The pairing determinant of the exponential pair against itself is (b ω ω) ^ 2: the pair is orthogonal with equal square, so the off-diagonal term drops.

theorem Mukai.mem_positiveFramesPlus_exp {V : Type u_1} [AddCommGroup V] [Module ℝ V] (b : V →ₗ[ℝ] V →ₗ[ℝ] ℝ) (β ω : V) (hb : ∀ (x y : V), (b x) y = (b y) x) (hω : 0 < (b ω) ω) : (expRe b β ω, expIm b β ω) ∈ PeriodDomain.positiveFramesPlus (realForm b) (expRe b β ω) (expIm b β ω)

The exponential pair lies in its own positive half.

Taking (expRe, expIm) as the reference is therefore not an arbitrary choice dressed up: the half it names is the one containing exp(β + iω), which is how Bridgeland specifies P⁺. Whether that half is independent of ω is the cocycle question, and is not settled here.