Empirical/CSD: Kochen-Specker (Cabello-18) contextual Born weights as Kähler volumes

Category: 3-Local (CSD-ontic volume reading; a quick-win instantiation of the already-proved context-generic engine CSD.Empirical.CSDBridge.ContextVolume.context_born_frequency_volume).

This is the volume-ratio companion to the impossibility readings of the Kochen-Specker theorem:

• QM side (Empirical/QM/Contextuality/KS18.lean): the Cabello-Estebaranz-García-Alcaine 1996 18-ray / 9-basis data, pairwise orthogonality cabello_pairwise_orthogonal_in_basis, and the no-go ks_no_value_assignment_cabello18 / no_value_assignment_18_9.
• CSD impossibility side (Empirical/CSD/Contextuality/KS18.lean): no_csd_ks_assignment_bundle — no non-contextual ontic-outcome partition discipline is satisfiable.

The two halves of the KS story, told honestly:

1. Each Cabello context carries genuine Born weights as FS typicality volumes. Taking a representative context (basis 0, the rays {v0, v1, v2, v3}), the four un-normalised real Cabello rays are complexified (cabelloVecC) and normalised (ksCtxVec) into a genuine OrthonormalBasis (Fin 4) ℂ (EuclideanSpace ℂ (Fin 4)) (ksContextBasis). Orthonormality is not re-proved: the off-diagonal inner products are pulled from the QM-side cabello_pairwise_orthogonal_in_basis through the complexification transport cabelloVecC_inner (⟨cabelloVecC i, cabelloVecC j⟩_ℂ = ↑⟨cabelloVec i, cabelloVec j⟩_ℝ). Instantiating the engine context_born_frequency_volume at this basis, every ray's context-dependent Born weight ‖⟨ksContextBasis i, ψ⟩‖² is the almost-sure limit of empirical frequencies of the barycentric Born region bornRegion on the fixed ontic Σ = ℂℙ³ — a Fubini-Study typicality volume (ks18_context_born_frequency_volume).
2. Yet no single non-contextual value assignment reproduces all 9 contexts jointly (ks_no_value_assignment_cabello18, the combinatorial 9 = 2k impossibility).

The CSD reading of contextuality. The context-dependence the KS theorem exploits is, on the CSD ontology, which projective carving of the one ontic Σ is measured — not a hidden variable. Each context's outcome weights are typicality volumes on the same Σ = ℂℙ³, recomputed per measurement frame B (which orthonormal frame carves the moment regions). There is no global 0/1 labelling of all 18 rays consistent across the overlapping contexts, because no global section of the carved-volume assignment exists — exactly the combinatorial no-go, now sitting beside a genuine per-context volume realisation.

Scope and honesty

• Rank-1. The Cabello rays are rank-1, matching context_born_frequency_volume's rank-1 scope (degenerate eigenspaces would route through block_born_frequency_volume).
• One representative context built. Basis 0 is built explicitly; the other 8 Cabello contexts (cabelloBasis 1 … 8) are identical instantiations of the same engine at the corresponding orthonormal frame — the only per-context input is the 4-ray orthogonal tuple, already certified for all 9 bases by cabello_pairwise_orthogonal_in_basis. No new mathematics; building all 9 is mechanical repetition and is omitted.
• Realisation, not derivation. As for the whole Empirical/CSD/*Volume series and the engine it specialises: the Born = FS-volume identity is derived one layer down (the Duistermaat-Heckman / moment-map cluster, LF4.born_frequency_convergence_N_uncond, Gleason-free, no Born put in) and imported here; Φ = id (no dynamics exercised). The KS no-go itself stays at the QM-validity layer (Empirical/QM/).
• Gleason-free, foundational-triple-only. The engine is busch_effect_gleason-free; this instantiation inherits that.

Complexification of the Cabello rays and the inner-product transport

noncomputable def CSD.Empirical.CSDBridge.KochenSpecker.cabelloVecC (i : Fin 18) : EuclideanSpace ℂ (Fin 4)

The complexification ℝ⁴ → ℂ⁴ of the i-th un-normalised Cabello ray (componentwise real-to-complex coercion).

Equations

• CSD.Empirical.CSDBridge.KochenSpecker.cabelloVecC i = WithLp.toLp 2 fun (k : Fin 4) => ↑(CSD.Empirical.KochenSpecker.cabelloMat i k)

theorem CSD.Empirical.CSDBridge.KochenSpecker.real_scalar_inner (a b : ℝ) : inner ℝ a b = a * b

Scalar real inner product on ℝ (the RCLike.toInnerProductSpaceReal instance produced by PiLp.inner_apply on a real EuclideanSpace): ⟨a, b⟩_ℝ = a * b.

theorem CSD.Empirical.CSDBridge.KochenSpecker.cplx_scalar_inner (a b : ℝ) : inner ℂ ↑a ↑b = ↑(a * b)

Scalar complex inner product of two real coercions: ⟨↑a, ↑b⟩_ℂ = ↑(a * b).

theorem CSD.Empirical.CSDBridge.KochenSpecker.cabelloVecC_inner (i j : Fin 18) : inner ℂ (cabelloVecC i) (cabelloVecC j) = ↑(inner ℝ (KochenSpecker.cabelloVec i) (KochenSpecker.cabelloVec j))

Complexification transport. The complex inner product of two complexified Cabello rays is the real-to-complex coercion of their real inner product: ⟨cabelloVecC i, cabelloVecC j⟩_ℂ = ↑⟨cabelloVec i, cabelloVec j⟩_ℝ. This is the bridge that lets the QM-side orthogonality cabello_pairwise_orthogonal_in_basis (stated in ℝ⁴) feed the complex orthonormality below without re-proving any inner-product computation.

The representative context (basis 0) as an OrthonormalBasis

def CSD.Empirical.CSDBridge.KochenSpecker.ksRayIdx : Fin 4 → Fin 18

The four ray indices of the representative Cabello context cabelloBasis 0 = {0,1,2,3}.

Equations

• CSD.Empirical.CSDBridge.KochenSpecker.ksRayIdx = ![0, 1, 2, 3]

theorem CSD.Empirical.CSDBridge.KochenSpecker.cabelloVecC_normSq (i : Fin 18) : ‖cabelloVecC i‖ ^ 2 = inner ℝ (KochenSpecker.cabelloVec i) (KochenSpecker.cabelloVec i)

‖cabelloVecC i‖² = ⟨cabelloVec i, cabelloVec i⟩_ℝ (the complexification preserves the squared norm), via cabelloVecC_inner at i = j and inner_self_eq_norm_sq_to_K.

theorem CSD.Empirical.CSDBridge.KochenSpecker.cabelloVecC_ne_zero (j : Fin 4) : cabelloVecC (ksRayIdx j) ≠ 0

The four complexified rays of the representative context are nonzero (their squared norms 1, 1, 2, 2 are positive).

noncomputable def CSD.Empirical.CSDBridge.KochenSpecker.ksCtxVec (j : Fin 4) : EuclideanSpace ℂ (Fin 4)

The normalised complexified rays of the representative context.

Equations

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

theorem CSD.Empirical.CSDBridge.KochenSpecker.norm_ksCtxVec (j : Fin 4) : ‖ksCtxVec j‖ = 1

Each normalised context ray has norm one.

theorem CSD.Empirical.CSDBridge.KochenSpecker.ksCtxVec_orthonormal : Orthonormal ℂ ksCtxVec

The representative Cabello context is orthonormal. Diagonal from norm_ksCtxVec; off-diagonal from the QM-side cabello_pairwise_orthogonal_in_basis (basis 0) transported through cabelloVecC_inner — no orthogonality is re-proved.

noncomputable def CSD.Empirical.CSDBridge.KochenSpecker.ksContextBasis : OrthonormalBasis (Fin 4) ℂ (EuclideanSpace ℂ (Fin 4))

The representative Cabello context as a Mathlib OrthonormalBasis. A 4-element orthonormal family in the 4-dimensional EuclideanSpace ℂ (Fin 4) spans (cardinality = finrank), so OrthonormalBasis.mk applies. This is the projective measurement frame fed to the engine context_born_frequency_volume.

Equations

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

theorem CSD.Empirical.CSDBridge.KochenSpecker.ksContextBasis_apply (j : Fin 4) : ksContextBasis j = ksCtxVec j

ksContextBasis i is the i-th normalised Cabello ray.

The headline: Cabello-context Born weights as FS typicality volumes

theorem CSD.Empirical.CSDBridge.KochenSpecker.ks18_context_born_frequency_volume (p₀ : LF4.CPN 4) (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ‖ψ‖ = 1) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 4) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (i : Fin 4), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion (ksContextBasis.repr ψ) ⋯ i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion (ksContextBasis.repr ψ) ⋯ i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (ksContextBasis i) ψ‖ ^ 2))

Kochen-Specker (Cabello-18) contextual 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 four barycentric Born regions (carved in the rotated frame ksContextBasis.repr ψ) converge, on a single almost-sure event, to the context-dependent Born weights ‖⟨ksContextBasis i, ψ⟩‖² of measuring the unit preparation ψ in the representative Cabello context cabelloBasis 0.

A direct instantiation of context_born_frequency_volume at M = 3, the representative Cabello orthonormal frame ksContextBasis, and an arbitrary unit ψ — carving-free, Gleason-free, unconditional (every unit preparation, eigenstates of the context included), no new mathematics. The other 8 Cabello contexts (cabelloBasis 1 … 8) are identical instantiations at their orthonormal frames; their per-context orthogonality is already certified by cabello_pairwise_orthogonal_in_basis.

This grounds each Cabello context's rank-1 outcome weight — the context-dependent weights that no non-contextual hidden-variable assignment can jointly reproduce (ks_no_value_assignment_cabello18) — as a genuine Fubini-Study typicality volume on the fixed ontic Σ. The CSD reading of contextuality: context-dependence is which projective carving of the one Σ is measured, not a hidden variable.

theorem CSD.Empirical.CSDBridge.KochenSpecker.ks18_context_born_frequency_volume_canonical (p₀ : LF4.CPN 4) (ψ : EuclideanSpace ℂ (Fin 4)) (hψ : ‖ψ‖ = 1) : ∀ᵐ (ω : LF4.fsTrialSpace 4) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial 4 k ⁻¹' LF4.bornRegion (ksContextBasis.repr ψ) ⋯ i).indicator (fun (x : LF4.fsTrialSpace 4) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (ksContextBasis i) ψ‖ ^ 2))

ks18_context_born_frequency_volume on the canonical i.i.d. Fubini-Study trial witness (fsTrialMeasure / fsTrial): the trial bundle is discharged, so the hypothesis set is Lean-inhabited, not merely classically satisfiable. Direct instantiation of context_born_frequency_volume_canonical.