jcost_phi_pos
plain-language theorem explainer
The result shows that the J-cost evaluated at the golden ratio is strictly positive. Researchers modeling the Hubble tension within Recognition Science cite it to bound the predicted amplitude J(φ) log 2. The proof is a one-line wrapper that invokes the general positivity lemma for the J-cost function at any positive argument not equal to one.
Claim. $0 < Jcost(φ)$ where $φ$ is the golden ratio and $Jcost$ is the J-cost function satisfying $Jcost(x) = (x - 1)^2 / (x (x + 1))$ for $x > 0$.
background
J-cost is defined so that $Jcost(x) > 0$ whenever $x > 0$ and $x ≠ 1$, as stated in the upstream lemma Jcost_pos_of_ne_one. The golden ratio $φ$ satisfies $φ ≠ 1$ by the lemma phi_ne_one imported from Constants and from PhiLadderLattice. The present module sits inside the Hubble Tension from BIT development, whose module documentation states that RS predicts the tension amplitude $H_0^{local}/H_0^{CMB} - 1 = J(φ) × log 2 ∈ (0.075, 0.091)$.
proof idea
One-line wrapper that applies the lemma Jcost_pos_of_ne_one to the specific arguments phi, phi_pos and phi_ne_one.
why it matters
The declaration supplies the positivity fact required to place J(φ) inside the open interval (0.11, 0.13) used by the sibling results hubbleTensionAmplitude and hubble_tension_pos. It thereby closes one step in the chain that derives the RS prediction for the Hubble tension amplitude from the J-uniqueness property (T5) and the forcing of φ as self-similar fixed point (T6). No open scaffolding remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.