structure
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 36.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
33 rw [pow_succ, div_eq_iff hpos.ne']
34 ring
35
36structure PolymerChainCert where
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