theorem proved term proof

`amplitudes_normalized`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  80theorem amplitudes_normalized (rot : TwoBranchRotation) :
  81  initialAmplitudeSquared rot + complementAmplitudeSquared rot = 1 := by

proof body

Term-mode proof.

  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) -/

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
independent in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
independent in IndisputableMonolith.Foundation.RSCoupledAxis decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
complementAmplitudeSquared in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use
initialAmplitudeSquared in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use
TwoBranchRotation in IndisputableMonolith.Measurement.TwoBranchGeodesic decl_use