theorem proved term proof

`growth_factor_cert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 136theorem growth_factor_cert : GrowthFactorCert where
 137  D_positive := D_growth_pos

proof body

Term-mode proof.

 138  D_ge_a := D_growth_ge_a
 139  f_gt_one := f_growth_gt_one
 140  beta_positive := beta_growth_pos
 141
 142end
 143
 144end ILGGrowthFactor
 145end Gravity
 146end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.

beta_growth_pos in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
D_growth_ge_a in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
D_growth_pos in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
f_growth_gt_one in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
GrowthFactorCert in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
f_growth_gt_one in IndisputableMonolith.ILG.ISWSign decl_use