`amplitudes_normalized`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.TwoBranchGeodesic on GitHub at line 80.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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
  88
  89end Measurement
  90end IndisputableMonolith

papers checked against this theorem

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