cert_inhabited
plain-language theorem explainer
The structural certificate for Foundation module 6 is nonempty: there exists a witness packing diagonal vanishing and nonnegativity of the domain cost together with positivity of the canonical threshold. Anyone citing the RS phi self-similarity package (fixed point of the continued fraction) uses this inhabitation fact. The proof is a one-line term that supplies the prebuilt certificate value.
Claim. There exists a certificate packing three facts: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$ the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
Module RS_FDN_Structural_006 packages the structural side of RS phi uniqueness: phi as the self-similar fixed point of the infinite continued fraction $1+1/(1+1/(1+\cdots))$. Status is a pure structural theorem (zero sorry, zero axiom).
The certificate structure bundles three elementary properties of the local cost data. Domain cost is the two-argument cost used on the module's domain; the first field requires it to vanish on the diagonal away from zero, the second that it is nonnegative on the positive orthant. Canonical threshold is the positive scale cut used in the same package; the third field only asserts it is strictly positive.
Upstream, the structure itself is the sole dependency: inhabitation is exactly the statement that some value of that structure type exists.
proof idea
Term-mode one-liner. The proof is the anonymous constructor ⟨cert⟩, which exhibits the already-defined value cert as a witness of Nonempty for the certificate structure. No tactics, no further lemmas.
why it matters
This is the inhabitation seal for Structural Module 6, the foundation package whose module doc identifies it with RS phi uniqueness (self-similar fixed point). In the forcing chain that is the T6 landmark: phi forced as the unique self-similar scale. The certificate does not itself derive the closed form of phi; it only guarantees that the supporting cost and threshold facts are realized, so downstream structural arguments can assume a nonempty certificate rather than re-proving the three fields.
No used_by edges are recorded yet, so the immediate consumers are whatever later foundation or constants lemmas import this module and open the certificate. It closes the structural side of the module (0 sorry, 0 axiom) and keeps the phi package citation-ready.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.