def
definition
polymerChainCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.PolymerChainLengthFromPhiLadder on GitHub at line 40.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
37 five_regimes : Fintype.card PolymerRegime = 5
38 phi_ratio : ∀ k, persistenceLength (k + 1) / persistenceLength k = phi
39
40noncomputable def polymerChainCert : PolymerChainCert where
41 five_regimes := polymerRegimeCount
42 phi_ratio := persistenceLengthRatio
43
44end IndisputableMonolith.Chemistry.PolymerChainLengthFromPhiLadder