`initialAmplitudeSquared`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Measurement.TwoBranchGeodesic on GitHub at line 72.

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

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

papers checked against this theorem

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