cert
plain-language theorem explainer
Packages three structural facts for the eight-tick foundation module: domain cost vanishes on the diagonal, stays non-negative for positive mass and energy, and the canonical threshold is strictly positive. Anyone citing the RS structural certificate for period-8 recognition will pull this inhabitant. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate recording that (i) for every nonzero real $r$, the domain cost of $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and (iii) the canonical threshold is strictly positive.
background
Module 5 of the RS foundation structural series treats the eight-tick octave: one full traversal of the binary recognition lattice with period $2^D = 8$ (forcing landmark T7). Status is structural theorem, zero sorry and zero axiom.
The certificate structure bundles three properties of a domain-level cost functional and a positive threshold. Domain cost is the cost assigned to a pair of positive reals (mass/energy style arguments); it is required to vanish when the two arguments coincide (nonzero) and to stay nonnegative off the diagonal. The canonical threshold is the positive scale against which recognition events are compared.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has nonnegative cost via the J-cost minimum at identity.
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 tactic work occurs.
why it matters
Gives a single named certificate object for Structural Module 5 so downstream foundation code can assume the eight-tick cost package without re-proving diagonal vanishing, nonnegativity, or threshold positivity. Aligns with the T7 eight-tick octave (period $2^3 = 8$) in the forcing chain. No used-by edges are recorded yet; the natural consumer is any lemma that needs an inhabited RSFDNStructural005Cert (for example the sibling cert_inhabited). Closes the structural packaging step for this module rather than an open analytic gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.