CanonicalCert
plain-language theorem explainer
CanonicalCert packages five properties of the recognition cost function J into a reusable structure for domain certificates. Researchers in acoustics, astronomy, astrophysics, and chemistry cite it to anchor J-cost thresholds without re-proving core identities. The declaration is introduced as a bare structure definition with no attached proof body or lemmas.
Claim. A structure requiring that the function $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(1) = 0$, $J(x) = J(1/x)$ for all nonzero real $x$, $J(phi) > 0$, $0.11 < J(phi) < 0.13$, and $J(phi^{-2}) > 0$.
background
The Canonical J-Cost Band module supplies a reusable template for J-cost certificates across the master cert chain and B-tier whole-science openings. The core function is defined by $J(x) := (x + x^{-1})/2 - 1$. Upstream results include the reciprocal automorphism from CostAlgebra, which encodes the symmetry under inversion, and the reciprocal event from LedgerForcing, which realizes the same symmetry on recognition events.
proof idea
The declaration is a direct structure definition. No lemmas are applied and no tactics are used; the five fields are declared as the required properties of J.
why it matters
CanonicalCert supplies the common threshold reused by forty downstream domain certificates, including UltrasoundTherapyCert (five modalities), StellarEvolutionCert (five phases), AccretionDiskCert (five regimes), MagneticReconnectionCert (five regimes), and CatalysisCert (five mechanisms). It fills the reusable phi-band slot in the module template, anchoring the J-uniqueness step (T5) and the self-similar fixed point (T6) of the forcing chain for all domain applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.