SL-3: the §13.2 ontic lift on the non-trivial-fibre Kähler instance

Category: 4-Foundations (the sector-symmetry→Wigner→U_isometry chain, made explicit on kSectorData).

The §13.2 ontic lift asks: on a concrete Kähler SectorData, thread the deterministic flow Φ down to a projective ray map f_Φ, prove f_Φ is transition-probability preserving, and feed that into Wigner rigidity to recover the Hilbert-space unitary (U_isometry) — the forward sector-symmetry → Wigner → U_isometry chain. This has been done for cpSectorData (π = id, cpSectorActionBundle, WignerDischarge.lean); SL-3 does it on the NON-TRIVIAL-FIBRE instance kSectorData (Σ = ℂℙ^{N-1} × T², π = pr₁ genuinely many-to-one, fibres = T²), where the descent of Φ along a many-to-one π is a real quotient step, not identity-on-Σ.

Two honest halves (both here)

• Part 1 — thread Φ (degenerate on this instance). The sector flow of kSectorDataFlow is Φ = kFlow sh, which moves ONLY the T² fibre (kFlow_preserves_rays). So its descent along π = pr₁ is the identity on rays (kProjectedFlow), and the descent equation π ∘ Φ = f_Φ ∘ π (kSectorDataFlow_projectable) holds on the many-to-one fibration. f_Φ is transition-probability preserving (kProjectedFlow_transProbPreserving) — honest but degenerate, exactly like trivialKahlerOnticSetup_transProbPreserving: the moving dynamics of this instance lives in the fibre, so the ray flow is trivial. Fed through Wigner it realises the unitary branch with U = 1 (kProjectedFlow_unitary_or_antiunitary, kProjectedFlow_eq_one_smul).

• Part 2 — the genuine content (caveat C-1: sector-action-carries-isometry). The non-degenerate TransProbPreserving datum on this instance is the sector U(N)-action g • · (transProbPreserving_unitary), the posited sector symmetry (SO-1). The cpSectorActionBundle analogue on kSectorData (kSectorActionBundle) builds a CSDUnitaryBundle whose U_isometry is DERIVED via Wigner from that action's transition-probability preservation, with the no-time-reversal selection from smul_action_not_antiunitary (N ≥ 2). Unitarity is the OUTPUT of Wigner, not a posit. This is the sector-symmetry → Wigner → U_isometry chain on the non-trivial-fibre Kähler SectorData.

Honesty flag (what SL-3 does NOT do)

The TransProbPreserving f_Φ of Part 1 holds because f_Φ = id, NOT because Φ is measure-preserving: there is deliberately no measure-preserving Φ ⟹ TransProbPreserving f_Φ step, since measure-preservation is strictly weaker than metric (transition-probability) preservation — that false implication is the §13.2 trap and the open D1/SO-1 gap (specs/LF4-todo.md). SL-3 makes the chain explicit on this instance without touching the sector origin (SO-1): the ray flow is trivial here, and the genuine isometry content (Part 2) rides on the posited U(N) sector action, not on the flow.

Part 1 — threading Φ: the flow descends to a ray map f_Φ, which is TransProbPreserving

def CSD.LF4.kProjectedFlow {N : ℕ} (_sh : KTorus) : CPN N → CPN N

The ray-descent f_Φ of the sector flow Φ = kFlow sh. Since kFlow moves only the T² fibre (kFlow_preserves_rays), the map it induces on the base ℂℙ^{N-1} of rays is the identity.

Equations

• CSD.LF4.kProjectedFlow _sh = id

theorem CSD.LF4.kSectorDataFlow_projectable {N : ℕ} [NeZero N] (p₀ : CPN N) (sh : KTorus) (x : KSigma N) : (kSectorDataFlow p₀ sh).π ((kSectorDataFlow p₀ sh).toOntic.Φ x) = kProjectedFlow sh ((kSectorDataFlow p₀ sh).π x)

The flow descends along the many-to-one π. π ∘ Φ = f_Φ ∘ π: the deterministic Σ-flow kFlow sh projects to kProjectedFlow sh on the quotient of rays. This is the genuine projectable descent equation on the NON-TRIVIAL fibration π = pr₁ (fibres = T²), the kSectorData analogue of a KahlerOnticSetup's projectedFlow descent — here it holds by kFlow_preserves_rays.

theorem CSD.LF4.kProjectedFlow_transProbPreserving {N : ℕ} (sh : KTorus) : Projectivization.TransProbPreserving (kProjectedFlow sh)

SL-3 Part 1 headline (thread Φ): the projected flow f_Φ is transition-probability preserving. Since f_Φ = kProjectedFlow sh = id (the flow is fibre-trivial on rays), this is honest but degenerate — compare trivialKahlerOnticSetup_transProbPreserving, which degenerates the same way (a comparison, not a dependency: this proof is rfl and uses nothing). It is NOT derived from measure-preservation of Φ (the §13.2 trap / open D1 gap); it holds because the ray-descent is literally the identity. The moving dynamics of this instance lives in the T² fibre; the non-degenerate isometry content is the sector U(N)-action (Part 2).

theorem CSD.LF4.kProjectedFlow_eq_one_smul {N : ℕ} (sh : KTorus) (p : CPN N) : kProjectedFlow sh p = 1 • p

The projected flow is realised by 1 ∈ U(N) (it is id), so the Wigner dichotomy below is non-vacuous on its unitary branch.

theorem CSD.LF4.kProjectedFlow_unitary_or_antiunitary {N : ℕ} (sh : KTorus) : (∃ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (p : CPN N), kProjectedFlow sh p = U • p) ∨ ∃ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (p : CPN N), kProjectedFlow sh p = U • Projectivization.conjProj p

sector-symmetry → Wigner → U_isometry, made explicit on the projected dynamics. Feeding the transition-probability preservation of the ray-descended flow into Wigner rigidity yields the unitary ∨ antiunitary dichotomy; the flow realises the unitary branch (with U = 1, since f_Φ = id, kProjectedFlow_eq_one_smul). The chain "deterministic Σ-flow → ray-descent f_Φ → Wigner → one-parameter unitary family" is thereby explicit on the non-trivial-fibre instance (degenerate here: the ray flow is trivial; the genuine content is Part 2).

Part 2 — the genuine content: the sector U(N)-action carries the FS-isometry (caveat C-1)

noncomputable def CSD.LF4.kBridgeData {N : ℕ} [NeZero N] (p₀ : CPN N) : LF2.MeasureBridgeData (kSectorData p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

Measure-bridge data for kSectorData (π = pr₁, c = 1), built axiom-free: the U(N)-invariance of μ_FS (fubiniStudyMeasure_smul_invariant) and the pr₁-pushforward π_*(μ_FS ⊗ vol_{T²}) = μ_FS (the torus volume being a probability measure, Measure.fst_prod). The kSectorData analogue of cpBridgeData.

Equations

• CSD.LF4.kBridgeData p₀ = { is_inv := ⋯, c := 1, bridge_eq := ⋯ }

noncomputable def CSD.LF4.kContext {N : ℕ} [NeZero N] (p₀ : CPN N) : Empirical.CSDBridge.Context (kSectorData p₀)

The bridge context for the non-trivial-fibre Kähler instance kSectorData.

Equations

• CSD.LF4.kContext p₀ = { μFS := Matrix.UnitaryGroup.fubiniStudyMeasure p₀, hμFS_prob := ⋯, bridge := CSD.LF4.kBridgeData p₀ }

noncomputable def CSD.LF4.kSectorActionBundle {N : ℕ} [NeZero N] (hN : 2 ≤ N) (p₀ : CPN N) (g : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : Empirical.CSDBridge.Gates.CSDUnitaryBundle (kSectorData p₀) N (EuclideanSpace ℂ (Fin N))

SL-3 Part 2 headline (the genuine content, caveat C-1): the sector U(N)-action on the non-trivial-fibre instance carries the Fubini–Study isometry. The cpSectorActionBundle analogue on kSectorData (π = pr₁ many-to-one, not π = id): a CSDUnitaryBundle on the Kähler instance whose U_isometry is DERIVED via Wigner (CSDUnitaryBundle.ofTransProbPreserving) from the sector action's transition-probability preservation (transProbPreserving_unitary g), with the no-time-reversal selection from smul_action_not_antiunitary (N ≥ 2). Unitarity is the OUTPUT of Wigner, not a posit — the sector-symmetry → Wigner → U_isometry chain, now on the non-trivial-fibre Kähler SectorData.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF4.kSectorActionBundle_U_isometry {N : ℕ} [NeZero N] (hN : 2 ≤ N) (p₀ : CPN N) (g : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (x y : EuclideanSpace ℂ (Fin N)) : inner ℂ ((kSectorActionBundle hN p₀ g).U x) ((kSectorActionBundle hN p₀ g).U y) = inner ℂ x y

The derived isometry, surfaced. The U carried by kSectorActionBundle is a genuine Fubini–Study / Hilbert isometry: ⟪U x, U y⟫ = ⟪x, y⟫ for all x, y — a THEOREM (Wigner output), not a posit. This is the U_isometry obligation of §13.2, discharged on the non-trivial-fibre Kähler instance.