theorem proved tactic proof

`cLag_lt_one`

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

formal statement (Lean)

 125theorem cLag_lt_one : cLag_from_phi < 1 := by

proof body

Tactic-mode proof.

 126  have hlt : cLag_from_phi < 1 / 10 := cLag_lt_one_tenth
 127  have : (1 / 10 : ℝ) < 1 := by norm_num
 128  exact lt_trans hlt this
 129
 130/-- PROVEN: Product < 0.1 using algebraic bounds. -/

used by (1)

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

rs_params_small_proven in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use

depends on (3)

Lean names referenced from this declaration's body.

lt_trans in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
cLag_from_phi in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use
cLag_lt_one_tenth in IndisputableMonolith.Relativity.GRLimit.Parameters decl_use