J_phi_pos
plain-language theorem explainer
The theorem shows that the recognition cost evaluated at the golden ratio is strictly positive. Domain certificates in astrophysics and spectral emergence cite it to confirm that departure from unity always incurs positive cost. The proof is a short tactic sequence that unfolds the definition, substitutes the quadratic identity to obtain the inverse, and closes with linear arithmetic against the bound greater than 1.5.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. Then $J(phi) > 0$, where $phi = (1 + sqrt(5))/2$ satisfies $phi^2 = phi + 1$.
background
The module supplies reusable identities for the six-clause J-cost template used in every domain certificate. Clause 5 requires J(phi) > 0. The definition J(x) = (x + x^{-1})/2 - 1 is the canonical recognition cost that vanishes only at unity and is symmetric under inversion. Upstream lemmas supply the two arithmetic facts needed: phi^2 = phi + 1 and the tighter bound phi > 1.5.
proof idea
Unfold the definition of J. Obtain phi^2 = phi + 1 from Constants.phi_sq_eq and phi > 0 from the constants bundle. Derive the inverse identity phi^{-1} = phi - 1 by showing the product equals 1 and clearing the denominator. Rewrite the expression and close with linarith against the bound phi > 1.5.
why it matters
This supplies the golden-step-positive clause inside the CanonicalCert structure that every domain certificate reuses. It is invoked by the Schumann resonance master certificate and by the empirical band checks in astrophysics; the same statement reappears in SpectralEmergence. It directly supports the positivity-off-match requirement in the master cert chain and aligns with J-uniqueness in the forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.