Jcost_phi_val
plain-language theorem explainer
The lemma supplies the exact evaluation J(φ) = φ - 3/2 for the golden-ratio fixed point. Cosmologists and materials scientists cite it when anchoring cross-section bands or energy deviations inside Recognition Science models. The proof rewrites Jcost via its squared-ratio form, inserts the quadratic identity φ² = φ + 1, and closes the equality with division clearing plus nonlinear arithmetic.
Claim. The J-cost evaluated at the golden ratio satisfies $J(φ) = φ - 3/2$.
background
In Recognition Science the J-cost quantifies deviation from self-similarity and admits the closed form J(x) = (x + x^{-1})/2 - 1, which rewrites as (x-1)^2/(2x) for x ≠ 0. The golden ratio φ is the unique positive root of x² - x - 1 = 0 and therefore obeys φ² = φ + 1. The present lemma lives inside the Constants module that assembles RS-native constants together with the fundamental time quantum τ₀ = 1 tick.
proof idea
The term proof first applies the squared-ratio identity Jcost_eq_sq under the hypothesis phi_ne_zero. It then records the quadratic relation phi_sq_eq. A division-equivalence step clears the remaining denominator, after which nlinarith on positivity of φ and the square identity discharges the goal.
why it matters
The exact value is invoked verbatim by jcost_phi_band to locate J(φ) inside (0.11, 0.13), by dmCrossSection_in_band for the dark-matter cross-section window, and by solarWindCost_at_parker for Parker-spiral energy balance. It therefore supplies the numerical anchor after T5 J-uniqueness and T6 phi fixed-point in the forcing chain, enabling the phi-ladder applications that appear throughout cosmology, astrophysics and materials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.