Pith. sign in
module module moderate

IndisputableMonolith.Verification.Necessity.PhiNecessity

show as:
view Lean formalization →

Module packaging the minimal self-similarity axioms that force the golden ratio as the unique preferred scale. A verification or foundations reader cites it for the T6 step: self-similarity plus a positive fixed scale yields φ. The argument chains discrete self-similarity into a fixed-point equation whose only positive solution is φ.

claimUnder a minimal self-similarity structure on a positive preferred scale $s$, one has $s = 1 + 1/s$, hence $s = \varphi := (1+\sqrt{5})/2$, the unique positive root of $x^2 = x + 1$.

background

Recognition Science forces the dimensionless scale factor $\varphi$ as the unique self-similar fixed point (forcing chain T6). The cost functional $J$ and the Recognition Composition Law already single out multiplicative structure; self-similarity then pins the numerical value of the rung ratio.

This module sits in the Verification/Necessity layer. It imports RS constants (including the native tick $\tau_0$) and the elementary golden-ratio support lemmas: $\varphi^2 = \varphi + 1$, the fixed-point identity $\varphi = 1 + 1/\varphi$, and uniqueness of the positive root of $x^2 = x + 1$. Those facts depend only on real algebra and Mathlib's goldenRatio API.

The local notion is a bare self-similarity interface (a positive preferred scale closed under the discrete doubling/halving that the eight-tick octave later uses). No continuum limit or full J-calculus is required at this stage.

proof idea

The module is theorem-bearing, not a pure definition file. It introduces a minimal self-similarity predicate, derives positivity of the preferred scale, obtains the fixed-point relation $s = 1 + 1/s$ from discrete self-similarity, and invokes the uniqueness lemma for the positive root of $x^2 = x + 1$ to conclude $s = \varphi$. Downstream named results package the same chain as "self-similarity forces $\varphi$" and "$\varphi$ is mathematically necessary."

why it matters in Recognition Science

Closes the T6 landmark: $\varphi$ is forced as the self-similar fixed point once a positive preferred scale exists. That value propagates into every RS-native constant ($\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$, the mass ladder yardstick $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, Berry threshold $\varphi^{-1}$, $Z_{\mathrm{cf}} = \varphi^5$). The module supplies the necessity certificates that later verification and inevitability pipelines quote when they claim $\varphi$ is not an empirical fit. No external used-by edges are recorded on the page; the sibling theorems themselves are the export surface for the rest of the monolith.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)