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

  26private lemma log_phi_lt_0483 : Real.log Constants.phi < (0.483 : ℝ) := by

proof body

Term-mode proof.

  27  have h := IndisputableMonolith.Numerics.log_phi_lt_0483
  28  simpa [IndisputableMonolith.Constants.phi, Real.goldenRatio] using h
  29
  30/-! ## Part I: GCIC Constants -/
  31
  32/-- **GCIC STIFFNESS CONSTANT**: κ = (ln φ)²/2 ≈ 0.116. -/

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_lt_0483 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
mf_critical_temperature_bounds in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use
phase_barrier_upper in IndisputableMonolith.Papers.GCIC.Thermodynamics decl_use

depends on (3)

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
log_phi_lt_0483 in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
log_phi_lt_0483 in IndisputableMonolith.Numerics.Interval.Log decl_use