cert
plain-language theorem explainer
Packages three already-proved facts about the domain cost into a single structural certificate for the eight-tick physics module: diagonal vanishing, non-negativity on positive reals, and positivity of the canonical threshold. Anyone citing the RS eight-tick structural layer uses this bundle rather than the three lemmas separately. The construction is a pure structure instance, wiring named sibling proofs into the certificate fields.
Claim. There is a structural certificate asserting: (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
This module records the RS eight-tick structural layer: one full traversal of the binary recognition lattice has period $2^D = 8$, matching the T7 octave in the forcing chain. Status is a structural theorem (no sorry, no axioms).
The certificate type collects three properties of a real-valued domain cost on pairs of positive scales. Diagonal vanishing says matched mass and energy (or matched recognition ratios) incur zero cost. Non-negativity is the physical lower bound on recognition cost. The canonical threshold is the positive cutoff used to separate sub-threshold from above-threshold events.
Upstream, non-negativity of recognition-event cost is already known from ObserverForcing: any recognition event has cost at least zero because the J-cost is nonnegative on positive states. The present certificate specializes that idea to the domain-cost function used in this physics module.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new algebra is performed; the definition only assembles those proofs into the certificate record.
why it matters
Gives a single named inhabitant of the structural certificate for RS Physics Structural Module 5, so downstream code can depend on one object rather than three separate lemmas. The module doc frames this as the eight-tick structural theorem (period $2^D = 8$), which is the T7 landmark in the forcing chain: one complete traversal of the binary recognition lattice.
No downstream dependents are recorded yet (used_by is empty), so the certificate is presently a leaf packaging step inside the module. It sits beside cert_inhabited and the domain-cost lemmas, closing the local structural interface without introducing axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.