cert
plain-language theorem explainer
Packages the three structural properties of the Cu FCC materials cost into a single certificate: vanishing on the diagonal, non-negativity off the identity, and a positive canonical threshold. Materials auditors cite it as the inhabited witness that Module 3 meets its RS cost interface. Construction is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate for the Cu FCC materials module consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 3 treats the copper FCC lattice spacing against the RS length scale $\phi^4 a_0$, reported as $3.626,\mathrm{\AA}$ versus the experimental $3.615,\mathrm{\AA}$ (about $0.3%$ relative error), and is marked a structural theorem with no sorries or axioms.
The local cost is domainCost, a two-argument real function built from the Recognition Science $J$-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). The certificate structure RSMatl003Cert demands three interface facts: the cost vanishes when the two arguments coincide (away from zero), stays non-negative for positive arguments, and the module's canonical threshold is positive.
Upstream, non-negativity of recognition costs is already established in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost non-negativity on positive states. The three field proofs live as sibling lemmas in this same module.
proof idea
One-line structure instance. The three fields of RSMatl003Cert are filled by direct assignment to the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactic work or rewriting occurs; the definition is pure packaging of already-proved facts.
why it matters
Gives Module 3 a single named witness that its Cu FCC cost satisfies the standard RS materials interface (diagonal vanishing, non-negativity, positive threshold). That interface is the materials-side shadow of the $J$-cost axioms forced in the T5 uniqueness step of the forcing chain, specialized to lattice spacing comparisons on the $\phi$-ladder.
No downstream consumers are recorded yet (used_by is empty), so the certificate presently closes the module's own structural claim rather than feeding a larger theorem. Together with the sibling cert_inhabited, it documents that the $0.3%$ Cu match sits on a fully discharged cost interface, not on an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.