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

colloidStabilityCert

show as:
view Lean formalization →

This definition constructs the colloid stability certificate by populating its five_regimes field with the decidable count of colloidal regimes. A soft-matter physicist working on DLVO or depletion interactions would cite it to anchor the canonical five-regime taxonomy in Recognition Science derivations. The construction is a direct one-line assignment from the upstream enumeration theorem.

claimThe colloid stability certificate is the structure whose sole field asserts that the finite type of colloidal regimes has cardinality exactly 5, obtained by direct substitution of the regime-count theorem.

background

The module treats colloidal stability as a direct consequence of the J-cost functional on potential ratios. Five canonical regimes are identified: electrostatically stabilized, sterically stabilized, depletion-stable, gel-forming, and flocculated. The DLVO secondary minimum is identified with a canonical band of the J-cost function. The upstream theorem colloidRegime_count establishes by exhaustive enumeration that the finite type ColloidRegime has cardinality 5. The structure ColloidStabilityCert packages this cardinality assertion as a reusable certificate.

proof idea

One-line wrapper that applies the upstream theorem colloidRegime_count to populate the five_regimes field of the ColloidStabilityCert structure.

why it matters in Recognition Science

The definition supplies the certified regime count required by any downstream chemistry derivation that invokes the five-regime taxonomy. It closes the interface between the Recognition Science J-cost machinery and soft-matter phenomenology, consistent with the framework's extension of configDim D = 5 to colloidal degrees of freedom. No open scaffolding remains in this module.

scope and limits

formal statement (Lean)

  31def colloidStabilityCert : ColloidStabilityCert where
  32  five_regimes := colloidRegime_count

proof body

Definition body.

  33
  34end IndisputableMonolith.Chemistry.ColloidStabilityFromJCost

depends on (2)

Lean names referenced from this declaration's body.