LF4 §8: the first concrete ontic-shell instantiation

Category: 3-Local (the first concrete ontic-shell instantiation).

This file discharges the structural part of LF4 §8 (specs/LF4-todo.md): it exhibits a concrete CSD.LF2.SectorData, proving that LF2's abstract framework is inhabited (it had never been instantiated), and that the sector-conditional measure bridge holds axiom-free for the instance. For this base case (π = id) the bridge is the trivial c = 1 identity. The non-trivial-fibre instance KahlerInstance.lean (Σ = ℂℙ^{M-1} × T², π = pr₁) likewise builds its bridge axiom-free, via the product marginal (Measure.fst_prod), not via any uniqueness axiom. (invariant_measure_uniqueness_cpn is the proved ℂℙ^{N-1} invariant-measure-uniqueness fact available for bridges that need it; the abstract CSD.LF2.invariant_measure_uniqueness axiom it once realised, and the abstract measure_bridge lemma it served, were removed 2026-06-04 as unused.)

The instance

cpSectorData p₀ is the minimal shell:

• Σ = P = ℂℙ^{N-1} = ℙ ℂ (EuclideanSpace ℂ (Fin N));
• G = U(N) = Matrix.unitaryGroup (Fin N) ℂ, acting on ℂℙ^{N-1} as usual;
• π = id;
• μL = fubiniStudyMeasure p₀ (the U(N)-invariant Borel probability measure), Φ = id, Ω₀ = univ.

Honest scope. This is the base case. With π = id the projection has trivial (point) fibres, so there is no unresolved ontic structure and the bridge constant is c = 1. The value here is exactly: (i) LF2's SectorData is now proven non-vacuous, and (ii) cp_measure_bridge is axiom-free, demonstrating that the LF2 axiom is dischargeable in the concrete ℂℙ^{N-1} / U(N) setting. A non-trivial-fibre instance (ℂℙ^{N-1} × ℂℙ^{N-1}, π = pr₁) and, separately, the de-isolation dynamics that turn volume ratios into Born weights, are future work; this shell is the scaffold they attach to. It does not by itself reproduce any Born prediction.

@[reducible, inline]

abbrev CSD.LF4.CPN (N : ℕ) : Type

ℂℙ^{N-1}.

Equations

• CSD.LF4.CPN N = Projectivization ℂ (EuclideanSpace ℂ (Fin N))

instance CSD.LF4.instNonemptyCPN {N : ℕ} [NeZero N] : Nonempty (CPN N)

ℂℙ^{N-1} is nonempty for N ≥ 1 (it carries projective rays of a nonzero space).

noncomputable def CSD.LF4.cpOnticSetup {N : ℕ} [NeZero N] (p₀ : CPN N) : LF1.OnticSetup (CPN N)

The minimal ontic-shell OnticSetup: μL is Fubini–Study, the flow is the identity, and the preparation region is everything.

Equations

• CSD.LF4.cpOnticSetup p₀ = { μL := ⟨Matrix.UnitaryGroup.fubiniStudyMeasure p₀, ⋯⟩, Φ := id, hΦ_pres := ⋯, Ω0 := Set.univ, hΩ0_meas := ⋯, hΩ0_nonzero := ⋯ }

noncomputable def CSD.LF4.cpSectorData {N : ℕ} [NeZero N] (p₀ : CPN N) : LF2.SectorData (CPN N) (CPN N) ↥(Matrix.unitaryGroup (Fin N) ℂ)

First concrete SectorData. Σ = P = ℂℙ^{N-1}, G = U(N), π = id. Witnesses that LF2's abstract framework is inhabited.

Equations

• CSD.LF4.cpSectorData p₀ = { toOntic := CSD.LF4.cpOnticSetup p₀, π := id, measurable_π := ⋯, measurable_smul_σ := ⋯, measurable_smul_P := ⋯, hμL_inv := ⋯, hπ_equiv := ⋯ }

theorem CSD.LF4.cp_measure_bridge {N : ℕ} [NeZero N] (p₀ : CPN N) : ∃ (c : ENNReal), MeasureTheory.Measure.map (cpSectorData p₀).π (cpSectorData p₀).μL = c • Matrix.UnitaryGroup.fubiniStudyMeasure p₀

Axiom-free measure bridge for the instance. π∗μL = c · μFS with c = 1 (since π = id and μL = μFS). Proved via Measure.map_id, so it cites only the foundational triple — no LF2 axiom.