cert
plain-language theorem explainer
Packages three structural facts about the domain J-cost into a single decoherence-time certificate: vanishing on the diagonal, nonnegativity for positive arguments, and a strictly positive canonical threshold. Physicists citing the RS decoherence timescale τ_D = ħ/(J(φ) k_B T) use this bundle as the formal support object. The definition is a direct structure instance wiring three local lemmas.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives a quantum decoherence timescale from the Recognition Science J-cost. In RS-native units the thermal decoherence rate is $J(\varphi)/\hbar$ at the recognition temperature $T=E_{\mathrm{coh}}/k_B$, equivalently $\tau_D=\hbar/(J(\varphi),k_B T)$.
The J-cost is the unique nonnegative cost functional forced by the Recognition Composition Law, with $J(x)=(x+x^{-1})/2-1$ and minimum $J(1)=0$. Here domainCost is the local bivariate cost used for mass/energy pairs; the certificate demands it vanish when the two arguments coincide and stay nonnegative off the identity.
Upstream, cost_nonneg in ObserverForcing records that every recognition event has nonnegative cost via Jcost_nonneg. The structure DecoherenceTimeCert is the local interface collecting the three positivity/vanishing facts needed before quoting a decoherence timescale.
proof idea
One-line structure instance. The three fields of DecoherenceTimeCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional reasoning: the definition is pure packaging.
why it matters
Gives the inhabited certificate object for the module's structural claim that decoherence timescales descend from J-cost (Plan v7, 102nd pass; 0 sorry, 0 axiom). Downstream consumers that need a single term of type DecoherenceTimeCert (for example the sibling cert_inhabited) point here rather than re-proving diagonal vanishing, nonnegativity, and threshold positivity.
In the broader RS chain this sits under the forced J-uniqueness (T5) and the self-similar fixed point $\varphi$ (T6): the decoherence rate is evaluated at $J(\varphi)$, so the certificate's nonnegativity and positive threshold keep $\tau_D$ well-defined and positive. No further used-by edges are recorded yet; the object is the local anchor for that physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.