cert
plain-language theorem explainer
Packages three elementary properties of the domain cost and the canonical threshold into one cosmic-string certificate. Anyone deriving the RS bound on string tension Gμ from the φ-ladder cites this as the assembled witness that the cost is a genuine nonnegative defect with positive threshold. The body is a structure instance wiring three already-proved lemmas; no new argument.
Claim. A cosmic-string certificate: the domain cost vanishes on the diagonal ($\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$); the domain cost is nonnegative for all positive mass and energy arguments; and the canonical threshold is strictly positive.
background
The module derives cosmic-string tension from the φ-ladder. In RS units the tension takes the schematic form $G\mu = J(\varphi),(\Lambda_{\mathrm{string}}/M_{\mathrm{Pl}})^2$, with $\Lambda_{\mathrm{string}}$ the formation scale. For a GUT-scale formation the numerical window is $G\mu\sim 10^{-6}$–$10^{-7}$, consistent with the observational ceiling $G\mu<10^{-7}$.
The domain cost is the local cost functional on mass–energy pairs used to measure defect away from the self-similar fixed point. Its diagonal vanishing and nonnegativity are the minimal axioms that make it a genuine defect measure. The canonical threshold is the positive cutoff against which string-forming configurations are compared.
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $J\ge 0$ (ObserverForcing), since $J(x)=(x+x^{-1})/2-1$ is nonnegative for $x>0$. The certificate simply specializes that discipline to the astrophysical domain cost.
proof idea
One-line structure instance. The three fields of CosmicStringCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on the positive quadrant), and canonicalThreshold_pos (strict positivity of the threshold). No additional tactic work; the definition is pure packaging.
why it matters
Gives the module a single named witness that the cost side of the cosmic-string argument is well-posed: defect vanishes on match, never goes negative, and the comparison threshold is positive. The module status is structural (0 sorry, 0 axiom); this certificate is the local assembly point for those three facts.
Downstream use is not yet wired in-tree (used_by empty), but the intended consumer is any theorem that turns the φ-ladder cost into a numerical $G\mu$ bound. Framework landmarks in play: T5 $J$-uniqueness (the cost shape), T6 $\varphi$ as self-similar fixed point (the ladder rung), and the RS-native constants that convert ladder ratios into Planck units. No open scaffold remains on this declaration itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.