PatternForcingCert
plain-language theorem explainer
Bundles the Alpha Genesis M2 pattern-forcing certificate: every admissible eight-tick ladder equals φ^n, the GapWeight φ-pattern is that ladder on the eight-tick window, pattern and forced measure are reciprocal tick-by-tick, and geometric spectral weight equals sin²(kπ/8) times forced lattice weight. Cited by anyone discharging the no-fit “canonical φ-pattern” choice. Verification is a four-conjunct refine applying the four forcing lemmas.
Claim. A pattern-forcing certificate is a unit inhabitant whose verification predicate asserts four claims: (i) every eight-tick ladder $L$ satisfies $L.u(n)=\varphi^n$ for all $n\in\mathbb{N}$; (ii) the GapWeight $\varphi$-pattern at each tick $t\in\{0,\ldots,7\}$ equals $L.u(t)$ for every such ladder; (iii) $\varphi$-pattern$(t)$ times the forced lattice weight at $t$ equals $1$ for every tick; (iv) for every nonzero mode $k$, geometric weight equals $\sin^2(k\pi/8)$ times forced lattice weight at $k$.
background
Alpha Genesis M2 treats the φ-pattern consumed by the w₈ spectral projection as forced, not chosen. An eight-tick ladder is a sequence u : ℕ → ℝ with unit base u(0)=1, constant positive step ratio, and self-similar ratio r² = r + 1 (the T6 fixed-point equation), indexed on the T7 eight-tick carrier.
The module’s reciprocity structure pairs two displays of one object: the time-domain growth pattern φᵗ and the spectral decay envelope φ⁻ᵏ. Their product is identically 1 tick by tick, which is the ledger J-symmetry J(x)=J(1/x) written in display form. The forced measure itself comes from Foundation.MeasureForcing (T9 recognition weight).
Upstream, pattern_forced proves every admissible ladder is exactly φⁿ by induction on the step and ratio_eq_phi. phiPattern_is_forced identifies GapWeight.phiPattern with that ladder on Fin 8. pattern_mul_forced_measure is the reciprocity identity. geometricWeight_eq_sin_mul_forced_measure equates the spectral decay envelope inside geometricWeight to sin²(kπ/8) times latticeWeight.
proof idea
The structure is a bare inhabited unit. The content lives in the simp predicate verified, a four-way conjunction, and in verified_any, which proves the predicate for every certificate.
verified_any is a one-line-per-conjunct refine: intro the ladder and n, apply pattern_forced; intro ladder and tick, apply phiPattern_is_forced; discharge reciprocity by pattern_mul_forced_measure; discharge the envelope identity by geometricWeight_eq_sin_mul_forced_measure. No new algebra is done at the certificate layer.
why it matters
This is the M2 closure bundle for Alpha Genesis. The module doc states the theorem: any eight-tick ladder with unit base, constant positive step, and T6 self-similarity is exactly φᵗ, and the decay envelope φ⁻ᵏ inside the spectral weight is the T9 forced measure term for term. That discharges discrete choice (ii) of the no-fit proposition (the “canonical φ-pattern” choice): the pattern is forced by T6 given the T7 carrier, and its conjugate envelope is the unique forced measure.
Framework landmarks in play are T6 (φ as self-similar fixed point), T7 (eight-tick octave), and the MeasureForcing lattice weight. Reciprocity pattern · forcedMeasure = 1 is the cost/weight form of J-symmetry. STATUS target is theorem with zero sorry and no CODATA. used_by is currently empty; the certificate is the export surface for downstream α-genesis and gap-weight consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.