canonicalLadder
plain-language theorem explainer
The map n ↦ φⁿ is exhibited as a concrete eight-tick ladder: unit base, constant positive ratio φ, geometric steps, and T6 self-similarity φ² = φ + 1. It is the non-vacuity witness that the EightTickLadder structure is inhabited. Anyone citing pattern forcing or uniqueness of the φ-pattern needs this existence half. Construction is a structure instance filled by golden-ratio identities and ring/norm_num.
Claim. The sequence $u_n = \varphi^n$ defines an eight-tick ladder pattern: base $u_0 = 1$, constant step ratio $r = \varphi > 0$, recurrence $u_{n+1} = r\, u_n$ for all $n$, and self-similarity $r^2 = r + 1$ (the T6 fixed-point equation).
background
Module Alpha Genesis M2 (Pattern Forcing) shows that the time-domain φ-pattern consumed by the w₈ spectral weight is not a free choice. An eight-tick ladder is a sequence u : ℕ → ℝ with unit base u(0) = 1, a single positive step ratio r, the geometric recurrence u(n+1) = r·u(n), and the T6 self-similarity constraint r² = r + 1. The carrier is the T7 eight-tick window (indexed by ℕ, read at Fin 8).
The golden ratio φ is the positive root of x² − x − 1 = 0; the upstream identity φ² = φ + 1 is exactly that equation rewritten. The module pairs this growth display with the reciprocal spectral envelope φ⁻ᵏ (the T9 forced measure), linked by J-symmetry J(x) = J(1/x).
This definition supplies one concrete ladder so later uniqueness theorems are not vacuous.
proof idea
Structure-instance construction, not a tactic proof. The pattern field is u(n) = φⁿ. Base u(0) = 1 is discharged by norm_num. The ratio field is set to φ, with positivity from the library fact φ > 0. The step obligation (geometric recurrence) is closed by ring. Self-similarity is exactly the upstream lemma φ² = φ + 1.
why it matters
In the Recognition forcing chain, T6 forces φ as the self-similar fixed point and T7 fixes the eight-tick octave. This witness shows the EightTickLadder axioms are satisfiable, so the module's uniqueness claim (any such ladder equals φᵗ) has a model. That uniqueness discharges discrete choice (ii) of the no-fit proposition: the canonical φ-pattern is forced, not fitted.
The same object underwrites the reciprocity story in the module doc: pattern · forcedMeasure = 1 tick by tick, so the growth display and the decay envelope are conjugate faces of one ledger symmetry rather than independent inputs. Sibling results (pattern forced, φ-pattern is forced, pattern times forced measure) sit on top of this inhabited structure. STATUS target for the file is theorem with zero sorry and no CODATA.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.