IndisputableMonolith.Measurement.C2ABridgeLight

   1import Mathlib
   2import IndisputableMonolith.Measurement.TwoBranchGeodesic
   3
   4/-!
   5# C = 2A Bridge (Lightweight Export)
   6
   7Paper-safe export of the central bridge as a theorem to avoid heavy dependencies.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Measurement
  12
  13open Real
  14
  15/-- Lightweight export: existence of C and A with C = 2A and exp(-C) match. -/
  16theorem C_equals_2A (rot : TwoBranchRotation) :
  17  ∃ (C A : ℝ), C = 2 * A ∧ Real.exp (-C) = initialAmplitudeSquared rot := by
  18  use 2 * rateAction rot, rateAction rot
  19  refine ⟨by ring, ?_⟩
  20  simp only [initialAmplitudeSquared]
  21  have h := born_weight_from_rate rot
  22  convert h using 2
  23  ring
  24
  25end Measurement
  26end IndisputableMonolith
  27