cert
plain-language theorem explainer
Packages the three structural facts needed for the quantum-dot Coulomb-blockade certificate: vanishing of the domain cost on the diagonal, non-negativity off it, and positivity of the canonical J(φ) threshold. Anyone citing the RS blockade regime k_B T < E_C / J(φ) uses this bundle. The body is a pure structure instance wiring three already-proved lemmas.
Claim. There is a certificate recording that the quantum-dot domain cost vanishes on equal arguments ($\mathrm{domainCost}(r,r)=0$ for $r\neq 0$), is non-negative for positive mass and energy arguments, and that the canonical threshold (tied to $J(\varphi)$) is strictly positive.
background
The module treats Coulomb blockade in a quantum dot as a J-cost phenomenon. Classically the charging energy is $E_C=e^2/(2C)$; in Recognition Science the blockade is observable once $E_C$ exceeds $J(\varphi),k_B T$, i.e. once $k_B T < E_C/J(\varphi)\approx 8.47,E_C$, matching the experimental $k_B T\ll E_C$ window.
The domain cost is the local cost functional on mass/energy coordinates used to compare recognition events inside the dot. The canonical threshold is the positive scalar built from $J(\varphi)$ that sets the blockade floor. The certificate structure simply records the three algebraic properties those quantities must satisfy: diagonal vanishing, non-negativity, and threshold positivity.
Upstream, non-negativity of recognition cost is already forced in ObserverForcing via $J$-cost non-negativity on positive states; the in-module lemmas specialize that fact and the diagonal identity to the quantum-dot domain cost.
proof idea
One-line structure instance. The three fields of QDChargingCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (non-negativity for positive arguments), and canonicalThreshold_pos (strict positivity of the $J(\varphi)$-scale threshold). No additional reasoning is performed at this site.
why it matters
This is the inhabited certificate that closes the structural side of the quantum-dot Coulomb-blockade claim in the Plan v7 105th pass. The module is marked structural theorem (0 sorry, 0 axiom); the certificate is the single object that witnesses the three cost axioms the blockade inequality rests on.
It sits downstream of the J-cost non-negativity forced in ObserverForcing and of the T5 uniqueness of $J(x)=(x+x^{-1})/2-1$. The numerical factor $1/J(\varphi)\approx 8.47$ is the RS-native translation of the experimental temperature window. No further parent theorems are recorded in the graph yet; the certificate is the export surface for any later derivation that needs a packaged QD charging witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.