IndisputableMonolith.Support.PhiApprox
This module supplies coarse numerical bounds on the golden ratio φ for use in downstream numerics. Researchers performing approximate phi-ladder or mass calculations in Recognition Science would cite it. The module consists of short lemmas establishing inequalities on sqrt(5) that immediately yield 1.6 < φ < 1.7.
claimCoarse bounds: $2.2 < 5^{1/2} < 2.4$, hence $1.6 < (1 + 5^{1/2})/2 < 1.7$.
background
Recognition Science forces φ as the unique positive fixed point of the self-similar map at step T6 of the UnifiedForcingChain. The module imports Constants, whose sole content is the RS time quantum τ₀ = 1 tick. These coarse bounds on φ therefore sit between the exact algebraic definition of φ and the numerical work required for the phi-ladder mass formula.
proof idea
This is a collection of short lemmas. Each applies Mathlib real-number tactics (norm_num, linarith, or field_simp) to verify the elementary inequalities sqrt(5) > 2.2, sqrt(5) < 2.4, and the two resulting bounds on φ.
why it matters in Recognition Science
The bounds close the gap between the exact φ definition and practical numerics required by downstream modules that implement the phi-ladder and mass formulas. The module doc-comment states they are intended precisely for such downstream numerics modules.
scope and limits
- Does not supply high-precision decimal expansions of φ.
- Does not prove any relation involving the Recognition Composition Law.
- Does not connect φ bounds to constants α or G.
- Does not address the Berry creation threshold or Z_cf.