polymerChainCert
plain-language theorem explainer
PolymerChainCert packages the assertion that polymer chains admit exactly five regimes together with the geometric ratio of persistence lengths being the golden ratio phi. Materials modelers working in Recognition Science would cite this certificate when deriving chain statistics from the phi-ladder. The definition is assembled directly from the regime-count theorem and the persistence-length ratio theorem.
Claim. The polymer chain certificate states that the number of polymer regimes is five and that the persistence length satisfies $L_p(k+1)/L_p(k) = phi$ for all natural numbers $k$.
background
Polymer chains in this framework are characterized by a persistence length that scales as powers of phi, with the ratio between consecutive levels fixed at phi. The module defines five canonical regimes (rigid rod, worm-like chain, ideal chain, excluded-volume, collapsed) matching a configuration dimension of five. Upstream, polymerRegimeCount establishes the cardinality five by decision, while persistenceLengthRatio proves the ratio equality by unfolding the definition and applying algebraic simplification with positivity.
proof idea
The definition constructs the PolymerChainCert structure by assigning the five_regimes field to the result of polymerRegimeCount and the phi_ratio field to persistenceLengthRatio. No additional tactics are required beyond the structure constructor.
why it matters
This definition supplies the concrete certificate required for polymer models in the Chemistry tier of Recognition Science. It closes the interface for chain-length derivations from the phi-ladder, consistent with the self-similar scaling forced by T6. No downstream uses are recorded yet, leaving open its integration into explicit mass or length formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.