PhaseDiagramCert
plain-language theorem explainer
The PhaseDiagramCert structure records that the set of matter phases has cardinality five and that the equilibrium threshold satisfies the six-clause canonical J-band conditions. Chemists building RS-derived phase diagrams cite it to fix the five-phase enumeration and the J-minimization property at the triple point. It is introduced as a bare record whose two fields are supplied directly by the Fintype instance on MatterPhase and an imported CanonicalCert.
Claim. A structure asserting that the cardinality of the set of matter phases equals five together with a canonical certificate requiring $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(ϕ)>0$, $0.11<J(ϕ)<0.13$, and $J(1/ϕ^2)>0$.
background
MatterPhase is the inductive enumeration solid | liquid | gas | plasma | supercritical equipped with DecidableEq, Repr, BEq and Fintype. CanonicalCert is the six-clause record imported from CanonicalJBand that encodes the essential algebraic properties of the J-cost function: it vanishes at unity, is reciprocal-invariant, positive at the golden ratio, confined to the narrow band (0.11,0.13), and positive at the reciprocal square of phi. The module documentation places the certificate inside the recognition-science account of the triple point, where the three primary phases simultaneously attain J-cost zero at a unique (T,P) locus.
proof idea
The declaration is a bare structure definition that simply packages the Fintype cardinality of MatterPhase and a reference to CanonicalCert. No lemmas are applied and no tactics are executed; the structure aggregates the two facts without further reduction.
why it matters
PhaseDiagramCert supplies the two data items consumed by the immediately downstream phaseDiagramCert definition in the same module, thereby closing the local scaffolding for the five-phase diagram. The cardinality field aligns with the module statement that five canonical phases equal configDim D=5, while the equilibrium_threshold field imports the J-uniqueness properties required by the T5 landmark of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.