Posterior Interiority under Equivalent Laws
Abstract
Equivalent transcript laws keep the limiting binary posterior strictly interior and exclude measurable zero-error separation.
Theorem 1.1 (Equivalent laws keep the limiting posterior interior).
Proof. Machine-checked in Lean as D5/S3/Observer/MeasureSeparation/EquivalentLawPosteriorInterior.equivalent_law_posterior_stays_interior (✓ std3). ∎
Source. Repository-derived.
Commentary.
The two state-indexed transcript laws are probability measures on one measurable space. A real prior strictly between zero and one constructs their displayed mixture law.
The limiting likelihood is the real Radon–Nikodym density of the first law with respect to the second. Mutual absolute continuity makes this density finite and positive almost everywhere under the mixture, so the displayed Bayesian normalization is strictly between zero and one.
The second conjunct applies the frozen null-set transport result: no measurable event can have mass one under the first law and mass zero under the equivalent second law.
References
- Truth anchor:
D5/S3/Observer/MeasureSeparation/EquivalentLawPosteriorInterior.equivalent_law_posterior_stays_interior - Dependency: D5/S3/Observer/MeasureSeparation/EquivalentMeasuresExcludePerfectSeparator