Shortest-Distance Semantics

Abstract

First-mismatch distance exactly measures future separation and stable depth.

Theorem 1.1 (First separation determines distance and stable depth).

$$\begin{array}{c}\forall Y,O,\\ \mathrm{FiniteNonempty}(Y),\tau :Y\to Y,q:Y\to O,\\ \forall y,y^{\prime }\in Y,(d_q(y,y^{\prime })<\infty )\iff (\exists k\in \mathbb{N},q({\tau }^k(y))\ne q({\tau }^k(y^{\prime }))),\\ \forall k\in \mathbb{N},(d_q(y,y^{\prime })=k)\iff (q({\tau }^k(y))\ne q({\tau }^k(y^{\prime }))\wedge \forall j<k,q({\tau }^j(y))=q({\tau }^j(y^{\prime }))),\\ (d_q(y,y^{\prime })=\infty )\iff (\forall k\in \mathbb{N},q({\tau }^k(y))=q({\tau }^k(y^{\prime }))),\\ ((\exists y,y^{\prime }\in Y,d_q(y,y^{\prime })<\infty )\Rightarrow m_{\ast }=\max \{d_q(y,y^{\prime })\mid y,y^{\prime }\in Y,d_q(y,y^{\prime })<\infty \})\wedge \\ ((\forall y,y^{\prime }\in Y,d_q(y,y^{\prime })=\infty )\Rightarrow m_{\ast }=0).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/PredictionCertificates/ShortestDistanceSemantics.shortest_distance_exact_semantics (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let Y be a finite nonempty state carrier, tau its deterministic update, and q a readout. The imported canonical distance is the least future readout-mismatch time, with none representing infinity.

The public statement gives both the existence criterion and the exact least-time characterization. Infinite distance is stated directly as equality at every future readout time.

The canonical least observation-stability depth equals the largest finite pair distance. The finite supremum uses zero for infinite entries, so the separate no-distinguishable-pair clause yields the source convention that the depth is zero.

The proof applies the existing infinity criterion and finite-history stability theorem. Pinned Mathlib’s least-witness and finite-supremum lemmas bridge the two canonical depth objects; no distance, relation, or stability primitive is redeclared.

References

• Truth anchor: D5/S3/ObserverMemory/PredictionCertificates/ShortestDistanceSemantics.shortest_distance_exact_semantics
• Dependency: D5/S3/Observer/Separation/FiniteHistoryStability
• Dependency: D5/S3/ObserverMemory/PredictionCertificates/LocalCertificateMinimality