cert_inhabited
plain-language theorem explainer
The certificate type for RS structural module 6 is nonempty: there exists a package of domain-cost diagonal vanishing, nonnegativity, and a strictly positive canonical threshold. Anyone citing the module's structural status (phi as self-similar fixed point) can point here for inhabitance. The proof is a one-line term witness via the explicit certificate constructor.
Claim. There exists a certificate packing three facts: (i) the domain cost of any nonzero real against itself is zero; (ii) for positive reals $m,e$ the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_006 is the structural mathematics layer for Recognition Science phi uniqueness: phi is forced as the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$. Status is a structural theorem with zero sorry and zero axioms.
The certificate structure bundles three elementary properties of the module's domain cost and threshold. Domain cost vanishes on the diagonal for nonzero arguments, is nonnegative on the positive quadrant, and the canonical threshold is positive. These are the local algebraic hygiene conditions that sit under the phi fixed-point story (forcing chain T6 in the broader RS development).
Upstream, the structure itself is the only dependency: inhabitance is exactly the claim that some term of that structure type exists.
proof idea
Term-mode one-liner. The proof supplies the explicit in-module certificate cert as the witness for Nonempty, via the anonymous constructor. No tactics, no intermediate lemmas: inhabitance is definitional once the certificate term is in scope.
why it matters
This declaration closes the inhabitance obligation for the module's certificate type, so downstream consumers can treat the structural package as a real object rather than an empty interface. The module doc frames the whole file as the structural theorem for phi uniqueness (self-similar fixed point), which is landmark T6 in the RS forcing chain. No further used-by edges are recorded yet; the value is local completeness of the certificate layer that underwrites the phi story and the related cost/threshold facts (diagonal vanishing, nonnegativity, positive threshold).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.