cert
plain-language theorem explainer
Packages three elementary domain-cost facts into a single Polymorphism3Cert record: diagonal vanishing, nonnegativity, and a positive canonical threshold. Materials theorists citing the RS polymorphism-rate claim use this certificate as the structural witness that the J-cost domain model is well-posed. The body is a pure structure constructor wiring three already-proved lemmas.
Claim. There is a certificate 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
The module treats crystal polymorphism rates as a J-cost phenomenon. Active pharmaceutical ingredients show polymorphs in roughly 30–50% of cases; Recognition Science predicts a rate $J(\varphi)^{1/2}\approx 34.4%$, inside that band. The local cost is a domain-level specialization of the universal recognition cost $J$, imported from the Cost and Constants layers.
Polymorphism3Cert is the structural interface that packages the three well-posedness properties any such domain cost must satisfy before a rate theorem can fire: vanishing on the diagonal (equal mass and energy parameters), nonnegativity off the diagonal, and a strictly positive decision threshold. Upstream, cost_nonneg in ObserverForcing already records that every recognition event has nonnegative cost via Jcost_nonneg.
proof idea
One-line structure constructor. The three fields of Polymorphism3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No additional tactics or algebraic work occur at this site; the definition only assembles those proofs into the certificate record.
why it matters
Gives the materials layer a single named witness that the J-cost domain model is coherent. The module status line marks the surrounding development as a structural theorem (zero sorry, zero axiom), and this certificate is the packaged hypothesis bundle that any downstream polymorphism-rate statement would consume. It sits under the broader RS forcing chain: T5 fixes $J(x)=(x+x^{-1})/2-1$, and the materials prediction $J(\varphi)^{1/2}$ inherits nonnegativity and the identity minimum from that uniqueness. No used_by edges are recorded yet, so the certificate is presently a terminal packaging step rather than an active lemma in a larger proof tree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.