  26
  27noncomputable def persistenceLength (k : ℕ) : ℝ := phi ^ k
  28
  29theorem persistenceLengthRatio (k : ℕ) :
  30    persistenceLength (k + 1) / persistenceLength k = phi := by
  31  unfold persistenceLength
  32  have hpos := pow_pos phi_pos k
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.