SL-2: a genuine Φ ≠ id on the concrete ENTANGLED (singlet) sector

Category: 3-Local (a genuine Φ ≠ id on the concrete ENTANGLED (singlet) sector).

D1c-1 (LF4/KahlerFlow.lean) discharged the "Φ = id in the concrete Kähler instance" debt for the GENERIC sector: kSectorDataFlow carries the non-identity measure-preserving flow Φ = kFlow sh (a free T²-fibre translation), and kFlow_frequency_convergence makes its Liouville-preservation load-bearing (it pins the law of the evolved trials kFlow sh ∘ sample).

This module does the same for the entangled sector — the two-qubit singlet on Σ = ℂℙ³ × T² (LF4/SingletKahler.lean), SL-2. The singlet preparation ofKählerPreparation was built over kSectorData (Φ = id); here it is rebuilt over kSectorDataFlow p₀ sh (Φ = kFlow sh ≠ id), and the per-sector frequency capstone fires with the trials genuinely evolved by the sector's own flow.

The mechanism is exact and requires no new engine. An LF1 OutcomeRegion's scored event is preEvent = Φ ⁻¹' Ω (LF1/Outcomes.lean), so with Φ = kFlow sh the capstone scores X ⁻¹' preEvent = (kFlow sh ∘ X) ⁻¹' kRegion — each sampled microstate is pushed one flow-step before its outcome block is read. Liouville preservation is load-bearing through bridge_op_p: the carving identity now reads kMuPsi (kFlow sh ⁻¹' kRegion) = kMuPsi (kRegion) = P_st, the first equality being kFlow_measurePreserving_muPsi (the singlet analogue of kFlow_measurePreserving). So the empirical frequency of the flow-evolved singlet trials still converges a.s. to the Born weight P_st.

Deliverables

• kFlow_measurePreserving_muPsi — kFlow sh preserves the singlet fibre law μψ = δ_{[singlet]} ⊗ vol_{T²} (fixes the base ray, translates the fibre);
• ofKählerPreparationFlow — the singlet PureSingletPreparation over the Φ ≠ id sector kSectorDataFlow p₀ sh;
• ofKählerPreparationFlow_phi_ne_id — its sector genuinely carries Φ ≠ id;
• ofKählerPreparationFlow_flow_frequency_convergence — the per-sector empirical frequencies of the trials evolved by kFlow sh converge a.s. to P_st.

Honest scope (unchanged from D1c-1)

kFlow is a free fibre translation: a genuine measure-preserving Φ ≠ id, but dynamically trivial (it is not a de-isolation / measurement flow, nor a Hamiltonian flow generated by the Kähler form; it moves only within the fibre over a fixed ray). So this is the structural discharge of "Φ = id in the concrete entangled instance", making Liouville-preservation load-bearing on the singlet — NOT a derivation of the sector. The sector origin is untouched (the entangled sector / Fubini–Study typicality is still posited; that is SO-1, distinct from Paper C Axiom A5). Foundational-triple-only / Gleason-free, inherited from ofKählerPreparation and the LF3 chain.

kFlow preserves the singlet fibre law μψ

theorem CSD.LF4.kFlow_measurePreserving_muPsi (sh : KTorus) : MeasureTheory.MeasurePreserving (kFlow sh) kMuPsi kMuPsi

The fibre flow preserves the singlet fibre law. kFlow sh fixes the base ray (so it preserves the Dirac δ_{[singlet]} on ℂℙ³) and translates the T² fibre (so it preserves the Haar volume there). This is the singlet analogue of kFlow_measurePreserving, and the genuine Liouville content that makes Φ load-bearing in the frequency capstone below.

The preparation bundle over the Φ ≠ id sector

Each component of ofKählerPreparation references the sector only through its projection π = Prod.fst and Liouville measure μL = kMuL p₀ — both DEFINITIONALLY equal between kSectorData and kSectorDataFlow (they differ only in Φ). So the bridge / preparation / outcome-region proofs port verbatim.

noncomputable def CSD.LF4.kBridgeFlow (p₀ : CPN 4) (sh : KTorus) : LF2.MeasureBridgeData (kSectorDataFlow p₀ sh) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The axiom-free measure bridge for the Φ ≠ id sector (c = 1, π∗μL = μFS via Measure.fst_prod), identical to kBridge — the bridge does not see Φ.

Equations

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

noncomputable def CSD.LF4.kPurePrepFlow (p₀ : CPN 4) (sh : KTorus) : LF2.PurePreparation (kSectorDataFlow p₀ sh) kMuPsi 4

The singlet PurePreparation over the Φ ≠ id sector (constant rep, Dirac concentration through π = Prod.fst), identical to kPurePrep.

Equations

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

noncomputable def CSD.LF4.kOutcomeRegionFlow (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (sh : KTorus) (s t : LF3.Sign) : (kOnticSetupFlow p₀ sh).OutcomeRegion

The per-sector outcome region over the Φ ≠ id ontic setup: same carved set kRegion as kOutcomeRegion (the region is base-flow-agnostic). Its scored event is preEvent = kFlow sh ⁻¹' kRegion — the flow enters HERE.

Equations

• CSD.LF4.kOutcomeRegionFlow ctx p₀ sh s t = { Ω := CSD.LF4.kRegion ctx s t, hΩ_meas := ⋯ }

noncomputable def CSD.LF4.ofKählerPreparationFlow (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (sh : KTorus) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) : LF3.PureSingletPreparation (kSectorDataFlow p₀ sh) ctx 4

SL-2: the singlet preparation on the Φ ≠ id sector. The concrete LF3.PureSingletPreparation for the two-qubit singlet over kSectorDataFlow p₀ sh (Φ = kFlow sh ≠ id). Identical to ofKählerPreparation except the underlying sector carries the genuine non-identity flow, so the scored event is preEvent = kFlow sh ⁻¹' kRegion. bridge_op_p holds because kMuPsi (kFlow sh ⁻¹' kRegion) = kMuPsi (kRegion) = P_st — the first equality is kFlow's Liouville-preservation (kFlow_measurePreserving_muPsi), now load-bearing; the second is the carving identity kMuPsi_kRegion.

Equations

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

theorem CSD.LF4.ofKählerPreparationFlow_phi_ne_id (p₀ : CPN 4) {sh : KTorus} (hsh : sh ≠ 0) : (kSectorDataFlow p₀ sh).toOntic.Φ ≠ id

The underlying sector genuinely carries Φ ≠ id (for any nonzero fibre shift), via kFlow_ne_id. This is the SL-2 headline: the concrete ENTANGLED sector now carries a genuine non-identity flow.

theorem CSD.LF4.ofKählerPreparationFlow_preEvent (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (sh : KTorus) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) (s t : LF3.Sign) : ((ofKählerPreparationFlow ctx p₀ sh hgen).O_region s t).preEvent = kFlow sh ⁻¹' kRegion ctx s t

The scored event of the flow preparation is the flow-pullback of the carved region: preEvent = kFlow sh ⁻¹' kRegion. So scoring trial X n on it reads X n ⁻¹' preEvent = (kFlow sh ∘ X n) ⁻¹' kRegion — the microstate is evolved one flow-step before its outcome block is checked.

The load-bearing capstone: frequencies of flow-evolved singlet trials

theorem CSD.LF4.ofKählerPreparationFlow_flow_frequency_convergence (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (sh : KTorus) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] {X : ℕ → Ω → KSigma 4} (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = kMuPsi) (hindep : ∀ (s t : LF3.Sign), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (kFlow sh ∘ X n ⁻¹' kRegion ctx s t).indicator fun (x : Ω) => 1)) (s t : LF3.Sign) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (kFlow sh ∘ X i ⁻¹' kRegion ctx s t).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (LF3.P_st ctx.a ctx.b s t))

SL-2 capstone: the singlet frequencies survive the sector's own flow. For i.i.d. trials with the posited singlet fibre law μψ, the per-sector empirical frequencies of the trials evolved by the sector's non-identity flow kFlow sh ≠ id — i.e. of (kFlow sh ∘ X) ⁻¹' kRegion — converge almost surely to the Born weight P_st ctx.a ctx.b s t.

The deterministic flow kFlow sh is applied to every sampled microstate, and its Liouville-preservation (kFlow_measurePreserving_muPsi) is exactly what keeps the limit at P_st (via bridge_op_p / weight_eq_P_st). This is D1c-1's load-bearing-flow achievement realised on the ENTANGLED singlet preparation. Foundational-triple-only / Gleason-free. Standing gap unchanged: SO-1 (the entangled sector is posited) and kFlow is dynamically trivial (a free fibre translation).