RSMatl003Cert
plain-language theorem explainer
Certificate structure bundling three structural properties for the copper FCC materials module: domain cost vanishes on the diagonal, is nonnegative for positive mass/energy arguments, and the canonical threshold is positive. Anyone citing the Cu lattice match (φ⁴ a₀ ≈ 3.615 Å at 0.3%) uses this bundle as the formal witness type. Pure structure definition; inhabitants are assembled from sibling lemmas.
Claim. A certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost satisfies $C(r,r)=0$; (ii) for all positive reals $m,e$, one has $C(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
background
Materials RS Module 3 treats the copper FCC lattice spacing against the Recognition Science length ladder. The module reports φ⁴ a₀ = 3.626 Å versus the experimental 3.615 Å (0.3% relative error) and classifies the result as a structural theorem with no sorry and no axioms.
The domain cost $C(m,e)$ is the materials-side specialization of the Recognition cost (imported from Cost and Constants). Upstream, ObserverForcing records that every recognition-event cost is nonnegative, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. The certificate isolates the three algebraic facts needed locally: diagonal vanishing, nonnegativity on the positive quadrant, and positivity of a fixed threshold scale used by the module.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge those three fields; the structure itself only names the interface.
proof idea
No proof body: this is a structure declaration whose fields are propositions. Inhabitation is deferred to the downstream definition cert, which fills the three fields by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonempty witness cert_inhabited is then the trivial constructor application ⟨cert⟩.
why it matters
Gives the typed witness that Module 3 is a closed structural certificate rather than a numerical claim floating free of the cost calculus. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty RSMatl003Cert, which is the standard RS pattern for module-level certification.
The parent materials narrative is the Cu FCC match at the φ-ladder rung φ⁴ a₀. The cost fields tie that geometric claim back to the global J-cost nonnegativity and identity-minimum story (T5 J-uniqueness, RCL), so the lattice spacing is not an isolated fit but sits inside the same cost geometry used elsewhere in the monolith. No open scaffold remains in this module: status is zero sorry, zero axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.