Finite-path rigidity and matrix decay

Abstract

Weighted finite-path rigidity, boundary observability, and spectral power decay.

Lemma 1.1 (Successive differences telescope).

$$\forall n\in \mathbb{N},\forall f\in \mathrm{Fin}\left(n+1\right)\to \mathbb{C},\sum _{j:\mathrm{Fin}\left(n\right)}(f\left(\mathrm{Fin}.\mathrm{succ}\left(j\right)\right)-f\left(\mathrm{Fin}.\mathrm{castSucc}\left(j\right)\right))=f\left(\mathrm{Fin}.\mathrm{last}\left(n\right)\right)-f\left(0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.sum_succ_sub_castSucc (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural n and complex-valued function f on Fin (n + 1), the sum of successor differences is the last value minus the first value.

Definition 1.2 (Zero endpoint extension).

$$\forall m\in \mathbb{N},\forall z\in \mathrm{Fin}\left(m\right)\to \mathbb{C},\mathrm{zeroExtend}\left(z\right)=\mathrm{Fin}.\mathrm{cases}\left(0,\mathrm{Fin}.\mathrm{snoc}\left(z,0\right)\right)$$

Formalization. D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.zeroExtend (✓ std3).

Source. Repository-derived.

Commentary.

For every m and complex vector z on Fin m, Fin.cases places zero at the left endpoint and Fin.snoc places zero at the right endpoint. The resulting vector has domain Fin(m + 2).

Lemma 1.3 (The interior values are unchanged).

$$\forall m\in \mathbb{N},\forall z\in \mathrm{Fin}\left(m\right)\to \mathbb{C},\forall i\in \mathrm{Fin}\left(m\right),\mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{succ}\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right)\right)\right)=z\left(i\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.extend_interior (✓ std3). ∎

Source. Repository-derived.

Commentary.

Interior coordinate i is coordinate i + 1 of the zero endpoint extension.

Lemma 1.4 (The right endpoint is zero).

$$\forall m\in \mathbb{N},\forall z\in \mathrm{Fin}\left(m\right)\to \mathbb{C},\mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{last}\left(m+1\right)\right)=0$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.extend_last (✓ std3). ∎

Source. Repository-derived.

Commentary.

The last coordinate of the extended vector is zero.

Theorem 1.5 (Weighted harmonic Dirichlet rigidity).

$$\forall m\in \mathbb{N},\forall v\in \mathrm{Fin}\left(m+1\right)\to \mathbb{R},\left(\forall j\in \mathrm{Fin}\left(m+1\right),0<v\left(j\right)\right)\Rightarrow \left(\forall z\in \mathrm{Fin}\left(m\right)\to \mathbb{C},\left(\forall i\in \mathrm{Fin}\left(m\right),\frac{z\left(i\right)-\mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{castSucc}\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right)\right)\right)}{(v\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right)\right):\mathbb{C})}=\frac{\mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{succ}\left(\mathrm{Fin}.\mathrm{succ}\left(i\right)\right)\right)-z\left(i\right)}{(v\left(\mathrm{Fin}.\mathrm{succ}\left(i\right)\right):\mathbb{C})}\right)\Rightarrow z=0\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.harmonic_dirichlet_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

For arbitrary m and positive velocities, equal adjacent weighted slopes force every interior complex coordinate to vanish. Finite induction makes all edge slopes equal. Their telescoping sum is zero; the strictly positive total velocity forces the common slope to zero.

Theorem 1.6 (A boundary zero propagates through the path).

$$\forall m\in \mathbb{N},1\le m\Rightarrow \left(\forall z\in \mathrm{Fin}\left(m\right)\to \mathbb{C},z\left(\mathrm{Fin}.\mathrm{mk}\left(0\right)\right)=0\Rightarrow \left(\left(\forall i\in \mathrm{Fin}\left(m\right),z\left(i\right)=0\Rightarrow \left(\mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{castSucc}\left(\mathrm{Fin}.\mathrm{castSucc}\left(i\right)\right)\right)=0\Rightarrow \mathrm{zeroExtend}\left(z\right)\left(\mathrm{Fin}.\mathrm{succ}\left(\mathrm{Fin}.\mathrm{succ}\left(i\right)\right)\right)=0\right)\right)\Rightarrow z=0\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.boundary_zero_observability (✓ std3). ∎

Source. Repository-derived.

Commentary.

For m ≥ 1, a zero first interior coordinate and a recurrence propagating two adjacent zeros imply that the entire vector is zero. The left endpoint supplied by zeroExtend starts the induction.

Theorem 1.7 (Strict spectral bounds give real trajectory decay).

$$\forall m\in \mathbb{N},1\le m\Rightarrow \left(\forall N\in \mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{R}\right),\left(\forall c\in \mathbb{C},c\in \mathrm{spectrum}\left(\mathbb{C},\mathrm{Matrix}.\mathrm{map}\left(N,\mathrm{algebraMap}\left(\mathbb{R},\mathbb{C}\right)\right)\right)\Rightarrow \Vert c\Vert <1\right)\Rightarrow \left(\forall u\in \mathrm{Fin}\left(m\right)\to \mathbb{R},\mathrm{Filter}.\mathrm{Tendsto}\left((\lambda k:\mathbb{N},\mathrm{Matrix}.\mathrm{mulVec}\left(N^k,u\right)),\mathrm{Filter}.\mathrm{atTop},\mathrm{nhds}\left(0\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.real_mulVec_powers_tendsto_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

For m ≥ 1 and a real matrix N, every complex spectral modulus below one implies convergence of (N^k).mulVec u to zero for every real vector u. Gelfand’s formula gives an eventual geometric bound on matrix powers in the complex operator norm. Continuity of matrix-vector multiplication and of coordinatewise real parts yields the real trajectory limit.

References

• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.boundary_zero_observability
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.extend_interior
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.extend_last
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.harmonic_dirichlet_zero
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.real_mulVec_powers_tendsto_zero
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.sum_succ_sub_castSucc
• Truth anchor: D5/S3/Quantum/Dynamics/TridiagonalSweeps/FinitePathDynamics.zeroExtend