J_phi_pos
plain-language theorem explainer
J_phi_pos proves that the J-cost evaluated at the golden ratio is strictly positive. Researchers building the phi-ladder mass hierarchy or the Canonical J-band certificate cite it to confirm that the identity state is the unique zero-cost ground state. The proof is a short term-mode reduction that rewrites the definition via the squared-ratio identity for Jcost and splits positivity across numerator and denominator using standard real-arithmetic lemmas.
Claim. $0 < J(φ)$ where $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$.
background
The J-cost function quantifies departure from the identity element in the Recognition framework. It is defined by J(x) = (x + x^{-1})/2 - 1 and admits the equivalent squared form J(x) = (x-1)^2/(2x) for x ≠ 0. In the Spectral Emergence module this cost is applied to phi-ratio edges on the ladder generated from D = 3 and the binary cube Q₃.
proof idea
The proof unfolds J_phi to Jcost phi, rewrites via Jcost_eq_sq (using phi ≠ 0), then applies div_pos. The numerator positivity follows from sub_ne_zero on phi - 1 together with positivity; the denominator positivity follows from linarith on phi_pos.
why it matters
This theorem supplies the phi_pos clause inside the CanonicalCert structure that is consumed by SchumannResonanceCert and the J-band certification. It directly instantiates the claim that departure from unity always costs, a necessary step after T6 forces phi as the self-similar fixed point. The result is invoked whenever the master certificate must certify that the ground state remains unique.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.