Canonical Discounted Future Geometry

Abstract

Discounted future distance is the canonical bounded-observer pseudometric.

Theorem 1.1 (Discounted future distance gives the observer pseudometric).

$$\begin{gathered} 0<gamma<1\wedge \mathrm{BoundedOutputMetric}\left(q,B\right)\Rightarrow \\ \exists Dgamma,\mathrm{CanonicalDiscountedDistance}\left(Dgamma,F,q,gamma\right)\wedge \mathrm{PseudoMetric}\left(Y,Dgamma\right)\wedge \\ \forall x,y\in Y, \\ d\left(q\left(x\right),q\left(y\right)\right)\le \mathrm{Dgamma}\left(x,y\right)\wedge \\ \mathrm{Dgamma}\left(F\left(x\right),F\left(y\right)\right)\le gamm{a}^{-1}\mathrm{Dgamma}\left(x,y\right)\wedge \\ \mathrm{LipschitzWith}\left(gamm{a}^{-1},F,Dgamma\right)\wedge \\ (\mathrm{Dgamma}\left(x,y\right)=0)⟺\mathrm{KInfinity}\left(x,y\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/MetricGeometryLaws/CanonicalDiscountedFutureGeometry.canonical_discounted_future_geometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let F be a deterministic state update and q a readout into a bounded metric space. For a discount gamma strictly between zero and one, D_gamma is the supremum of gamma^n times the output distance after n updates.

The existing Bellman equation supplies both current-output domination and the one-step gamma-inverse contraction. The latter is also packaged as the standard Mathlib LipschitzWith predicate.

Strict positivity of every discount power makes zero D_gamma equivalent to equality of every finite future readout, namely membership in the infinite-future relation K_infty.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/CanonicalDiscountedFutureGeometry.canonical_discounted_future_geometry
• Dependency: D5/S3/Observer/MetricGeometryLaws/DiscountedPredictionPseudometric
• Dependency: D5/S3/Observer/Separation/FiniteFutureCongruence