Itinerary First Difference Power Law

Abstract

Canonical complete itineraries determine the discounted discrete prediction distance.

Theorem 1.1 (Itinerary first difference determines discounted distance).

$$\begin{gathered} \forall Y,O,[\mathrm{DecidableEq}\left(O\right)],tau:Y\to Y,q:Y\to O,gamma:\mathbb{R},(0<gamma\le 1)\Rightarrow \\ \forall y,y^{\prime }\in Y, \\ (\mathrm{FutureIndistinguishable}(tau,q,y,y^{\prime })\Rightarrow \mathrm{discountedPredictionDistance}(tau,q,discreteOutputDistance,gamma,y,y^{\prime })=0)\wedge \\ (\exists k\in \mathbb{N},q(\mathrm{iterate}(tau,k,y))\ne q(\mathrm{iterate}(tau,k,y^{\prime }))\Rightarrow \mathrm{discountedPredictionDistance}(tau,q,discreteOutputDistance,gamma,y,y^{\prime })=gamm{a}^{\min \{k\in \mathbb{N}\mid q(\mathrm{iterate}(tau,k,y))\ne q(\mathrm{iterate}(tau,k,y^{\prime }))\}}). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Future indistinguishability is the canonical equality of complete readout itineraries. The distance is the existing discounted supremum using the discrete output discrepancy.

Equal complete itineraries make every discrepancy term zero. If the states are distinguishable, the least separating time gives the largest nonzero discounted term.

Both source clauses remain public: zero distance for canonically future-indistinguishable states and the exact first-difference power law for distinguishable states.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/ItineraryFirstDifferencePowerLaw.itinerary_first_difference_power_law
• Dependency: D5/S3/Observer/MetricGeometry/BellmanMaxEquation
• Dependency: D5/S3/Observer/MetricGeometry/DiscretePredictionUltrametric
• Dependency: D5/S3/ObserverMemory/InverseLimits/IdentityFuturePastGap