cert_inhabited
plain-language theorem explainer
The Module-3 forcing certificate is inhabited: there is a witness packing diagonal vanishing of domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold. Anyone citing the RS gap-45 structural package (g_D = 45 at D = 3) uses this existence fact. The proof is a one-line term that injects the concrete certificate into Nonempty.
Claim. There exists a certificate packing three facts: the domain cost vanishes on the diagonal ($C(r,r)=0$ for all $r\neq 0$), the domain cost is nonnegative for positive arguments, and the canonical threshold is strictly positive.
background
Module 3 of the RS forcing chain records the gap-45 structural fact: $g_D = D^2(D+2)$ evaluates to $9\cdot 5 = 45$ at spatial dimension $D=3$, the minimum depth supporting self-reference. The local certificate structure packages three elementary cost properties needed for that package.
Domain cost is the two-argument cost functional used in this module (imported from the Cost layer). Its diagonal vanishing and nonnegativity on positive reals are the standard J-cost sanity conditions. The canonical threshold is the positive real cutoff associated with the same module; positivity is recorded as a separate field so downstream consumers can treat the whole triple as a single inhabited Prop-free record.
The module is marked structural (zero sorry, zero axiom).
proof idea
One-line term proof. The concrete value cert already assembles the three fields of the certificate structure; wrapping it as ⟨cert⟩ is the standard Lean inhabitant of Nonempty RSForcingChain003Cert. No tactics, no further lemmas.
why it matters
Closes the existence side of Foundation Module 3 (RS gap-45 at $D=3$). The forcing-chain landmarks T7 (eight-tick octave) and T8 ($D=3$ spatial dimensions) sit upstream of the gap formula $g_D=D^2(D+2)$; this certificate is the local structural witness that the cost and threshold side-conditions hold in that setting. No downstream consumers are wired yet in the graph, so the declaration presently serves as the module's public inhabitedness stamp rather than a lemma inside a larger proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.