`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

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Bridge.DataCore on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

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.