EightTickLadder
plain-language theorem explainer
An eight-tick ladder is a geometric sequence on ℕ with unit base, positive constant step ratio, and self-similar ratio obeying r² = r + 1 (the T6 equation). Pattern-forcing and Alpha Genesis certificates cite it as the admissible-pattern type on the T7 carrier. It is a pure structure definition: the fields are the axioms, with no proof body.
Claim. An eight-tick ladder is a sequence $u:\mathbb{N}\to\mathbb{R}$ together with a ratio $r\in\mathbb{R}$ such that $u(0)=1$, $r>0$, $u(n+1)=r\cdot u(n)$ for every $n$, and $r^{2}=r+1$.
background
Module Alpha Genesis M2 (Pattern Forcing) shows that the time-domain φ-pattern consumed by the w₈ spectral projection is not a free choice. Any ladder with unit base, constant positive step, and T6 self-similarity is exactly φⁿ, and its conjugate decay envelope is the T9 forced measure.
The structure packages those admissibility axioms. The carrier is the T7 eight-tick window (ℕ indices, later restricted to Fin 8). Self-similarity is the T6 fixed-point equation r² = r + 1, whose unique positive root is φ. Upstream constants supply the fundamental tick τ₀ = 1 and the identity event at the J-cost minimum x = 1; the geometric step is the discrete one-step extension of the recognition calculus.
Reciprocity in the module pairs the growth display φᵗ with the weight display φ⁻ᵏ: pattern · forcedMeasure = 1 tick by tick, the ledger J-symmetry J(x) = J(1/x).
proof idea
No proof: this is a structure definition. The fields are the mathematical content (sequence, unit base, positive ratio, constant-ratio recurrence, T6 self-similarity). Downstream lemmas such as ratio_eq_phi discharge uniqueness of the positive root, and pattern_forced inducts on the recurrence once the ratio is identified with φ.
why it matters
This is the admissible-pattern type for M2. Downstream, ratio_eq_phi identifies every ladder ratio with φ; pattern_forced concludes u(n) = φⁿ for all n; canonicalLadder supplies the non-vacuous witness u(n) = φⁿ; phiPattern_is_forced equates GapWeight.phiPattern on Fin 8 with any such ladder. PatternForcingCert bundles those facts (every admissible ladder is φᵗ; pattern and forced measure are reciprocal). AlphaGenesisCert consumes the same forcing as item (2) of the forward α derivation.
Framework landmarks: T6 (φ as self-similar fixed point) and T7 (eight-tick octave). The structure discharges discrete choice (ii) of the no-fit proposition: the canonical φ-pattern is forced by T6 on the T7 carrier, not fitted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.