cert
plain-language theorem explainer
Packages three domain-cost facts into a single RS4 Avogadro certificate: diagonal cost vanishes, cost is nonnegative off the axes, and the canonical threshold is positive. Chemists or RS auditors cite it as the inhabited witness that the Avogadro structure is realizable. The body is a pure structure assembly from three sibling lemmas.
Claim. There exists a certificate for the RS4 Avogadro structure: for every nonzero real $r$, the domain cost of $(r,r)$ is zero; for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; and the canonical threshold is strictly positive.
background
The Chemistry module is marked as a structural theorem package (zero sorry, zero axiom) under the heading AvogadroRS4Cert. It sits on the RS cost layer imported from Constants and Cost, and on the observer-forcing nonnegativity of recognition cost.
Domain cost is the local cost functional on pairs of positive reals used to score mole-scale matching. The structure Avogadro_Number_RS4 is the Prop-bundle of three requirements: cost vanishes on the diagonal (equal measure and expectation), cost is nonnegative for positive arguments, and a fixed positive threshold (the canonical cutoff) exists. Upstream, observer forcing already proves that every recognition event has nonnegative J-cost via Cost.Jcost_nonneg.
The certificate is the concrete inhabitant of that structure, not a new inequality.
proof idea
One-line structure construction. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis occurs.
why it matters
Closes the inhabitedness side of the RS Chemistry AvogadroRS4Cert package: the structure is not an empty interface. MODULE_DOC frames the whole file as a structural theorem with zero sorry and zero axiom, so this definition is the explicit witness that the three cost axioms hold simultaneously.
It does not yet feed a named parent theorem in the graph (no used_by edges), but it is the natural handle for any later mole-count or Avogadro-ladder argument that needs a single certificate object. In the broader forcing chain it sits downstream of J-cost nonnegativity (observer forcing) and of the RS cost calculus, not of T5–T8 geometric forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.