cert
plain-language theorem explainer
Packages three structural facts about the RS domain cost and barrier threshold into one certificate for the quantum-tunneling module. Anyone citing the RS Gamow-factor setup (rate = ν exp(-G) with G built from J(φ)) would point here for the nonnegativity and normalization side conditions. The body is a pure structure assembly: three already-proved sibling lemmas fill the three fields.
Claim. There is a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive mass and energy arguments; and (iii) the canonical tunneling threshold is strictly positive.
background
The module treats RS quantum tunneling with rate $\nu,e^{-G}$, where the Gamow factor is $G=2J(\varphi),Q_{\mathrm{barrier}}/Q_{\mathrm{kinetic}}$. Here $J$ is the Recognition Science cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain, and $\varphi$ is the self-similar fixed point from T6.
domainCost is the local cost functional on mass/energy pairs used to score barrier crossings; the certificate demands it vanish when the two arguments coincide (no mismatch) and stay nonnegative when both are positive. canonicalThreshold is the positive cutoff against which barrier strength is compared.
Upstream, nonnegativity of recognition costs is already known from ObserverForcing: "The cost of any recognition event is non-negative," via Cost.Jcost_nonneg. The present certificate lifts that style of guarantee to the tunneling domain cost and threshold.
proof idea
Pure structure construction. The three fields of RSQuantumTunnelingCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra algebra or tactics: the definition is the inhabited instance that witnesses the three Prop fields.
why it matters
Gives the module a single named witness that the cost and threshold side conditions of the RS tunneling setup hold, matching the module status line "STRUCTURAL THEOREM (0 sorry, 0 axiom)." It sits under the RS Gamow factor $G=2J(\varphi),Q_{\mathrm{barrier}}/Q_{\mathrm{kinetic}}$, so the double-barrier exponent prefactor $J(\varphi)$ is only meaningful once cost nonnegativity and a positive threshold are on record.
No downstream consumers are wired yet (used_by is empty); the natural parent is any theorem that quotes the tunneling rate or compares barrier quanta to the canonical threshold. Framework landmarks in play: T5 $J$-uniqueness and T6 $\varphi$, which fix the numerical prefactor in $G$. Closes the structural packaging for this file; does not itself derive the exponential rate law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.