cert
plain-language theorem explainer
Packages the three algebraic facts needed for the quantum-capacitance certificate: domain cost vanishes on the diagonal, is nonnegative off it, and the canonical threshold is positive. Anyone citing the RS claim that C_Q/C_geo equals J(φ) at the geometric-to-quantum crossover will pull this bundle. The definition is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate recording that the domain cost $D$ satisfies $D(r,r)=0$ for all $r\neq 0$, that $D(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $t_*$ is strictly positive.
background
The module treats quantum capacitance in Recognition Science units. Classically $C_Q=e^2 D(E_F)$ with $D$ the density of states; the RS claim is that the ratio of quantum to geometric capacitance equals the J-cost at the golden ratio, $C_Q/C_{\mathrm{geo}}=J(\varphi)\approx 0.118$, at the recognition crossover.
Domain cost is the two-argument cost used on mass/energy (or similar) pairs in this module; it is built from the standard J-cost $J(x)=(x+x^{-1})/2-1$. The sibling lemmas already show it vanishes when both arguments agree, stays nonnegative for positive arguments, and that the module's canonical threshold (the crossover scale) is positive.
Upstream, nonnegativity of recognition cost is the general fact that every recognition event has $J$-cost $\ge 0$ (ObserverForcing), which underwrites the domain-cost nonnegativity field here.
proof idea
One-line structure instance. The three fields of QCapacitanceCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra tactics or rewriting.
why it matters
Gives a single named inhabitant of the quantum-capacitance certificate so downstream physics lemmas can assume the three cost/threshold axioms by name rather than re-proving them. The module status is structural (0 sorry, 0 axiom); this def is the packaging step that makes that status usable.
It sits under the broader RS forcing picture: J is the unique cost from the Recognition Composition Law (T5), and $\varphi$ is the self-similar fixed point (T6), so the numerical target $J(\varphi)\approx 0.118$ is forced rather than fitted. No downstream consumers are wired yet in the graph; the natural next use is any theorem that quotes the crossover ratio $C_Q/C_{\mathrm{geo}}=J(\varphi)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.