cert
plain-language theorem explainer
Packages three structural facts for the perovskite solar-cell J-cost model: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Materials workers citing the RS efficiency certificate reach for this bundle. The definition is a pure structure constructor wiring three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost at $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats perovskite power-conversion efficiency (PCE) as a Recognition Science materials claim. Empirically PCE is climbing toward the Shockley–Queisser ceiling near 33.7%; RS predicts an initial improvement rate $J(\varphi)^{-1}%$ per year (about 8.47%/yr), consistent with the observed 6–10%/yr band from 2012–2020.
Domain cost is the local cost functional on material and energy coordinates; it is built from the global J-cost $J(x)=(x+x^{-1})/2-1$, the unique nonnegative cost forced by the Recognition Composition Law. The structure PerovskiteSolarCert packages the three minimal analytic properties any such cost must satisfy before efficiency statements are well-posed: diagonal vanishing (perfect match costs nothing), nonnegativity, and a positive canonical threshold.
Upstream, nonnegativity of recognition-event cost is already proved in ObserverForcing via Jcost_nonneg. The three field witnesses here are sibling lemmas in the same module.
proof idea
Pure structure construction. The three fields of PerovskiteSolarCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactics or algebraic work; the definition is the certificate object itself.
why it matters
Gives the inhabited certificate that the module’s structural theorem status (0 sorry, 0 axiom) rests on. Downstream the sibling cert_inhabited and any later PCE-rate theorems can quote a single object rather than three separate lemmas. In the broader RS chain this sits in the materials layer that applies the forced J-cost (T5) and the golden-ratio fixed point $\varphi$ (T6) to a concrete device class; it does not itself re-derive J or $\varphi$. No external used-by edges are recorded yet, so the certificate is presently a local anchor for the perovskite efficiency narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.