CosmicStringCert
plain-language theorem explainer
Certificate bundling three structural facts for cosmic-string tension on the φ-ladder: domain cost vanishes on the diagonal, is non-negative for positive scales, and the canonical threshold is positive. Cited by anyone discharging the RS Gμ consistency claim. Pure structure definition; inhabited via the module's concrete witness.
Claim. A cosmic-string certificate is a record of three properties: (i) the domain cost $C$ vanishes on equal nonzero scales, $r \neq 0 \Rightarrow C(r,r)=0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $T$ satisfies $T>0$.
background
The module treats cosmic-string tension in Recognition Science units. Observationally one wants $G\mu < 10^{-7}$ (Planck). RS writes $G\mu = J(\varphi),(\Lambda_{\mathrm{string}}/M_{\mathrm{Pl}})^2$, with $\Lambda_{\mathrm{string}}$ the formation scale; at GUT scale this lands near $10^{-6}$–$10^{-7}$, hence consistency.
The cost functional $J$ is the unique nonnegative self-similar cost from the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). Domain cost here is the two-argument cost used to compare mass and energy scales on the $\varphi$-ladder; the canonical threshold is the positive cutoff against which string formation is judged.
Upstream, non-negativity of recognition cost is already forced: any recognition event has $0\le e.\mathrm{cost}$ via $J$-cost non-negativity on positive states.
proof idea
No proof body: this is a structure (record type) with three propositional fields. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line Nonempty theorem that wraps that witness.
why it matters
Gives the typed interface the module needs before claiming a structural (0-sorry) cosmic-string certificate. Downstream, cert assembles the three field proofs into one value of this type, and cert_inhabited records Nonempty of the certificate—closing the module's structural claim.
In the framework this sits under astrophysics consistency of the $\varphi$-ladder: $J(\varphi)$ and the ladder yardstick fix $G\mu$ once the string scale is chosen, tying back to T5 $J$-uniqueness and T6 $\varphi$ as self-similar fixed point. It does not itself compute a numerical $G\mu$; it packages the cost and threshold hypotheses that any such bound must rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.