lemma proved term proof

`alphaLock_pos`

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

formal statement (Lean)

 228lemma alphaLock_pos : 0 < alphaLock := by

Term-mode proof.

 229  have hphi := one_lt_phi
 230  unfold alphaLock
 231  have : 1 / phi < 1 := (div_lt_one phi_pos).mpr hphi
 232  linarith
 233

From the project-wide theorem graph. These declarations reference this one in their body.

alphaLock_in_unit_interval in IndisputableMonolith.Constants.FineStructureConstant decl_use
alphaLock_pos in IndisputableMonolith.Constants.FineStructureConstant decl_use
fine_structure_derived in IndisputableMonolith.Constants.FineStructureConstant decl_use
omega_lambda_lt_one in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
omega_lambda_pos in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
A_amplitude_bounds in IndisputableMonolith.Gravity.GravityParameters decl_use
p_steepness_pos in IndisputableMonolith.Gravity.GravityParameters decl_use
D_growth_ge_a in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
f_growth_gt_one in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
eightTickKernelParams in IndisputableMonolith.ILG.Kernel decl_use
rsKernelParams in IndisputableMonolith.ILG.Kernel decl_use

Lean names referenced from this declaration's body.

alphaLock in IndisputableMonolith.Constants decl_use
one_lt_phi in IndisputableMonolith.Constants decl_use
alphaLock_pos in IndisputableMonolith.Constants.FineStructureConstant decl_use
one_lt_phi in IndisputableMonolith.PhiSupport decl_use
one_lt_phi in IndisputableMonolith.PhiSupport.Lemmas decl_use