PolymerChainCert
PolymerChainCert packages the assertions that polymer regimes number exactly five and that persistence lengths scale geometrically by the golden ratio phi. Materials modelers in the Recognition Science framework cite it when mapping the phi-ladder to chain stiffness scales. The declaration is a direct structure definition with no lemmas or computational obligations.
claimA structure consisting of the properties that the set of polymer regimes has cardinality five and that persistence length satisfies $L_p(k+1)/L_p(k)=phi$ for all natural numbers $k$, where $L_p(k)=phi^k$.
background
The module treats polymer chains through persistence length $L_p(k):=phi^k$ on the phi-ladder and five canonical regimes encoded by the inductive type with constructors rigidRod, wormLikeChain, idealChain, excludedVolume, collapsed. This type derives DecidableEq, Repr, BEq, and Fintype, so its cardinality is five by construction. The local setting equates these regimes to a configuration dimension of five, consistent with the Flory exponent approximation $nu approx 0.60$ derived from $1/phi^{1/3}$.
proof idea
This is a structure definition that directly records the two properties. No lemmas are applied and no tactics are used; the fields are populated later by the downstream construction polymerChainCert via polymerRegimeCount and persistenceLengthRatio.
why it matters in Recognition Science
PolymerChainCert supplies the interface instantiated by polymerChainCert in the same module. It fills the materials-tier claim that five regimes arise from the phi-ladder, linking T5 J-uniqueness and T6 phi fixed point to observable stiffness scales. The construction closes the mapping from the eight-tick octave to chain length without introducing new hypotheses.
scope and limits
- Does not derive explicit end-to-end distances or Flory exponents.
- Does not compute numerical persistence lengths for specific polymers.
- Does not address temperature or solvent corrections beyond phi scaling.
- Does not connect to the mass ladder or Berry threshold.
formal statement (Lean)
36structure PolymerChainCert where
37 five_regimes : Fintype.card PolymerRegime = 5
38 phi_ratio : ∀ k, persistenceLength (k + 1) / persistenceLength k = phi
39