sq_22360679_lt_5
plain-language theorem explainer
This theorem verifies the inequality (2.2360679)^2 < 5 over the reals. Numerics work in Recognition Science cites it to anchor lower bounds on sqrt(5) and therefore on the golden ratio phi. The proof is a direct norm_num evaluation of the floating-point square.
Claim. $(2.2360679)^2 < 5$
background
The module supplies rigorous decimal bounds on phi = (1 + sqrt(5))/2 by sandwiching sqrt(5) between successive approximations. The local strategy records that 2.236^2 < 5 < 2.237^2 implies 2.236 < sqrt(5) < 2.237 and therefore 1.618 < phi < 1.6185, with tighter versions obtained by adding decimal places. This specific bound belongs to the family of squared comparisons that tighten the interval for sqrt(5).
proof idea
One-line wrapper that applies norm_num to confirm the floating-point computation.
why it matters
The result is invoked directly by sqrt5_gt_22360679 to obtain 2.2360679 < sqrt(5). That step contributes the numerical scaffolding needed for the phi-ladder mass formula and the self-similar fixed-point property of phi in the T5-T6 segment of the forcing chain. It closes one concrete interval in the module's strategy for producing bounds inside the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.