DecoherenceTimeCert
plain-language theorem explainer
Certificate structure packaging three algebraic properties of the domain J-cost used to underwrite a decoherence timescale: vanishing on equal nonzero arguments, nonnegativity for positive mass and energy, and positivity of the canonical threshold. Anyone deriving tau_D from Recognition Science J-cost cites this bundle. Pure structure definition with no proof body; inhabited later by an explicit witness.
Claim. A decoherence-time certificate is a triple of facts: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative on the positive quadrant, $C(m,e)\geq 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold $\theta$ satisfies $\theta>0$.
background
The module derives a quantum decoherence timescale from the Recognition Science J-cost. In RS units the structural claim is $\tau_D=\hbar/(J(\varphi),k_B T)$ at the recognition temperature, equivalently a thermal rate $J(\varphi)/\hbar$ when $T=E_{\mathrm{coh}}/k_B$.
The domain cost $C(m,e)$ is the local cost functional on positive mass and energy coordinates; the certificate only needs its diagonal vanishing and nonnegativity. Upstream, recognition-event cost is already known to be nonnegative via the standard J-cost inequality ($J(x)\geq 0$ for $x>0$), which seeds the domain-cost nonnegativity field.
The canonical threshold is the positive cutoff against which the cost is compared when stating a decoherence-time bound. The structure packages exactly those three Prop-level obligations and nothing else.
proof idea
No proof: this is a structure declaration. Its three fields are Prop-valued hypotheses (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling witness cert, which fills the fields by the corresponding lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the module a single named interface for the algebraic side-conditions of the decoherence-timescale claim, so downstream code can depend on one certificate rather than three scattered lemmas. The explicit witness cert and the inhabitation theorem cert_inhabited both target this structure, closing the structural half of the Plan v7 decoherence pass (0 sorry, 0 axiom).
In the broader RS chain this sits under the J-cost uniqueness landmark (T5: $J(x)=(x+x^{-1})/2-1$) and the constants $c=1$, $\hbar=\varphi^{-5}$. It does not itself compute a numerical $\tau_D$; it only certifies the cost inequalities the rate formula needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.