PCMThresholdCert
plain-language theorem explainer
Certificate structure bundling three facts for the RS phase-change memory threshold: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Materials theorists citing the prediction that GST switches at J(φ)≈0.118 of melt energy density use this bundle. It is a pure structure definition; inhabitants are built elsewhere.
Claim. A PCM threshold certificate is a triple of properties: (i) domain cost vanishes on equal nonzero arguments, $C(r,r)=0$ whenever $r\neq 0$; (ii) for positive mass and energy, $C(m,e)\ge 0$; (iii) the canonical threshold $T_*$ satisfies $T_*>0$.
background
The module treats phase-change memory (PCM) materials such as GST, which switch between amorphous and crystalline states at a threshold current density. Recognition Science predicts the dimensionless ratio of threshold to melt energy density equals the J-cost at the golden ratio: $J_{\mathrm{th}}/J_{\mathrm{melt}}=J(\varphi)\approx 0.118$.
Domain cost is the materials-side specialization of the RS cost functional (imported from Cost and Constants). The upstream nonnegativity result states that the cost of any recognition event is nonnegative, via $J$-cost nonnegativity on positive states. The canonical threshold is the positive scalar fixed by that $J(\varphi)$ evaluation; sibling lemmas prove diagonal vanishing, nonnegativity of domain cost, and positivity of the threshold separately.
This structure packages those three properties as a single certificate type for downstream use.
proof idea
No proof body: the declaration is a structure with three fields. Each field is a Prop stating one of the algebraic requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the structural hypotheses behind the PCM threshold claim in the materials layer. Downstream, cert builds a concrete inhabitant by wiring the three sibling lemmas, and cert_inhabited records Nonempty PCMThresholdCert. That closes the structural half of the module status line (0 sorry, 0 axiom) for the Plan v7 pass on phase-change memory from J-cost.
In the broader framework the certificate sits under the J-uniqueness landmark (T5): the same $J(x)=(x+x^{-1})/2-1$ that forces $\varphi$ also supplies the numerical switch ratio $J(\varphi)$. The structure does not itself compute the 0.118 figure; it only guarantees the cost and threshold side-conditions any such derivation must satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.