RSUniquenessMaster3Cert
plain-language theorem explainer
Certificate bundle of three elementary cost axioms: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream uniqueness assembly cites it as the interface that must be inhabited. Pure structure definition; inhabitation is discharged separately by the sibling `cert` construction.
Claim. A uniqueness certificate is a triple of properties: (i) for every $r\neq 0$, the domain cost of the pair $(r,r)$ is zero; (ii) for all $m,e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module states the RS Uniqueness Master Theorem v3: $J$ is the unique function satisfying the four Recognition Science axioms, with the consequence that physical constants, masses, and cosmological parameters are forced from $J$. Status is structural (zero sorry, zero axiom).
Local siblings introduce a real-valued domain cost on pairs of positive reals and a canonical threshold scalar. The first field of this structure asks that cost vanish when the two arguments coincide (off zero). The second asks nonnegativity on the positive quadrant. The third asks that the threshold sit strictly above zero.
Upstream, ObserverForcing already proves that every recognition-event cost is nonnegative via $J$-cost nonnegativity. The present certificate lifts that style of positivity into the domain-cost language used by the master uniqueness argument.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements, not constructions. Inhabitation is supplied by the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and by the one-line Nonempty witness that wraps that definition.
why it matters
Gives the master uniqueness module a single named interface for the cost and threshold side-conditions it needs before claiming $J$-uniqueness. Downstream, the concrete certificate and the Nonempty theorem close the interface, so later steps can assume the three properties without re-proving them. In the broader forcing chain this sits under the uniqueness of $J$ (T5 landmark: $J(x)=(x+x^{-1})/2-1$), which the module doc presents as forcing all constants and masses once uniqueness is secured. It does not itself run the uniqueness argument; it only packages the cost hypotheses that argument consumes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.