colloidRegime_count
plain-language theorem explainer
The declaration asserts that the finite type enumerating colloidal stability regimes contains exactly five elements. Soft-matter researchers applying the Recognition Science J-cost model to DLVO systems would cite this result to confirm the completeness of the five-regime classification. The proof is a one-line decision procedure that exhausts the inductive constructors and computes the cardinality directly.
Claim. The set of colloidal stability regimes has cardinality five: $|$ {electrostatically stabilized, sterically stabilized, depletion-stable, gel-forming, flocculated} $| = 5$.
background
The Colloid Stability from J-Cost module classifies soft-matter behavior into five regimes derived from the J-cost function that arises from the Recognition Composition Law. The inductive type ColloidRegime enumerates these regimes explicitly: electrostatic, steric, depletion, gelForming, and flocculated, each equipped with decidable equality and a Fintype instance. This enumeration corresponds to a configuration dimension of five, tied to the DLVO secondary minimum expressed as a canonical band in the J(φ) potential ratio.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic uses the Fintype instance derived from the five constructors of ColloidRegime to compute the cardinality and confirm it equals five.
why it matters
This cardinality supplies the five_regimes field inside the ColloidStabilityCert definition, which certifies the completeness of the stability classification. It aligns with the Recognition Science framework's use of finite enumerations for discrete regime counts, here fixing configDim D = 5 for colloidal systems under the J-cost derivation. The result closes the enumeration step without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.