Biaxial Observation Refinement

Abstract

Joint refinement enlarges the observation schedule and shrinks its indistinguishability relation.

Theorem 1.1 (Both observation axes refine in their natural directions).

$$\begin{array}{r}\forall X:\mathrm{Type},O:\mathrm{Type},\\ J:\mathrm{Finset}\left(\mathbb{N}\right),K:\mathrm{Finset}\left(\mathbb{N}\right),m:\mathbb{N},n:\mathbb{N},\\ readout:\mathbb{N}\to \left(X\to O\right),T:X\to X,\\ J\subseteq K\wedge m\le n\Rightarrow \\ \mathrm{observationSchedule}\left(J,m\right)\subseteq \mathrm{observationSchedule}\left(K,n\right)\wedge \\ \mathrm{Indist}\left(K,n,readout,T\right)\subseteq \mathrm{Indist}\left(J,m,readout,T\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Refinement/BiaxialObservationRefinement.biaxial_observation_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The observation schedule is the existing set of index-time pairs whose index lies in the finite set and whose time is below the horizon.

Containment of index sets and ordering of horizons first include the smaller schedule in the larger schedule. This is the source’s first public set relation.

The imported biaxial monotonicity theorem then reverses inclusion of the associated indistinguishability relations, providing the second public set relation without restating its proof.

References

• Truth anchor: D5/S3/Observer/Refinement/BiaxialObservationRefinement.biaxial_observation_refinement
• Dependency: D5/S3/Observer/Refinement/BiaxialMonotoneRefinement