`C_equals_2A`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.C2ABridgeLight
domain: Measurement
line: 16 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.C2ABridgeLight on GitHub at line 16.

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

  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

papers checked against this theorem

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