RSMTHStructural006Cert
plain-language theorem explainer
Certificate structure packing three structural facts: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites it as the witness type for RS structural module 6 (phi as self-similar fixed point). No proof body: it is a Prop-bundling record inhabited by the concrete cert definition.
Claim. A certificate is a triple of statements: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (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 RS_MTH_Structural_006 is the mathematics structural package for RS phi uniqueness: phi is forced as the self-similar fixed point of the continued fraction $1+1/(1+1/(1+\cdots))$. Status is structural theorem (zero sorry, zero axiom).
The certificate refers to two local objects. Domain cost is a real-valued cost on pairs of positive (or nonzero) reals used as the structural stand-in for recognition cost in this module; the diagonal identity domainCost r r = 0 encodes zero defect when measure and expectation agree. Canonical threshold is the positive cutoff constant against which that cost is compared.
Upstream, ObserverForcing already records that every recognition-event cost is nonnegative, via nonnegativity of the J-cost on positive states. The present fields lift that nonnegativity (and the zero-on-diagonal minimum) into the module's domain-cost language.
proof idea
Definition only: a structure whose three fields are propositions. There is no proof body. Inhabitation is supplied separately by cert, which fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and by cert_inhabited, which packages that witness as Nonempty.
why it matters
Gives the typed witness interface for structural module 6 on phi uniqueness (primer T6: phi forced as the self-similar fixed point). Downstream, cert builds a concrete inhabitant and cert_inhabited records nonemptiness, so later structural lemmas can assume the bundled cost and threshold facts without re-proving them inline.
In the Recognition chain this sits under the J-cost / forcing layer: nonnegativity and zero-at-identity are the same qualitative shape as the unique J-cost minimum at $x=1$ (T5), specialized here to the domain-cost presentation used for the phi fixed-point argument. It does not itself derive phi; it only certifies the cost-threshold side conditions the module treats as structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.