SigmaLayer/ConditioningLink: the conditional→Lüders correspondence

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

SL-T5 follow-on. The corpus proves TWO conditioning rules that were not yet connected (external review 2026-07-14):

• the ontic record-history conditioning (IsolationPreparation.HistoryPreparation.conditionalMeasure_apply): appending a record conditions the Liouville measure on the record-compatible region, conditionalMeasure A = μL(A ∩ compatibleSet) / μL(compatibleSet) (the epistemic-support update compatibleSet_appendEstablishedFact);
• the projective Lüders state update (Luders.ludersUpdate_conditional): the post-measurement Born weight of a finer projection is projWeight q (ludersUpdate p x) = projWeight q x / projWeight p x.

This module makes their identity explicit at the RULE level: BOTH are the single Bayesian conditioning rule bayesianConditional w = w(fine) / w(coarse), differing only in the WEIGHT — the Liouville measure μL for the ontic record update, the Born weight for the projective state update.

That the two weights AGREE is proved separately in SigmaLayer/ConditioningLuders.lean (onticRegion_measure_eq_born : μL(π⁻¹ bornRegion i) = ‖⟨eᵢ,ψ⟩‖², via π_* μL = μFS (B1) + Born-from-volume), so the ontic record conditioning and the projective Lüders update give the SAME conditional probability, seen through π. The ..._correspondence bundle below states only the two Bayesian-rule halves; the weight agreement — and hence the genuine coincidence — lives in that companion file.

References: specs/future-work.md (SL-T5 follow-on); SigmaLayer/Luders.lean (ludersUpdate_conditional), SigmaLayer/IsolationPreparation.lean (conditionalMeasure_apply), SigmaLayer/MeasurementRecord.lean (compatibleSet_appendEstablishedFact), SigmaLayer/MeasureBridge.lean (B1).

def CSD.SigmaLayer.bayesianConditional {α : Type u_1} {β : Type u_2} [Div β] (w : α → β) (coarse fine : α) : β

Bayesian conditioning of a weight. The probability of the finer event given the coarser, w(fine) / w(coarse). Both the projective Lüders update (Born weight) and the ontic record-history conditioning (Liouville measure) are instances of this single rule.

Equations

• CSD.SigmaLayer.bayesianConditional w coarse fine = w fine / w coarse

The projective Lüders update is Bayesian conditioning of the Born weight

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

The Lüders update reproduces Bayesian conditioning of the Born weight. For a finer projection q inside the range of p (q ∘ p = q), the post-measurement Born weight of q is the Bayesian conditional of the Born weight projWeight · x given the outcome p. Restates Luders.ludersUpdate_conditional in the shared bayesianConditional form.

The ontic record-history conditioning is Bayesian conditioning of the Liouville measure

theorem CSD.SigmaLayer.historyConditioning_isBayesianConditional {Sigma : Type u} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} (HP : HistoryPreparation D R S) (A : Set Sigma) (hA : MeasurableSet A) : ↑HP.toPreparation.conditionalMeasure A = bayesianConditional (fun (T : Set Sigma) => ↑D.muL T) (compatibleSet S HP.history) (A ∩ compatibleSet S HP.history)

The record-history conditioning reproduces Bayesian conditioning of the Liouville measure. Appending a record conditions μL on the record-compatible region: the conditional measure of A is the Bayesian conditional of μL given compatibleSet. Restates IsolationPreparation.HistoryPreparation.conditionalMeasure_apply in the shared bayesianConditional form.

The correspondence

theorem CSD.SigmaLayer.luders_record_conditioning_correspondence {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (p q : E →ₗ[ℂ] E) (hqp : ∀ (y : E), q (p y) = q y) (x : E) (hx : p x ≠ 0) {Sigma : Type u_2} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} {R : RecordSignature} {S : RecordSemantics Sigma R} (HP : HistoryPreparation D R S) (A : Set Sigma) (hA : MeasurableSet A) : projWeight q (ludersUpdate p x) = bayesianConditional (fun (r : E →ₗ[ℂ] E) => projWeight r x) p q ∧ ↑HP.toPreparation.conditionalMeasure A = bayesianConditional (fun (T : Set Sigma) => ↑D.muL T) (compatibleSet S HP.history) (A ∩ compatibleSet S HP.history)

The conditional→Lüders correspondence. The projective Lüders state update and the ontic record-history conditioning are the SAME Bayesian conditioning rule w(fine)/w(coarse), applied to the Born weight and to the Liouville measure respectively. Given the projective sector Born-from-volume bridge (π_* μL = μFS, B1), the two weights agree on the sector, so the state-level Lüders update and the ontic-level record conditioning coincide.