cert
plain-language theorem explainer
Packages three elementary facts about the domain J-cost into a single coherence-time certificate: the cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the structural coherence-time story in this module will pull this bundle rather than the three lemmas separately. The definition is a pure structure instance wiring those three proofs.
Claim. There is a coherence-time certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for every $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 qubit coherence-time ratios from the Recognition Science J-cost. Empirically $T_1\approx T_2\cdot\varphi$ for many superconducting qubits; RS attributes the factor $\varphi$ to an asymmetry between longitudinal (amplitude) relaxation and transverse (phase) dephasing.
The local cost on a pair of positive reals is the domain cost built from the standard J-cost $J(x)=(x+x^{-1})/2-1$. The certificate structure records three minimal analytic properties of that cost: it is zero when the two arguments coincide (and are nonzero), it is nonnegative for positive arguments, and a fixed positive threshold (the canonical threshold) is available for comparison.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing via $J\ge 0$ on positive reals. The three field lemmas in this module specialize that fact and the diagonal identity to the domain-cost wrapper.
proof idea
One-line structure instance. The three fields of CoherenceTimeCert 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 further tactic work.
why it matters
Gives a single named witness that the domain J-cost satisfies the three inequalities the coherence-time development needs. The module is marked structural (zero sorry, zero axiom) and aims at the RS claim $T_1/T_2=\varphi$ from recognition relaxation versus dephasing. The golden ratio $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain; the J-cost itself is the unique cost from T5 and the Recognition Composition Law. No downstream consumers are recorded yet; the certificate is the local packaging step before ratio theorems are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.