Product Completion Depth Upper Bound

Abstract

The maximum local completion depth completes a pointwise product observer.

Theorem 1.1 (The slowest local completion depth suffices for the product).

$$\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 (\forall i\in I,\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))\Rightarrow \\ \forall x,y\in \prod _{i\in I}Y\left(i\right),\mathrm{word}\left(\mathrm{pointwiseUpdate}\left(F\right),\mathrm{pointwiseReadout}\left(q\right),\mathrm{finiteMax}\left(I,m\right),x\right)=\mathrm{word}\left(\mathrm{pointwiseUpdate}\left(F\right),\mathrm{pointwiseReadout}\left(q\right),\mathrm{finiteMax}\left(I,m\right),y\right)\Rightarrow \mathrm{itinerary}\left(\mathrm{pointwiseUpdate}\left(F\right),\mathrm{pointwiseReadout}\left(q\right),x\right)=\mathrm{itinerary}\left(\mathrm{pointwiseUpdate}\left(F\right),\mathrm{pointwiseReadout}\left(q\right),y\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

A finite index type carries dependent state and output families, with one update, readout, and completion depth at every coordinate.

The sole semantic premise says that each local word through its stated depth determines that factor’s complete itinerary. No sharp witness, least-depth assumption, or nonemptiness premise is required.

The global update and readout are the pointwise products of the local maps. Equality of their word through the finite maximum restricts to equality of every local word, so the local completion laws give equality of the complete product itineraries.

Repository primitives futureReadoutWord and completeItinerary are used directly. The sharper product-depth equality theorem is not applied because its witness premises are absent from this upper-bound claim.

References

• Truth anchor: D5/S3/ObserverMemory/Fusion/ProductCompletionDepthUpperBound.product_completion_depth_upper_bound
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion