J_phi_band
plain-language theorem explainer
J(φ) lies strictly between 0.11 and 0.13 under the Recognition Science cost function. Domain certificates and acoustics models cite this bound to close the golden-step clause without repeating the arithmetic. The proof reduces the claim to linear arithmetic after substituting the reciprocal identity obtained from φ² = φ + 1 and applying the supplied numerical bounds on φ.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. Then $0.11 < J(φ) < 0.13$, where φ satisfies φ² = φ + 1 and 1.61 < φ < 1.62.
background
The function J is the canonical recognition cost, defined by J(x) = (x + x^{-1})/2 - 1. This module supplies the six-clause template for J-cost on ratios, including the golden-step band for φ. Upstream lemmas establish the key identities: φ² = φ + 1, φ > 1.61, and φ < 1.62.
proof idea
The proof unfolds the definition of J, invokes phi_sq_eq to obtain φ² = φ + 1, derives the reciprocal φ⁻¹ = φ - 1 by algebraic manipulation, and then applies linarith to the two inequalities using the bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
why it matters
This result supplies the phi_band clause for the CanonicalCert definition and is invoked directly by therapy_window_in_band to place the therapy J-cost in the same interval. It completes the golden-step-band item in the six-clause J-cost template. The bound supports the T5 J-uniqueness and the phi-ladder constructions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.