cert_inhabited
plain-language theorem explainer
The structural certificate packing diagonal vanishing, nonnegativity of domain cost, and positivity of the canonical threshold is inhabited. Anyone needing a concrete witness that the RS J-cost package is realizable cites this. The proof is a one-line term inhabitant built from the module's concrete certificate value.
Claim. The type of certificates asserting (i) domain cost vanishes on equal nonzero arguments, (ii) domain cost is nonnegative for positive mass and energy arguments, and (iii) the canonical threshold is strictly positive, is nonempty.
background
This module packages structural facts about the Recognition Science J-cost near the golden ratio. The module header states the target identity $J(\varphi)=\varphi-3/2\approx 0.11803$, the recognition cost at the self-similar fixed point forced by the T5--T6 chain.
Domain cost is the two-argument cost used on mass/energy pairs in this structural layer; the certificate requires it to vanish when both arguments equal a nonzero real, and to be nonnegative whenever both arguments are positive. The canonical threshold is a positive real cutoff tied to that cost geometry.
RSMTHStructural002Cert is the structure bundling those three propositions. Upstream, the structure itself only declares the fields; inhabitation is separate and is what this theorem supplies.
proof idea
One-line term proof. The module already defines a concrete value cert : RSMTHStructural002Cert. The theorem is Nonempty introduced by the anonymous constructor ⟨cert⟩, i.e. the standard Lean witness for inhabited structure types. No tactics, no further lemmas.
why it matters
In the Recognition framework this is the inhabitance seal for Structural Module 2: the J-cost package at $\varphi$ is not merely postulated as a Prop bundle, it has a zero-sorry witness. That matches the module status line (structural theorem, 0 sorry, 0 axiom) and sits under the T5 J-uniqueness / T6 $\varphi$-fixed-point landmarks, where $J(x)=(x+x^{-1})/2-1$ and $\varphi$ is forced as the self-similar point.
No downstream consumers are wired in the graph yet (used_by empty). The declaration exists so later mass-ladder, threshold, or cost-comparison theorems can assume a single certificate rather than three loose hypotheses. It closes the local scaffolding question "is the structural cert realizable?" in the affirmative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.