SigmaLayer/Luders: the projective (Lüders) state update

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

Ledger target T8, the projective post-measurement (Lüders) update, closing the gap left by SigmaLayer/MeasurementRecord.lean (which supplies only the epistemic-support conditioning compatibleSet_appendEstablishedFact and explicitly declines to call it a Lüders update until an equality with the Lüders rule is proved).

For a projection p (self-adjoint idempotent) and a state x with p x ≠ 0, the Lüders update is the normalised projected state ludersUpdate p x = (‖p x‖)⁻¹ • p x. Its Born weight for a projection is projWeight p x = ‖p x‖² (equal to Re⟨x, p x⟩, the effect/POVM weight, projWeight_eq_re_inner). We prove the three defining properties:

• normalisation (ludersUpdate_norm): the updated state is a unit vector;
• repeatability (ludersUpdate_repeatable): p fixes the updated state, so an immediate re-measurement yields the same outcome with certainty (Born weight 1);
• Lüders = conditional probability (ludersUpdate_conditional): for a finer projection q inside the range of p (q ∘ p = q), the Born weight of q in the updated state is projWeight q x / projWeight p x — the update reproduces the CONDITIONAL Born probabilities.

The third property is the content of "Lüders update", the state-space counterpart of the ontic conditioning compatibleSet_appendEstablishedFact (both condition on the realised outcome); it is Bayesian conditionalisation at the level of Born weights. Matrix projections instantiate the abstract IsProjection via isProjection_toEuclideanLin, connecting to the repository's matrix-based Born weights and LF2.POVM effects.

Everything is proved for a general finite-dimensional complex inner product space; no new postulate.

structure CSD.SigmaLayer.IsProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) : Prop

A projection: a self-adjoint idempotent operator. The observable's spectral projector for a measurement outcome.

• selfAdjoint : LinearMap.adjoint p = p

  The projector is self-adjoint.

• idempotent (x : E) : p (p x) = p x

  The projector is idempotent.

noncomputable def CSD.SigmaLayer.projWeight {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : E →ₗ[ℂ] E) (x : E) : ℝ

The projective Born weight of a state. ‖p x‖², the probability of the outcome whose projector is p.

Equations

• CSD.SigmaLayer.projWeight p x = ‖p x‖ ^ 2

noncomputable def CSD.SigmaLayer.ludersUpdate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : E →ₗ[ℂ] E) (x : E) : E

The Lüders update. The normalised projected state (‖p x‖)⁻¹ • p x (and 0 on the null set p x = 0).

Equations

• CSD.SigmaLayer.ludersUpdate p x = (↑‖p x‖)⁻¹ • p x

theorem CSD.SigmaLayer.projWeight_eq_re_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) (hp : IsProjection p) (x : E) : projWeight p x = (inner ℂ x (p x)).re

The projective Born weight is the effect expectation Re⟨x, p x⟩. For a projection, ‖p x‖² = Re⟨x, p x⟩, so projWeight agrees with the LF2.POVM/effect weight convention on projective effects.

theorem CSD.SigmaLayer.norm_inv_ofReal_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) (x : E) : ‖(↑‖p x‖)⁻¹‖ = ‖p x‖⁻¹

Norm of the scalar (‖p x‖ : ℂ)⁻¹.

theorem CSD.SigmaLayer.ludersUpdate_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) (x : E) (hx : p x ≠ 0) : ‖ludersUpdate p x‖ = 1

Normalisation. The Lüders update is a unit vector whenever the outcome is possible (p x ≠ 0).

theorem CSD.SigmaLayer.ludersUpdate_repeatable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) (hp : IsProjection p) (x : E) : p (ludersUpdate p x) = ludersUpdate p x

Repeatability. The projector p fixes its own Lüders update, so an immediate re-measurement of the same observable returns the same outcome with certainty (projWeight p of the updated state is 1).

theorem CSD.SigmaLayer.ludersUpdate_conditional {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p q : E →ₗ[ℂ] E) (hqp : ∀ (x : E), q (p x) = q x) (x : E) (hx : p x ≠ 0) : projWeight q (ludersUpdate p x) = projWeight q x / projWeight p x

Lüders = conditional probability. For a finer projection q supported inside the range of p (q ∘ p = q), the Born weight of q in the Lüders-updated state equals the conditional probability projWeight q x / projWeight p x: the projective update reproduces Bayesian conditionalisation of the Born weights.

theorem CSD.SigmaLayer.luders_capstone {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p : E →ₗ[ℂ] E) (hp : IsProjection p) : (∀ (x : E), p x ≠ 0 → ‖ludersUpdate p x‖ = 1) ∧ (∀ (x : E), p (ludersUpdate p x) = ludersUpdate p x) ∧ ∀ (q : E →ₗ[ℂ] E), (∀ (x : E), q (p x) = q x) → ∀ (x : E), p x ≠ 0 → projWeight q (ludersUpdate p x) = projWeight q x / projWeight p x

T8: the projective (Lüders) update, its three defining properties. For any projection p, the Lüders update ludersUpdate p is normalised, repeatable, and reproduces the conditional Born probabilities. This is the projective post-measurement state update, the state-space counterpart of the ontic conditioning compatibleSet_appendEstablishedFact.

theorem CSD.SigmaLayer.isProjection_toEuclideanLin {N : ℕ} (P : Matrix (Fin N) (Fin N) ℂ) (hh : P.conjTranspose = P) (hi : P * P = P) : IsProjection (Matrix.toEuclideanLin P)

Matrix projections are projections. A Hermitian idempotent matrix P (Pᴴ = P, P * P = P) gives a projection Matrix.toEuclideanLin P, connecting the abstract Lüders update to the repository's matrix-based Born weights and LF2.POVM effects.