Compatible Fusion Embedding

Abstract

An intersection completion is exactly the compatible image of its component completions.

Theorem 1.1 (The intersection completion embeds as the compatible image).

$$\begin{array}{c}\forall I,Y:\mathrm{Type},O:I\to \mathrm{Type},\\ u:Y\to Y,q:\prod _i(Y\to O_i),\\ \mathrm{let}J:=\mathrm{completionEmbedding}\left(\mathrm{componentCompletionRelation}\left(u,q\right)\right);\\ \mathrm{Injective}\left(J\right)\wedge \\ (\forall z\in \mathrm{Fused}\left(q\right),\forall i\in I,\\ J{\left(\mathrm{completedFusionDynamics}\left(u,q,z\right)\right)}_i=\mathrm{completedComponentDynamics}\left(u,q,i,J{\left(z\right)}_i\right))\wedge \\ \mathrm{range}\left(J\right)=\mathrm{Comp}\left(q\right)\wedge \\ \exists e:\mathrm{Fused}\left(q\right)\equiv \mathrm{Comp}\left(q\right),\forall z\in \mathrm{Fused}\left(q\right),\mathrm{coe}\left(e\left(z\right)\right)=J\left(z\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

Let qi be a family of readouts on a state type Y with update u. Each readout defines complete-future equivalence through the repository’s complete itinerary. The fused completion is the quotient by the intersection of these component relations, and J sends a fused class to its class in every component quotient.

The compatible subset Comp consists exactly of component tuples z for which there is one state y whose canonical class in every component is zi. The theorem proves that J is injective, its range is Comp, and the fused quotient is canonically equivalent to Comp with underlying map J.

Advancing both states shifts equality of complete itineraries and therefore preserves every component relation. The induced fused and component updates require no additional hypothesis, and the theorem proves that J intertwines all of them.

Pinned Mathlib supplies Quotient.map and Quotient.exact for the quotient arguments, followed by Equiv.ofInjective and Equiv.setCongr for the canonical equivalence. Repository search found related two-component refinement and product-fullness results, but no declaration containing all four family-indexed conclusions.

References

• Truth anchor: D5/S3/ObserverMemory/Fusion/CompatibleFusionEmbedding.compatible_fusion_embedding
• Dependency: D5/S3/ObserverMemory/Prediction/ItineraryCompletion