pith. machine review for the scientific record. sign in
structure definition def or abbrev high

ColloidStabilityCert

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  28structure ColloidStabilityCert where
  29  five_regimes : Fintype.card ColloidRegime = 5
  30

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.