`kappa_einstein_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants
domain: Constants
line: 459 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 459.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 456  rw [Real.rpow_neg phi_pos.le]
 457  field_simp [phi_ne_zero]
 458
 459lemma kappa_einstein_pos : 0 < kappa_einstein := by
 460  unfold kappa_einstein
 461  apply div_pos
 462  · apply mul_pos
 463    · apply mul_pos
 464      · norm_num
 465      · exact Real.pi_pos
 466    · exact G_pos
 467  · exact pow_pos c_pos 4
 468
 469/-!
 470  ## CODATA / SI constants (quarantined)
 471
 472  The empirical SI/CODATA numeric constants live in
 473  `IndisputableMonolith/Constants/Codata.lean` and are intentionally **excluded**
 474  from the certified surface import-closure.
 475
 476  If you need them for numeric comparisons or empirical reports, import
 477  `IndisputableMonolith.Constants.Codata` explicitly.
 478-/
 479
 480/-- Minimal RS units used in Core. -/
 481structure RSUnits where
 482  tau0 : ℝ
 483  ell0 : ℝ
 484  c    : ℝ
 485  c_ell0_tau0 : c * tau0 = ell0
 486
 487/-- Dimensionless bridge ratio \(K\).
 488
 489Defined (non-circularly) as \(K = \varphi^{1/2}\). -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.