Empirical/CSD: arbitrary projective measurement contexts as derived Kähler volumes #
Category: 3-Local (CSD-ontic layer; genuine volume derivation, not a transport tag, and not conditional on any preparation bundle).
The context-generic surfacing of LF4.born_frequency_convergence_N_uncond:
measuring a pure state ψ on ℂℙ^M in any orthonormal-basis (rank-1
projective) context B, the outcome Born weights ‖⟨B i, ψ⟩‖² are genuine
typicality measures on the ontic Σ. Carving-free,
Gleason-free, unconditional — every unit preparation, eigenstates of the
context included (no genericity hypothesis; hpos-free since the 2026-06-11
call-site migration onto LF4/BornRegionUncond.lean). In the spirit of
Empirical/CSD/BellVolume.lean, Empirical/CSD/GHZVolume.lean, and
Empirical/CSD/HardyVolume.lean, but parameterised over the context rather
than a fixed state.
⚠️ Two routes live here, on purpose #
Since CR-4 (2026-09-06) this module carries the context engine twice:
context_born_frequency_basin/block_born_frequency_basin— on the fibred arenaΣ = ℂℙ^M × T², withepistemicMeasure [B.repr ψ]and global basins. These are what every downstream consumer uses (KCBS, KS18, Mermin–Peres, Uncertainty).context_born_frequency_volume/block_born_frequency_volume— the original Fubini–Study statements on the baseΣ = ℂℙ^M, with global basins. They have no consumers, and that is deliberate:CSD.RecordLayer.globalBasin_toReal_eq_bornRegion_toRealis an equality between the two routes, so the base statements are what the fibred ones are compared against. Do not delete them as dead code.
The union-event restatement and the Z⊗Z witness at the bottom are on the fibred side.
The key reduction (no new geometry) #
Measuring ψ in the orthonormal context B is, coordinate-for-coordinate,
measuring the rotated coordinate vector B.repr ψ in the computational basis:
⟨B i, ψ⟩ = (B.repr ψ) i = ⟨eᵢ, B.repr ψ⟩ (OrthonormalBasis.repr_apply_apply
+ EuclideanSpace.inner_single_left)
so ‖⟨B i, ψ⟩‖² = ‖⟨eᵢ, B.repr ψ⟩‖². Since B.repr is a LinearIsometryEquiv,
‖B.repr ψ‖ = ‖ψ‖, so the rotated state inherits norm-one. Instantiating
born_frequency_convergence_N_uncond at B.repr ψ therefore lands exactly on
the context Born weights ‖⟨B i, ψ⟩‖², with the Born = ontic-volume content
(fs_born_volume_ratio_N_uncond / _apex_uncond) already discharged for the
rotated state — vanishing rotated amplitudes give FS-null cells, which is
the Born weight 0. No Busch, no carving.
Why this is the grounding for contextuality #
The Kochen–Specker / Mermin–Peres no-go statements (Empirical/QM/) turn on
the fact that the outcome weights a measurement assigns are context-dependent:
no single non-contextual hidden-variable assignment of 0/1 values to all rays
reproduces the quantum statistics across overlapping contexts. This file realises
each such context's rank-1 outcome weight as a genuine epistemic typicality
measure on the same ontic Σ = ℂℙ^M — the context enters only through which
orthonormal frame B carves the moment regions, not through any extra ontic
structure. The context-dependence the KS/MP theorems exploit is, on the CSD
ontology, the dependence of the carved volume regions on the measurement frame.
Honest scope #
No genericity hypothesis: the capstones cover every unit preparation ψ,
including eigenstates of the context (ψ = B i, the Kochen–Specker-interesting
boundary preparations) — resolving the earlier limitation, recorded at the
a9c3a50 landing, that ψ = B 0 failed the engine-inherited hpos. Zero-weight
outcome cells genuinely collapse to FS-null sets (BornRegionUncond per-cell
dichotomy); they are not redefined to hit Born values. The LHV / KS / MP
impossibility itself lives in Empirical/QM/ (KochenSpecker, MerminPeres).
Degenerate-eigenspace extension (rank-1 scope note closed) #
A degenerate projective measurement has outcome projectors Pₐ of rank ≥ 1.
Picking an orthonormal eigenbasis B adapted to the spectral decomposition and a
block labelling blk : Fin (M+1) → ι (the ι-many outcome labels), the outcome-a
projector is Pₐ = ∑_{blk i = a} |B i⟩⟨B i|, so the outcome Born weight is the
block sum of per-ray Born weights:
⟨ψ, Pₐ ψ⟩ = ∑_{blk i = a} ‖⟨B i, ψ⟩‖² (block_born_eq_blockSum)
a finite sum of epistemic typicality measures on the same ontic Σ = ℂℙ^M.
The block (degenerate-outcome) empirical frequency is the finite sum of the per-ray
frequencies (the per-ray barycentric regions are disjoint, so summing the
frequencies is the frequency of their union, the block outcome region), and it
converges to the block Born weight: block_born_frequency_volume. This closes the
rank-1 scope note above: degenerate contexts — including the two-qubit Mermin–Peres
rank-2 eigenspace observables and any other rank ≥ 1 projective context — are now
grounded as block sums of basin measures. block_born_eq_blockSum writes the block
Born weight via the explicit rank-1-sum projector image Pₐ ψ = ∑_{blk i = a} ⟨B i, ψ⟩ • B i; the equivalent reading is ∑_{blk i = a} ‖⟨B i, ψ⟩‖² = ‖orthogonalProjection (span {B i : blk i = a}) ψ‖² (Parseval over the orthonormal
sub-family), which is the standard "projection onto the eigenspace" statement.
Honest scope unchanged from the rank-1 case: this is a faithful realisation,
not a derivation (Φ = id, the FS regions carved in the rotated frame); the
contextuality / KS / MP no-go stays at the QM-validity layer (Empirical/QM/).
The context-rotation identity (step 1) #
Context ↔ rotated-state Born identity. The Born weight of outcome i when
measuring ψ in the orthonormal context B equals the i-th computational Born
weight of the rotated coordinate vector B.repr ψ. Pure inner-product geometry:
⟨B i, ψ⟩ = (B.repr ψ) i = ⟨eᵢ, B.repr ψ⟩ (OrthonormalBasis.repr_apply_apply
Rotated-state norm and genericity transport #
B.repr is a LinearIsometryEquiv, so the rotated state preserves the norm.
The rotated state is nonzero (it has norm one).
Genericity transports along the rotation: if every context Born weight is
strictly positive, so is every computational Born weight of B.repr ψ.
No longer consumed by the capstones below (they route through the hpos-free
born_frequency_convergence_N_uncond); retained for callers of the conditional
engine born_frequency_convergence_N.
The context volume-frequency capstone #
★★ Rotated-basis context frequencies on the fibred arena — the fibred twin of
context_born_frequency_volume (CR-4).
Same statement with the epistemic measure at [B.repr ψ] in place of fsMeasure p₀ and
global basins in place of rotated Born regions, so the base measure leaves the statement. Proof is
the base-side proof with globalBasin_born_frequency substituted; the rotation identity
context_born_eq_rotated after it is unchanged, being about the basis rather than the trial law.
This is the engine the contextuality entries (KCBS, KS18, Mermin–Peres) delegate to.
Any projective measurement context's outcome Born weights as derived Kähler
volumes. For i.i.d. trials drawing microstates from the Fubini–Study typicality
measure on the ontic Σ = ℂℙ^M, the empirical frequencies of the N = M+1
barycentric Born outcome regions (carved in the rotated frame B.repr ψ)
converge, on a single almost-sure event, to the context Born weights
‖⟨B i, ψ⟩‖² of measuring the norm-one preparation ψ in the orthonormal
context B.
Carving-free, Gleason-free, unconditional — no busch_effect_gleason, no carved
regions, no preparation bundle, no genericity hypothesis. The proof is the
rotation reduction: instantiate born_frequency_convergence_N_uncond at
B.repr ψ (norm one by repr_norm), then rewrite the computational Born
weights back to the context weights via context_born_eq_rotated.
This grounds every rank-1 projective measurement context at every unit
preparation — eigenstates of the context included (ψ = B i: the other rays'
cells are FS-null and their frequencies converge to 0) — the reusable
contextuality primitive (Kochen–Specker, the rank-1 Mermin–Peres parts): each
context-dependent outcome weight that a non-contextual hidden-variable assignment
cannot jointly reproduce is here a genuine Fubini–Study typicality volume on the
fixed ontic Σ. Honest scope: rank-1 (non-degenerate) contexts; degenerate
eigenspaces via block_born_frequency_volume (see the module docstring).
Degenerate-eigenspace blocks (step 1: the block Born weight) #
Degenerate-outcome Born weight = block sum of per-ray Born weights. For an
orthonormal eigenbasis B adapted to a block labelling blk, the rank-≥1
eigenspace projector for outcome a is Pₐ = ∑_{blk i = a} |B i⟩⟨B i|, so
Pₐ ψ = ∑_{blk i = a} ⟨B i, ψ⟩ • B i. Sandwiching against ψ (real part) gives the
block sum of per-ray Born weights ∑_{blk i = a} ‖⟨B i, ψ⟩‖², the outcome-a Born
weight ⟨ψ, Pₐ ψ⟩.
Delivered in the block-sum-direct form (the projector applied to ψ written as
its explicit rank-1 sum), not the orthogonalProjection-over-subfamily-span form:
the latter requires constructing an orthonormal basis of the span submodule from the
sub-family of B, which is span-of-subfamily friction in Mathlib with no payoff here.
The equivalent projector reading is
∑_{blk i = a} ‖⟨B i, ψ⟩‖² = ‖orthogonalProjection (span ℂ {B i : blk i = a}) ψ‖²
(Parseval over the orthonormal sub-family). Proof: inner_sum + inner_smul_right +
inner_conj_symm + RCLike.mul_conj, termwise.
The degenerate-context block volume-frequency capstone (step 2) #
★ Degenerate-block frequencies on the fibred arena — the fibred twin of
block_born_frequency_volume (CR-4). Sums the per-outcome basin frequencies over a degeneracy
block; the Mermin–Peres square's eight observables all delegate to this.
Degenerate projective measurement context's block (eigenspace) Born weight as a
derived sum of Kähler volumes. For i.i.d. trials drawing microstates from the
Fubini–Study typicality measure on the ontic Σ = ℂℙ^M, the empirical frequency of
the degenerate outcome a — the finite sum of the per-ray empirical frequencies
over the block {i : blk i = a} — converges, on a single almost-sure event, to the block
Born weight ∑_{blk i = a} ‖⟨B i, ψ⟩‖² = ⟨ψ, Pₐ ψ⟩ (see block_born_eq_blockSum).
(This sum-of-per-ray-frequencies equals the frequency of the union of the block's
barycentric per-ray regions, because those regions are pairwise disjoint — the
barycentric subdivision is a genuine partition, now formalised as
CSD.LF4.bornRegion_pairwiseDisjoint (LF5-F engine half). The union-event
restatement is block_born_frequency_volume_event below, stated on the fibred arena; the sum
form proved here needs only additivity of limits.)
Carving-free, Gleason-free, unconditional — no genericity hypothesis (every unit
preparation, eigenvectors of any block included).
Proof: take the single a.s. event from context_born_frequency_volume (which gives
every ray i's convergence simultaneously) and sum the block's per-ray
convergences via tendsto_finsetSum. The per-ray frequency summand is verbatim the
conclusion of context_born_frequency_volume, so the per-ray limits feed in directly.
This closes the rank-1 scope note of context_born_frequency_volume: degenerate-
eigenspace contexts (the two-qubit Mermin–Peres rank-2 observables and any rank ≥ 1
projective context) are grounded as block sums of FS typicality volumes on the fixed
ontic Σ. Honest scope unchanged: realisation not derivation (Φ = id, FS regions
carved in the rotated frame); the KS / MP no-go stays at the QM-validity layer.
The union-event restatement (the owed aeece86 form) #
Degenerate-outcome block frequency, as the frequency of a single union
event. The aeece86-owed restatement of block_born_frequency_basin: the empirical
frequency of the degenerate outcome a, on the fibred arena, stated as the frequency of the
single union event ⋃_{blk i = a} globalBasin … (the eigenspace outcome region),
converging to the block Born weight ∑_{blk i = a} ‖⟨B i, ψ⟩‖². The union form is available
because the per-outcome basins are pairwise disjoint
(CSD.RecordLayer.globalBasin_pairwiseDisjoint), so the indicator of the union equals the sum
of the per-outcome indicators (CSD.LF4.indicator_iUnion_disjoint). The sum form
(block_born_frequency_basin) is untouched.
Concrete degenerate (rank-2) witness: the two-qubit parity Z⊗Z #
Concrete degenerate (rank-2) witness: the two-qubit parity observable Z⊗Z.
The parity / Z⊗Z outcome Born weight realised as a block sum of epistemic
typicality measures — the Mermin–Peres rank-2 observable case made explicit.
Z⊗Z on EuclideanSpace ℂ (Fin 4) has eigenvalues ±1, each eigenspace of
rank 2; its eigenbasis is the computational basis (no rotation needed), so we
take B := EuclideanSpace.basisFun (Fin 4) ℂ (whose i-th vector is
EuclideanSpace.single i 1, EuclideanSpace.basisFun_apply). The block labelling
blk = ![0,1,1,0] : Fin 4 → Fin 2 is the parity grouping of the two-qubit strings:
indices {0,3} (|00⟩, |11⟩, even parity, eigenvalue +1) ↦ outcome 0; indices
{1,2} (|01⟩, |10⟩, odd parity, eigenvalue −1) ↦ outcome 1.
Instantiating block_born_frequency_basin at B, blk, a = 0 and collapsing the
even-parity block {0,3} (Finset.sum_pair, decide on the filter), the empirical
frequency of the even-parity (Z⊗Z = +1) outcome converges almost surely to the
Z⊗Z = +1 Born weight ‖⟨e₀, ψ⟩‖² + ‖⟨e₃, ψ⟩‖² = ⟨ψ, P₊ ψ⟩, a block sum of two
epistemic typicality measures on the fibred ontic Σ = ℂℙ³ × T². Carving-free, Gleason-free,
foundational-triple-only.
Honest scope unchanged from the generic degenerate case (block_born_frequency_basin):
this is a faithful realisation of the rank-2 outcome weight as a sum of ontic
volumes, not a derivation (Φ = id, the basins read at the computational ray);
the Mermin–Peres / Kochen–Specker no-go itself stays at the QM-validity layer
(Empirical/QM/). No genericity hypothesis: every unit two-qubit preparation is
covered, the computational eigenstates |00⟩, |01⟩, |10⟩, |11⟩ (and the Bell
states with vanishing components) included.