`lambda_rec_dimensionless_id_physical`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Bridge.DataCore on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  60          field_simp [mul_comm, mul_left_comm, mul_assoc, pow_succ, pow_mul]
  61
  62/-- Dimensionless identity packaged with a physical-assumptions helper. -/
  63lemma lambda_rec_dimensionless_id_physical (B : BridgeData) (H : Physical B) :
  64  (B.c ^ 3) * (lambda_rec B) ^ 2 / (B.hbar * B.G) = 1 / Real.pi :=
  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.