cert
plain-language theorem explainer
Packages three domain-cost facts into a single Planck-energy certificate: diagonal vanishing, nonnegativity for positive mass and energy, and a positive canonical threshold. Anyone citing the RS4 Planck-energy interface uses this witness. The body is a pure structure assembly of three sibling lemmas; no new algebra.
Claim. There exists a certificate for the RS4 Planck-energy interface: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive mass $m$ and energy $e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The module is the final RS physics session: a structural theorem package with zero sorry and zero axioms, centered on a Planck-energy certificate.
Planck_Energy_RS4 is a structure bundling three interface properties of a domain cost on mass–energy pairs: (i) the cost vanishes on the diagonal away from zero, (ii) the cost is nonnegative whenever mass and energy are positive, and (iii) a fixed canonical threshold is positive. Domain cost is the local cost functional used to compare mass and energy scales in RS units; nonnegativity is the continuum shadow of the recognition-event cost law (upstream: cost of any recognition event is nonnegative, via $J$-cost nonnegativity).
Sibling lemmas already prove each field: diagonal identity, nonnegativity, and threshold positivity. This declaration only names the assembled witness.
proof idea
One-line structure construction. Fill cost_at_eq by domainCost_at_eq, cost_nonneg by domainCost_nonneg, and threshold_pos by canonicalThreshold_pos. No tactics and no new inequalities; the proof is pure packaging of three preexisting facts into the Planck_Energy_RS4 record.
why it matters
Gives the named RS4 Planck-energy certificate the module advertises (PlanckEnergy_RS4Cert). Downstream consumers can depend on a single inhabited interface rather than three scattered lemmas. In the broader framework this is bookkeeping for energy-scale comparison under the recognition cost (tied to $J$-cost nonnegativity from ObserverForcing), not a new forcing step: it does not itself force $\phi$, the eight-tick octave, or $D=3$. With empty used_by in the current graph, it is the terminal witness of this physics session rather than an intermediate lemma in a longer chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.