theorem 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)

  30theorem alphaLock_pos : 0 < alphaLock := Constants.alphaLock_pos

Term-mode proof.

  31
  32/-- α_lock < 1 (re-export from Constants). -/

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

alphaLock_pos in IndisputableMonolith.Constants decl_use
alphaLock_in_unit_interval 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.