RSPHYStructural005Cert
plain-language theorem explainer
Certificate bundle for the fifth RS structural physics claim: diagonal domain cost vanishes, off-axis domain cost stays non-negative for positive arguments, and the canonical threshold is strictly positive. Structural auditors and eight-tick lattice proofs cite it as the packaged interface. It is a pure structure definition; inhabitance is discharged elsewhere by the sibling lemmas.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module RS_PHY_Structural_005 packages structural facts tied to the RS eight-tick: one full traversal of the binary recognition lattice has period $2^D=8$ (with $D=3$ from the forcing chain). Status is structural theorem, zero sorry and zero axiom.
Domain cost is the local cost functional on pairs of positive reals used in this physics layer; on the diagonal it is required to vanish (identity recognition costs nothing), and elsewhere it inherits nonnegativity from the J-cost calculus. The upstream foundation result states that the cost of any recognition event is nonnegative, via $J$-cost nonnegativity on positive states. The canonical threshold is the positive cutoff against which structural comparisons are made in this module.
proof idea
No proof body: this is a structure declaration (three Prop fields). Inhabitance is not proved here. The sibling definition cert fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then wraps that value as Nonempty.
why it matters
Gives a single named certificate type that the module's cert and cert_inhabited inhabit, so downstream physics structural checks can demand one object rather than three loose lemmas. Sits in the eight-tick structural layer (period $2^D=8$), aligned with forcing-chain T7 (eight-tick octave) and T8 ($D=3$). Does not itself derive the mass ladder or $\alpha$ band; it only packages cost-vanishing, cost-nonnegativity, and threshold positivity for structural use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.