ColloidStabilityCert
plain-language theorem explainer
ColloidStabilityCert packages the claim that the colloidal stability problem admits exactly five regimes under the J-cost model. Soft-matter physicists would cite it when mapping DLVO potentials onto the Recognition Science phi-ladder. The structure is a thin wrapper that records the Fintype cardinality of the five-constructor inductive type ColloidRegime.
Claim. Let $R$ be the finite set of colloidal stability regimes. Then $|R| = 5$, where the regimes are electrostatic stabilization, steric stabilization, depletion stability, gel formation, and flocculation.
background
The module treats colloid stability as a direct consequence of the J-cost functional. It defines five canonical regimes via the inductive type ColloidRegime whose constructors are electrostatic, steric, depletion, gelForming, and flocculated; this type derives Fintype so that its cardinality is well-defined. The local setting identifies these regimes with configDim D = 5 and equates the DLVO secondary minimum to the canonical J(φ) band on the potential ratio.
proof idea
The declaration is a structure definition whose single field asserts Fintype.card ColloidRegime = 5. No tactics appear; the equality is supplied by the sibling definition colloidRegime_count and is simply recorded in the downstream constructor colloidStabilityCert.
why it matters
The structure supplies the cardinality fact required by colloidStabilityCert, completing the classification of soft-matter regimes inside the Chemistry module. It extends the Recognition Science forcing chain to colloidal scales by fixing five distinct J-cost bands, consistent with the five-regime count stated in the module header. No open questions or scaffolding remain in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.