phi_inv2_gt
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 in Recognition Science
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.
scope and limits
- Does not supply an upper bound on (φ^{-1})^2.
- Does not relate the numerical bound to physical constants such as α or G.
- Does not generalize the inequality beyond the real numbers.
- Does not prove the exact algebraic closed form of φ^{-1}.
Lean usage
have h2 := phi_inv2_gtformal statement (Lean)
409theorem phi_inv2_gt : (0.381 : ℝ) < goldenRatio⁻¹ ^ 2 := by
proof body
Term-mode proof.
410 have h := phi_inv_gt
411 have hpos : 0 < goldenRatio⁻¹ := inv_pos.mpr goldenRatio_pos
412 nlinarith [sq_nonneg goldenRatio⁻¹]
413