Pith. sign in
module module moderate

IndisputableMonolith.Verification.PhiNonDegenerateCert

show as:
view Lean formalization →

Verification certificate that the RS self-similar scale φ is non-degenerate (strictly greater than 1, cost and ladder do not collapse). Downstream verification and constant-export code cite it to justify φ-powers and J-evaluations. The module is a thin packaging layer over Constants, not a deep existence proof.

claimA verification certificate that the Recognition Science scale $\varphi$ (self-similar fixed point of the forcing chain) is non-degenerate: $\varphi \neq 1$, the $J$-cost stays strictly positive away from $1$, and $\varphi$-ladder steps remain invertible.

background

Recognition Science forces a unique dimensionless scale $\varphi$ as the self-similar fixed point of the Recognition Composition Law and the $J$-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T6). Non-degeneracy means that fixed point is not the trivial root $x=1$ where $J$ vanishes, so geometric powers $\varphi^r$ and eight-tick octave structure stay well-defined.

This module lives in the Verification domain. It imports Mathlib and IndisputableMonolith.Constants, whose module doc records the RS time quantum $\tau_0=1$ tick and the native constant suite. The certificate is the named object PhiNonDegenerateCert exposed by the module.

proof idea

Certificate/definition module rather than a long tactic development. It packages non-degeneracy facts already available from Constants (and Mathlib inequalities on the golden-ratio fixed point) into a single verification-facing certificate. No independent forcing argument is re-derived here; the structure is export and naming for downstream checks.

why it matters in Recognition Science

Non-degenerate $\varphi$ is a prerequisite for the $\varphi$-ladder mass formula, the eight-tick octave (T7), and any claim that uses $\varphi^{\pm n}$ or $J(\varphi^k)$. The module sits in Verification so audit and export layers can point at one certificate instead of ad-hoc inequalities. The dependency graph currently lists no used_by edges, so it is an available cert rather than a node already wired into a parent theorem on this page. It supports the T5–T6 uniqueness story without reopening the full UnifiedForcingChain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)