PhaseCoexistenceCert
plain-language theorem explainer
The structure certifies that exactly five phase-coexistence topologies are recognized under the J-cost model. Thermodynamic chemists would cite it when classifying diagrams such as binodals and eutectics governed by the chemical-potential ratio. It is introduced as a direct structure definition that records the Fintype cardinality of the enumerated inductive type.
Claim. A certificate asserting that the finite set of phase-coexistence topologies has cardinality five, where the topologies are the binodal, eutectic, peritectic, azeotrope, and tricritical cases.
background
The module derives phase coexistence from the J-cost functional. It identifies five canonical topologies: two-phase binodal, three-phase eutectic, four-phase peritectic, azeotrope, and tricritical point, with binodal curvature gated by the canonical J(φ) band on the chemical-potential ratio. The local setting treats these as the complete list of configDim D = 5 configurations in the Recognition Science chemistry layer.
proof idea
This is a structure definition whose single field directly records that Fintype.card of the inductive PhaseCoexistenceTopology equals 5. It functions as a one-line wrapper that packages the built-in Fintype instance on the five-constructor inductive type.
why it matters
The certificate is instantiated by the downstream phaseCoexistenceCert definition in the same module. It confirms the enumeration of five topologies, consistent with the module's statement of configDim D = 5 and the forcing-chain landmarks T7 eight-tick octave and D = 3 spatial dimensions. No open questions are flagged in the supplied documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.