RSMTHStructural005Cert
plain-language theorem explainer
Certificate record that packages three structural facts for the eight-tick module: diagonal domain cost vanishes off zero, domain cost is nonnegative on positive pairs, and the canonical threshold is positive. Downstream code cites the inhabited instance when a single structural package is required. Pure structure definition; the three fields are discharged by sibling lemmas in the module certificate.
Claim. A structural certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost of the pair $(r,r)$ equals $0$; (ii) for all reals $m,e > 0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module is the fifth RS structural mathematics unit. Its setting is the eight-tick octave: one full traversal of the binary recognition lattice with period $2^D = 8$ (forcing landmark T7). The module is marked structural (zero sorry, zero axiom).
The certificate talks about a real-valued domain cost on pairs $(m,e)$ and a fixed positive canonical threshold. Sibling lemmas establish that the cost vanishes on the diagonal away from zero, stays nonnegative for positive arguments, and that the threshold is positive. Upstream, recognition-event cost is already known to be nonnegative: any recognition event has cost $0 \le e.\mathrm{cost}$ via nonnegativity of the J-cost on positive states.
The structure does not redefine those objects; it only names the three Prop fields a consumer must supply.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements. Inhabitation is supplied later by the module certificate, which assigns the sibling lemmas for diagonal vanishing, nonnegativity on positive pairs, and positivity of the canonical threshold into those fields. Upstream nonnegativity of recognition-event cost (via J-cost) is the conceptual ancestor of the domain-cost nonnegativity field, but is not invoked inside this declaration itself.
why it matters
Gives the module a single named package for its three structural obligations. Downstream, the concrete certificate fills the fields, and the inhabited theorem records that the package is nonempty. That pattern lets later mathematics or physics layers depend on one certificate rather than three separate lemmas.
Framework role is local to the eight-tick structural layer (period $2^D = 8$, T7). It does not itself force dimension, the golden ratio, or the J-cost functional equation; those live in the forcing chain. It does lock the cost and threshold hygiene needed before any eight-tick counting or lattice-traversal argument can treat domain cost as a genuine nonnegative defect with a positive cutoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.