RSSTDStructural006Cert
plain-language theorem explainer
Certificate structure bundling three structural properties of domain cost and the canonical threshold for the RS Standard Model module on phi uniqueness (self-similar fixed point). Downstream code cites it when building or inhabiting the module-6 certificate. Pure definition: three Prop fields, no proof body.
Claim. A certificate is a triple of statements: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m$ and $e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS Standard Model structural layer targets phi uniqueness: phi as the self-similar continued-fraction fixed point $1+1/(1+1/(1+\cdots))$, matching forcing-chain step T6. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on pairs of positive reals used in this module (sibling of the certificate). The first field requires that cost to vanish on the diagonal away from zero; the second requires nonnegativity for positive arguments. The third field asserts positivity of a fixed canonical threshold used as a comparison scale.
Upstream, recognition-event cost is already known nonnegative via the J-cost minimum at identity ($x=1$). The certificate rephrases the analogous nonnegativity and diagonal-vanishing facts at the domain-cost level for Standard Model packaging.
proof idea
No proof: this is a structure declaration. It only names three fields of type Prop (diagonal vanishing of domain cost, nonnegativity of domain cost on positives, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural hypotheses of RS Standard Model module 6 (phi uniqueness / self-similar fixed point, T6 in the forcing chain). Downstream, cert builds a concrete value by wiring the three sibling lemmas, and cert_inhabited records Nonempty of that type, closing the module's certificate interface.
Without this bundle, later Standard Model structural theorems would thread three separate hypotheses. The certificate keeps the module's zero-sorry structural claim auditable as one inhabited object rather than a loose conjunction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.