IndisputableMonolith.Verification.PhiDecimalBoundsCert
Certification module for rigorous decimal bounds on the Recognition Science constant φ (the self-similar fixed point). Supplies machine-checkable inequalities that pin φ between explicit rationals so downstream numeric and mass-ladder arguments stay exact. Imports only Mathlib and the Constants layer; the argument is a short verified-arithmetic certificate, not a deep existence proof.
claimThe module packages certified rational bounds on the RS constant $\varphi$ (golden-ratio fixed point), of the form $a < \varphi < b$ with explicit $a,b\in\mathbb{Q}$, together with any supporting lemmas needed to discharge decimal comparisons in verification code.
background
Recognition Science forces a unique dimensionless scale factor $\varphi$ as the self-similar fixed point of the cost functional (forcing step T6). In RS-native units every rung of the mass ladder, the eight-tick period, and several coupling normalizations are powers of $\varphi$. Numeric claims therefore need tight, fully proved decimal enclosures rather than floating-point approximations.
The Constants import supplies the ambient RS units (including the fundamental tick $\tau_0=1$). This verification module sits above that layer and only adds certified inequalities that pin the decimal expansion of $\varphi$ between explicit rationals, so later certificates can rewrite inequalities without leaving the type-checked kernel.
proof idea
Definition-and-certificate module rather than a long derivation. It introduces a named certificate object (PhiDecimalBoundsCert) whose fields are the rational lower and upper bounds together with proofs that those rationals sandwich $\varphi$. The proofs are short verified-arithmetic reductions (Mathlib inequality tactics or norm_num-style evaluation) against the closed-form definition of $\varphi$ already present in Constants. No new analytic existence argument is given; the work is purely to lock decimal digits for downstream use.
why it matters in Recognition Science
Downstream verification and mass-ladder certificates need concrete decimal digits of $\varphi$ while remaining fully proved. This module is the single place those digits are locked, so every later claim that writes "$\varphi\approx 1.618\ldots$" can cite a kernel-checked enclosure instead of an axiom. It does not itself appear in the T0–T8 forcing chain; it is infrastructure that keeps numeric corollaries (alpha-band checks, rung comparisons, Berry-threshold inequalities) honest. With an empty used-by list in the current graph it is a leaf certificate ready for import by any verification script that compares powers of $\varphi$ against rationals.
scope and limits
- Does not redefine or re-derive φ; assumes the Constants definition.
- Does not prove uniqueness or forcing of φ (that is T5–T6).
- Does not supply floating-point or interval-arithmetic tactics beyond the stated rational bounds.
- Does not bound derived constants (α, masses, G) except insofar as they reduce to powers of φ.
- Does not claim the bounds are optimal; only that they are proved.