Documentation

CsdLean4.LF4.POVMVolume

LF4: POVM Born weight as a dilated rank-1 block sum (P.3a) #

Category: 3-Local (LF4 POVM volume reading).

This is P.3a of the POVM tranche (specs/povm-plan.md): the block decomposition that turns the Naimark Born transfer (born_transfer, P.2) into a sum of dilated computational-basis (rank-1) Born weights:

pᵢ(ψ)  =  ⟨ψ, Eᵢ ψ⟩  =  ⟨Vψ, Πᵢ (Vψ)⟩  =  ∑ₙ ‖⟨e_{(n,i)}, Vψ⟩‖².

The ancilla-i projector Πᵢ = I_N ⊗ |i⟩⟨i| is a coarse (rank-N) outcome — the union of the N computational-basis cells {(n, i) : n} on the dilated space. So the POVM weight is the sum, over that block, of the dilated rank-1 Born weights, each of which the achieved general-N result reads as a Fubini–Study volume on ℂℙ^{N·|ι|−1} (the FS-volume identification, P.3b, sits on top of this via the Fin N × ι ≃ Fin (N·|ι|) reindex).

The reindex isometry preserves computational-basis Born weights. For the piLpCongrLeft e reindex isometry L, ‖⟨e_{e p}, L w⟩‖² = ‖⟨e_p, w⟩‖² — the cell p maps to the coordinate e p with the Born weight unchanged.

theorem CSD.LF4.normSq_inner_single {N : } {ι : Type u_1} [Fintype ι] [DecidableEq ι] (w : EuclideanSpace (Fin N × ι)) (p : Fin N × ι) :

‖⟨e_p, w⟩‖² = ‖w_p‖² on the dilated EuclideanSpace ℂ (Fin N × ι).

theorem CSD.LF4.blockProj_born_eq_block_sum {N : } {ι : Type u_1} [Fintype ι] [DecidableEq ι] (i : ι) (w : EuclideanSpace (Fin N × ι)) :

Block decomposition. The projective Born weight of w against the ancilla-i projector is the sum of the rank-1 computational-basis Born weights over the i-th block: re ⟨w, Πᵢ w⟩ = ∑ₙ ‖⟨e_{(n,i)}, w⟩‖².

theorem CSD.LF4.povm_born_eq_block_sum {N : } {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace (Fin N)) (i : ι) :

POVM Born weight as a dilated rank-1 block sum (P.3a). Composing the Naimark Born transfer with the block decomposition: the POVM weight pᵢ(ψ) is the sum, over the i-th ancilla block {(n, i) : n}, of the dilated computational-basis Born weights of . Each summand is a rank-1 projective Born weight on ℂℙ^{N·|ι|−1}, read as a Fubini–Study volume by the achieved general-N result (P.3b).

theorem CSD.LF4.povm_born_eq_dilated_volume {N : } {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : } (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace (Fin N)) (i : ι) (e : Fin N × ι Fin (M + 1)) (p₀ : CPN (M + 1)) (hnorm : (LinearIsometryEquiv.piLpCongrLeft 2 e) ((Matrix.toEuclideanLin D.V) ψ) = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < inner (EuclideanSpace.single j 1) ((LinearIsometryEquiv.piLpCongrLeft 2 e) ((Matrix.toEuclideanLin D.V) ψ)) ^ 2) :

POVM Born weight as a sum of Fubini–Study volumes (P.3b). Given a reindex e : Fin N × ι ≃ Fin (M+1) of the dilated index (concretely finProdFinEquiv after ι ≃ Fin |ι|, so N·|ι| = M+1) and the induced reindex isometry L = piLpCongrLeft e, write ψ' = L (Vψ) for the reindexed dilated state on ℂℙ^M. When ψ' is a unit, fully-generic preparation (all M+1 amplitudes nonzero — the dilation genericity condition), the POVM Born weight is the sum, over the i-th ancilla block, of the genuine Fubini–Study typicality volumes of the dilated barycentric cells:

pᵢ(ψ)  =  ∑ₙ  μ_FS( bornRegion ψ' (e (n, i)) ).

This is the headline of the ontic POVM reading: the (non-projective) POVM Born weight is a Kähler volume on the dilated configuration space Σ' = ℂℙ^{N·|ι|−1}, carving-free and Gleason-free — it composes the Naimark Born transfer with the achieved general-N Born = FS-volume result (bornRegion_fs_measure), no busch_effect_gleason. Honest scope: the dilation V is supplied (P.2), so this relocates POVM Born onto a larger posited configuration space (system + ancilla); genericity (hpos) excludes dilated states with a vanishing amplitude. An hpos-free form is available: povm_born_eq_dilated_volume_uncond (BornRegionUncond.lean).

theorem CSD.LF4.povm_born_frequency_volume {N : } {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : } (P : LF2.POVM N ι) (D : NaimarkDilation P) (ψ : EuclideanSpace (Fin N)) (e : Fin N × ι Fin (M + 1)) (ψ' : EuclideanSpace (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 e) ((Matrix.toEuclideanLin D.V) ψ)) (hψ'0 : ψ' 0) (hnorm : ψ' = 1) (hpos : ∀ (j : Fin (M + 1)), 0 < inner (EuclideanSpace.single j 1) ψ' ^ 2) (p₀ : CPN (M + 1)) {Ω : Type u_2} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ΩCPN (M + 1)) (hX : ∀ (n : ), Measurable (X n)) (hlaw : ∀ (n : ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω) => ProbabilityTheory.IndepFun f g Pr) fun (n : ) => (X n ⁻¹' bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) :
∀ᵐ (ω : Ω) Pr, ∀ (i : ι), Filter.Tendsto (fun (m : ) => n : Fin N, (∑ kFinset.range m, (X k ⁻¹' bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / m) Filter.atTop (nhds (P.weight ψ i))

POVM empirical frequencies as a dilated Kähler-volume convergence (P.4). The observable capstone. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on the dilated ontic Σ' = ℂℙ^{N·|ι|−1} (the reindexed dilated state ψ' = L (Vψ) being a unit, fully-generic preparation), the empirical frequency of the i-th POVM outcome — the sum, over the i-th ancilla block, of the dilated barycentric-cell frequencies — converges, on a single almost-sure event, to the POVM Born weight pᵢ(ψ).

Composes the general-N per-cell convergence born_frequency_convergence_N (joint a.s. over all M+1 cells) with the finite block sum (tendsto_finsetSum), landing the limit on pᵢ(ψ) via the P.3a block decomposition. Carving-free, Gleason-free — the empirical → Born chain for a general (non-projective) POVM runs entirely on the ontic FS-volume derivation, no busch_effect_gleason. Honest scope: dilation supplied; the block frequency is the sum of the cells' frequencies (the cells are the rank-1 dilated outcomes), and genericity (hpos) is assumed. An hpos-free form is available: povm_born_frequency_volume_uncond (BornRegionUncond.lean).