Controlled Intervention Descent Uniqueness

Abstract

Every controlled update descends uniquely through canonical behavior completion.

Theorem 1.1 (All controlled updates descend uniquely).

$$\begin{gathered} \forall Y,U,O,F:U\to Y\to Y,q:Y\to O,\forall u\in U,\exists !{\overline{F}}_u:\mathrm{ControlledCompletion}(F,q)\to \mathrm{ControlledCompletion}(F,q), \\ \mathrm{completionProjection}\left(F,q\right)\circ F(u)={\overline{F}}_u\circ \mathrm{completionProjection}\left(F,q\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Dynamics/ControlledInterventionDescentUniqueness.all_interventions_unique_completion_descent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the canonical quotient by equality of every finite-word readout, and pi is its canonical projection. No separate completion or projection primitive is introduced.

For every control u, there is exactly one endomap of the completion that makes the update square commute. Existence is witnessed by the canonical completion update; uniqueness follows from surjectivity of the quotient projection.

Pointwise table and output projections lift this unique underlying square to the source’s simultaneous diagonal naturality law.

References

• Truth anchor: D5/S3/ObserverMemory/Dynamics/ControlledInterventionDescentUniqueness.all_interventions_unique_completion_descent
• Dependency: D5/S0/Rewriting/Quotients/DynamicsDescent
• Dependency: D5/S3/ObserverMemory/Prediction/ControlledBehaviorUniversality