CoherenceTimeCert
plain-language theorem explainer
Certificate structure bundling three axioms on the domain-level cost and its threshold: diagonal vanishing, non-negativity for positive arguments, and a strictly positive canonical threshold. Physicists deriving T1/T2 from J-cost cite it as the interface that the inhabited cert instance discharges. Pure structure definition with no proof body.
Claim. A coherence-time certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every $r\neq 0$; (ii) the domain cost is non-negative on positive pairs, $\mathrm{cost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical coherence threshold is strictly positive.
background
The module derives qubit coherence times from the Recognition Science J-cost. Empirically $T_1\approx T_2\cdot\varphi$ for many superconducting qubits; RS attributes the ratio to an asymmetry between longitudinal (amplitude) relaxation and transverse (phase) dephasing, with the slower channel scaled by the golden ratio $\varphi$.
The underlying cost is the unique J-functional $J(x)=(x+x^{-1})/2-1$ forced at T5, known to be non-negative (upstream cost_nonneg: "the cost of any recognition event is non-negative"). Here domainCost specializes that cost to a pair of positive reals (mass/energy-like arguments), and canonicalThreshold is the positive cutoff used when converting cost excess into a coherence-time bound.
The local setting is a structural theorem package (0 sorry, 0 axiom) that isolates exactly the cost axioms needed before the $\varphi$-ratio arithmetic begins.
proof idea
No proof: this is a structure declaration. Its three fields are Prop-valued requirements. The sibling definition cert inhabits them by supplying domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The theorem cert_inhabited then packages that instance as Nonempty CoherenceTimeCert.
why it matters
This certificate is the typed interface that lets the rest of the coherence-time development stay modular. Downstream, cert and cert_inhabited discharge it inside the same module; the quantum sibling module QuantumCoherenceTimeFromJCost carries a richer certificate (phi-ratio across rungs, $\varphi^8$ and $\varphi^{12}$ amplitude bounds) that builds on the same naming pattern.
In the Recognition framework it sits under the physics layer that converts J-cost asymmetry into the observed $T_1/T_2=\varphi$ relation, using the T5 uniqueness of $J$ and the T6 fixed point $\varphi$. It does not itself compute the ratio; it only freezes the cost hypotheses so later lemmas can cite a single inhabited certificate rather than three separate axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.