Empirical/CSD: weak / unsharp measurement as a partial volume nudge (Build 15c)

Category: 3-Local (CSD-ontic volume layer; the unsharp-POVM / continuous-strength entry of the open-system tranche, after einselection (15a) and QEC-decoherence (15b)).

A weak (unsharp) measurement of strength η ∈ [0,1] is the one-parameter qubit POVM interpolating the sharp σ_z measurement (η = 1) and no measurement at all (η = 0):

weakEffectPlus  η = (1/2) (I + η σ_z),   weakEffectMinus η = (1/2) (I − η σ_z),

with σ_z = !![1,0;0,-1]. The two effects are PSD with eigenvalues (1±η)/2 ∈ [0,1] and sum to I, so {weakEffectPlus η, weakEffectMinus η} is a genuine (non-projective for 0 < η < 1) POVM weakPOVM η.

The interpolation (the genuine content)

The plus-outcome Born weight on a unit preparation ψ is

⟨ψ, weakEffectPlus η ψ⟩ = (1 + η (‖ψ₀‖² − ‖ψ₁‖²)) / 2 = (1 + η ⟨ψ, σ_z ψ⟩) / 2,

(weak_born_weight_plus, weak_born_weight_plus_unit), so the information content (the deviation of the weight from 1/2) scales linearly with η:

• η = 0 (no measurement): weakEffectPlus 0 = (1/2) I, weight = 1/2 for every ψ — no information and (the maximally unsharp, trivial POVM, connecting to 15a's degenerate scalar·I, no basis distinguished);
• η = 1 (projective): weakEffectPlus 1 = |0⟩⟨0| the sharp σ_z-projector, weight = ‖ψ₀‖² = ‖⟨e₀, ψ⟩‖² the full Born weight (the sharp carve).

weak_born_unsharp_interpolation states both endpoints; weak_partial_information_witness exhibits an intermediate η = 1/2 weight 3/4 strictly between the trivial 1/2 and the sharp Born weight 1 (genuine partial information).

The CSD volume reading (the "nudge")

Run weakPOVM η through the POVM tranche: canonicalNaimark is its Naimark dilation, and povm_born_frequency_volume_uncond reads the weak-outcome Born weight as a sum of Fubini–Study volumes on the dilated ontic Σ' = ℂℙ³ — carving-free, Gleason-free, unconditional (weak_born_frequency_volume). The honest reading: the weak measurement is a partial volume nudge — at η = 0 the dilated volumes are the trivial 1/2 split (no nudge), at η = 1 the full projective carve, intermediate η a partial nudge of the Σ-volume.

Honest scope: static / operational vs continuous dynamics

This is the static / operational weak measurement: the unsharp POVM, its Born weights, and the volume reading. The continuous measurement — repeated weak measurements as a dynamical flow, measurement-strength-as-time, weak-value back-action as a Σ-flow — is the dynamics question, gated to D1 / the entangled tier (LF6) and NOT claimed here. The "nudge vs carve" is the operational / volume reading; the ontic flow that realises the nudge is D1-gated. Every concrete SectorData still carries Φ = id.

All exports are foundational-triple-only (off busch_effect_gleason): concrete Matrix algebra over the Effect / POVM types and the unconditional FS-volume engine.

The measurement axis and the computational basis vectors

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.σz : Matrix (Fin 2) (Fin 2) ℂ

The measurement observable σ_z = !![1,0;0,-1] (the unit Pauli-Z axis).

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.σz = !![1, 0; 0, -1]

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.e0 : EuclideanSpace ℂ (Fin 2)

The computational basis vector e₀ = |0⟩.

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.e0 = EuclideanSpace.single 0 1

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.e1 : EuclideanSpace ℂ (Fin 2)

The computational basis vector e₁ = |1⟩.

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.e1 = EuclideanSpace.single 1 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e0_ofLp_zero : e0.ofLp 0 = 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e0_ofLp_one : e0.ofLp 1 = 0

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e1_ofLp_zero : e1.ofLp 0 = 0

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e1_ofLp_one : e1.ofLp 1 = 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e0_norm : ‖e0‖ = 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.e1_norm : ‖e1‖ = 1

The unsharp effects

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM (η : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The plus-outcome unsharp effect matrix (1/2)(I + η σ_z).

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM η = (1 / 2) • (1 + ↑η • CSD.Empirical.CSDBridge.WeakMeasurement.σz)

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM (η : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The minus-outcome unsharp effect matrix (1/2)(I − η σ_z).

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM η = (1 / 2) • (1 - ↑η • CSD.Empirical.CSDBridge.WeakMeasurement.σz)

theorem CSD.Empirical.CSDBridge.WeakMeasurement.outer_e0 : LF2.outerProduct e0 = !![1, 0; 0, 0]

|0⟩⟨0| = !![1,0;0,0].

theorem CSD.Empirical.CSDBridge.WeakMeasurement.outer_e1 : LF2.outerProduct e1 = !![0, 0; 0, 1]

|1⟩⟨1| = !![0,0;0,1].

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM_decomp (η : ℝ) : weakPlusM η = ↑((1 + η) / 2) • LF2.outerProduct e0 + ↑((1 - η) / 2) • LF2.outerProduct e1

(1/2)(I + η σ_z) = ((1+η)/2)|0⟩⟨0| + ((1−η)/2)|1⟩⟨1| — the diagonal form.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM_decomp (η : ℝ) : weakMinusM η = ↑((1 - η) / 2) • LF2.outerProduct e0 + ↑((1 + η) / 2) • LF2.outerProduct e1

(1/2)(I − η σ_z) = ((1−η)/2)|0⟩⟨0| + ((1+η)/2)|1⟩⟨1|.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM_isHermitian (η : ℝ) : (weakPlusM η).IsHermitian

weakPlusM η is Hermitian.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM_isHermitian (η : ℝ) : (weakMinusM η).IsHermitian

weakMinusM η is Hermitian.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM_psd (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : (weakPlusM η).PosSemidef

Unsharpness constraint (plus): weakPlusM η is PSD for 0 ≤ η ≤ 1 (eigenvalues (1±η)/2 ∈ [0,1]).

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM_psd (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : (weakMinusM η).PosSemidef

Unsharpness constraint (minus): weakMinusM η is PSD for 0 ≤ η ≤ 1.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakM_sum (η : ℝ) : weakPlusM η + weakMinusM η = 1

POVM completeness at the matrix level: (1/2)(I+ησ) + (1/2)(I−ησ) = I.

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakEffectPlus (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : LF2.Effect 2

The plus-outcome unsharp effect weakEffectPlus η = (1/2)(I + η σ_z).

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.weakEffectPlus η h0 h1 = { M := CSD.Empirical.CSDBridge.WeakMeasurement.weakPlusM η, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakEffectMinus (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : LF2.Effect 2

The minus-outcome unsharp effect weakEffectMinus η = (1/2)(I − η σ_z).

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.weakEffectMinus η h0 h1 = { M := CSD.Empirical.CSDBridge.WeakMeasurement.weakMinusM η, isHermitian := ⋯, nonneg := ⋯, le_one := ⋯ }

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_effects_sum_one (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : (weakEffectPlus η h0 h1).M + (weakEffectMinus η h0 h1).M = 1

(Part A) The unsharp effects sum to the identity.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_effect_psd (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : (weakEffectPlus η h0 h1).M.PosSemidef ∧ (weakEffectMinus η h0 h1).M.PosSemidef

(Part A) The unsharpness constraint: both effects are PosSemidef. Together with weak_effects_sum_one and the Effect.le_one fields, {weakEffectPlus η, weakEffectMinus η} is a genuine POVM.

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakPOVM (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : LF2.POVM 2 (Fin 2)

(Part A) The unsharp POVM {(1/2)(I+ησ), (1/2)(I−ησ)} of strength η, indexed by Fin 2 (0 = +, 1 = −).

Equations

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

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakPOVM_weight_zero (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) : (weakPOVM η h0 h1).weight ψ 0 = RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakPlusM η)) ψ))

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weakPOVM_weight_one (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) : (weakPOVM η h0 h1).weight ψ 1 = RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakMinusM η)) ψ))

Born weights

theorem CSD.Empirical.CSDBridge.WeakMeasurement.re_add (a b : ℂ) : RCLike.re (a + b) = RCLike.re a + RCLike.re b

theorem CSD.Empirical.CSDBridge.WeakMeasurement.inner_two (x y : EuclideanSpace ℂ (Fin 2)) : inner ℂ x y = star (x.ofLp 0) * y.ofLp 0 + star (x.ofLp 1) * y.ofLp 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.inner_psi_e0 (ψ : EuclideanSpace ℂ (Fin 2)) : inner ℂ ψ e0 = star (ψ.ofLp 0)

theorem CSD.Empirical.CSDBridge.WeakMeasurement.inner_psi_e1 (ψ : EuclideanSpace ℂ (Fin 2)) : inner ℂ ψ e1 = star (ψ.ofLp 1)

theorem CSD.Empirical.CSDBridge.WeakMeasurement.normSq_inner_psi_e0 (ψ : EuclideanSpace ℂ (Fin 2)) : ‖inner ℂ ψ e0‖ ^ 2 = ‖ψ.ofLp 0‖ ^ 2

theorem CSD.Empirical.CSDBridge.WeakMeasurement.normSq_inner_psi_e1 (ψ : EuclideanSpace ℂ (Fin 2)) : ‖inner ℂ ψ e1‖ ^ 2 = ‖ψ.ofLp 1‖ ^ 2

theorem CSD.Empirical.CSDBridge.WeakMeasurement.sum_ofLp_normSq (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : ‖ψ.ofLp 0‖ ^ 2 + ‖ψ.ofLp 1‖ ^ 2 = 1

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_weight_plus (η : ℝ) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakPlusM η)) ψ)) = (1 + η) / 2 * ‖ψ.ofLp 0‖ ^ 2 + (1 - η) / 2 * ‖ψ.ofLp 1‖ ^ 2

(Part B) The weak Born weight (explicit-amplitude form). For a unit preparation, ⟨ψ, weakEffectPlus η ψ⟩ = ((1+η)/2)‖ψ₀‖² + ((1−η)/2)‖ψ₁‖².

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_weight_minus (η : ℝ) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakMinusM η)) ψ)) = (1 - η) / 2 * ‖ψ.ofLp 0‖ ^ 2 + (1 + η) / 2 * ‖ψ.ofLp 1‖ ^ 2

The minus analogue: ⟨ψ, weakEffectMinus η ψ⟩ = ((1−η)/2)‖ψ₀‖² + ((1+η)/2)‖ψ₁‖².

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_weight_plus_unit (η : ℝ) (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakPlusM η)) ψ)) = (1 + η * (‖ψ.ofLp 0‖ ^ 2 - ‖ψ.ofLp 1‖ ^ 2)) / 2

(Part B) The weak Born weight in σ_z-expectation form. For a unit preparation, ⟨ψ, weakEffectPlus η ψ⟩ = (1 + η (‖ψ₀‖² − ‖ψ₁‖²)) / 2 = (1 + η ⟨ψ, σ_z ψ⟩)/2. The deviation from 1/2 scales linearly with the strength η.

The no-measurement ↔ projective interpolation

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_unsharp_interpolation (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) : weakPlusM 0 = (1 / 2) • 1 ∧ RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakPlusM 0)) ψ)) = 1 / 2 ∧ weakPlusM 1 = LF2.outerProduct e0 ∧ RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin (weakPlusM 1)) ψ)) = ‖ψ.ofLp 0‖ ^ 2

(Part B headline) The unsharp interpolation: no-measurement (η=0) ↔ projective (η=1). For every unit preparation ψ:

1. weakEffectPlus 0 = (1/2) I — the maximally unsharp / trivial POVM (no basis distinguished, cf. 15a's degenerate scalar·I);
2. its weight is 1/2 regardless of ψ — no information;
3. weakEffectPlus 1 = |0⟩⟨0| — the sharp σ_z-projector;
4. its weight is ‖ψ₀‖² = ‖⟨e₀,ψ⟩‖² — the full Born weight (the sharp carve).

So η is the measurement strength / sharpness, interpolating no-measurement ↔ projective.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_partial_information_witness : 1 / 2 < RCLike.re (inner ℂ e0 ((Matrix.toEuclideanLin (weakPlusM (1 / 2))) e0)) ∧ RCLike.re (inner ℂ e0 ((Matrix.toEuclideanLin (weakPlusM (1 / 2))) e0)) < ‖e0.ofLp 0‖ ^ 2

(Part B) Genuine partial information (non-vacuity). At intermediate strength η = 1/2 on the basis preparation e₀ (sharp Born weight 1, no-measurement weight 1/2), the weak plus-weight is 3/4 — strictly between the trivial 1/2 and the sharp Born weight ‖e₀.ofLp 0‖² = 1. Neither trivial nor sharp: genuine partial information.

The CSD volume reading (the "nudge")

noncomputable def CSD.Empirical.CSDBridge.WeakMeasurement.weakNaimark (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) : LF4.NaimarkDilation (weakPOVM η h0 h1)

The canonical Naimark dilation of the unsharp POVM (it exists, like every POVM's). The ancilla is the apparatus; the dilated ontic space is Σ' = ℂℙ³.

Equations

• CSD.Empirical.CSDBridge.WeakMeasurement.weakNaimark η h0 h1 = CSD.LF4.canonicalNaimark (CSD.Empirical.CSDBridge.WeakMeasurement.weakPOVM η h0 h1)

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_frequency_volume (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 2 ≃ Fin 4) (ψ' : EuclideanSpace ℂ (Fin 4)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (weakNaimark η h0 h1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 4) {Ω : 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 : ∀ (j : Fin 4), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 2), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (X l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds ((weakPOVM η h0 h1).weight ψ i))

(Part C) The weak-measurement Born weights as Kähler volumes (the volume companion). Instantiating the unconditional POVM volume engine povm_born_frequency_volume_uncond at the unsharp weakPOVM η: i.i.d. Fubini–Study trials on the dilated ontic Σ' = ℂℙ³ have the i-th weak-outcome empirical frequency converge, on a single almost-sure event, to the weak Born weight (weakPOVM η).weight ψ i — realised as a sum of Fubini–Study volumes of the dilated barycentric cells.

This is the partial volume nudge reading: at η = 0 the dilated volumes are the trivial 1/2 split (no nudge); at η = 1 the full projective carve; intermediate η a partial nudge of the Σ-volume. Carving-free, Gleason-free, unconditional (no genericity on the dilated state). The ontic flow that realises the nudge dynamically is D1-gated (LF6), not claimed here.

theorem CSD.Empirical.CSDBridge.WeakMeasurement.weak_born_frequency_volume_canonical (η : ℝ) (h0 : 0 ≤ η) (h1 : η ≤ 1) (ψ : EuclideanSpace ℂ (Fin 2)) (e : Fin 2 × Fin 2 ≃ Fin 4) (ψ' : EuclideanSpace ℂ (Fin 4)) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (weakNaimark η h0 h1).V) ψ)) (hψ'0 : ψ' ≠ 0) (hnorm : ‖ψ'‖ = 1) (p₀ : LF4.CPN 4) : ∀ᵐ (ω : LF4.fsTrialSpace 4) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin 2), Filter.Tendsto (fun (m : ℕ) => ∑ n : Fin 2, (∑ l ∈ Finset.range m, (LF4.fsTrial 4 l ⁻¹' LF4.bornRegion ψ' hψ'0 (e (n, i))).indicator (fun (x : LF4.fsTrialSpace 4) => 1) ω) / ↑m) Filter.atTop (nhds ((weakPOVM η h0 h1).weight ψ i))

weak_born_frequency_volume on the canonical i.i.d. FS process (the trial bundle is discharged, so the hypothesis set is Lean-inhabited).