LF4 §14: observable correspondence for general self-adjoint observables (general N) #
Category: 3-Local (LF4 §14 discharge — the general-N, all-eigenvalue observable correspondence for arbitrary self-adjoint observables).
This module discharges the §14 observable-correspondence obligation for every finite-dimensional
self-adjoint observable on Σ = ℂℙ^{N-1}, at general N and for every real eigenvalue
vector — the general lift of LF4/SingleQubitKahler.lean's single-qubit projector result
sg_observable_correspondence. It is built in two layers: first for observables diagonal in the
reference basis, then for arbitrary self-adjoint observables via spectral unitary transport
of the state.
What §14 means, and what is discharged here #
The §14 obligation (see BRIDGE-OBLIGATIONS.md, LF4-todo §14) asks that each self-adjoint
Hilbert observable arise as the lift of a measurable Σ-valued function whose Σ-average is
the Hilbert expectation. For a diagonal observable this is delivered here:
diag_expectation— the Hilbert side:⟨ψ, diagonal(lam·) ψ⟩ = ∑ₖ lam k · ‖⟨e_k, ψ⟩‖²(spectral expansion + the standard-basis Born weights).fsMeasure_bornRegionN— the ontic side: the Fubini–Study volume of the moment-sublevel regionbornRegionN ψ konΣequals the Born weight‖⟨e_k, ψ⟩‖², for every basis indexk : Fin N. This unifiesfs_born_volume_ratio_N(free coordinates) andfs_born_volume_ratio_N_apex(the apex coordinate) viaFin.lastCases.observable_correspondence_diagonal— the pointwise-volume form:⟨ψ, diagonal(lam·) ψ⟩ = ∑ₖ lam k · vol(bornRegionN ψ k), i.e. the expectation is the eigenvalue-weighted sum of the ontic Born-region volumes.observable_correspondence_diagonal_integral— the canonical integral form⟨ψ, diagonal(lam·) ψ⟩ = ∫ A_ontic dμ_FS, withA_ontic = ∑ₖ lam k · 𝟙_{Rₖ}(aOntic) an explicit measurableΣ-function (bornRegionN_measurableSet), and the integral evaluated by finite additivity over the eigenvalue-weighted region indicators.hermitian_observable_correspondence/_integral— the general (non-diagonal) case: for any HermitianA = U·diag(λ)·Uᴴ(spectral theorem,U = eigenvectorUnitary),⟨ψ, A ψ⟩ = ∑ₖ λₖ · vol(bornRegionN φ k) = ∫ aOntic φ λ dμ_FS, whereφ = Uᴴ ψis the state transported by the spectral unitary. The unitary covariance is nothing more than that state transport (hermitian_expectation_transport+ the isometrytransport_norm).pure_state_born_prob_eq_volume— the §14 states obligation for pure states / rank-one projectors:‖⟨Φ, ψ⟩‖² = vol(bornRegionN (Wᴴ ψ) 0), the Born probability of the pure outcome|Φ⟩(= expectation of the projector|Φ⟩⟨Φ|) as a single ontic Fubini–Study volume, using a unitaryWwithW e₀ = Φ(exists_unitary_e_zero_eq). This realises pure states / rank-one projectors as ontic objects — the state-side content underlying the resource bundles (Bell-state projectors, teleportation input state).
Scope (honest) #
All finite-dimensional self-adjoint observables are now covered. For the diagonal case the ontic
regions realise the standard-basis projectors |e_k⟩⟨e_k|; the general case handles an arbitrary
eigenbasis by transporting the state through the spectral unitary (φ = Uᴴ ψ), so the same Born
regions of φ do the work — no separate §13 Σ-flow machinery is needed. The genericity
hypothesis hpos (no vanishing amplitude of the relevant state — for the general case, ψ has
nonzero overlap with every eigenvector of A) is the same one carried by fs_born_volume_ratio_N
(it makes each barycentric region a homeomorphic image of the open simplex). This module builds
axiom-free (foundational triple), carving-free, Gleason-free.
References: LF4/MomentBornN.lean (fs_born_volume_ratio_N, fs_born_volume_ratio_N_apex,
ratioN, momentMap, replaceMap, apexLin, openSimplexFree); LF4/SingleQubitKahler.lean
(sg_observable_correspondence, the single-qubit projector precursor); specs/LF4-todo.md §14;
specs/future-work.md; BRIDGE-OBLIGATIONS.md (the §14 bundle fields).
The Hilbert side of §14 for a diagonal observable. For a real eigenvalue vector lam
and any ψ, the expectation of the diagonal matrix diagonal (lam ·) in the state ψ is the
lam-weighted sum of the coordinate Born weights ‖⟨e_k, ψ⟩‖².
The free Born vector of ψ (the moment-ratio coordinates of [ψ]).
Equations
- CSD.LF4.bornVecN ψ hψ0 = CSD.LF4.ratioN fun (j : Fin (M + 1)) => CSD.LF4.momentMap (Projectivization.mk ℂ ψ hψ0) j
Instances For
The per-basis-index simplex Born region: the free replaceMap image for a castSucc
coordinate, the affine apex image for the last coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ontic Born region on Σ = ℂℙ^{N-1} for basis index k: the moment-ratio preimage of
bornSimplexRegion. Its Fubini–Study measure is the Born weight ‖⟨e_k, ψ⟩‖²
(fsMeasure_bornRegionN).
Equations
- CSD.LF4.bornRegionN ψ hψ0 k = (fun (p : CSD.LF4.CPN (M + 1)) => CSD.LF4.ratioN fun (j : Fin (M + 1)) => CSD.LF4.momentMap p j) ⁻¹' CSD.LF4.bornSimplexRegion (CSD.LF4.bornVecN ψ hψ0) k
Instances For
The ontic side of §14 for basis projectors (general N). The Fubini–Study measure of the
Born region for basis index k is exactly the Born weight ‖⟨e_k, ψ⟩‖². Unifies
fs_born_volume_ratio_N (free coordinates) and fs_born_volume_ratio_N_apex (apex) via
Fin.lastCases.
§14 observable correspondence for a diagonal observable (general N). The Hilbert
expectation of the diagonal self-adjoint observable A = diagonal (lam ·) in the state ψ is the
eigenvalue-weighted sum of the Fubini–Study volumes of the ontic Born regions:
⟨ψ, A ψ⟩ = ∑ₖ lam k · vol(Rₖ), where Rₖ = bornRegionN ψ k is the moment-sublevel region on
Σ = ℂℙ^{N-1} whose volume is the Born weight ‖⟨e_k, ψ⟩‖². This realises each diagonal
observable as (the average over Σ of) the eigenvalue-weighted indicator sum ∑ₖ lam k · 𝟙_{Rₖ} —
the general-N, all-eigenvalue analogue of the single-qubit sg_observable_correspondence.
Foundational triple; carving-free, Gleason-free.
The integral form: A_ontic as an explicit measurable Σ-function #
Each ontic Born region is measurable (an open-image moment-ratio preimage; the moment map is
measurable and each simplex Born region is an open set, being the image of the open simplex under a
determinant-≠ 0 affine map).
The ontic observable realising a diagonal Hilbert observable: the eigenvalue-weighted sum
of the Born-region indicators, A_ontic = ∑ₖ lam k · 𝟙_{Rₖ} — a measurable simple function on
Σ = ℂℙ^{N-1}.
Equations
- CSD.LF4.aOntic ψ hψ0 lam p = ∑ k : Fin (M + 1), lam k * (CSD.LF4.bornRegionN ψ hψ0 k).indicator 1 p
Instances For
The Σ-average of A_ontic is the weighted Born-volume sum (finite additivity of the
integral over the eigenvalue-weighted indicators, each integrable since μ_FS is a probability
measure and each region is measurable).
§14 observable correspondence, integral form (general N, diagonal observables). The
Hilbert expectation of the diagonal observable diagonal (lam ·) equals the Fubini–Study
Σ-average of the ontic observable A_ontic = ∑ₖ lam k · 𝟙_{Rₖ}. This is the canonical §14
statement — ⟨ψ, A ψ⟩ = ∫ A_ontic dμ_FS, with A_ontic an explicit measurable Σ-function —
of which observable_correspondence_diagonal is the pointwise-volume form. Foundational triple.
Non-diagonal (general self-adjoint) observables, via spectral unitary transport #
Expectation transport under the spectral unitary. For a Hermitian A, its Hilbert
expectation in ψ equals the diagonal expectation of its eigenvalues in the transported state
φ = Uᴴ ψ (U = eigenvectorUnitary).
§14 observable correspondence for a general (self-adjoint) observable, general N. For a
Hermitian matrix A, the Hilbert expectation ⟨ψ, A ψ⟩ equals the eigenvalue-weighted sum of the
Fubini–Study volumes of the ontic Born regions of the transported state φ = Uᴴ ψ
(U = eigenvectorUnitary): ⟨ψ, A ψ⟩ = ∑ₖ (eigenvalues k) · vol(bornRegionN φ k). The unitary
covariance is exactly the state transport ψ ↦ Uᴴ ψ; the genericity hpos is on φ (i.e. ψ
has nonzero overlap with every eigenvector of A). Foundational triple.
§14, general self-adjoint observable, integral form. ⟨ψ, A ψ⟩ = ∫ A_ontic dμ_FS, with
A_ontic = aOntic φ (eigenvalues) the ontic observable of the transported state φ = Uᴴ ψ.
§14 states obligation: pure states / rank-one projectors as ontic volumes #
Unitary inner-adjoint. ⟨W x, y⟩ = ⟨x, Wᴴ y⟩ for a unitary W (matrix action).
The transport Wᴴ ψ preserves the norm: ‖Wᴴ ψ‖ = ‖ψ‖.
§14 states obligation — the pure-state / rank-one-projector case. The Born probability
‖⟨Φ, ψ⟩‖² of the pure outcome |Φ⟩ (equivalently the expectation of the rank-one projector
|Φ⟩⟨Φ| in ψ) is realised as a single ontic Fubini–Study volume: the volume of the Born
region (index 0) of the state φ = Wᴴ ψ transported by any unitary W sending e₀ ↦ Φ.
Genericity hpos is on φ. This realises pure states / rank-one projectors as ontic objects —
the §14 states content underlying the resource bundles (Bell-state projectors, teleportation
input state). Foundational triple.