Pith. sign in
module module moderate

IndisputableMonolith.Verification.PhiSelfSimilarityCert

show as:
view Lean formalization →

Verification module packaging a certificate that the golden ratio is the unique positive self-similar fixed point of the Recognition scaling law. Auditors of the T6 forcing step cite it to confirm φ satisfies φ = 1 + 1/φ and is the sole positive root of x² = x + 1. The argument is assembled from elementary real-algebra lemmas already proved in PhiSupport.

claimCertificate that $\varphi = (1+\sqrt{5})/2$ is the unique positive real satisfying the self-similarity fixed-point equation $\varphi = 1 + 1/\varphi$ (equivalently $\varphi^2 = \varphi + 1$).

background

Recognition Science forces the dimensionless scale factor of the theory to be the golden ratio $\varphi$. In the forcing chain this is step T6: self-similarity of the cost functional selects the unique positive fixed point of $x \mapsto 1 + 1/x$.

The supporting algebra lives in PhiSupport.Lemmas: Mathlib's identity $\varphi^2 = \varphi + 1$, the rearranged fixed-point form $\varphi = 1 + 1/\varphi$, and uniqueness of the positive root of $x^2 = x + 1$. Those facts use only elementary real arithmetic.

This verification module sits in the certificate layer. It does not re-prove the algebra; it packages the self-similarity claim in the form expected by downstream audit and export tooling.

proof idea

Definition-and-certificate module rather than a deep proof development. It imports the golden-ratio support lemmas and exposes a named certificate object asserting φ-self-similarity. The underlying equalities are one-line appeals to Mathlib's Real.goldenRatio_sq and the uniqueness lemma for the positive root of $x^2-x-1=0$; no new analytic work occurs here.

why it matters in Recognition Science

Closes the verification surface for T6 (φ forced as the self-similar fixed point) in the Recognition forcing chain. Downstream mass-ladder, eight-tick, and coupling-constant certificates rely on φ being uniquely pinned; this module is the audit handle that those layers can cite without re-opening the real-algebra development. With no further used-by edges recorded yet, it functions as a leaf certificate ready for export into the global consistency report.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)