cert
plain-language theorem explainer
Packages three elementary facts about the materials-module domain cost into a single Hall-resistance certificate: the cost vanishes on equal nonzero arguments, stays nonnegative for positive masses and energies, and the canonical threshold is strictly positive. Materials or condensed-matter workers citing the RS structural derivation of R_H = h/e^{2} use this bundle. The body is a pure structure constructor that wires three already-proved sibling lemmas.
Claim. There exists 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
Materials RS Module 8 is a structural (zero-sorry, zero-axiom) package whose physical target is the Hall resistance identity $R_H = h/e^2$, obtained from the Recognition Science fine-structure derivation rather than from a transport calculation.
The local cost is a two-argument real function domainCost. Its diagonal vanishing and nonnegativity are the materials-side specializations of the global J-cost nonnegativity theorem: the cost of any recognition event is nonnegative, and the identity event sits at the J-cost minimum $x=1$. The canonical threshold is a positive real scale against which that cost is compared.
The certificate structure simply records the three Prop-valued fields that any later Hall-resistance argument in this module is allowed to assume.
proof idea
One-line structure constructor. The three fields of RSMatl008Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional rewriting or case analysis occurs; the definition is pure packaging.
why it matters
Gives the module a single named inhabitant of the Hall-resistance certificate type, so downstream materials lemmas can depend on one object rather than three separate hypotheses. The module doc marks the whole file as a structural theorem supporting $R_H = h/e^2$ from the RS fine-structure constant (the $\alpha^{-1}$ band near 137). It sits downstream of the global cost-nonnegativity result in ObserverForcing and of the T5 J-uniqueness forcing chain that fixes $J(x)=(x+x^{-1})/2-1$. No further used-by edges are recorded yet; the certificate is the local closure point for the three cost/threshold obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.