cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical horizon threshold into a single certificate structure. Anyone citing the RS structural resolution of the cosmological horizon problem (8-tick / 44 e-fold route) would point at this witness. The definition is a pure structure assembly: it wires already-proved diagonal vanishing, non-negativity, and threshold positivity lemmas into the certificate fields.
Claim. There is a certificate asserting: (i) the domain cost satisfies $C(r,r)=0$ for every real $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical horizon threshold is strictly positive.
background
The module treats the cosmological horizon problem as a structural consequence of the eight-tick octave and the J-cost. In RS units the inflationary expansion is read off the golden ratio ladder: $N_e=44$ e-folds at temperature $T=J(\varphi),T_{\mathrm{Planck}}$, giving an expansion factor $\varphi^{44}\sim 10^{9}$ that the module interprets as consistent with the classical $10^{24}$–$10^{26}$ requirement under the appropriate rung accounting.
Domain cost is the local cost functional on pairs of positive reals used to compare causal patches; it is built from the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The certificate structure records exactly the three properties needed downstream: vanishing on the diagonal (matched patches cost nothing), non-negativity for positive arguments, and positivity of a fixed canonical threshold against which horizon separation is measured.
Upstream, non-negativity of recognition-event cost is already forced by $J\ge 0$ on $(0,\infty)$ (ObserverForcing.cost_nonneg).
proof idea
Pure structure construction, not a tactic proof. The three fields of the certificate are filled by named sibling lemmas already in the module: diagonal vanishing (domainCost_at_eq), non-negativity on the positive quadrant (domainCost_nonneg), and positivity of the canonical threshold (canonicalThreshold_pos). No further rewriting or case analysis occurs.
why it matters
This is the concrete inhabitant that turns the horizon-problem certificate type into a usable zero-sorry witness. The module status line marks the whole development as a structural theorem (0 sorry, 0 axiom) in the Plan v7 115th-pass cosmology stack. It sits on the RS forcing chain landmarks T5 (J-uniqueness) and T7 (eight-tick octave), and on the mass/temperature ladder that places inflation at $J(\varphi),T_{\mathrm{Planck}}$ with $N_e=44$. No downstream consumers are recorded yet in the graph; the certificate is the export surface for any later theorem that needs a packaged proof that domain cost is a genuine non-negative defect with a positive horizon cutoff.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.