Feedback Completion Naturality

Abstract

Projected-state feedback preserves a family of semiconjugate updates.

Theorem 1.1 (Projected-state feedback preserves semiconjugate updates).

$\forall Y, Z, U : Type, u p d a t e : U \to (Y \to Y), co m pl e t e d U p d a t e : U \to (Z \to Z), p ro j ec t i o n : Y \to Z, f ee d ba c k : Z \to U, (\forall u, p ro j ec t i o n \circ u p d a t e (u) = co m pl e t e d U p d a t e (u) \circ p ro j ec t i o n) \Rightarrow p ro j ec t i o n \circ (y \mapsto u p d a t e (f ee d ba c k (p ro j ec t i o n (y))) (y)) = (z \mapsto co m pl e t e d U p d a t e (f ee d ba c k (z)) (z)) \circ p ro j ec t i o n .$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FeedbackCompletionNaturality.feedback_completion_naturality (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let update and completedUpdate be families of state updates indexed by a common control type, and let projection map the original state into the completed state. Assume projection semiconjugates the two updates for every control value.

Choose each control value by applying feedback to the projected current state. Then projection also semiconjugates the resulting closed-loop updates. The control on both sides is identical because it depends only on that projected state.

Loogle found Function.Semiconj.comp_eq as an exact library result for turning pointwise semiconjugacy into function equality; the Lean proof imports and applies it. Loogle also returned the pointwise and equivalence forms, while a shaped family query did not elaborate. LeanSearch returned only generic semiconjugacy and flow results. Repository and receipt searches found no equal or stronger closed-loop theorem. A Boolean instance witnesses that the hypotheses are satisfiable.

References

Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackCompletionNaturality.feedback_completion_naturality

Keyboard shortcuts

trureturing Blueprint

Feedback Completion Naturality

Abstract

References