Pith. sign in
module module high

IndisputableMonolith.Constants.AlphaGenesis.PatternForcing

show as:
view Lean formalization →

Forces the unique positive root of $x^2=x+1$ to be $\varphi$, then installs that scale as the only admissible geometric pattern on the eight-tick ladder. Anyone deriving gap weights or the $\alpha$ dressing cites it for the T6 self-similarity step and the link from $\varphi$-ratios to the forced T9 measure. The argument is algebraic uniqueness plus matching against the canonical ladder and measure-forcing identities.

claimThe unique positive solution of $x^2 = x + 1$ is $\varphi$. On the eight-tick ladder the successive rung ratios equal $\varphi$, so the canonical $\varphi$-pattern is forced. That pattern multiplies the forced recognition measure, and the geometric gap weight equals $\sin(\cdot)$ times the forced measure factor.

background

Recognition Science fixes the cost $J$ and the self-similar scale before any coupling constant is assembled. T6 of the forcing chain states that the unique positive fixed point of the self-similarity equation $x^2 = x + 1$ is the golden ratio $\varphi$. The eight-tick octave (period $2^3$) is already forced by T7; the ladder of recognition rungs therefore carries a discrete geometric progression whose common ratio must be identified.

Upstream, GapWeight.Formula supplies the canonical $\varphi$-pattern used in mass and coupling weights, while MeasureForcing (T9) answers which weighting sits on the allowed recognition states once the shape of the law is fixed. This module sits between those two: it proves the pattern is not an input but the unique scale compatible with self-similarity on the eight-tick ladder, then multiplies it into the forced measure.

Constants are carried in RS-native units ($c=1$, $\hbar=\varphi^{-5}$, etc.). The local objects are the positive-root uniqueness lemma, the eight-tick ladder type, the canonical ladder, and certificates that the $\varphi$-pattern and its product with the forced measure are the only admissible choices.

proof idea

The module opens with a self-contained uniqueness proof that the positive root of $x^2=x+1$ is $\varphi$ (T6). It then defines the eight-tick ladder and shows successive rung ratios equal $\varphi$, so the geometric pattern on the ladder is forced. A short certificate packages that uniqueness. Downstream lemmas identify the pattern-times-forced-measure product and rewrite the geometric gap weight as a sine factor times that forced product, matching the spectral and gap-weight side of Alpha Genesis. Structure is definition-plus-uniqueness lemmas rather than a single long tactic script.

why it matters in Recognition Science

Alpha Genesis derives $\alpha^{-1}$ forward, mirroring the mass program. This module supplies the geometric $\varphi$-pattern that every later Alpha Genesis stage imports: the aggregator, calibration forcing (elimination of unit-linear-response as an input), the EM recognition-loop certificate (channel budget $4\pi\times 11$), and spectral forcing (the $\sin^2(k\pi/8)$ factor as DFT-8 spectrum of the one-step difference on the eight-tick cycle).

Without a forced pattern, gap weights and the dressing seed would remain modeling choices. By closing T6 on the ladder and tying the pattern to the T9 measure, the module removes that freedom before resummation and loop certificates run. It is the constants-side hinge between the Unified Forcing Chain and the fine-structure assembly.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (9)