`lambda_rec_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Bridge.DataCore
domain: Bridge
line: 68 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Bridge.DataCore on GitHub at line 68.

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

  65  lambda_rec_dimensionless_id B H.c_pos H.hbar_pos H.G_pos
  66
  67/-- Positivity of λ_rec under physical assumptions. -/
  68lemma lambda_rec_pos (B : BridgeData) (H : Physical B) : 0 < lambda_rec B := by
  69  -- λ_rec = √(ħ G / (π c³)) > 0 since all components positive
  70  unfold lambda_rec
  71  apply Real.sqrt_pos.mpr
  72  apply div_pos
  73  · exact mul_pos H.hbar_pos H.G_pos
  74  · exact mul_pos Real.pi_pos (pow_pos H.c_pos 3)
  75
  76end IndisputableMonolith.BridgeData

papers checked against this theorem

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