lemma proved tactic proof

`log_phi_lt_0483`

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

formal statement (Lean)

 183private lemma log_phi_lt_0483 : log IndisputableMonolith.Constants.phi < (0.483 : ℝ) := by

proof body

Tactic-mode proof.

 184  rw [Real.log_lt_iff_lt_exp IndisputableMonolith.Constants.phi_pos]
 185  have hphi_hi : IndisputableMonolith.Constants.phi < (((16209 / 10000 : ℚ) : ℝ)) := by
 186    have hphi : IndisputableMonolith.Constants.phi < (1.6180340 : ℝ) := W8Bounds.phi_lt_16180340
 187    linarith
 188  exact lt_trans hphi_hi exp_0483_gt
 189

used by (8)

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

bcs_ratio_approx in IndisputableMonolith.Chemistry.SuperconductingTc decl_use
f_gap_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
log_phi_in_interval in IndisputableMonolith.Numerics.Interval.Log decl_use
log_phi_lt_0483 in IndisputableMonolith.Numerics.Interval.Log decl_use
gcic_stiffness_bounds in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use
log_phi_lt_0483 in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use
mf_critical_temperature_bounds in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use
phase_barrier_upper in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use

depends on (7)

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
lt_trans in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
exp_0483_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
log_phi_lt_0483 in IndisputableMonolith.Numerics.Interval.Log decl_use
phi_lt_16180340 in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
phi_lt_16180340 in IndisputableMonolith.Numerics.Interval.W8Bounds decl_use
log_phi_lt_0483 in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use