cert
plain-language theorem explainer
Packages three proved properties of the Andreev domain cost into a single certificate: diagonal vanishing, nonnegativity for positive masses/energies, and a strictly positive canonical barrier threshold. Anyone citing the RS structural account of Andreev reflection T_A from J-cost would reach for this bundle. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost satisfies $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical Andreev barrier threshold is strictly positive.
background
The module treats Andreev reflection (electron-to-hole conversion at a normal-superconductor interface) as a J-cost phenomenon. Classically $T_A=1/(1+(Z^2+Z^4/4)^2)$ with barrier strength $Z$; the RS claim is that $T_A=J(\varphi)$ when $Z=J(\varphi)^{-1/4}\approx 1.71$ in barrier units.
The domain cost $C(m,e)$ is the local cost functional on mass/energy-like arguments used to encode that barrier. The certificate structure demands three elementary facts about it: vanishing on the diagonal $m=e$, nonnegativity off the diagonal for positive arguments, and positivity of a fixed canonical threshold (the RS barrier scale).
Upstream, nonnegativity of recognition cost is already forced: any recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals. The present certificate specializes that discipline to the Andreev domain cost and threshold.
proof idea
One-line structure construction. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No extra algebra is performed at this site.
why it matters
This is the inhabited certificate that makes the module's structural theorem usable: once the three cost/threshold facts are bundled, downstream Andreev arguments can assume a single object rather than re-proving diagonal vanishing and positivity each time.
It sits inside the Plan v7 pass that derives Andreev $T_A$ from the J-cost, tying the condensed-matter barrier $Z$ to the forced cost $J$ (T5 uniqueness: $J(x)=(x+x^{-1})/2-1$) and the golden ratio fixed point $\varphi$ (T6). No further used-by edges are recorded yet; the immediate consumer is the module's own inhabitedness lemma and any later probability identity that needs a positive threshold and a nonnegative domain cost.
The declaration itself is definitional packaging, not a new physical identity. Its value is hygiene: it freezes the interface that a full $T_A=J(\varphi)$ derivation must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.