QCapacitanceCert
plain-language theorem explainer
Certificate structure bundling three algebraic facts used to derive quantum capacitance from J-cost: diagonal vanishing of domain cost, nonnegativity off the diagonal, and positivity of the canonical threshold. Downstream code builds a concrete inhabited instance. Pure definitional packaging of field obligations; no proof body.
Claim. A quantum-capacitance certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats quantum capacitance in the Recognition Science setting. Classically $C_Q = e^2 D(E_F)$ with $D$ the density of states; RS identifies the geometric-to-quantum crossover ratio $C_Q/C_{\mathrm{geo}}$ with the J-cost evaluated at the golden ratio, $J(\varphi)\approx 0.118$.
Domain cost is the two-argument cost used on mass/energy-like coordinates in this derivation; the certificate demands it vanish on the diagonal (equal arguments, nonzero) and stay nonnegative for positive arguments. The canonical threshold is the positive scale separating geometric and quantum capacitance regimes.
Upstream, recognition-event cost is already known nonnegative via the J-cost nonnegativity lemma in ObserverForcing ("The cost of any recognition event is non-negative").
proof idea
No proof: this is a structure declaration. It only names three Prop-valued fields that any inhabitant must supply. The concrete filler cert assigns domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos to those fields; cert_inhabited then wraps that instance as Nonempty.
why it matters
Gives a single named interface for the algebraic side-conditions of the quantum-capacitance-from-J-cost argument, so later lemmas can depend on one certificate rather than three free-floating hypotheses. Downstream, cert inhabits it and cert_inhabited records nonemptiness, closing the structural theorem status claimed by the module (0 sorry, 0 axiom).
In the RS forcing picture this sits under the J-uniqueness landmark (T5): the same J that solves the Recognition Composition Law supplies the numerical crossover $J(\varphi)\approx 0.118$. The certificate does not itself compute that number; it only packages the cost and threshold facts the derivation needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.