Chapter 6 · The Recursion Theorem

Structure of the Proof

The Recursion Theorem is proved in two stages. §6.1 establishes the quantitative contraction estimate — showing that the emergence operator $E = R$ is a strict contraction with $\kappa < 1$. §6.2 applies the Banach Fixed Point Theorem to the compact invariant orbit closure $K$ to obtain existence and uniqueness of the fixed point. No convexity assumption is required — compactness of $K$ replaces it.

§6.1 Pythagorean Contraction Estimate

Under Lemma 5.1 (SH), the perpendicular increments at each step are mutually orthogonal. This allows a Pythagorean decomposition: each step subtracts a non-negative orthogonal component from the distance.

★ Proposition 6.1 (Contraction Estimate) [v2] ✓ Lean 4 under SH

$E$ is a strict contraction with constant $\kappa < 1$

Let $v = \Delta(x)$, $v' = \Delta(y)$ with $|v| = |v'| = 1$. Under SH and Proposition 5.1:

‖A^(12) v - A^(12) v'‖² ≤ ‖v - v'‖² - Σᵢ ‖Δ_⊥(O_i(x)) - Δ_⊥(O_i(y))‖²

Each orthogonal term ≥ (2/3)² ‖v - v'‖² / 12  (from Prop 5.1, Lemma 5.1)

⟹  κ² ≤ 1 - 12·(4/9)/12 = 1 - 4/9 = 5/9   ⟹   κ ≤ √(5/9) < 1

The Pythagorean engine

The Pythagorean decomposition works because Lemma 5.1 guarantees the perpendicular components point in orthogonal directions — so each step's contribution to the distance reduction is independent of all others. Twelve independent reductions combine multiplicatively. This is why 12 phases (and not, say, 6 or 9) is the right count: $4 imes 3$ is the product of four base operators and three invariants, and it is exactly this product structure that makes the Pythagorean sum close with $\kappa < 1$.

§6.2 Banach Fixed Point — Existence and Uniqueness

★ Theorem 6.1 (Recursion Theorem) [v2] ✓ Lean 4 under SH

The orbit closure $K$ has a unique fixed point of $E$

Let $K = \overline{\{E^n(x_0) : n \geq 0\}}$ be the compact invariant orbit closure (compact by Axiom 5, invariant by construction). By Proposition 6.1, $E : K o K$ is a strict contraction with constant $\kappa < 1$. By the Banach Fixed Point Theorem: there exists a unique $x^* \in K$ with $E(x^*) = x^*$, and $E^n(x_0) o x^*$ geometrically.

E : K → K strict contraction (κ < 1, K compact)
⟹  ∃! x* ∈ K : E(x*) = x*
     d(Eⁿ(x₀), x*) ≤ κⁿ/(1−κ) · d(x₀, E(x₀)) → 0

Corollary 6.2 — Geometric convergence rate

$d(E^n(x_0), x^*) \leq \kappa^n \cdot d(x_0, x^*)$. With $\kappa \leq \sqrt{5/9} pprox 0.745$, convergence to $x^*$ is geometric at rate $pprox 25\%$ distance reduction per 12-step cycle.

The Spiral Return Theorem (Theorem T1)

Theorem T1 (Spiral Return) ✓ AXLE · Chain_updated.lean · 0 sorry

$G^{64}(x_0) eq x_0$ — the circuit is generative

There exists a SpiralReturn structure with $x_0' eq x_0$: the 64-step orbit does not return to its origin. The circuit is generative, not periodic.

theorem spiral_return_exists (G : GChain X) (x₀ : X)
    (h₁ : G.iter 64 x₀ ≠ x₀) (h₂ : G.iter 128 x₀ ≠ x₀) :
    ∃ sr : SpiralReturn X G, sr.x₀' ≠ sr.x₀

This theorem — proved in AXLE with 0 sorry — establishes that the GTCT circuit is not a closed loop. The orbit converges to $x^*$ (Theorem 6.1) but each 64-step circuit arrives at a new point, structurally equivalent to $x_0$ but distinct. The seed transforms; it does not repeat.

The Recursion Theorem [v2]