RSMTHStructural001Cert
plain-language theorem explainer
Certificate packing three structural facts about domain cost and the canonical threshold: diagonal vanishing, non-negativity on positive arguments, and a strictly positive threshold. Downstream code cites it via the module inhabitant `cert` and the Nonempty proof. Pure structure definition with no proof body; the three fields are discharged by sibling lemmas.
Claim. A certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of $(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 a structural prediction of Recognition Science: the J-cost takes the forced form $J(x)=\frac12(x+1/x)-1$, with $\varphi$ the golden ratio and spatial dimension $D=3$. Status is a structural theorem block (zero sorry, zero axiom).
Domain cost is the real-valued cost used at the mathematics layer (imported from Cost and Constants). It is the continuum shadow of the recognition cost: upstream, ObserverForcing proves that every recognition event has nonnegative cost via Cost.Jcost_nonneg on a positive state. The diagonal identity $J(1)=0$ is the continuum analogue of the canonical identity event sitting at the J-cost minimum.
The canonical threshold is the positive cutoff used by this structural certificate; sibling lemmas establish its positivity and the two domain-cost identities that the structure demands.
proof idea
No proof body: this is a structure definition whose three fields are propositions. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The Nonempty theorem is then the one-line constructor ⟨cert⟩.
why it matters
Gives a single named bundle for the three structural side-conditions that the RS mathematics layer needs before quoting J-uniqueness and the forced constants. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of the certificate type, so later structural theorems can assume one object rather than three separate lemmas.
In the forcing chain this sits under the T5 J-uniqueness landmark ($J(x)=\cosh(\log x)-1$) and the module claim that $\varphi$ and $D=3$ are forced. It does not itself prove those landmarks; it packages the cost and threshold hygiene they rely on at the real-analysis interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.