IndisputableMonolith.Chemistry.PolymerMorphologyFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Polymer Morphology from configDim — B15 Materials Depth
   6
   7Five canonical block-copolymer morphologies (= configDim D = 5):
   8  spherical, cylindrical, gyroid, lamellar, inverse (double gyroid /
   9  inverse cylindrical).
  10
  11Each morphology corresponds to a distinct minority-block volume-fraction
  12band on the φ-ladder.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith.Chemistry.PolymerMorphologyFromConfigDim
  18
  19inductive PolymerMorphology where
  20  | spherical
  21  | cylindrical
  22  | gyroid
  23  | lamellar
  24  | inverseMorph
  25  deriving DecidableEq, Repr, BEq, Fintype
  26
  27theorem polymerMorphology_count : Fintype.card PolymerMorphology = 5 := by decide
  28
  29structure PolymerMorphologyCert where
  30  five_morphologies : Fintype.card PolymerMorphology = 5
  31
  32def polymerMorphologyCert : PolymerMorphologyCert where
  33  five_morphologies := polymerMorphology_count
  34
  35end IndisputableMonolith.Chemistry.PolymerMorphologyFromConfigDim
  36