Linear Projection Descent Criterion

Abstract

Orthogonal-projection descent is exactly vanishing directed flow, and self-adjoint dynamics make it commutation.

Theorem 1.1 (Projection descent, directed flow, and commutation).

$$\begin{array}{c}\forall n,P,T:\mathrm{Matrix}\left(n,n,\mathbb{C}\right),\\ (\mathrm{IsIdempotentElem}\left(P\right)\wedge \mathrm{IsHermitian}\left(P\right))\Rightarrow (\mathrm{TFAE}\left(\mathrm{EffectiveDescent}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),\mathrm{InterfaceCongruence}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),\mathrm{NoCarry}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),\mathrm{FactorsThrough}\left(\mathrm{compose}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),\mathrm{toLin}\left(P\right)\right),\mathrm{PullbackInvariant}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),\mathrm{depthZeroKernel}\left(\mathrm{toLin}\left(P\right)\right)=\mathrm{depthOneKernel}\left(\mathrm{toLin}\left(P\right),\mathrm{toLin}\left(T\right)\right),P\cdot T\cdot (1-P)=0\right)\wedge \\ (\mathrm{IsHermitian}\left(T\right)\Rightarrow (P\cdot T\cdot (1-P)=0\iff P\cdot T-T\cdot P=0))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Dynamics/LinearProjectionDescentCriterion.linear_projection_descent_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the finite complex Hilbert space of coordinate vectors. Idempotence and Hermiticity make P an orthogonal projection, and the complementary hidden projection is constructed as I minus P.

The public seven-condition equivalence includes effective-image descent, interface congruence, absence of carry, factorization, pullback invariance, one-step kernel stability, and the directed cross-block equation.

For self-adjoint T, taking the conjugate transpose of the visible cross block supplies the reverse cross block. The imported commutator identity then makes directed vanishing equivalent to commutation.

The existing sixfold interface theorem and commutator identity are applied directly. Repository and pinned-library searches found no theorem packaging the added matrix clause on this carrier.

References

• Truth anchor: D5/S3/Observer/Dynamics/LinearProjectionDescentCriterion.linear_projection_descent_criterion
• Dependency: D5/S3/ConceptDynamics/Dialectics/DeterministicInterfaceEquivalence
• Dependency: D5/S3/Observer/HiddenFlow/ProjectionCommutatorIdentity