Documentation

CsdLean4.Empirical.CSD.Contextuality.KCBSVolume

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_volume, 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)

Instances For

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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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 FS typicality volumes #

theorem CSD.Empirical.CSDBridge.KCBS.kcbs_context_born_frequency_volume (p₀ : LF4.CPN 3) (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 3) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (i : Fin 3), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion (kcbsContextBasis.repr ψ) ⋯ i).indicator fun (x : Ω) => 1)) :

∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 3), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion (kcbsContextBasis.repr ψ) ⋯ 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 Fubini–Study typicality measure on the ontic Σ = ℂℙ², the empirical frequencies of the three barycentric Born regions (carved in the rotated frame 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 (p₀ : LF4.CPN 3) (ψ : EuclideanSpace ℂ (Fin 3)) (hψ : ‖ψ‖ = 1) :

∀ᵐ (ω : LF4.fsTrialSpace 3) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 3), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial 3 k ⁻¹' LF4.bornRegion (kcbsContextBasis.repr ψ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace 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.