Earliest Future Witness

Abstract

Memory is the earliest future distinction of states merged by the current readout.

Theorem 1.1 (Canonical memory records the first future mismatch).

$$\begin{gathered} \forall Y,O:\mathrm{Type},F:Y\to Y,q:Y\to O, \\ x,y\in Y,n\in \mathbb{N}, \\ q\left(x\right)=q\left(y\right)\Rightarrow (\mathrm{shortestDistance}\left(F,q,x,y\right)=\mathrm{some}\left(n\right)⟺(0<n\wedge I\left(x,n\right)\ne I\left(y,n\right)\wedge \\ \forall m<n,I\left(x,m\right)=I\left(y,m\right))). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Assume two states have the same current readout. Their canonical finite shortest distance is some positive depth exactly when their future readouts differ at that depth and agree at every earlier depth.

Thus the stored distinction is selected by the first future mismatch, rather than by an arbitrary record of the past. The theorem places no finiteness assumption on the state or readout carrier.

References

• Truth anchor: D5/S3/ObserverMemory/PredictionCertificates/EarliestFutureWitness.memory_is_earliest_future_witness
• Dependency: D5/S3/ObserverMemory/PredictionCertificates/LocalCertificateMinimality