LF4 Tranche A: a non-trivial measure-preserving flow on the Kähler instance

Category: 3-Local (a non-trivial measure-preserving flow on the Kähler instance).

Every concrete SectorData built so far (LF4/Instance.lean, LF4/KahlerInstance.lean, Tests/Examples.lean) hard-codes Φ := id, so the LF1 deterministic-typicality theorem, when instantiated, runs the strong law over i.i.d. preparation draws with no ontic evolution. The hΦ_pres (Liouville preservation) field is consumed only via its measurability content; its preservation payload has never been load-bearing (see LF1/Setup.lean).

This module installs the first non-trivial deterministic flow on the existing Kähler space KSigma N = ℂℙ^{N-1} × T²: a constant translation kFlow sh : (p, t) ↦ (p, sh + t) on the T² fibre. It is measure-preserving for kMuL = μFS ⊗ vol_{T²} because the fibre volume is the (translation- invariant) Haar measure on AddCircle 1 × AddCircle 1, and it acts trivially on the base. The frequency capstone kFlow_frequency_convergence fires the law-agnostic LF1 theorem freq_tendsto_of_iid on the evolved trials kFlow sh ∘ sampleₙ, and the measure-preservation of kFlow is exactly what pins law(kFlow sh ∘ sampleₙ) = kMuL p₀, hence the limiting frequency to the volume ratio (kMuL O).toReal. So hΦ_pres is load-bearing here for the first time.

What this does and does not establish

• Does: exhibits Φ ≠ id on a genuinely compact-Kähler Σ, makes the LF1 deterministic structure non-vacuous on a concrete instance, and shows the ontic volume ratio is stable under deterministic evolution — the structural role Sigma0 §2.4 assigns to (Φ_t)∗ μL = μL. The flow preserves projective rays (kFlow_preserves_rays: (kFlow sh p).1 = p.1, i.e. π ∘ kFlow = π since (kSectorData _).π = Prod.fst), matching CSD's constraint-surface reading — the flow moves only within a fibre over a fixed quantum state [ψ].
• Does not: escape the carve-out. The limit (kMuL O).toReal is the chosen volume of O; a translation flow has Haar as its invariant measure, so even with Birkhoff the space-average is the carved measure. Deriving the outcome region (and hence its Born weight) from the dynamics is Tranche B (specs/carve-out-plan.md §4, the §9.5 / G3b target), not this module.

noncomputable def CSD.LF4.kFlow {N : ℕ} (sh : KTorus) : KSigma N → KSigma N

The fibre-translation flow on Σ = ℂℙ^{N-1} × T²: translate the T² coordinate by a fixed sh, leaving the base ray fixed.

Equations

• CSD.LF4.kFlow sh p = (p.1, sh + p.2)

@[simp]

theorem CSD.LF4.kFlow_apply {N : ℕ} (sh : KTorus) (p : KSigma N) : kFlow sh p = (p.1, sh + p.2)

@[simp]

theorem CSD.LF4.kFlow_preserves_rays {N : ℕ} (sh : KTorus) (p : KSigma N) : (kFlow sh p).1 = p.1

The fibre flow preserves projective rays: (kFlow sh p).1 = p.1. Since (kSectorData _).π = Prod.fst, this is the constraint-surface compatibility hypothesis h_flow_π of SectorData.outcomeOfProjective — the deterministic flow moves only within the fibre over a fixed quantum state [ψ].

theorem CSD.LF4.kFlow_ne_id {N : ℕ} (p₀ : CPN N) {sh : KTorus} (hsh : sh ≠ 0) : kFlow sh ≠ id

The flow is non-trivial for a nonzero fibre shift: dynamics is genuinely present, unlike the Φ = id base instances.

theorem CSD.LF4.kFlow_measurePreserving {N : ℕ} (p₀ : CPN N) (sh : KTorus) : MeasureTheory.MeasurePreserving (kFlow sh) (kMuL p₀) (kMuL p₀)

The flow is measure-preserving for the Kähler/Liouville volume. This is the genuine hΦ_pres content (Liouville's theorem) for a non-identity flow: translation is Haar-invariant on the T² fibre and the base factor is fixed.

theorem CSD.LF4.kFlow_frequency_convergence {N : ℕ} (p₀ : CPN N) (sh : KTorus) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (sample : ℕ → Ω → KSigma N) (hsample : ∀ (n : ℕ), Measurable (sample n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (sample n) Pr = kMuL p₀) {O : Set (KSigma N)} (hO : MeasurableSet O) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (kFlow sh ∘ sample n ⁻¹' O).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (kFlow sh ∘ sample i ⁻¹' O).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds ((kMuL p₀) O).toReal)

Tranche A frequency capstone. For i.i.d. preparation draws sampleₙ with common law kMuL p₀, the empirical frequency of a measurable outcome region O evaluated on the evolved states kFlow sh ∘ sampleₙ converges almost surely to the ontic volume ratio (kMuL p₀ O).toReal.

The deterministic flow kFlow sh (non-trivial for sh ≠ 0, by kFlow_ne_id) is applied to every sampled microstate, and kFlow_measurePreserving is what makes law(kFlow sh ∘ sampleₙ) = kMuL p₀, hence pins the limit to the volume ratio. This is the LF1 deterministic-typicality theorem realised with a genuine flow on a compact-Kähler Σ.

D1c-1: the concrete Kähler SectorData with Φ = kFlow ≠ id

Every concrete SectorData shipped so far (cpSectorData, kSectorData) hard-codes Φ := id in its underlying OnticSetup, leaving the standing structural debt: the corpus has a genuine measure-preserving non-identity flow (kFlow, above) but no concrete SectorData carrying it. This block discharges that debt for the Kähler instance by rebuilding kOnticSetup / kSectorData with Φ := kFlow sh.

Only the three flow-related OnticSetup fields change (Φ, hΦ_pres, and the derived measurable_Φ); μL, Ω0, and their hypotheses are reused verbatim. The SectorData G-action fields (measurable_smul_σ, measurable_smul_P, hμL_inv, hπ_equiv) are about the U(N)-action and π = Prod.fst, never about Φ, so they are reused verbatim from kSectorData (hμL_inv reads toOntic.μL, which is unchanged = kMuL p₀).

Honest scope. kFlow is a free T²-fibre translation: a genuine measure-preserving Φ ≠ id, but dynamically trivial — it is not a measurement / de-isolation flow (LF5's Φ_vN), nor a symplectic / Hamiltonian flow generated by the Kähler form. So this is the structural discharge of the "Φ = id in the concrete Kähler instance" debt, not its physical content. Deferred (D1c-2): threading a de-isolation or Hamiltonian flow as the instance's Φ. SO-1 is untouched — D1c is necessary-but-not-sufficient for deriving the sector + Fubini–Study typicality from the dynamics (SO-1 additionally needs the flow ergodic / mixing to force μFS). cpSectorData still carries Φ = id; only the Kähler instance is addressed here.

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

The Kähler OnticSetup with the non-identity flow Φ := kFlow sh. Identical to kOnticSetup p₀ except for the three flow fields: Φ is the fibre translation, hΦ_pres is kFlow_measurePreserving (genuine Liouville content, not MeasurePreserving.id). μL, Ω0, and their hypotheses are reused.

Equations

• CSD.LF4.kOnticSetupFlow p₀ sh = { μL := ⟨CSD.LF4.kMuL p₀, ⋯⟩, Φ := CSD.LF4.kFlow sh, hΦ_pres := ⋯, Ω0 := Set.univ, hΩ0_meas := ⋯, hΩ0_nonzero := ⋯ }

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

The concrete compact-Kähler SectorData carrying a genuine measure-preserving Φ ≠ id. Identical to kSectorData p₀ except its underlying ontic data is kOnticSetupFlow p₀ sh (so Φ = kFlow sh). The G = U(N) action fields are reused verbatim from kSectorData; none of them mention Φ.

Equations

• CSD.LF4.kSectorDataFlow p₀ sh = { toOntic := CSD.LF4.kOnticSetupFlow p₀ sh, π := Prod.fst, measurable_π := ⋯, measurable_smul_σ := ⋯, measurable_smul_P := ⋯, hμL_inv := ⋯, hπ_equiv := ⋯ }

@[simp]

theorem CSD.LF4.kSectorDataFlow_phi {N : ℕ} [NeZero N] (p₀ : CPN N) (sh : KTorus) : (kSectorDataFlow p₀ sh).toOntic.Φ = kFlow sh

The instance's flow is exactly kFlow sh (definitional).

theorem CSD.LF4.kSectorDataFlow_phi_ne_id {N : ℕ} [NeZero N] (p₀ : CPN N) {sh : KTorus} (hsh : sh ≠ 0) : (kSectorDataFlow p₀ sh).toOntic.Φ ≠ id

D1c-1 headline. The concrete Kähler SectorData genuinely carries Φ ≠ id: the structural "Φ = id in the concrete Kähler instance" debt is discharged. Reuses kFlow_ne_id.

theorem CSD.LF4.kSectorDataFlow_phi_measurePreserving {N : ℕ} [NeZero N] (p₀ : CPN N) (sh : KTorus) : MeasureTheory.MeasurePreserving (kSectorDataFlow p₀ sh).toOntic.Φ (kMuL p₀) (kMuL p₀)

The instance's flow is measure-preserving for the Kähler/Liouville volume kMuL p₀ (the genuine hΦ_pres content surfaced on the SectorData).

theorem CSD.LF4.kSectorDataFlow_frequency_convergence {N : ℕ} [NeZero N] (p₀ : CPN N) (sh : KTorus) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (sample : ℕ → Ω → KSigma N) (hsample : ∀ (n : ℕ), Measurable (sample n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (sample n) Pr = kMuL p₀) {O : Set (KSigma N)} (hO : MeasurableSet O) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => ((kSectorDataFlow p₀ sh).toOntic.Φ ∘ sample n ⁻¹' O).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, ((kSectorDataFlow p₀ sh).toOntic.Φ ∘ sample i ⁻¹' O).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds ((kMuL p₀) O).toReal)

Non-vacuity link to LF1. The LF1 deterministic-typicality theorem is non-vacuous on kSectorDataFlow: for i.i.d. preparation draws, the empirical frequency of a measurable outcome region O evaluated on the states evolved by the instance's own flow (kSectorDataFlow p₀ sh).toOntic.Φ converges almost surely to the ontic volume ratio (kMuL p₀ O).toReal. This is just kFlow_frequency_convergence stated through the instance (Φ = kFlow sh is definitional), so the moving flow that pins the limit is the SectorData's own Φ ≠ id, not the identity. LF1 is cited, not re-proved.