Jcost_phi_bounds
plain-language theorem explainer
The theorem proves that the J-cost evaluated at the golden ratio φ satisfies 0.11 < J(φ) < 0.12. Cosmologists modeling the σ₈ tension would cite this bound when quantifying recognition strain Q accumulated over eight-tick cycles. The argument obtains tight bounds on φ and 1/φ from prior lemmas on the golden ratio, sums them, and reduces the resulting inequality via linear arithmetic after unfolding the J-cost definition.
Claim. $0.11 < J(φ) < 0.12$, where $J(x) = (x + x^{-1})/2 - 1$ and φ is the golden ratio.
background
The module resolves the σ₈ tension between Planck CMB (≈0.811) and weak lensing (≈0.76) via recognition strain Q that suppresses growth below the λ_8 scale set by eight-tick neutrality. The J-cost is defined by J(x) = (x + x^{-1})/2 - 1. This numerical bound on J(φ) supplies the strain_scale component of the verified suppression certificate.
proof idea
The tactic proof invokes one_lt_phi for 1 < φ and phi_pos for positivity. It applies phi_lt_two to obtain φ < 1.62 and derives 1.61 < φ from phi_gt_one_and_half plus linarith. Reciprocal bounds are obtained via div_lt_div_of_pos_left, the sum φ + 1/φ is sandwiched by linarith, and the claim follows by simp only [Jcost] followed by constructor and linarith.
why it matters
This supplies the strain_scale field inside sigma8Suppression_verified, which certifies that the predicted σ₈ matches observations to within 2σ. It instantiates the recognition strain arising from the eight-tick octave (T7) and the self-similar fixed point φ (T6), closing the numerical link from J-uniqueness (T5) to the cosmology module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.