cert_inhabited
plain-language theorem explainer
The Logo5 certificate packing diagonal vanishing, nonnegativity of the domain cost, and positivity of the canonical threshold is inhabited. Anyone citing the absolute final Logo5 structural package uses this existence fact. The proof is a one-line term witness introducing the prebuilt certificate record.
Claim. There exists a certificate packing three properties of the recognition domain cost: (i) for every nonzero real $r$, the cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module packages the Recognition Science logo curve $J(x)=(x+1/x)/2-1$ on $(0,\infty)$. That cost has a unique minimum $J(1)=0$ and rises to $J(\varphi)$ at the golden ratio; the module presents this single curve as the structural core of the framework (zero sorry, zero axiom).
The domain cost is the two-argument form of that $J$-cost used on positive reals. The certificate structure bundles three elementary facts: the cost vanishes on the diagonal away from zero, it is nonnegative on the positive quadrant, and a fixed positive threshold (the canonical threshold) sits above zero. Those three fields are exactly the content of the certificate type whose inhabitance is asserted here.
proof idea
One-line term proof. The certificate record cert already assembles the three field proofs (diagonal vanishing, nonnegativity, threshold positivity). The theorem simply packages that record as a witness for Nonempty, via the standard constructor ⟨cert⟩. No further tactics or lemmas are invoked.
why it matters
This is the inhabitance seal on the Logo5 structural package: once the certificate type is known to be nonempty, downstream consumers can treat the three logo properties as a single inhabited bundle rather than three separate lemmas. The module frames the package as the absolute final Logo5 session, identifying the $J$-curve itself with Recognition Science.
In the forcing chain this sits at the T5 landmark (uniqueness of $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$). The certificate does not itself force $\varphi$, the eight-tick octave, or $D=3$, but it freezes the cost-function side of that chain in a zero-sorry form. No downstream users are recorded yet; the declaration is the terminal inhabitance fact of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.