LF4 Tranche 1: the Born weights as the torus moment map on ℂℙ^{N-1}

The Kähler structure on ℂℙ^{N-1} carries a canonical object the CSD corpus never invokes: the moment map of the maximal-torus action. For the standard phase action of Tᴺ on ℂℙ^{N-1}, the moment map is

Φ : ℂℙ^{N-1} → Δ_{N-1},   Φ([z])ᵢ = |zᵢ|² / ‖z‖²

landing in the standard simplex (coordinates nonnegative, summing to one). Its coordinates are the Born weights in the measurement eigenbasis: at a unit preparation ψ,

Φ([ψ])ᵢ = |ψᵢ|² = ‖⟨eᵢ, ψ⟩‖²    (eᵢ = EuclideanSpace.single i 1).

Mathematically this is a theorem of symplectic geometry — the coordinate formula is forced by the Fubini–Study Kähler structure together with the torus action — not an arc carved to a target value (SingletKahler.kMuPsi_kRegion) and not an operational-consistency postulate (busch_effect_gleason). It exhibits the Born weight vector as a canonical invariant of the very structure the programme takes as primitive (the compact Kähler Σ). See specs/carve-out-plan.md (Tranche 1).

Formalisation boundary (honest scope). In Lean, momentMap is defined directly by the coordinate formula ‖p.rep i‖²/‖p.rep‖²; the statement that this function satisfies the Hamiltonian moment-map equation ι_{X_i} ω = dΦᵢ for the FS symplectic form is the (standard, unformalised) symplectic fact motivating the name — Mathlib has no symplectic-form API and no Kähler API, so the "forced by the Kähler structure" claim is mathematical narrative, not a Lean theorem. What is machine-verified: well-definedness on rays (momentMap_mk), the simplex constraints (momentMap_nonneg, momentMap_sum_eq_one), the Born-weight identity (momentMap_mk_eq_inner_sq), and — by the measure-theoretic Gaussian route, not symplectic machinery — the Duistermaat–Heckman pushforward law (fs_moment_pushforward_uniform, qubit, proved 2026-05-31; fs_moment_joint_dirichlet_N, the joint Dirichlet law for general N, proved 2026-06-02). An earlier revision of this docstring listed the DH pushforward as not yet proved; that scope note is superseded.

Scope of this slice (historical). This module delivers the moment map, the simplex constraints, and the headline Born-weight identity. The ψ-dependence of preparations still enters through the preparation measure μψ, whose principled construction is the open G3b content.

Category: conceptually 1-Mathlib (CSD-free projective/Kähler geometry); kept here in CSD.LF4 for now as it drives the carve-out programme. Extraction candidate (cf. LF4-todo §10).

noncomputable def CSD.LF4.momentMap {N : ℕ} (p : CPN N) (i : Fin N) : ℝ

The torus moment map on ℂℙ^{N-1}, in coordinates: Φ([z])ᵢ = |zᵢ|²/‖z‖². Well-defined on the projective point (scale-invariant; see momentMap_mk).

Equations

• CSD.LF4.momentMap p i = ‖(Projectivization.rep p).ofLp i‖ ^ 2 / ‖Projectivization.rep p‖ ^ 2

theorem CSD.LF4.euclidean_norm_sq_eq_sum {N : ℕ} (v : EuclideanSpace ℂ (Fin N)) : ‖v‖ ^ 2 = ∑ i : Fin N, ‖v.ofLp i‖ ^ 2

‖v‖² = ∑ᵢ ‖vᵢ‖² on Euclidean space (Parseval in coordinate form).

theorem CSD.LF4.momentMap_nonneg {N : ℕ} (p : CPN N) (i : Fin N) : 0 ≤ momentMap p i

Each moment coordinate is nonnegative.

theorem CSD.LF4.momentMap_sum_eq_one {N : ℕ} (p : CPN N) : ∑ i : Fin N, momentMap p i = 1

The moment coordinates sum to one: the image lands in the simplex, so the Born weights form a probability vector.

theorem CSD.LF4.momentMap_le_one {N : ℕ} (p : CPN N) (i : Fin N) : momentMap p i ≤ 1

Each moment coordinate is at most one (‖p.rep i‖² ≤ ∑ⱼ ‖p.rep j‖² = ‖p.rep‖²).

theorem CSD.LF4.momentRatio_smul {N : ℕ} (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ (Fin N)) (i : Fin N) : ‖(c • v).ofLp i‖ ^ 2 / ‖c • v‖ ^ 2 = ‖v.ofLp i‖ ^ 2 / ‖v‖ ^ 2

The coordinate ratio ‖vᵢ‖²/‖v‖² is invariant under nonzero rescaling of v (the projective well-definedness of momentMap).

theorem CSD.LF4.momentMap_mk {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0) (i : Fin N) : momentMap (Projectivization.mk ℂ ψ hψ) i = ‖ψ.ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

The moment map evaluated at a representative ψ: Φ([ψ])ᵢ = ‖ψᵢ‖²/‖ψ‖². The value depends only on ψ (not on the chosen rep), by scale-invariance.

theorem CSD.LF4.momentMap_mk_eq_inner_sq {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) : momentMap (Projectivization.mk ℂ ψ hψ0) i = ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2

Headline (Tranche 1): the Born weight is the moment-map coordinate. For a unit preparation ψ, the i-th coordinate of the Fubini–Study torus moment map at [ψ] equals the Born weight ‖⟨eᵢ, ψ⟩‖² in the measurement eigenbasis eᵢ = EuclideanSpace.single i 1. Forced by the Kähler structure + torus action; no carving, no operational-consistency postulate.

Regularity: momentMap is continuous, hence measurable

momentMap is defined through p.rep, which is a Classical.choice representative — so it cannot be attacked directly: Projectivization.rep is not continuous as a map out of ℙ, and no amount of unfolding makes it so. The route is the quotient. The coordinate ratio v ↦ ‖vᵢ‖²/‖v‖² is continuous on the nonzero subtype and scale-invariant (momentRatio_smul), and mk' is a quotient map (Projectivization.isQuotientMap_mk'), so the descended function is continuous. Measurability is then immediate because ℙ K V carries the Borel σ-algebra of that same topology (Projectivization.instBorelSpace).

Needed by the record layer: the context-fixed basin Bᵢ(M) is a preimage under (p, θ) ↦ (momentMap p, θ), so its measurability rests on exactly this.

theorem CSD.LF4.continuous_momentMap {N : ℕ} (i : Fin N) : Continuous fun (p : CPN N) => momentMap p i

The moment-map coordinate is continuous. Proved by descent through the quotient map mk', since momentMap's defining formula goes through the choice-based rep.

theorem CSD.LF4.measurable_momentMap {N : ℕ} (i : Fin N) : Measurable fun (p : CPN N) => momentMap p i

The moment-map coordinate is measurable. Immediate from continuity, since ℙ ℂ V carries the Borel σ-algebra of the quotient topology (Projectivization.instBorelSpace). This is the prerequisite for the context-fixed basin Bᵢ(M) to be a measurable subset of Σ.