J_inv_phi_sq_pos
plain-language theorem explainer
The theorem establishes that the recognition cost J applied to one over phi squared is strictly positive. Domain certificates in the master chain cite it to satisfy the recovery-positivity clause of the six-clause J-band template. The tactic proof unfolds J, invokes the phi-squared bounds lemma together with phi positivity, rewrites the reciprocal, and closes the resulting inequality by field simplification followed by linarith.
Claim. Let $J(x) := (x + x^{-1})/2 - 1$. Then $J(1/phi^2) > 0$.
background
The module supplies reusable identities for the canonical recognition cost so that domain certificates need not reprove them. J is defined by J(x) = (x + x^{-1})/2 - 1. The six-clause template requires matched-zero at 1, nonnegativity for positive arguments, reciprocity, strict positivity off the match point, positivity at phi, and a numerical band around that value. The present result supplies the recovery-positivity clause for the inverse golden step. Upstream, the lemma phi_squared_bounds states that phi squared lies between 2.5 and 2.7, which is used to guarantee the sign after algebraic reduction.
proof idea
The proof unfolds the definition of J. It obtains 0 < phi from Constants.phi_pos and 0 < phi^2 from pow_pos. It retrieves the interval bounds via phi_squared_bounds, rewrites the reciprocal of 1/phi^2 as phi^2, shows that (phi^2 - 1)^2 is strictly positive by nlinarith, divides by phi^2 to obtain a positive quantity, equates the result to the expanded form phi^2 + 1/phi^2 - 2 by field_simp and ring, and closes the target inequality by linarith.
why it matters
This theorem supplies the recovery_pos field inside the CanonicalCert structure defined later in the same module. The certificate is the reusable six-clause object consumed by B-tier whole-science openings and the forty-something domain certificates. It therefore anchors the positivity-off-match clause for the inverse golden ratio step that appears throughout the phi-ladder constructions and the Recognition Composition Law. The result closes one concrete instance of the J-uniqueness identity (T5) inside the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.