cert
plain-language theorem explainer
The definition cert assembles the reusable CanonicalCert structure for the J-cost band by supplying five pre-proven identities. Domain certs across the master chain cite it to inherit the phi-band properties without re-deriving them. It is a direct structure constructor that delegates each clause to a sibling theorem in the same module.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. The canonical certificate cert is the structure satisfying $J(1) = 0$, $J(x) = J(1/x)$ for all $x > 0$, $J(phi) > 0$, $0.11 < J(phi) < 0.13$, and $J(1/phi^2) > 0$, where $phi$ denotes the golden ratio.
background
The module CanonicalJBand supplies a reusable six-clause template for J-cost certificates. Each domain cert must prove matched-zero at 1, reciprocal symmetry, positivity off the match point, golden-step positivity, the numerical band (0.11, 0.13), and recovery positivity at $1/phi^2$. The structure CanonicalCert packages exactly these five fields (non-negativity is handled upstream). J itself is the cost function imported from CostAlgebra, where J_reciprocal encodes the algebraic double-entry symmetry $J(x) = J(x^{-1})$ for $x > 0$.
proof idea
The definition is a one-line structure constructor. It maps matched_zero to the sibling theorem J_one, reciprocal to J_reciprocal, phi_pos to J_phi_pos, phi_band to J_phi_band, and recovery_pos to J_inv_phi_sq_pos. No tactics or reductions occur beyond field assignment.
why it matters
cert supplies the single reusable instance of CanonicalCert that every downstream domain certificate imports to satisfy the master-chain template. It closes the phi-side identities once, so B-tier openings and Plan v7 domain certs need only define their own ratio. The construction directly supports the J-uniqueness step (T5) and the self-similar fixed-point step (T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.