cert
plain-language theorem explainer
Packages three elementary properties of the astrophysical domain cost and its canonical threshold into a single certificate record for RS structural module 6 (phi as self-similar fixed point). Anyone citing the module's structural status uses this inhabitant. The body is a pure field assembly: three already-proved lemmas are plugged into the structure.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ vanishes; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 6 of the RS astrophysics structural series records the uniqueness of $\varphi$ as the self-similar fixed point $\varphi=1+1/(1+1/(1+\cdots))$, status STRUCTURAL (zero sorry, zero axiom). The local cost is a domain-level specialization of the Recognition J-cost $J(x)=(x+x^{-1})/2-1$, which is nonnegative and vanishes only at the identity $x=1$.
The certificate structure bundles three Prop fields: diagonal vanishing of domain cost, nonnegativity on the positive quadrant, and positivity of a canonical numerical threshold used as a comparison scale. Upstream, the foundation lemma cost_nonneg states that every recognition event has nonnegative cost, via $J$-cost nonnegativity on positive states; the module-local lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos specialize that picture to the astrophysical domain cost.
proof idea
One-line structure inhabitant. The three fields of RSASTStructural006Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No new arithmetic is performed; the definition is pure packaging of already-established facts.
why it matters
Gives a single named witness that the cost/threshold side conditions of structural module 6 hold, so downstream astrophysics arguments can assume the certificate rather than re-prove diagonal vanishing, nonnegativity, and threshold positivity. The module frames this as part of the RS $\varphi$-uniqueness story (forcing-chain landmark T6: $\varphi$ forced as the self-similar fixed point). No used_by edges are recorded yet; the companion cert_inhabited likely only asserts that this record is nonempty. The declaration closes no open sorry; it is bookkeeping for an already-proved structural block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.