IndisputableMonolith.Support.PhiApprox
The PhiApprox module supplies coarse numerical bounds on the golden ratio φ for use in Recognition Science numerics. Downstream approximation code cites these lemmas to avoid symbolic overhead or high-precision libraries. The module structure is four direct inequality lemmas plus one stub, all relying on elementary real comparisons.
claim$\sqrt{5} > 2.2$, $\sqrt{5} < 2.4$, $1.6 < \phi < 1.7$, together with a placeholder stub for refined bounds on $\phi$.
background
Recognition Science forces φ as the unique positive fixed point of the self-similar map arising from J-uniqueness (T5) and the composition law. The module imports Constants, whose sole documented object is the RS time quantum τ₀ = 1 tick, and Mathlib for real-number infrastructure.
The supplied siblings implement the concrete bounds via direct comparison; the module doc-comment states their intended role as coarse estimates for downstream numerical work.
proof idea
This is a support module providing inequality lemmas; the argument consists of four independent direct comparisons with no shared sub-lemmas or advanced tactics.
why it matters in Recognition Science
The module supplies the numerical interface for φ, the self-similar fixed point forced at T6, so that numerics modules can proceed without waiting for exact symbolic results. Its doc-comment explicitly marks it as input to downstream approximation code; no used-by edges are recorded yet.
scope and limits
- Does not derive φ from the forcing chain or J-cost equation.
- Does not supply error bounds or propagation rules for the approximations.
- Does not connect the numerical interval to constants such as α or G.
- Does not replace the exact phi definition used in the main theory.