CosmicStrings4Cert
plain-language theorem explainer
A certificate structure packaging three analytic facts needed for the cosmic-string J-cost story: the domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is strictly positive. Cosmology and RS-constants work cites it as the interface that `cert` inhabits. There is no proof body; it is a pure Prop-bundle definition.
Claim. A cosmic-strings certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost at equal arguments satisfies $\mathrm{cost}(r,r)=0$; (ii) for all positive reals $m,e$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
The module treats a cosmic-string network as a structural consequence of the Recognition Science J-cost. In RS units the string tension is written $G\mu = J(\varphi),(E_{\mathrm{string}}/M_{\mathrm{Pl}})^2$, with $J(\varphi)\approx 0.118$, and is compared to the observational bound $G\mu<10^{-7}$. At a GUT-scale vev $v\sim 10^{16},\mathrm{GeV}$ one obtains $G\mu\sim 8\times 10^{-6}$, marginally excluded yet still in the ballpark of current limits.
The local cost object is a two-argument real function (domain cost) built from the same J-cost that appears in the forcing chain (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$). Upstream, cost_nonneg records that every recognition event has nonnegative cost via $J\ge 0$ on positive reals. The certificate also names a canonical positive threshold against which that cost is compared when deciding whether a string-forming defect is recognized.
proof idea
No proof: this is a structure definition. The three fields are bare propositions. Downstream, the concrete inhabitant cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. Inhabitation is then recorded by cert_inhabited : Nonempty CosmicStrings4Cert.
why it matters
The structure is the typed interface for the Plan-v7 cosmic-strings pass: it freezes exactly which J-cost facts the cosmology layer is allowed to use when claiming a string network from recognition cost. Downstream cert and cert_inhabited close the module as a structural theorem (zero sorry, zero axiom) by exhibiting one such certificate.
In the broader RS picture this sits under the J-uniqueness landmark (T5) and the RCL identity that forces $J$. The numerical story ties string tension to $J(\varphi)$ and the Planck hierarchy; the certificate itself does not compute $G\mu$, but guarantees the cost side of that comparison is well-posed (vanishes on matched scales, never negative, threshold positive). It does not settle the observational tension at $v=10^{16},\mathrm{GeV}$; it only licenses the cost hypotheses used in that estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.