PolymerMorphology
plain-language theorem explainer
The declaration introduces an inductive type for the five canonical block-copolymer morphologies tied to configDim equal to 5. A polymer physicist mapping volume-fraction bands on the phi-ladder to self-assembled structures would cite this enumeration. The inductive definition with five constructors automatically supplies decidable equality and finite-type cardinality for immediate downstream use.
Claim. The inductive type of polymer morphologies consists of five constructors: spherical, cylindrical, gyroid, lamellar, and inverseMorph, each corresponding to a distinct minority-block volume-fraction band on the phi-ladder when configDim equals 5.
background
The module treats polymer morphology as a direct function of configDim set to 5 within the B15 materials depth of Recognition Science. Five canonical block-copolymer morphologies are listed: spherical, cylindrical, gyroid, lamellar, and inverse (double gyroid or inverse cylindrical). Each morphology is assigned a distinct minority-block volume-fraction band on the phi-ladder.
proof idea
The declaration is a pure inductive definition introducing five constructors. It derives DecidableEq, Repr, BEq, and Fintype automatically with no proof obligations or lemmas applied.
why it matters
This definition supplies the finite set whose exact cardinality of 5 is asserted by the structure PolymerMorphologyCert and proved by the theorem polymerMorphology_count. It fills the configDim slot in the B15 materials depth, linking morphologies to phi-ladder bands consistent with the self-similar fixed point phi and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.