First Difference Power Law

Abstract

The discounted discrete prediction distance is the power of the first differing readout.

Theorem 1.1 (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{orbitReadoutRelation}(tau,q,y,y^{\prime })\Rightarrow \mathrm{discountedPredictionDistance}(tau,q,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,gamma,y,y^{\prime })=\mathrm{pow}(gamma,\mathrm{firstDifferenceIndex}(tau,q,y,y^{\prime }))). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The relation R_q is equality of the q-readout at every iterate of the deterministic update tau. The distance is the existing discounted supremum using the discrete output discrepancy.

If two states are R_q-related, every discrepancy term is zero. If they are distinguishable, Nat.find supplies the minimum time at which the readouts differ; all earlier terms vanish and later powers of gamma are no larger, giving the displayed power exactly.

The theorem exposes both source clauses: zero distance on the relation and the first-difference power law for every separating witness.

References

• Truth anchor: D5/S3/Observer/MetricGeometryLaws/FirstDifferencePowerLaw.first_difference_power_law
• Dependency: D5/S3/Observer/MetricGeometry/BellmanMaxEquation
• Dependency: D5/S3/Observer/MetricGeometry/DiscretePredictionUltrametric