Prediction Closure as Dynamical Repair

Abstract

The least invariant observer closure induces dynamics on the visible quotient.

Theorem 1.1 (Prediction closure is the least dynamical repair).

$$\begin{array}{c}\forall V:\mathrm{FiniteDimensionalRealHilbertSpace},\\ \forall K:\mathrm{End}(V),\forall W:\mathrm{Submodule}(V),\\ W\subseteq \mathrm{Cl}(K,W)\wedge \mathrm{Invariant}(K,\mathrm{Cl}(K,W))\wedge \mathrm{Invariant}(\mathrm{adjoint}(K),\mathrm{Cl}(K,W{)}^{\perp })\wedge \\ (\forall x,y\in V,x-y\in \mathrm{Cl}(K,W{)}^{\perp }\Rightarrow \mathrm{adjoint}(K)(x)-\mathrm{adjoint}(K)(y)\in \mathrm{Cl}(K,W{)}^{\perp })\wedge \\ \overline{\mathrm{adjoint}(K)}\circ \mathrm{quotientProjection}(\mathrm{Cl}(K,W{)}^{\perp })=\mathrm{quotientProjection}(\mathrm{Cl}(K,W{)}^{\perp })\circ \mathrm{adjoint}(K)\wedge \\ (\forall U:\mathrm{Submodule}(V),(W\subseteq U\wedge \mathrm{Invariant}(K,U))\Rightarrow \mathrm{Cl}(K,W)\subseteq U).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/PredictionClosureDynamicalRepair.prediction_closure_minimal_dynamical_repair (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let K be a linear evolution of observables on a finite-dimensional real Hilbert space, with no invariance assumption on the current visible subspace W. Its prediction closure C is constructed from all forward K-orbits of W, and its final invisible residual R is the orthogonal complement of C.

The existing observer-orbit theorem directly proves that C contains W, is K-invariant, and lies in every K-invariant observable extension containing W. Mathlib’s exact adjoint-invariance theorem then makes R invariant under the adjoint state evolution.

Consequently, differences in R remain in R after state evolution, so final invisibility is a dynamical congruence. Mathlib’s quotient map construction supplies the induced linear evolution on V/R and its canonical projection equation.

The source compares time evolution with self-reference, contextual, completion, and refinement closures only at the level of a common minimal-stability pattern. This theorem formalizes that pattern for a linear target operation and does not identify objects belonging to those different domains.

Repository search found and directly applies observer_closure_is_least_invariant. Pinned Mathlib search found and directly applies Module.End.mem_invtSubmodule_adjoint_iff, Submodule.mapQ, and Submodule.mapQ_mkQ. No theorem was found that packages all of the residual, congruence, quotient, and leastness clauses.

References

• Truth anchor: D5/S3/Quantum/Dynamics/PredictionClosureDynamicalRepair.prediction_closure_minimal_dynamical_repair
• Dependency: D5/S3/Quantum/Dynamics/ObserverOrbitClosure