theorem proved term proof

`alphaLock_lt_one`

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

formal statement (Lean)

  33theorem alphaLock_lt_one : alphaLock < 1 := Constants.alphaLock_lt_one

Term-mode proof.

  34
  35/-- α_lock lies in the open unit interval. -/

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

alphaLock_lt_one 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_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

Lean names referenced from this declaration's body.