cert
plain-language theorem explainer
Packages three elementary properties of the module's domain cost and canonical threshold into a single certificate record for RS structural module 5 (eight-tick lattice). Anyone citing the eight-tick structural bundle uses this inhabitant rather than the three lemmas separately. The definition is a pure structure constructor: it wires the sibling equalities and inequalities into the certificate fields.
Claim. There is a certificate whose fields assert: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 5 is the Standard Model structural layer for the RS eight-tick: 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 type bundles three Prop-valued fields about a real-valued domain cost on pairs $(m,e)$ and a positive real threshold. Domain cost is the local cost functional used in this structural module; on the diagonal it is required to vanish (identity recognition costs nothing), and off-diagonal it stays nonnegative for positive arguments. That nonnegativity pattern mirrors the global recognition cost law: the cost of any recognition event is nonnegative, which ultimately rests on nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$.
The third field only demands that the module's canonical threshold is positive, so later comparisons against that threshold are well-posed.
proof idea
One-line structure inhabitant. The three certificate fields are filled by the sibling lemmas that already prove diagonal vanishing of domain cost, nonnegativity of domain cost on positive pairs, and positivity of the canonical threshold. No extra algebra is performed at this site; the definition only assembles those three results into RSSTDStructural005Cert.
why it matters
Gives a single named witness that the eight-tick structural cost package is inhabited. Downstream code can depend on the certificate rather than on three separate lemmas, which keeps the Standard Model structural layer modular. In the Recognition forcing chain this sits under T7 (eight-tick octave, period $2^3$) and the broader Standard Model structural series; the module doc marks the whole file as a structural theorem with no sorry and no axiom. No used-by edges are recorded yet, so the certificate is presently a terminal packaging step rather than an intermediate lemma in a longer proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.