J_phi_pos
plain-language theorem explainer
J(φ) > 0 holds under the canonical recognition cost for the golden ratio. Domain certificate authors in astrophysics and spectral emergence cite the result to close the golden-step-positive clause in their six-clause templates. The argument unfolds the cost definition, substitutes the reciprocal identity from the quadratic relation φ² = φ + 1, and reduces the inequality via a linear comparison with the bound φ > 1.5.
Claim. $J(φ) > 0$ where $J(x) := (x + x^{-1})/2 - 1$ and $φ = (1 + √5)/2$ is the golden ratio.
background
The module supplies reusable identities for the six-clause J-cost template that appears in every master certificate. J(x) is defined as the canonical recognition cost (x + 1/x)/2 - 1. The template requires matched-zero at unity, non-negativity for positive arguments, reciprocity, strict positivity off unity, positivity at φ, and a numerical band around that value. Upstream lemmas from Constants supply the quadratic identity φ² = φ + 1 and the tighter lower bound φ > 1.5; the same positivity statement is re-proved in SpectralEmergence for the J_phi abbreviation.
proof idea
The tactic proof unfolds the definition of J, applies phi_sq_eq to obtain the reciprocal identity φ^{-1} = φ - 1, then invokes linarith together with the bound φ > 1.5 to conclude the strict inequality.
why it matters
The result supplies the golden-step-positive clause inside CanonicalCert, which is consumed by SchumannResonanceCert to certify the resonance frequency band. It directly supports the framework claim that departure from unity always incurs positive cost, consistent with J-uniqueness in the forcing chain. The lemma is cited by both the empirical Schumann upper-bound theorem and the master certificate structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.