cert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove non-negativity of J on all positive reals.
- Does not define the cost function J or its algebraic properties.
- Does not establish the band bounds for any domain-specific ratio.
- Does not discharge any hypothesis_interface or scaffolding stub.
formal statement (Lean)
84def cert : CanonicalCert where
85 matched_zero := J_one
proof body
Definition body.
86 reciprocal := J_reciprocal
87 phi_pos := J_phi_pos
88 phi_band := J_phi_band
89 recovery_pos := J_inv_phi_sq_pos
90
91end
92
93end CanonicalJBand
94end Common
95end IndisputableMonolith