cert
plain-language theorem explainer
Packages three elementary properties of the cosmic-string domain cost into one certificate record: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Cosmologists citing the RS string-tension bound Gμ = J(φ)(v/M_Pl)² use this as the structural witness. The definition is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module develops a structural account of cosmic-string networks from the Recognition Science J-cost. In RS units the string tension is $G\mu = J(\varphi),(E_{\mathrm{string}}/M_{\mathrm{Pl}})^2$, with $J(\varphi)\approx 0.118$, so at a GUT-scale vev $v\sim 10^{16},\mathrm{GeV}$ one obtains $G\mu\sim 8\times 10^{-6}$, marginally excluded by the observational ceiling $G\mu<10^{-7}$.
The domain cost is the local cost functional on mass/energy pairs that feeds that tension formula. The certificate structure bundles three elementary analytic facts about that cost: it is zero when the two arguments coincide (identity recognition), it is nonnegative for positive arguments (inherited from the global J-cost nonnegativity theorem in ObserverForcing), and the canonical comparison threshold used downstream is positive.
Upstream, cost_nonneg states that every recognition event has nonnegative cost, via $J\ge 0$ on the positive reals.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No additional reasoning is performed at this site.
why it matters
This is the inhabited certificate that closes the structural theorem of the CosmicStrings4_FromJCost module (status: 0 sorry, 0 axiom). The module doc ties the construction to the RS string-tension prediction $G\mu = J(\varphi),(v/M_{\mathrm{Pl}})^2$ and to the observational bound $G\mu<10^{-7}$. The certificate itself does not compute a numerical $G\mu$; it only guarantees that the cost side of that formula is a well-behaved nonnegative functional with a positive threshold, so later numerical or inequality steps can cite a single record rather than three separate lemmas.
No downstream consumers are recorded yet; the natural parent is any theorem that needs a packaged witness that the cosmic-string domain cost is a valid J-cost restriction. Framework landmarks in play are the unique J-cost (forcing chain T5) and the RS-native constants that fix $J(\varphi)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.