Empirical/CSD: KCBS pentagon Born weights as Kähler volumes

Category: 3-Local (CSD-ontic volume reading; an instantiation of the context-generic engine context_born_frequency_basin, closing the KCBS gap found by the 2026-08-02 empirical-coverage audit — the last flagship test without a CSD twin).

The volume-ratio companion to the QM-side KCBS inequality (Empirical/QM/KCBS.lean): the five pentagon rays kv k violate the noncontextual bound 2 at the apex state with quantum value √5 (kcbs_qm_value, kcbs_quantum_violation). Here the per-context Born weights of that experiment are realised as Fubini–Study typicality volumes on the fixed ontic Σ = ℂℙ².

Construction

A KCBS context is an adjacent ray pair {kv k, kv (k+1)} — orthogonal by the pentagon overlap identity (kv_orth) — completed to a full projective frame by the cross product kv 0 ×₃ kv 1: orthogonal to both factors (dot_self_cross, dot_cross_self) and unit by the Lagrange identity (cross_dot_cross, 1·1 − 0² = 1). The three real vectors are complexified (c3), with the inner-product transport c3_inner pulling every orthonormality fact from the QM side's real dot products — no inner-product computation is re-proved.

Scope and honesty

• One representative context built ({kv 0, kv 1, ⋯×₃⋯}), as for KS18Volume: the other four pentagon contexts are identical instantiations at {kv k, kv (k+1)}, with per-context orthogonality already certified for all five by kv_orth. Mechanical repetition, omitted.
• Realisation, not derivation, as for the whole volume series: Born = FS-volume is derived one layer down (born_frequency_convergence_N_uncond, Gleason-free) and imported here; Φ = id — the dynamical-layer reading of KCBS is not exercised here (sequential statistics live in SequentialMeasurement.lean).
• The KCBS inequality itself (noncontextual bound 2, quantum √5) stays at the QM-validity layer; this file grounds the weights it is computed from.

References

Empirical/QM/KCBS.lean (kv, kv_orth, kv_unit, kv_apex_born, kcbs_qm_value); Empirical/CSD/ContextVolume.lean (the engine); Empirical/CSD/Contextuality/KS18Volume.lean (the sibling this mirrors); EMPIRICAL.md.

Complexification and the inner-product transport

noncomputable def CSD.Empirical.CSDBridge.KCBS.c3 (u : Fin 3 → ℝ) : EuclideanSpace ℂ (Fin 3)

Componentwise complexification ℝ³ → ℂ³.

Equations

• CSD.Empirical.CSDBridge.KCBS.c3 u = WithLp.toLp 2 fun (i : Fin 3) => ↑(u i)

theorem CSD.Empirical.CSDBridge.KCBS.c3_inner (u v : Fin 3 → ℝ) : inner ℂ (c3 u) (c3 v) = ↑(u ⬝ᵥ v)

Complexification transport: the complex inner product of two complexified real vectors is the coercion of their real dot product. Every orthonormality fact below is pulled from the QM side through this lemma — nothing is re-proved.

theorem CSD.Empirical.CSDBridge.KCBS.dot3_eq_dotProduct (u v : Fin 3 → ℝ) : QM.KCBS.dot3 u v = u ⬝ᵥ v

dot3 is the matrix dot product (Fin.sum_univ_three).

The representative pentagon context {kv 0, kv 1, kv 0 ×₃ kv 1}

noncomputable def CSD.Empirical.CSDBridge.KCBS.kcbsCross : Fin 3 → ℝ

The completing third leg: the cross product of the first adjacent pair.

Equations

• CSD.Empirical.CSDBridge.KCBS.kcbsCross = (crossProduct (CSD.Empirical.QM.KCBS.kv 0)) (CSD.Empirical.QM.KCBS.kv 1)

theorem CSD.Empirical.CSDBridge.KCBS.kv0_dot_kv0 : QM.KCBS.kv 0 ⬝ᵥ QM.KCBS.kv 0 = 1

The three dot-product facts of the frame, all sourced from the QM side or the cross-product API: unit legs, orthogonal pair, orthogonal completion, unit completion.

theorem CSD.Empirical.CSDBridge.KCBS.kv1_dot_kv1 : QM.KCBS.kv 1 ⬝ᵥ QM.KCBS.kv 1 = 1

theorem CSD.Empirical.CSDBridge.KCBS.kv0_dot_kv1 : QM.KCBS.kv 0 ⬝ᵥ QM.KCBS.kv 1 = 0

theorem CSD.Empirical.CSDBridge.KCBS.kv0_dot_cross : QM.KCBS.kv 0 ⬝ᵥ kcbsCross = 0

theorem CSD.Empirical.CSDBridge.KCBS.kv1_dot_cross : QM.KCBS.kv 1 ⬝ᵥ kcbsCross = 0

theorem CSD.Empirical.CSDBridge.KCBS.cross_dot_cross' : kcbsCross ⬝ᵥ kcbsCross = 1

noncomputable def CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec : Fin 3 → EuclideanSpace ℂ (Fin 3)

The representative KCBS context frame: the adjacent pair and its cross-product completion, complexified.

Equations

• CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec 0 = CSD.Empirical.CSDBridge.KCBS.c3 (CSD.Empirical.QM.KCBS.kv 0)
• CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec 1 = CSD.Empirical.CSDBridge.KCBS.c3 (CSD.Empirical.QM.KCBS.kv 1)
• CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec 2 = CSD.Empirical.CSDBridge.KCBS.c3 CSD.Empirical.CSDBridge.KCBS.kcbsCross

theorem CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec_orthonormal : Orthonormal ℂ kcbsCtxVec

The representative KCBS context is orthonormal — nine cases, each a transported real dot-product fact.

noncomputable def CSD.Empirical.CSDBridge.KCBS.kcbsContextBasis : OrthonormalBasis (Fin 3) ℂ (EuclideanSpace ℂ (Fin 3))

The representative KCBS context as a Mathlib OrthonormalBasis — the projective measurement frame fed to the engine.

Equations

• CSD.Empirical.CSDBridge.KCBS.kcbsContextBasis = OrthonormalBasis.mk CSD.Empirical.CSDBridge.KCBS.kcbsCtxVec_orthonormal CSD.Empirical.CSDBridge.KCBS.kcbsContextBasis._proof_1

theorem CSD.Empirical.CSDBridge.KCBS.kcbsContextBasis_apply (j : Fin 3) : kcbsContextBasis j = kcbsCtxVec j

The pentagon weight, transported

noncomputable def CSD.Empirical.CSDBridge.KCBS.apexC : EuclideanSpace ℂ (Fin 3)

The complexified apex preparation (0,0,1).

Equations

• CSD.Empirical.CSDBridge.KCBS.apexC = CSD.Empirical.CSDBridge.KCBS.c3 CSD.Empirical.QM.KCBS.apex

theorem CSD.Empirical.CSDBridge.KCBS.norm_apexC : ‖apexC‖ = 1

theorem CSD.Empirical.CSDBridge.KCBS.kcbs_pentagon_weight : ‖inner ℂ (kcbsContextBasis 0) apexC‖ ^ 2 = 1 / √5

The pentagon Born weight 1/√5, at the level of the frame. The apex overlap with the first pentagon ray, complexified: ‖⟨kcbsContextBasis 0, apexC⟩‖² = 1/√5 — the weight whose five-fold sum is the quantum KCBS value √5 (kcbs_qm_value).

The headline: KCBS context Born weights as ontic typicality measures

theorem CSD.Empirical.CSDBridge.KCBS.kcbs_context_born_frequency_volume (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.KSigma 3) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = RecordLayer.epistemicMeasure (Projectivization.mk ℂ (kcbsContextBasis.repr ψ) ⋯)) (hindep : ∀ (i : Fin 3), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 3) i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 3), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 3) i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (kcbsContextBasis i) ψ‖ ^ 2))

KCBS pentagon Born weights as Kähler volumes. For i.i.d. trials drawing microstates from the epistemic typicality measure on the fibred ontic Σ = ℂℙ² × T², the empirical frequencies of the three global basins (read at the rotated ray kcbsContextBasis.repr ψ) converge, on a single almost-sure event, to the context-dependent Born weights ‖⟨kcbsContextBasis i, ψ⟩‖² of measuring the unit preparation ψ in the representative pentagon context {kv 0, kv 1}.

At ψ = apexC, the ray-0 weight is the pentagon number 1/√5 (kcbs_pentagon_weight) — the quantity whose five-context sum √5 violates the noncontextual bound 2 (kcbs_quantum_violation). Each weight in that violation is an ontic typicality volume on the fixed Σ; the contextuality is which projective carving is measured, not a hidden variable. The other four pentagon contexts are identical instantiations (kv_orth certifies all five adjacencies).

theorem CSD.Empirical.CSDBridge.KCBS.kcbs_context_born_frequency_volume_canonical (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : MeasureTheory.iidSpace (LF4.KSigma 3)) ∂MeasureTheory.iidMeasure (RecordLayer.epistemicMeasure (Projectivization.mk ℂ (kcbsContextBasis.repr ψ) ⋯)), ∀ (i : Fin 3), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (MeasureTheory.iidTrial (LF4.KSigma 3) k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 3) i).indicator (fun (x : MeasureTheory.iidSpace (LF4.KSigma 3)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (kcbsContextBasis i) ψ‖ ^ 2))

kcbs_context_born_frequency_volume on the canonical i.i.d. Fubini–Study trial witness: the trial bundle is discharged, so the hypothesis set is Lean-inhabited, not merely classically satisfiable.