Sharp Product Completion Depth

Abstract

Sharp local witnesses give the maximum law for finite product completion depth.

Theorem 1.1 (The slowest sharp local factor fixes the product completion depth).

$$\begin{gathered} \forall I:\mathrm{Type},Y,O:I\to \mathrm{Type}, \\ F:\forall i\in I,Y\left(i\right)\to Y\left(i\right),q:\forall i\in I,Y\left(i\right)\to O\left(i\right),m:I\to \mathbb{N}, \\ \mathrm{Fintype}\left(I\right)\wedge \mathrm{Fintype}\left(\prod _{i\in I}Y\left(i\right)\right)\wedge (\forall i\in I,\mathrm{Nonempty}\left(Y\left(i\right)\right))\wedge \\ (\forall i\in I,0<m\left(i\right)\Rightarrow \forall x,y\in Y\left(i\right),\mathrm{word}\left(F,q,i,m\left(i\right),x\right)=\mathrm{word}\left(F,q,i,m\left(i\right),y\right)\Rightarrow \mathrm{itinerary}\left(F,q,i,x\right)=\mathrm{itinerary}\left(F,q,i,y\right))\wedge \\ (\forall i\in I,0<m\left(i\right)\Rightarrow \exists x,y\in Y\left(i\right),\mathrm{word}\left(F,q,i,m\left(i\right)-1,x\right)=\mathrm{word}\left(F,q,i,m\left(i\right)-1,y\right)\wedge \mathrm{itineraryAt}\left(F,q,i,x,m\left(i\right)\right)\ne \mathrm{itineraryAt}\left(F,q,i,y,m\left(i\right)\right))\wedge \\ (\forall i\in I,m\left(i\right)=0\Rightarrow \forall x,y\in Y\left(i\right),q\left(i,x\right)=q\left(i,y\right)\Rightarrow \mathrm{itinerary}\left(F,q,i,x\right)=\mathrm{itinerary}\left(F,q,i,y\right))\Rightarrow \\ \mathrm{observationStabilityDepth}\left(\mathrm{pointwiseUpdate}\left(F\right),\mathrm{pointwiseReadout}\left(q\right)\right)=\mathrm{finiteMax}\left(I,m\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Fusion/SharpProductCompletionDepth.sharp_product_completion_depth (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite index set carries dependent state and output families. The full dependent product of state carriers is finite, and every component state carrier is nonempty so a local witness can be embedded while all other coordinates remain fixed.

At every positive local depth, the finite word already determines the complete itinerary and a pair agrees through the preceding depth but differs at the stated depth. At local depth zero, equality of the current readout determines the complete itinerary.

The update and readout on the independent product are constructed pointwise from the component maps. The canonical least observation stability depth of that product is the finite maximum of the local depths.

The proof applies the existing exact semantics of shortest distance. Every global first mismatch is bounded by its differing coordinate, and every positive sharp local witness embeds as a global pair with the same first mismatch.

References

• Truth anchor: D5/S3/ObserverMemory/Fusion/SharpProductCompletionDepth.sharp_product_completion_depth
• Dependency: D5/S3/ObserverMemory/PredictionCertificates/ShortestDistanceSemantics