cert
plain-language theorem explainer
Packages three domain-cost identities into a single Bravais3Cert record for the 3D crystal-structure count. Materials workers citing the RS Bravais-lattice derivation use this certificate as the inhabited witness. Construction is a direct field assignment of the sibling lemmas on diagonal vanishing, nonnegativity, and positive threshold.
Claim. There is a certificate asserting: the materials domain cost $C$ vanishes on the diagonal ($r\neq 0\Rightarrow C(r,r)=0$); $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold is strictly positive.
background
The module treats the classical count of 14 Bravais lattices in three dimensions as an RS structural theorem. The module doc frames the count via a doubled ConfigDim law at $D=3$: $14=2\cdot(2^3-1)$, dual-lattice structure rather than a raw $\phi$-ladder floor.
Bravais3Cert is the local interface bundling three cost axioms the count argument needs: diagonal vanishing of the domain cost, nonnegativity for positive mass/energy arguments, and positivity of a canonical threshold. Domain cost is the materials-side specialization of the RS J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Upstream, cost_nonneg in ObserverForcing records that every recognition event has nonnegative cost via Jcost_nonneg. The sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the three fields concretely for this domain.
proof idea
Not a tactic proof: a structure-value definition. The three fields of Bravais3Cert are filled by direct assignment to the in-module lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further rewriting or case analysis.
why it matters
Supplies the inhabited cost certificate the module's Bravais-lattice structural theorem sits on. The parent narrative is the Plan v7 claim that the 14 three-dimensional Bravais types arise from the $D=3$ count law (doubled for dual lattices), inside the broader forcing chain that already fixes $D=3$ at T8 and the eight-tick octave at T7. No downstream consumers are wired yet (used_by empty); the sibling cert_inhabited is the natural next witness. Closes the local certificate interface with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.