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

 234lemma alphaLock_lt_one : alphaLock < 1 := by

proof body

Term-mode proof.

 235  have hpos : 0 < phi := phi_pos
 236  unfold alphaLock
 237  have : 1 / phi > 0 := one_div_pos.mpr hpos
 238  linarith
 239
 240/-- Canonical locked C_lag constant: C_lock = φ^{−5}. -/

used by (6)

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_lt_one 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

depends on (5)

Lean names referenced from this declaration's body.

alphaLock in IndisputableMonolith.Constants decl_use
alphaLock_lt_one in IndisputableMonolith.Constants.FineStructureConstant decl_use
C_lag in IndisputableMonolith.Gravity.EightTickResonance decl_use
C_lock in IndisputableMonolith.Gravity.ILGAsymptoticEnhancement decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use