lambda_rec_dimensionless_id

formal source

  36
  37/-- Dimensionless identity for λ_rec (under mild physical positivity assumptions):
  38    (c^3 · λ_rec^2) / (ħ G) = 1/π. -/
  39lemma lambda_rec_dimensionless_id (B : BridgeData)
  40  (hc : 0 < B.c) (hh : 0 < B.hbar) (hG : 0 < B.G) :
  41  (B.c ^ 3) * (lambda_rec B) ^ 2 / (B.hbar * B.G) = 1 / Real.pi := by
  42  -- Expand λ_rec and simplify using sqrt and algebra
  43  unfold lambda_rec
  44  have h_pos : 0 < B.hbar * B.G / (Real.pi * B.c ^ 3) := by
  45    apply div_pos (mul_pos hh hG)
  46    exact mul_pos Real.pi_pos (pow_pos hc 3)
  47  -- Use (sqrt x)^2 = x for x ≥ 0
  48  have h_nonneg : 0 ≤ B.hbar * B.G / (Real.pi * B.c ^ 3) := le_of_lt h_pos
  49  have hsq : (Real.sqrt (B.hbar * B.G / (Real.pi * B.c ^ 3))) ^ 2 =
  50    B.hbar * B.G / (Real.pi * B.c ^ 3) := by
  51    simpa using Real.sq_sqrt h_nonneg
  52  -- Now simplify the target expression
  53  calc
  54    (B.c ^ 3) * (Real.sqrt (B.hbar * B.G / (Real.pi * B.c ^ 3))) ^ 2 / (B.hbar * B.G)
  55        = (B.c ^ 3) * (B.hbar * B.G / (Real.pi * B.c ^ 3)) / (B.hbar * B.G) := by
  56          simp [hsq]
  57    _ = ((B.c ^ 3) * (B.hbar * B.G)) / ((Real.pi * B.c ^ 3) * (B.hbar * B.G)) := by
  58          field_simp
  59    _ = 1 / Real.pi := by
  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