LF4 §8: the ofKählerPreparation constructor for the singlet

Category: 3-Local (the ofKählerPreparation constructor for the singlet).

Assembles a concrete LF3.PureSingletPreparation kSectorData ctx 4 on the non-trivial-fibre compact-Kähler instance Σ = ℂℙ³ × T² (the N = 4 case for the two-qubit singlet), discharging the bundle's load-bearing fields as theorems for a fixed measurement context:

• the reindex singletPsi := kReindex singlet : EuclideanSpace ℂ (Fin 4);
• the posited fibre law μψ := (Measure.dirac ⟦singletPsi⟧).prod vol_{T²}, which pushes through π = pr₁ to the Dirac on the ray (Measure.fst_prod);
• the constant projective representative rep := fun _ => singletPsi (only its value at ray_point matters under Dirac integration, so this is sufficient for OperationalPackage.fromPreparation);
• the genuine joint spin eigenstate eig s t := kReindex (singletJointEig …), with MeasurementJointEig.born_eq_P_st discharged via singletJointEig_born (the §3 theorem) transported through the isometry;
• the outcome regions O_kReg s t with second factor a measure-P_st arc on the first AddCircle 1 of T² — bridge_op_p then holds because the fibre region has volume exactly P_st and the Dirac-integrated OP probability is the same P_st (proved Busch-free via born_rank_one_direct and singletJointEig_born).

Generic-context hypothesis. Restricted to ∀ s t, 0 < P_st ctx.a ctx.b s t, i.e. |a·b| < 1 — the generic non-collinear contexts, which include the four canonical CHSH-optimal pairs. ⚠️ Collinear settings (a = ±b) are excluded; the earlier wording "all Bell-test settings qualify" was too broad, since Bell experiments routinely discuss aligned and anti-aligned axes (corrected 2026-08-11). Those settings carry perfect (anti)correlation, not "no Born-content"; two of the four P_st vanish, which is exactly what hgen forbids. The local route LF6.localDeisolation_pointer_volume_local covers them.

Axiom posture. ofKählerPreparation is foundational-triple only (the constant rep + the _direct Born theorem keep Busch out of the construction). The concrete frequency capstone is also foundational-triple-only / Gleason-free: the LF3 chain's weight_eq_P_st routes through the Busch-free OP_p_at_jointEig_eq_P_st_direct (the 2026-06-02 re-route; AXIOMS.md §2.4), not through the Busch-mediated twin.

Honesty note (Tier-2 framing). bridge_op_p holds because the outcome regions are carved to fibre-volume P_st. This realises eq-12 (the volume-ratio thesis) concretely on a compact-Kähler Σ, but it does not derive P_st from independent geometry. The capstone-of-the-instance is non-vacuous; the further reduction "why do volumes select Born?" remains the constraint-surface-dynamics open problem (LF4-todo §8 outro).

Reindex isometry Fin 2 × Fin 2 → Fin 4

noncomputable def CSD.LF4.kReindex : EuclideanSpace ℂ (Fin 2 × Fin 2) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin 4)

The reindexing isometry, lifting finProdFinEquiv : Fin 2 × Fin 2 ≃ Fin 4 to a LinearIsometryEquiv of EuclideanSpace ℂs.

Equations

• CSD.LF4.kReindex = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ finProdFinEquiv

theorem CSD.LF4.P_st_le_one (a b : LF3.DetectorSetting) (s t : LF3.Sign) : LF3.P_st a b s t ≤ 1

A handy upper bound: P_st ≤ 1 (it is in fact ≤ 1/2, but ≤ 1 suffices).

Singlet vector in Fin 4 and its projective ray

noncomputable def CSD.LF4.singletPsi : EuclideanSpace ℂ (Fin 4)

The Bell singlet, re-indexed into EuclideanSpace ℂ (Fin 4).

Equations

• CSD.LF4.singletPsi = CSD.LF4.kReindex CSD.LF3.singlet

theorem CSD.LF4.singletPsi_norm : ‖singletPsi‖ = 1

theorem CSD.LF4.singletPsi_ne_zero : singletPsi ≠ 0

noncomputable def CSD.LF4.singletRay : CPN 4

The projective ray [singletPsi] ∈ ℂℙ³.

Equations

• CSD.LF4.singletRay = Projectivization.mk ℂ CSD.LF4.singletPsi CSD.LF4.singletPsi_ne_zero

Carving: an arc of AddCircle 1 with measure ℓ

noncomputable def CSD.LF4.fibreArc (ℓ : ℝ) : Set (AddCircle 1)

For ℓ ∈ [0, 1], the measurable subset of AddCircle 1 whose pre-image under the Ioc 0 1 chart is the sub-interval Ioc 0 ℓ; has Haar volume exactly ENNReal.ofReal ℓ. Uses equivIoc (the underlying Equiv) so measurePreserving_equivIoc applies directly.

Equations

• CSD.LF4.fibreArc ℓ = ⇑(AddCircle.equivIoc 1 0) ⁻¹' Subtype.val ⁻¹' Set.Ioc 0 ℓ

theorem CSD.LF4.fibreArc_measurable (ℓ : ℝ) : MeasurableSet (fibreArc ℓ)

theorem CSD.LF4.fibreArc_volume {ℓ : ℝ} (hℓ : ℓ ∈ Set.Icc 0 1) : MeasureTheory.volume (fibreArc ℓ) = ENNReal.ofReal ℓ

Outcome regions on Σ = ℂℙ³ × T²

noncomputable def CSD.LF4.kRegion (ctx : LF3.MeasurementContext) (s t : LF3.Sign) : Set (KSigma 4)

The outcome region at sector (s, t): all of ℂℙ³, times an arc of the first AddCircle of measure P_st, times the whole second AddCircle. The base-side factor univ_{ℂℙ³} will be inflated to a Dirac at the singlet ray by the fibre measure μψ.

Equations

• CSD.LF4.kRegion ctx s t = Set.univ ×ˢ CSD.LF4.fibreArc (CSD.LF3.P_st ctx.a ctx.b s t) ×ˢ Set.univ

theorem CSD.LF4.kRegion_measurable (ctx : LF3.MeasurementContext) (s t : LF3.Sign) : MeasurableSet (kRegion ctx s t)

noncomputable def CSD.LF4.kOutcomeRegion (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (s t : LF3.Sign) : (kOnticSetup p₀).OutcomeRegion

Packaged as an LF1 OutcomeRegion over kOnticSetup.

Equations

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

Fibre measure μψ

noncomputable def CSD.LF4.kMuPsi : MeasureTheory.Measure (KSigma 4)

The posited fibre trial law over [singletPsi]: δ_{[ψ]} ⊗ vol_{T²}. Pushes through π = pr₁ to the Dirac on the ray.

Equations

• CSD.LF4.kMuPsi = (MeasureTheory.Measure.dirac CSD.LF4.singletRay).prod MeasureTheory.volume

instance CSD.LF4.instProbKMuPsi : MeasureTheory.IsProbabilityMeasure kMuPsi

theorem CSD.LF4.kMuPsi_push : MeasureTheory.Measure.map Prod.fst kMuPsi = MeasureTheory.Measure.dirac singletRay

μψ's pushforward through π = pr₁ is the Dirac on the singlet ray.

theorem CSD.LF4.kMuPsi_kRegion (ctx : LF3.MeasurementContext) (s t : LF3.Sign) : kMuPsi (kRegion ctx s t) = ENNReal.ofReal (LF3.P_st ctx.a ctx.b s t)

The fibre-measure of an outcome region equals the fibre-arc volume, ENNReal.ofReal (P_st ctx.a ctx.b s t) (the carving identity).

PurePreparation over kSectorData and μψ

Constant rep := fun _ => singletPsi. Only its value at the ray matters under Dirac integration; rep_at_ray is rfl, push_dirac is kMuPsi_push.

noncomputable def CSD.LF4.kRep : CPN 4 → EuclideanSpace ℂ (Fin 4)

The constant projective representative.

Equations

• CSD.LF4.kRep x✝ = CSD.LF4.singletPsi

theorem CSD.LF4.kRep_unit (p : CPN 4) : ‖kRep p‖ = 1

theorem CSD.LF4.kRep_meas : Measurable kRep

noncomputable def CSD.LF4.kPurePrep (p₀ : CPN 4) : LF2.PurePreparation (kSectorData p₀) kMuPsi 4

The LF2.PurePreparation over kSectorData p₀ and the posited fibre law.

Equations

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

MeasurementJointEig for the singlet

The hgen : ∀ s t, 0 < P_st ctx.a ctx.b s t (generic-context) hypothesis is threaded explicitly through the lemmas.

noncomputable def CSD.LF4.kEig (ctx : LF3.MeasurementContext) (s t : LF3.Sign) : EuclideanSpace ℂ (Fin 4)

The genuine joint spin eigenstates, transported to Fin 4.

Equations

• CSD.LF4.kEig ctx s t = CSD.LF4.kReindex (CSD.LF3.singletJointEig s t ctx.a ctx.b)

theorem CSD.LF4.kEig_unit (ctx : LF3.MeasurementContext) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) (s t : LF3.Sign) : ‖kEig ctx s t‖ = 1

theorem CSD.LF4.kEig_distinct (ctx : LF3.MeasurementContext) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) {s t s' t' : LF3.Sign} (h : (s, t) ≠ (s', t')) : kEig ctx s t ≠ kEig ctx s' t'

theorem CSD.LF4.kEig_born (ctx : LF3.MeasurementContext) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) (s t : LF3.Sign) : ‖inner ℂ singletPsi (kEig ctx s t)‖ ^ 2 = LF3.P_st ctx.a ctx.b s t

noncomputable def CSD.LF4.kJED (ctx : LF3.MeasurementContext) (hgen : ∀ (s t : LF3.Sign), 0 < LF3.P_st ctx.a ctx.b s t) : LF3.MeasurementJointEig ctx singletPsi

The MeasurementJointEig bundle for the singlet, with born_eq_P_st discharged as a theorem.

Equations

• CSD.LF4.kJED ctx hgen = { eig := CSD.LF4.kEig ctx, eig_unit := ⋯, eig_distinct := ⋯, born_eq_P_st := ⋯ }

MeasureBridgeData for the Kähler instance (axiom-free, c = 1)

noncomputable def CSD.LF4.kBridge (p₀ : CPN 4) : LF2.MeasureBridgeData (kSectorData p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

The (axiom-free) MeasureBridgeData for kSectorData p₀: π∗μL = 1 · μFS via Measure.fst_prod. Builds the bridge fields directly, so it stays foundational-triple-only (this is now the only route — the abstract measure_bridge / invariant_measure_uniqueness axiom were removed 2026-06-04).

Equations

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

The ofKählerPreparation constructor

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

The constructor: a concrete LF3.PureSingletPreparation for the singlet on the non-trivial-fibre compact-Kähler kSectorData p₀, with bridge_op_p discharged as a theorem (via the carving identity kMuPsi_kRegion and the Busch-free LF2.PurePreparation.born_rank_one_direct).

The bundle composes:

• μψ = kMuPsi = (Measure.dirac singletRay).prod vol_{T²} (posited fibre law);
• μFS = fubiniStudyMeasure p₀, with axiom-free kBridge (c = 1 marginal);
• PP = kPurePrep p₀ (constant rep := singletPsi, ray = singletRay);
• jed = kJED ctx hgen (genuine joint spin eigenstates, born_eq_P_st proved);
• O_region = kOutcomeRegion ctx p₀ (outcome = univ_{ℂℙ³} × arc(P_st) × univ).

bridge_op_p: LHS = μψ(preEvent) = vol_{T²}(arc(P_st) × univ) = P_st (carving); RHS = OP.p(rankOneEffect(eig)) = ‖⟨singletPsi, eig⟩‖² = P_st (born_rank_one_direct + kEig_born). Both sides ENNReal.ofReal P_st.

Equations

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

Concrete capstone: non-vacuous instance of the LF1↔LF2↔LF3 chain

Applying LF3_singlet_frequency_convergence to the concrete ofKählerPreparation yields a fully non-parametric empirical statement: for i.i.d. trials with law (ofKählerPreparation …).μψ, the per-sector empirical frequencies converge almost surely to P_st. This is the witness that the LF3 chain capstones are non-vacuous: there exists a PureSingletPreparation they can be applied to.

theorem CSD.LF4.ofKählerPreparation_singlet_frequency_convergence (ctx : LF3.MeasurementContext) (p₀ : CPN 4) (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 = (ofKählerPreparation ctx p₀ hgen).μψ) (hindep : ∀ (s t : LF3.Sign), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' ((ofKählerPreparation ctx p₀ hgen).O_region s t).preEvent).indicator fun (x : Ω) => 1)) (s t : LF3.Sign) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' ((ofKählerPreparation ctx p₀ hgen).O_region s t).preEvent).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (LF3.P_st ctx.a ctx.b s t))

The chain is non-vacuous on this instance. For i.i.d. trials with the posited fibre law, the per-sector empirical frequencies converge a.s. to P_st ctx.a ctx.b s t. Foundational-triple-only / Gleason-free (the LF3 chain routes through the Busch-free weight_eq_P_st / OP_p_at_jointEig_eq_P_st_direct, 2026-06-02 re-route).