cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single structural certificate: the cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Anyone citing the RS structural module 1 package (J-form, golden ratio, D=3) can point at this inhabited certificate. The body is a pure structure constructor wiring three sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every nonzero real $r$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module RS_MTH_Structural_001 packages the Recognition Science structural prediction that the cost is $J(x)=\tfrac12(x+1/x)-1$, that $\varphi$ is the golden ratio, and that $D=3$ is forced, with zero sorry and zero axioms.
The certificate structure bundles three real-analytic properties of a domain-level cost: it vanishes when the two arguments coincide (nonzero), it is nonnegative on the positive quadrant, and a fixed positive threshold (the canonical threshold) is available for later comparison arguments.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The present certificate lifts that style of fact to the module's domain-cost wrapper.
proof idea
One-line structure inhabitation. The three fields are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively; no further rewriting or case analysis occurs.
why it matters
Gives a single named inhabitant of the structural certificate for Mathematics RS Structural Module 1, so downstream code can depend on one object rather than three separate lemmas. The module claims the classical RS landmarks: $J(x)=\tfrac12(x+x^{-1})-1$ (T5 J-uniqueness form), $\varphi$ as golden ratio (T6 fixed point), and $D=3$ forced (T8). No used_by edges are recorded yet; the sibling cert_inhabited is the natural consumer. This is packaging, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.