cert
plain-language theorem explainer
Packages three proved properties of the materials domain cost and the canonical PCM threshold into one certificate structure. Anyone citing the RS claim that GST phase-change memory switches at J(φ)≈0.118 of melt energy density would reach for this bundle. Construction is a pure structure assembly: three sibling lemmas are plugged into the three fields.
Claim. There exists a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive arguments; and (iii) the canonical threshold is strictly positive.
background
The module treats phase-change memory (PCM) materials such as GST, which switch between amorphous and crystalline states above a threshold current density $J_{\mathrm{th}}$. Recognition Science predicts the dimensionless ratio $J_{\mathrm{th}}/J_{\mathrm{melt}}=J(\varphi)\approx 0.118$, i.e. switching at about 11.8% of the melting energy density.
The domain cost is the materials-side specialization of the RS J-cost $J(x)=(x+x^{-1})/2-1$ (forced unique by T5). The certificate structure PCMThresholdCert packages the three algebraic facts needed before any threshold comparison: diagonal vanishing, nonnegativity, and positivity of the canonical threshold (itself the value of $J$ at $\varphi$). Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative."
proof idea
One-line structure construction. The three fields of PCMThresholdCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive mass/energy arguments), and canonicalThreshold_pos (strict positivity of the canonical threshold). No new arithmetic is performed; the def only witnesses that those three results inhabit the certificate type.
why it matters
Gives a single named inhabitant of the PCM threshold certificate so downstream materials arguments can assume the three structural hypotheses in one hypothesis rather than three. Sits inside the Plan v7 materials pass that derives the GST switching ratio from the J-cost alone, tying the prediction to T5 J-uniqueness and the golden ratio fixed point $\varphi$ from T6. The module is marked structural (0 sorry, 0 axiom). No downstream consumers are wired yet (used_by empty), so this is the local packaging step before experimental comparison lemmas are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.