cert
plain-language theorem explainer
Packages three elementary properties of the domain cost and the canonical threshold into a single certificate for the dark-energy density v4 construction. Cosmologists working the RS phi-ladder route to rho_Lambda cite it as the structural witness that the cost is a genuine nonnegative defect vanishing on the diagonal. The definition is a pure structure instance: it wires three already-proved lemmas into the certificate fields.
Claim. There exists a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ is strictly positive.
background
The module derives a structural expression for the dark-energy density from the Recognition Science J-cost on the phi-ladder. In RS-native units one has $\rho_\Lambda/\rho_{\mathrm{Pl}}=\phi^5/(45\pi)$, so $\rho_\Lambda$ is a fixed multiple of the Planck density; the numerical offset by a residual $\phi^k$ is left as a structural remark rather than a fitted parameter.
The domain cost is the two-argument cost used to compare mass and energy scales on that ladder. Its diagonal vanishing and nonnegativity are the minimal axioms that let a threshold separate vacuum from excited configurations. The canonical threshold is the positive cutoff against which the density ratio is measured.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative. The present certificate simply specialises that fact (and the diagonal identity) to the cosmology domain cost.
proof idea
One-line structure instance. The three fields of DEDensity4Cert 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.
why it matters
Gives the cosmology layer a single named witness that the cost-and-threshold data needed for the dark-energy density v4 formula are in place. The module status line marks the whole development as a structural theorem (zero sorry, zero axiom); this certificate is the concrete bundle those later density identities can assume.
It sits inside the broader RS forcing picture: J-uniqueness (T5) supplies the cost shape, phi is the self-similar fixed point (T6), and the Planck-to-Lambda ratio is expressed in pure powers of phi. No downstream consumers are recorded yet; the certificate is the hand-off point for any subsequent density or equation-of-state lemma that needs the three structural hypotheses in one package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.