def
definition
complementAmplitudeSquared
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.TwoBranchGeodesic on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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