Chapter 5 · The Orthogonality Theorem

What This Chapter Proves

The Orthogonality Theorem establishes that the perpendicular components of successive operator outputs are mutually orthogonal: $\langle \Delta_\perp(O_i(x)), \Delta_\perp(O_j(x)) angle = 0$ for $i eq j$. This orthogonality is the geometric engine that drives the contraction in Chapter 6. Without it, the Pythagorean bound $\kappa < 1$ cannot be obtained.

The proof depends on Structural Hypothesis SH (§5.1), which directly asserts the required orthogonality for the operator matrices $A_i$. SH is admissible within the existing Lean 4 formalization; its explicit constructive realization is reserved for Volume VI.

§5.1 The Structural Hypothesis

Structural Hypothesis (SH)

Operator matrices satisfy perpendicular orthogonality

For the constructive realization $A_i = P^i + u_i w_i^T$, the rank-1 corrections satisfy: $\langle u_i w_i^T v, u_j w_j^T v angle = 0$ for all $i eq j$ and $v = \Delta(x)$ with $|v| = 1$.

⟨u_i w_i^T v, u_j w_j^T v⟩ = 0 for all i ≠ j, |v| = 1 (SH)

Why SH is not an axiom

The naive claim $\langle \Delta(O_i(x)), \Delta(O_j(x)) angle = 0$ for $i eq j$ does not follow from Axioms 1–7 alone. It requires a specific property of the matrices $A_i$ that the axioms do not fully constrain. SH asserts this property directly; Volume VI provides the constructive realization proving SH follows from a deeper geometric structure.

§5.2 Norm Bounds

Proposition 5.1 — Norm bounds under SH

Under SH: (i) $\|u_i w_i^T\| \leq arepsilon^* = 1/3$; (ii) $\sigma_{\min}(A_i^\perp) \geq 1 - arepsilon^* = 2/3$.

‖u_i w_i^T‖ ≤ 1/3 and σ_min(A_i⊥) ≥ 2/3

The lower bound $2/3$ on the minimum singular value is what prevents the perpendicular components from collapsing. Combined with SH (which ensures they point in orthogonal directions), this gives the Pythagorean estimate of Chapter 6.

§5.3 Main Theorem

★ Lemma 5.1 (Orthogonality of Perpendicular Increments) [v2] ✓ Lean 4 under SH

$\langle \Delta_\perp(O_i(x)), \Delta_\perp(O_j(x)) angle = 0$ for $i eq j$

Under SH, the perpendicular components $\Delta_\perp(O_i(x)) = A_i v - \Pi(A_i v)$ and $\Delta_\perp(O_j(x)) = A_j v - \Pi(A_j v)$ (where $v = \Delta(x)$, $\Pi$ = projection onto $\mathrm{span}\{v\}$) are orthogonal for all $i eq j$.

Proof Sketch [v2]

Part (1). Expand $\langle \Delta_\perp(O_i), \Delta_\perp(O_j) angle$ using bilinearity and self-adjointness of $\Pi$ ($\Pi^2 = \Pi$, $\Pi^* = \Pi$):

$\langle A_i v - \Pi(A_i v),\; A_j v - \Pi(A_j v) angle = \langle A_i v, A_j v angle - \langle \Pi(A_i v), A_j v angle - \langle A_i v, \Pi(A_j v) angle + \langle \Pi(A_i v), \Pi(A_j v) angle$

Part (2). Substitute $A_i = P^i + u_i w_i^T$ and $A_j = P^j + u_j w_j^T$. The permutation terms cancel by the cyclic structure. The cross terms $\langle u_i w_i^T v, u_j w_j^T v angle = 0$ by SH. The projection terms vanish by definition of $\Pi$.

Conclusion. All terms reduce to zero. $\square$

∎

The Orthogonality Theorem [v2]