cert
plain-language theorem explainer
Packages three elementary cost and threshold facts into a single certificate for the RS grand-unification scale module. Anyone citing the structural GUT-scale claim (M_GUT = M_Z · φ^74.5) can point at this inhabited record. The definition is a pure structure assembly: three preexisting lemmas are plugged into the three fields.
Claim. There is a certificate consisting of: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) domain cost is nonnegative for positive mass and energy arguments; (iii) the canonical threshold is strictly positive.
background
The module fixes the Recognition Science reading of the grand-unification scale: $M_{\mathrm{GUT}}\sim 2\times 10^{16},\mathrm{GeV}$ is written as $M_Z\cdot\varphi^{r}$ with rung $r=\log(2.2\times 10^{14})/\log\varphi\approx 74.5$. Status is structural (zero sorry, zero axiom).
The certificate structure demands three properties of the local domain cost and of a canonical threshold. Domain cost is the RS cost functional restricted to the mass/energy pair used in this scale comparison; the diagonal vanishing and nonnegativity are the usual J-cost identities (cost zero at identity, cost $\ge 0$). The upstream nonnegativity fact from ObserverForcing states that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states.
Canonical threshold positivity is the remaining numeric guard that the scale cut sits strictly above zero.
proof idea
One-line structure inhabitant. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No further rewriting or case analysis occurs; the definition is pure packaging of already-proved facts into GUT_Scale_RS_v3Cert.
why it matters
Gives a single named witness that the cost and threshold side-conditions of the RS GUT-scale structural theorem hold. The module presents $M_{\mathrm{GUT}}=M_Z\cdot\varphi^{74.5}$ as a structural claim on the $\varphi$-ladder; this certificate is the local proof object that the supporting cost calculus is well-behaved (diagonal zero, nonnegative, positive threshold).
No downstream consumers are recorded yet. In the broader forcing chain the $\varphi$-ladder and J-cost uniqueness (T5–T6) underwrite the same cost identities used here; the declaration does not itself advance T0–T8, but keeps the GUT-scale layer aligned with those foundations. Sibling cert_inhabited is the natural next packaging step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.