`born_weight_from_rate`

proved

show as: view math explainer →

module: IndisputableMonolith.Measurement.TwoBranchGeodesic
domain: Measurement
line: 57 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.TwoBranchGeodesic on GitHub at line 57.

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

  54  exact Real.log_neg hsin_pos hsin_lt_one
  55
  56/-- Born weight from rate action: exp(-2A) = sin²(θ_s) -/
  57theorem born_weight_from_rate (rot : TwoBranchRotation) :
  58  Real.exp (- 2 * rateAction rot) = (Real.sin rot.θ_s) ^ 2 := by
  59  unfold rateAction
  60  -- exp(-2*(-log(sin θ))) = exp(2 log(sin θ))
  61  have ⟨h1, h2⟩ := rot.θ_s_bounds
  62  have hsin_pos : 0 < Real.sin rot.θ_s :=
  63    sin_pos_of_pos_of_lt_pi h1 (by linarith : rot.θ_s < π)
  64  calc Real.exp (- 2 * (- Real.log (Real.sin rot.θ_s)))
  65      = Real.exp (2 * Real.log (Real.sin rot.θ_s)) := by ring_nf
  66      _ = Real.exp (Real.log ((Real.sin rot.θ_s) ^ 2)) := by
  67        congr 1
  68        exact (Real.log_pow (Real.sin rot.θ_s) 2).symm
  69      _ = (Real.sin rot.θ_s) ^ 2 := Real.exp_log (pow_pos hsin_pos 2)
  70
  71/-- Initial amplitude |α₂|² = sin²(θ_s) from geometry -/
  72noncomputable def initialAmplitudeSquared (rot : TwoBranchRotation) : ℝ :=
  73  (Real.sin rot.θ_s) ^ 2
  74
  75/-- Complement amplitude |α₁|² = cos²(θ_s) -/
  76noncomputable def complementAmplitudeSquared (rot : TwoBranchRotation) : ℝ :=
  77  (Real.cos rot.θ_s) ^ 2
  78
  79/-- Amplitudes sum to 1 (normalization) -/
  80theorem amplitudes_normalized (rot : TwoBranchRotation) :
  81  initialAmplitudeSquared rot + complementAmplitudeSquared rot = 1 := by
  82  unfold initialAmplitudeSquared complementAmplitudeSquared
  83  exact Real.sin_sq_add_cos_sq rot.θ_s
  84
  85/-- The geodesic is independent of time parameterization (reparameterization invariance) -/
  86theorem residual_action_invariant (rot : TwoBranchRotation) :
  87  residualAction rot = π/2 - rot.θ_s := rfl

papers checked against this theorem

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