cert
plain-language theorem explainer
Packages three elementary facts about a domain cost into a single structural certificate: the cost vanishes on the diagonal, stays non-negative for positive arguments, and the canonical threshold is strictly positive. Physicists tracing the RS structural forcing chain (T5–T8) cite it as the inhabited witness for module 9. The body is a pure record assembly from three already-proved sibling lemmas.
Claim. There exists a structural certificate asserting: (i) for every nonzero real $r$, the domain cost satisfies $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
Module RS_PHY_Structural_009 sits in the physics layer of the Recognition Science forcing chain: T5 uniqueness of the J-cost, T6 forcing of $\varphi$, T7 the eight-tick octave, T8 spatial dimension $D=3$. Status is structural (zero sorry, zero axiom).
The certificate structure bundles three properties of a domain cost function on pairs of reals. The first says the cost of matching a nonzero scale to itself is zero (identity events sit at the J-cost minimum). The second is non-negativity for positive mass/energy-like arguments, in the same spirit as the upstream recognition-event cost theorem: "The cost of any recognition event is non-negative." The third asserts positivity of a fixed canonical threshold used as a comparison scale in the module.
Sibling lemmas already establish each field separately: diagonal vanishing, non-negativity, and threshold positivity. This definition only packages them.
proof idea
One-line record construction. The three structure fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional reasoning occurs; the definition is pure assembly of already-proved facts into the certificate type.
why it matters
Gives an inhabited value of the module-9 structural certificate, so downstream code can assume the three cost axioms as a single package rather than re-importing each lemma. The module doc places this inside the RS forcing spine from J-uniqueness (T5) through $\varphi$, the eight-tick period, and $D=3$ (T8). No further used-by edges are recorded yet; the immediate consumer is the companion inhabitedness witness in the same file. Closes the structural obligation for this physics module without introducing axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.