polymerRegimeCount
plain-language theorem explainer
The theorem fixes the number of polymer chain regimes at five by counting the constructors of the inductive type that enumerates rigid rod, worm-like chain, ideal chain, excluded-volume, and collapsed cases. Polymer physicists working in the Recognition Science materials tier would cite this cardinality when setting the configuration dimension for persistence-length scaling and Flory exponents. The proof is a one-line decision procedure that succeeds because the type derives Fintype.
Claim. The set of canonical polymer chain regimes has cardinality five, where the regimes are rigid rod, worm-like chain, ideal chain, excluded volume, and collapsed.
background
In the Chemistry tier, polymer chains are described by length scales tied to the phi-ladder: persistence length scales as a power of phi, while the end-to-end distance follows an exponent approximately 1/phi^{1/3} that is consistent with the Flory value 0.588. The module states that five regimes (rigid rod, worm-like chain, ideal chain, excluded-volume, collapsed) correspond to configuration dimension D = 5. The PolymerRegime inductive type enumerates exactly these five cases and derives DecidableEq, Repr, BEq, and Fintype, so its cardinality is computable by decision procedures.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds directly because PolymerRegime is an inductive type with five constructors that derives Fintype, making the cardinality statement decidable without further lemmas.
why it matters
This result supplies the five_regimes component of the PolymerChainCert structure defined later in the same module. It anchors the materials tier by fixing the discrete count of regimes at five, matching the configuration dimension stated in the module documentation and interfacing with phi-ladder scaling for persistence lengths. The declaration closes a small scaffolding gap by providing an explicit, machine-checked enumeration that downstream certificates can reference without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.