phi_inv2_gt
plain-language theorem explainer
The inequality supplies a concrete lower bound of 0.381 on the square of the reciprocal golden ratio. Numerics work in the Recognition Science phi-ladder cites it when chaining lower estimates for odd powers of φ^{-1} that enter mass formulas. The proof is a short algebraic reduction that invokes the prior bound on φ^{-1}, records its positivity, and closes via nlinarith on the non-negative square term.
Claim. $0.381 < (φ^{-1})^2$ where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio φ = (1 + √5)/2 by starting from the elementary inequalities 2.236² < 5 < 2.237² and deriving the interval 1.618 < φ < 1.6185, with tighter versions obtained by carrying more decimal places. The upstream theorem phi_inv_gt establishes the base lower bound 0.618 < φ^{-1} by rewriting φ^{-1} via its closed form and applying linarith to the already-proved bound phi_gt_1618. This declaration squares that base bound while preserving the inequality direction.
proof idea
The proof obtains the base inequality via the upstream result phi_inv_gt, records the positivity fact 0 < φ^{-1} from inv_pos.mpr goldenRatio_pos, and finishes with a single nlinarith application that incorporates the non-negative square sq_nonneg goldenRatio^{-1}.
why it matters
The result feeds directly into the proofs of phi_inv3_gt and phi_inv5_gt, which accumulate the numerical anchors required for the Recognition Science mass formula on the phi-ladder. It supplies concrete lower estimates for powers of φ^{-1} that appear in J-cost and defectDist calculations, supporting the self-similar fixed-point property of φ in the T6 step of the forcing chain. No open scaffolding is discharged here; the declaration simply tightens the interval arithmetic used by later numerics lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.