RSMatl008Cert
plain-language theorem explainer
Bundles three structural side-conditions for the Hall-resistance materials module: diagonal vanishing of the domain cost, non-negativity of that cost on the positive quadrant, and positivity of the canonical threshold. Anyone citing the module's inhabited certificate or the R_H = h/e^{2} structural claim uses this pack. It is a pure structure definition with no proof body; inhabitants are assembled from sibling lemmas.
Claim. A certificate for Materials Module 8 is a triple of facts: (i) for every nonzero real $r$, the domain cost at $(r,r)$ vanishes; (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 theorem package for the Hall resistance $R_H = h/e^2$, obtained from the Recognition Science fine-structure derivation. Status is structural: zero sorry, zero axiom.
The domain cost is the materials-side cost functional on a pair of positive reals (mass-like and energy-like coordinates). Its diagonal vanishing and non-negativity mirror the global recognition cost $J$, which is nonnegative on every recognition event (ObserverForcing: "The cost of any recognition event is non-negative"). The canonical threshold is the positive cutoff used to separate the structural Hall regime from off-shell configurations.
This structure does not itself compute $R_H$; it packages the three inequalities the module needs before the certificate can be inhabited.
proof idea
No proof body: the declaration is a structure (record type) with three fields of proposition type. Inhabitation is deferred to the sibling definition cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonempty witness cert_inhabited is then just ⟨cert⟩.
why it matters
Gives the typed interface that the Hall-resistance structural theorem must satisfy before the module can claim an inhabited certificate. Downstream, cert assembles a concrete inhabitant and cert_inhabited records Nonempty RSMatl008Cert, closing the structural status line (0 sorry, 0 axiom) for Module 8.
In the broader RS chain this sits on the materials side of the fine-structure story: Hall resistance $R_H = h/e^2$ is the condensed-matter readout of the same constants that fix $\alpha^{-1}$ in the RS band. The cost fields echo T5 J-uniqueness and the non-negativity of recognition cost; the positive threshold is the materials analogue of a creation or detection cutoff. The structure itself does not derive $R_H$; it only locks the side-conditions the derivation is allowed to use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.