Theorem Library

-- Source line 134
theorem hasDerivAt_momentum_of_constant_inertia
    (D : MechanicalData V) (m : ℝ) (t : ℝ) (a : V)
    (hI : ∀ s, D.inertia s = m)
    (hvel : HasDerivAt D.velocity a t) :
    HasDerivAt D.momentum (m • a) t

-- Source line 148
theorem effectiveForce_eq_drive_at
    (D : MechanicalData V) (m : ℝ) (hN : IsNewtonianReduction D m) (t : ℝ) :
    D.effectiveForce t = http://D.drive t

-- Source line 156
theorem effectiveForce_eq_drive
    (D : MechanicalData V) (m : ℝ) (hN : IsNewtonianReduction D m) :
    D.effectiveForce = http://D.drive

-- Source line 166
theorem newton_second_law
    (D : MechanicalData V) (m : ℝ) (t : ℝ) (a : V)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m)
    (hAccel : HasAccelerationAt D a t) :
    http://D.drive t = m • a

-- Source line 179
theorem newtonian_reduction_theorem
    (D : MechanicalData V) (m : ℝ) (t : ℝ) (a : V)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m)
    (hAccel : HasAccelerationAt D a t) :
    http://D.drive t = m • a

-- Source line 191
theorem force_eq_momentum_derivative
    (D : MechanicalData V) (m : ℝ) (t : ℝ)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m) :
    HasDerivAt D.momentum (http://D.drive t) t

-- Source line 203
theorem newton_first_law_local
    (D : MechanicalData V) (m : ℝ) (t : ℝ) (a : V)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m)
    (hAccel : HasAccelerationAt D a t)
    (hForce : http://D.drive t = 0) :
    a = 0

-- Source line 218
theorem velocity_deriv_zero_of_force_zero
    (D : MechanicalData V) (m : ℝ)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m)
    (hVelDiff : ∀ t, DifferentiableAt ℝ D.velocity t)
    (hForce : ∀ t, http://D.drive t = 0) :
    ∀ t, HasDerivAt D.velocity 0 t

-- Source line 233
theorem velocity_constant_of_force_zero
    (D : MechanicalData V) (m : ℝ)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hN : IsNewtonianReduction D m)
    (hVelDiff : Differentiable ℝ D.velocity)
    (hForce : ∀ t, http://D.drive t = 0) :
    ∃ v₀ : V, ∀ t, D.velocity t = v₀

-- Source line 255
theorem momentum_product_rule
    (D : MechanicalData V) (t : ℝ) (I I' : ℝ) (v' : V)
    (hI : HasDerivAt D.inertia I' t)
    (hIval : D.inertia t = I)
    (hvel : HasDerivAt D.velocity v' t) :
    HasDerivAt D.momentum (I' • D.velocity t + I • v') t

-- Source line 278
theorem linear_drag_reduction
    (D : MechanicalData V) (m γ : ℝ) (t : ℝ) (a : V)
    (hm : 0 < m)
    (hI : ∀ s, D.inertia s = m)
    (hR : D.resistance = linearResistance γ D.velocity)
    (hM : ∀ s, D.memory s = 0)
    (hC : ∀ s, D.constraint s = 0)
    (hEvolution : SatisfiesGeneralEvolution D)
    (hAccel : HasAccelerationAt D a t) :
    m • a = http://D.drive t - γ • D.velocity t

-- Source line 315
theorem pair_force_sum_zero
    (P : PairInteraction V) (hP : IsActionReaction P) (x₁ x₂ : V) :
    P.force x₁ x₂ + P.force x₂ x₁ = 0

-- Source line 328
theorem pair_internal_force_cancel
    (P : PairInteraction V) (hP : IsActionReaction P) (x₁ x₂ : V) :
    P.force x₁ x₂ + P.force x₂ x₁ = 0

-- Source line 76
lemma kineticEnergy_nonneg {m : ℝ} (hm : 0 ≤ m) (v : V) : 0 ≤ kineticEnergy m v

-- Source line 99
theorem hasGradientAt_kineticEnergy (m : ℝ) (v : V) :
    HasGradientAt (kineticEnergy (V := V) m) (m • v) v

-- Source line 111
theorem hasGradientAt_sub_const {f : V → ℝ} {g x : V} (c : ℝ) (h : HasGradientAt f g x) :
    HasGradientAt (fun y => f y - c) g x

-- Source line 117
theorem hasGradientAt_const_sub {f : V → ℝ} {g x : V} (c : ℝ) (h : HasGradientAt f g x) :
    HasGradientAt (fun y => c - f y) (-g) x

-- Source line 164
theorem eulerLagrangeForcedAt_zero (Λ : LagrangianData V) (q qdot : Trajectory V) (t : ℝ) :
    EulerLagrangeForcedAt Λ q qdot (fun _ => 0) t ↔ EulerLagrangeAt Λ q qdot t

-- Source line 194
theorem eulerLagrangeAt_standardLagrangian_iff (m : ℝ) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ) :
    EulerLagrangeAt (standardLagrangian m P) q qdot t ↔
      HasDerivAt (fun s => m • qdot s) (-P.gradU (q t)) t

-- Source line 201
theorem eulerLagrangeAt_standardLagrangian_iff_accel (m : ℝ) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ) (a : V) (hv : HasDerivAt qdot a t) :
    EulerLagrangeAt (standardLagrangian m P) q qdot t ↔ m • a = -P.gradU (q t)

-- Source line 231
theorem momentum_eq_const_smul {D : MechanicalData V} {m : ℝ} (hI : ∀ t, D.inertia t = m) :
    D.momentum = fun s => m • D.velocity s

-- Source line 238
theorem canonicalMomentum_eq_mechanicalMomentum (D : MechanicalData V) (m : ℝ)
    (P : PotentialData V) (q : Trajectory V) (hI : ∀ t, D.inertia t = m) (t : ℝ) :
    canonicalMomentum (standardLagrangian m P) q D.velocity t = D.momentum t

-- Source line 246
theorem hasDerivAt_canonicalMomentum (D : MechanicalData V) (m : ℝ) (P : PotentialData V)
    (q : Trajectory V) (t : ℝ) (a : V) (hI : ∀ s, D.inertia s = m)
    (hAccel : HasAccelerationAt D a t) :
    HasDerivAt (canonicalMomentum (standardLagrangian m P) q D.velocity) (m • a) t

-- Source line 258
theorem eulerLagrangeAt_iff_generalEvolution {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} (hL : IsLagrangianReduction D m P q) (t : ℝ) :
    EulerLagrangeAt (standardLagrangian m P) q D.velocity t ↔
      HasDerivAt D.momentum (D.effectiveForce t) t

-- Source line 269
theorem eulerLagrangeAt_of_generalEvolution {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} (hL : IsLagrangianReduction D m P q)
    (hEvo : SatisfiesGeneralEvolution D) (t : ℝ) :
    EulerLagrangeAt (standardLagrangian m P) q D.velocity t

-- Source line 276
theorem satisfiesGeneralEvolution_of_eulerLagrange {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} (hL : IsLagrangianReduction D m P q)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q D.velocity t) :
    SatisfiesGeneralEvolution D

-- Source line 286
theorem newton_second_law_of_eulerLagrange {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} {t : ℝ} {a : V}
    (hL : IsLagrangianReduction D m P q)
    (hEL : EulerLagrangeAt (standardLagrangian m P) q D.velocity t)
    (hAccel : HasAccelerationAt D a t) :
    http://D.drive t = m • a

-- Source line 297
theorem mass_accel_eq_neg_gradU {D : MechanicalData V} {m : ℝ} {P : PotentialData V}
    {q : Trajectory V} {t : ℝ} {a : V}
    (hEL : EulerLagrangeAt (standardLagrangian m P) q D.velocity t)
    (hAccel : HasAccelerationAt D a t) :
    m • a = -P.gradU (q t)

-- Source line 333
theorem hasDerivAt_potential_comp (P : PotentialData V) (q : Trajectory V) (v : V) (t : ℝ)
    (hq : HasDerivAt q v t) :
    HasDerivAt (fun s => P.U (q s)) (⟪P.gradU (q t), v⟫) t

-- Source line 341
theorem hasDerivAt_energyAlong_zero (m : ℝ) (P : PotentialData V) (q qdot : Trajectory V)
    (t : ℝ) (a : V) (hq : HasDerivAt q (qdot t) t) (hv : HasDerivAt qdot a t)
    (hEL : EulerLagrangeAt (standardLagrangian m P) q qdot t) :
    HasDerivAt (energyAlong (standardLagrangian m P) q qdot) 0 t

-- Source line 368
theorem lagrangianEnergy_conserved (m : ℝ) (P : PotentialData V) (q qdot : Trajectory V)
    (acc : Trajectory V)
    (hq : ∀ t, HasDerivAt q (qdot t) t) (hv : ∀ t, HasDerivAt qdot (acc t) t)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q qdot t) (t₁ t₂ : ℝ) :
    energyAlong (standardLagrangian m P) q qdot t₁ =
      energyAlong (standardLagrangian m P) q qdot t₂

-- Source line 383
theorem mechanicalEnergy_conserved {D : MechanicalData V} {m : ℝ} {P : PotentialData V}
    {q : Trajectory V} (acc : Trajectory V) (hL : IsLagrangianReduction D m P q)
    (hEvo : SatisfiesGeneralEvolution D)
    (hv : ∀ t, HasDerivAt D.velocity (acc t) t) (t₁ t₂ : ℝ) :
    kineticEnergy m (D.velocity t₁) + P.U (q t₁) =
      kineticEnergy m (D.velocity t₂) + P.U (q t₂)

-- Source line 405
theorem nonconservative_channels_vanish {D : MechanicalData V} {m : ℝ} {P : PotentialData V}
    {q : Trajectory V} (hL : IsLagrangianReduction D m P q) :
    (∀ t, D.resistance t = 0) ∧ (∀ t, D.memory t = 0) ∧ (∀ t, D.constraint t = 0)

-- Source line 411
theorem not_isLagrangianReduction_of_nonconservative {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} (h : HasNonconservativeChannel D) :
    ¬ IsLagrangianReduction D m P q

-- Source line 426
theorem eulerLagrangeForcedAt_of_generalEvolution (D : MechanicalData V) (m : ℝ)
    (P : PotentialData V) (q : Trajectory V)
    (hI : ∀ t, D.inertia t = m) (hcons : ∀ t, http://D.drive t = -P.gradU (q t))
    (hEvo : SatisfiesGeneralEvolution D) (t : ℝ) :
    EulerLagrangeForcedAt (standardLagrangian m P) q D.velocity
      (fun s => -D.resistance s + D.memory s + D.constraint s) t

-- Source line 460
theorem drag_drive_not_conservative :
    ¬ ∃ g : ℝ → ℝ, ∀ t, http://dragData.drive t = -g (Real.sin t)

-- Source line 470
theorem dragData_not_lagrangianReduction :
    ¬ ∃ (m : ℝ) (P : PotentialData ℝ), IsLagrangianReduction dragData m P Real.sin

-- Source line 477
theorem resistive_not_lagrangianReduction (D : MechanicalData V) (m : ℝ)
    (P : PotentialData V) (q : Trajectory V) (t₀ : ℝ) (h : D.resistance t₀ ≠ 0) :
    ¬ IsLagrangianReduction D m P q

-- Source line 500
theorem harmonic_eulerLagrange_iff (m k : ℝ) (q qdot : Trajectory ℝ) (t a : ℝ)
    (hv : HasDerivAt qdot a t) :
    EulerLagrangeAt (harmonicLagrangian m k) q qdot t ↔ m * a = -(k * q t)

-- Source line 509
theorem harmonic_cos_isSolution (t : ℝ) :
    EulerLagrangeAt (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t

-- Source line 517
theorem harmonic_energy (m k : ℝ) (q qdot : Trajectory ℝ) (t : ℝ) :
    energyAlong (harmonicLagrangian m k) q qdot t =
      (1 / 2) * m * (qdot t) ^ 2 + (1 / 2) * k * (q t) ^ 2

-- Source line 524
theorem harmonic_cos_energy_conserved (t₁ t₂ : ℝ) :
    energyAlong (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t₁ =
      energyAlong (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t₂

-- Source line 561
theorem eulerLagrangeAt_on_dwell (G : AtlasGauge V) (Λ : AtlasLagrangianGauge V)
    (Pot : State → PotentialData V) (σ : Schedule) (q v : Trajectory V) {s : State} {t : ℝ}
    {a : V} (hEvo : SatisfiesGeneralEvolution (coupled G σ v))
    (hd : DwellsAt σ s t) (hv : HasDerivAt v a t)
    (hsel : SelectsLagrangianRegime G Λ Pot q s) :
    EulerLagrangeAt (Λ s) q v t

-- Source line 577
theorem eulerLagrangeAt_on_dwell_interval (G : AtlasGauge V) (Λ : AtlasLagrangianGauge V)
    (Pot : State → PotentialData V) (σ : Schedule) (q v acc : Trajectory V) {s : State}
    {a b : ℝ} (hEvo : SatisfiesGeneralEvolution (coupled G σ v))
    (hconst : ∀ u ∈ Set.Ioo a b, σ u = s) (hv : ∀ t, HasDerivAt v (acc t) t)
    (hsel : SelectsLagrangianRegime G Λ Pot q s) :
    ∀ t ∈ Set.Ioo a b, EulerLagrangeAt (Λ s) q v t

-- Source line 589
theorem eulerLagrangeAt_on_sampled_window (G : AtlasGauge V) (Λ : AtlasLagrangianGauge V)
    (Pot : State → PotentialData V) (q v : Trajectory V) {h : ℝ} (hh : 0 < h)
    (s : ℕ → State) (k : ℕ) {t : ℝ} {acc : V}
    (ht : t ∈ Set.Ioo ((k : ℝ) * h) (((k : ℝ) + 1) * h))
    (hEvo : SatisfiesGeneralEvolution (coupled G (sampledSchedule h s) v))
    (hv : HasDerivAt v acc t)
    (hsel : SelectsLagrangianRegime G Λ Pot q (s k)) :
    EulerLagrangeAt (Λ (s k)) q v t

-- Source line 603
theorem selectsLagrangianRegime_of_flat (G : AtlasGauge V) (Λ : AtlasLagrangianGauge V)
    (P : PotentialData V) (q : Trajectory V) (m : ℝ) (hflat : FlatGauge G m)
    (hlag : ∀ s : State, Λ s = standardLagrangian m P)
    (hcons : ∀ (s : State) (t : ℝ), G.driveOf s t = -P.gradU (q t)) (s : State) :
    SelectsLagrangianRegime G Λ (fun _ => P) q s where
  lag_eq

-- Source line 619
theorem eulerLagrangeAt_of_flat_gauge (G : AtlasGauge V)
    (P : PotentialData V) (σ : Schedule) (q v : Trajectory V) (m : ℝ) {t : ℝ} {a : V}
    (hflat : FlatGauge G m)
    (hcons : ∀ (s : State) (t : ℝ), G.driveOf s t = -P.gradU (q t))
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v)) (hv : HasDerivAt v a t) :
    EulerLagrangeAt (standardLagrangian m P) q v t

-- Source line 632
theorem eulerLagrangeAt_global_of_constant_gauge (G : AtlasGauge V)
    (Λ : AtlasLagrangianGauge V) (P : PotentialData V) (σ : Schedule)
    (q v : Trajectory V) (m : ℝ) (s₀ : State) {t : ℝ} {a : V}
    (hflat : FlatGauge G m) (hlag : ∀ s : State, Λ s = standardLagrangian m P)
    (hcons : ∀ (s : State) (t : ℝ), G.driveOf s t = -P.gradU (q t))
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v)) (hv : HasDerivAt v a t) :
    EulerLagrangeAt (Λ s₀) q v t

-- Source line 651
theorem lagrangian_switch_legal (Λ : AtlasLagrangianGauge V) (C : Config) (s : State)
    (z : Metric) (next : State) (hstep : Step C s z next) :
    cdist s next ≤ C.r ∧
      (Λ next ≠ Λ s → next ∈ legalNbhd C s ∧ C.A s next ∧ next ≠ s)

-- Source line 669
theorem lagrangian_frozen_of_gate_fail (Λ : AtlasLagrangianGauge V) (C : Config) (s : State)
    (z : Metric) (next : State) (hstep : Step C s z next)
    (hgate : ∀ u ∈ legalNbhd C s, score C s z u - score C s z s < C.Δ) :
    Λ next = Λ s

-- Source line 703
theorem satisfiesPhysicalEnergyBalance_of_conserved (Λ : LagrangianData V)
    (q qdot : Trajectory V) (Vc : ℕ → ℝ) (κ : ℝ) (recovery : ℕ → ℝ)
    (hcons : ∀ t₁ t₂ : ℝ, energyAlong Λ q qdot t₁ = energyAlong Λ q qdot t₂) :
    SatisfiesPhysicalEnergyBalance (constraintEnergyDataOfLagrangian Λ q qdot Vc κ recovery)

-- Source line 716
theorem augmentedEnergy_nonincreasing_of_conservative_regime (Λ : LagrangianData V)
    (q qdot : Trajectory V) (Vc : ℕ → ℝ) (κ : ℝ) (recovery : ℕ → ℝ) (t : ℕ)
    (hcons : ∀ t₁ t₂ : ℝ, energyAlong Λ q qdot t₁ = energyAlong Λ q qdot t₂)
    (hκ : 0 ≤ κ)
    (hrec : IsConstraintRecovering (constraintEnergyDataOfLagrangian Λ q qdot Vc κ recovery)) :
    IsEnergyStableStep (constraintEnergyDataOfLagrangian Λ q qdot Vc κ recovery) t

-- Source line 755
theorem exampleGauge_selects :
    SelectsLagrangianRegime exampleGauge exampleLagrangianGauge
      (fun s => harmonicPotential (exampleStiffness s)) Real.cos 0 where
  lag_eq

-- Source line 767
theorem exampleGauge_satisfiesGeneralEvolution :
    SatisfiesGeneralEvolution (coupled exampleGauge exampleSchedule fun s => -Real.sin s)

-- Source line 782
theorem example_eulerLagrange_on_dwell (t : ℝ) :
    EulerLagrangeAt (exampleLagrangianGauge 0) Real.cos (fun s => -Real.sin s) t

-- Source line 63
theorem poissonBracket_antisymm (f g : Observable V) (q p : V) :
    poissonBracket f g q p = -poissonBracket g f q p

-- Source line 82
theorem hasDerivAt_observable_along (F : Observable V) (H : HamiltonianData V)
    (q p : Trajectory V) {t : ℝ} (hH : HamiltonEquationsAt H q p t) :
    HasDerivAt (fun s => F.fn (q s) (p s)) (poissonWithHamiltonian F H (q t) (p t) t) t

-- Source line 92
theorem hasDerivAt_observable_poissonBracket (F Hobs : Observable V) (H : HamiltonianData V)
    (hHobs : IsObservableHamiltonian Hobs H) (q p : Trajectory V) {t : ℝ}
    (hH : HamiltonEquationsAt H q p t) :
    HasDerivAt (fun s => F.fn (q s) (p s)) (poissonBracket F Hobs (q t) (p t)) t

-- Source line 102
theorem observable_const_of_poisson_zero (F : Observable V) (H : HamiltonianData V)
    (q p : Trajectory V) (hH : ∀ t, HamiltonEquationsAt H q p t)
    (hzero : ∀ t, poissonWithHamiltonian F H (q t) (p t) t = 0) (t₁ t₂ : ℝ) :
    F.fn (q t₁) (p t₁) = F.fn (q t₂) (p t₂)

-- Source line 150
theorem isObservableHamiltonian_standard (m : ℝ) (P : PotentialData V) :
    IsObservableHamiltonian (standardHamiltonianObservable m P) (standardHamiltonian m P) where
  gradPos_eq

-- Source line 157
theorem poissonBracket_momentumObservable_free (m : ℝ) (w q p : V) :
    poissonBracket (momentumObservable w) (standardHamiltonianObservable m (freePotential V))
      q p = 0

-- Source line 164
theorem momentumObservable_const_of_free (m : ℝ) (w : V) (q p : Trajectory V)
    (hH : ∀ t, HamiltonEquationsAt (freeHamiltonian m) q p t) (t₁ t₂ : ℝ) :
    ⟪w, p t₁⟫ = ⟪w, p t₂⟫

-- Source line 70
theorem hasGradientAt_const_add {f : V → ℝ} {g x : V} (c : ℝ) (h : HasGradientAt f g x) :
    HasGradientAt (fun y => c + f y) g x

-- Source line 76
theorem hasGradientAt_add_const {f : V → ℝ} {g x : V} (c : ℝ) (h : HasGradientAt f g x) :
    HasGradientAt (fun y => f y + c) g x

-- Source line 115
theorem LegendreData.momentumMap_bijective {Λ : LagrangianData V} (ℒ : LegendreData Λ)
    (q : V) (t : ℝ) : Function.Bijective (momentumMap Λ q t)

-- Source line 122
theorem LegendreData.vel_unique {Λ : LagrangianData V} (ℒ₁ ℒ₂ : LegendreData Λ)
    (q p : V) (t : ℝ) : ℒ₁.vel q p t = ℒ₂.vel q p t

-- Source line 132
theorem momentumMap_bijective {m : ℝ} (hm : m ≠ 0) :
    Function.Bijective (fun v : V => m • v)

-- Source line 184
theorem legendreHamiltonian_congr (Λ : LagrangianData V) (ℒ₁ ℒ₂ : LegendreData Λ)
    (q p : V) (t : ℝ) :
    legendreHamiltonian Λ ℒ₁ q p t = legendreHamiltonian Λ ℒ₂ q p t

-- Source line 192
theorem legendreHamiltonian_at_momentum (Λ : LagrangianData V) (ℒ : LegendreData Λ)
    (q v : V) (t : ℝ) :
    legendreHamiltonian Λ ℒ q (Λ.gradVel q v t) t = energyFunction Λ q v t

-- Source line 221
theorem standardHamiltonian_apply (m : ℝ) (P : PotentialData V) (q p : V) (t : ℝ) :
    (standardHamiltonian m P).ham q p t = ‖p‖ ^ 2 / (2 * m) + P.U q

-- Source line 230
theorem standardHamiltonian_eq_kinetic_add_potential (m : ℝ) (hm : m ≠ 0)
    (P : PotentialData V) (q p : V) (t : ℝ) :
    (standardHamiltonian m P).ham q p t
      = LagrangianReduction.kineticEnergy m (m⁻¹ • p) + P.U q

-- Source line 246
theorem legendreHamiltonian_standardLagrangian (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q p : V) (t : ℝ) :
    legendreHamiltonian (standardLagrangian m P) (standardLegendre m hm P) q p t =
      (standardHamiltonian m P).ham q p t

-- Source line 322
theorem isHamiltonianReduction_standard (m : ℝ) (hm : m ≠ 0) (P : PotentialData V) :
    IsHamiltonianReduction (standardLagrangian m P) (standardLegendre m hm P)
      (standardHamiltonian m P) where
  ham_eq

-- Source line 331
theorem standardHamiltonian_gradMom_eq_velocity (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ) :
    (standardHamiltonian m P).gradMom (q t) (canonicalMomentum (standardLagrangian m P) q qdot t) t
      = qdot t

-- Source line 339
theorem standardHamiltonian_neg_gradPos_eq_momentum_deriv (m : ℝ) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ)
    (hEL : EulerLagrangeAt (standardLagrangian m P) q qdot t) :
    HasDerivAt (canonicalMomentum (standardLagrangian m P) q qdot)
      (-(standardHamiltonian m P).gradPos (q t)
        (canonicalMomentum (standardLagrangian m P) q qdot t) t) t

-- Source line 351
theorem hamiltonEquationsAt_of_eulerLagrangeAt {Λ : LagrangianData V} {ℒ : LegendreData Λ}
    {H : HamiltonianData V} (hred : IsHamiltonianReduction Λ ℒ H) (q qdot : Trajectory V)
    {t : ℝ} (hq : HasDerivAt q (qdot t) t) (hEL : EulerLagrangeAt Λ q qdot t) :
    HamiltonEquationsAt H q (canonicalMomentum Λ q qdot) t

-- Source line 363
theorem eulerLagrangeAt_of_hamiltonEquationsAt {Λ : LagrangianData V} {ℒ : LegendreData Λ}
    {H : HamiltonianData V} (hred : IsHamiltonianReduction Λ ℒ H) (q p : Trajectory V)
    {t : ℝ} (hH : HamiltonEquationsAt H q p t) :
    EulerLagrangeAt Λ q (resolvedVelocity ℒ q p) t

-- Source line 374
theorem hasDerivAt_of_hamiltonEquationsAt {Λ : LagrangianData V} {ℒ : LegendreData Λ}
    {H : HamiltonianData V} (hred : IsHamiltonianReduction Λ ℒ H) (q p : Trajectory V)
    {t : ℝ} (hH : HamiltonEquationsAt H q p t) :
    HasDerivAt q (resolvedVelocity ℒ q p t) t

-- Source line 384
theorem eulerLagrangeAt_iff_hamiltonEquationsAt {Λ : LagrangianData V} {ℒ : LegendreData Λ}
    {H : HamiltonianData V} (hred : IsHamiltonianReduction Λ ℒ H) (q qdot : Trajectory V)
    {t : ℝ} (hq : HasDerivAt q (qdot t) t) :
    EulerLagrangeAt Λ q qdot t ↔ HamiltonEquationsAt H q (canonicalMomentum Λ q qdot) t

-- Source line 395
theorem eulerLagrangeAt_iff_hamiltonEquationsAt_standard (m : ℝ) (hm : m ≠ 0)
    (P : PotentialData V) (q qdot : Trajectory V) {t : ℝ} (hq : HasDerivAt q (qdot t) t) :
    EulerLagrangeAt (standardLagrangian m P) q qdot t ↔
      HamiltonEquationsAt (standardHamiltonian m P) q (fun s => m • qdot s) t

-- Source line 404
theorem hasDerivAt_momentum_of_hamilton (m : ℝ) (P : PotentialData V) (q p : Trajectory V)
    {t : ℝ} (hH : HamiltonEquationsAt (standardHamiltonian m P) q p t) :
    HasDerivAt p (-P.gradU (q t)) t

-- Source line 409
theorem hasDerivAt_config_of_hamilton (m : ℝ) (P : PotentialData V) (q p : Trajectory V)
    {t : ℝ} (hH : HamiltonEquationsAt (standardHamiltonian m P) q p t) :
    HasDerivAt q (m⁻¹ • p t) t

-- Source line 415
theorem mass_accel_eq_neg_gradU_of_hamilton (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q qdot : Trajectory V) {t : ℝ} {a : V} (hq : HasDerivAt q (qdot t) t)
    (hv : HasDerivAt qdot a t)
    (hH : HamiltonEquationsAt (standardHamiltonian m P) q (fun s => m • qdot s) t) :
    m • a = -P.gradU (q t)

-- Source line 427
theorem newton_second_law_of_hamilton {D : MechanicalData V} {m : ℝ} {P : PotentialData V}
    {q : Trajectory V} {t : ℝ} {a : V} (hm : m ≠ 0) (hL : IsLagrangianReduction D m P q)
    (hH : HamiltonEquationsAt (standardHamiltonian m P) q (fun s => m • D.velocity s) t)
    (hAccel : HasAccelerationAt D a t) :
    http://D.drive t = m • a

-- Source line 438
theorem satisfiesGeneralEvolution_of_hamilton {D : MechanicalData V} {m : ℝ}
    {P : PotentialData V} {q : Trajectory V} (hm : m ≠ 0) (hL : IsLagrangianReduction D m P q)
    (hH : ∀ t, HamiltonEquationsAt (standardHamiltonian m P) q (fun s => m • D.velocity s) t) :
    SatisfiesGeneralEvolution D

-- Source line 458
theorem standardHamiltonian_eq_energyFunction (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q v : V) (t : ℝ) :
    (standardHamiltonian m P).ham q ((standardLagrangian m P).gradVel q v t) t =
      energyFunction (standardLagrangian m P) q v t

-- Source line 467
theorem hamiltonianAlong_eq_energyAlong (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ) :
    hamiltonianAlong (standardHamiltonian m P) q
        (canonicalMomentum (standardLagrangian m P) q qdot) t =
      energyAlong (standardLagrangian m P) q qdot t

-- Source line 475
theorem hamiltonianAlong_eq_kinetic_add_potential (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q qdot : Trajectory V) (t : ℝ) :
    hamiltonianAlong (standardHamiltonian m P) q
        (canonicalMomentum (standardLagrangian m P) q qdot) t =
      LagrangianReduction.kineticEnergy m (qdot t) + P.U (q t)

-- Source line 485
theorem hamiltonianAlong_conserved (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q qdot acc : Trajectory V) (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hv : ∀ t, HasDerivAt qdot (acc t) t)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q qdot t) (t₁ t₂ : ℝ) :
    hamiltonianAlong (standardHamiltonian m P) q
        (canonicalMomentum (standardLagrangian m P) q qdot) t₁ =
      hamiltonianAlong (standardHamiltonian m P) q
        (canonicalMomentum (standardLagrangian m P) q qdot) t₂

-- Source line 500
theorem hamiltonianAlong_conserved_of_hamilton (m : ℝ) (hm : m ≠ 0) (P : PotentialData V)
    (q p : Trajectory V)
    (hH : ∀ t, HamiltonEquationsAt (standardHamiltonian m P) q p t) (t₁ t₂ : ℝ) :
    hamiltonianAlong (standardHamiltonian m P) q p t₁ =
      hamiltonianAlong (standardHamiltonian m P) q p t₂

-- Source line 541
theorem phaseNoetherQuantity_const {Λ : LagrangianData V} {ℒ : LegendreData Λ}
    {H : HamiltonianData V} (hred : IsHamiltonianReduction Λ ℒ H)
    (X : InfinitesimalGenerator V) (q p : Trajectory V)
    (hH : ∀ t, HamiltonEquationsAt H q p t)
    (hsym : IsLagrangianSymmetry Λ X q (resolvedVelocity ℒ q p)) (t₁ t₂ : ℝ) :
    phaseNoetherQuantity X q p t₁ = phaseNoetherQuantity X q p t₂

-- Source line 557
theorem phaseNoetherQuantity_const_of_eulerLagrange (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V)
    (hq : ∀ t, HasDerivAt q (qdot t) t) (hEL : ∀ t, EulerLagrangeAt Λ q qdot t)
    (hsym : IsLagrangianSymmetry Λ X q qdot) (t₁ t₂ : ℝ) :
    phaseNoetherQuantity X q (canonicalMomentum Λ q qdot) t₁ =
      phaseNoetherQuantity X q (canonicalMomentum Λ q qdot) t₂

-- Source line 587
theorem SelectsHamiltonianRegime.inertia_ne_zero {G : AtlasGauge V}
    {Λg : AtlasLagrangianGauge V} {Hg : AtlasHamiltonianGauge V}
    {Pot : State → PotentialData V} {q : Trajectory V} {s : State}
    (h : SelectsHamiltonianRegime G Λg Hg Pot q s) : G.inertiaOf s ≠ 0

-- Source line 596
theorem hamiltonEquationsAt_on_dwell (G : AtlasGauge V) (Λg : AtlasLagrangianGauge V)
    (Hg : AtlasHamiltonianGauge V) (Pot : State → PotentialData V) (σ : Schedule)
    (q v : Trajectory V) {s : State} {t : ℝ} {a : V}
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v)) (hd : DwellsAt σ s t)
    (hq : HasDerivAt q (v t) t) (hv : HasDerivAt v a t)
    (hsel : SelectsHamiltonianRegime G Λg Hg Pot q s) :
    HamiltonEquationsAt (Hg s) q (canonicalMomentum (Λg s) q v) t

-- Source line 611
theorem hamiltonEquationsAt_on_dwell_interval (G : AtlasGauge V) (Λg : AtlasLagrangianGauge V)
    (Hg : AtlasHamiltonianGauge V) (Pot : State → PotentialData V) (σ : Schedule)
    (q v acc : Trajectory V) {s : State} {a b : ℝ}
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v))
    (hconst : ∀ u ∈ Set.Ioo a b, σ u = s) (hq : ∀ t, HasDerivAt q (v t) t)
    (hv : ∀ t, HasDerivAt v (acc t) t)
    (hsel : SelectsHamiltonianRegime G Λg Hg Pot q s) :
    ∀ t ∈ Set.Ioo a b, HamiltonEquationsAt (Hg s) q (canonicalMomentum (Λg s) q v) t

-- Source line 624
theorem hamiltonEquationsAt_on_sampled_window (G : AtlasGauge V) (Λg : AtlasLagrangianGauge V)
    (Hg : AtlasHamiltonianGauge V) (Pot : State → PotentialData V) (q v : Trajectory V)
    {h : ℝ} (hh : 0 < h) (s : ℕ → State) (k : ℕ) {t : ℝ} {acc : V}
    (ht : t ∈ Set.Ioo ((k : ℝ) * h) (((k : ℝ) + 1) * h))
    (hEvo : SatisfiesGeneralEvolution (coupled G (sampledSchedule h s) v))
    (hq : HasDerivAt q (v t) t) (hv : HasDerivAt v acc t)
    (hsel : SelectsHamiltonianRegime G Λg Hg Pot q (s k)) :
    HamiltonEquationsAt (Hg (s k)) q (canonicalMomentum (Λg (s k)) q v) t

-- Source line 638
theorem hamiltonian_switch_legal (Hg : AtlasHamiltonianGauge V) (C : Config) (s : State)
    (z : Metric) (next : State) (hstep : Step C s z next) :
    cdist s next ≤ C.r ∧
      (Hg next ≠ Hg s → next ∈ legalNbhd C s ∧ C.A s next ∧ next ≠ s)

-- Source line 656
theorem hamiltonian_frozen_of_gate_fail (Hg : AtlasHamiltonianGauge V) (C : Config) (s : State)
    (z : Metric) (next : State) (hstep : Step C s z next)
    (hgate : ∀ u ∈ legalNbhd C s, score C s z u - score C s z s < C.Δ) :
    Hg next = Hg s

-- Source line 670
theorem freeHamiltonian_apply (m : ℝ) (q p : V) (t : ℝ) :
    (freeHamiltonian m).ham q p t = ‖p‖ ^ 2 / (2 * m)

-- Source line 677
theorem isHamiltonianReduction_free (m : ℝ) (hm : m ≠ 0) :
    IsHamiltonianReduction (freeLagrangian (V := V) m)
      (standardLegendre m hm (freePotential V)) (freeHamiltonian m)

-- Source line 684
theorem freeParticle_hamiltonEquationsAt (m : ℝ) (hm : m ≠ 0) (q₀ v₀ : V) (t : ℝ) :
    HamiltonEquationsAt (freeHamiltonian m) (fun s => q₀ + s • v₀) (fun _ => m • v₀) t

-- Source line 694
theorem freeHamiltonian_momentum_const (m : ℝ) (q p : Trajectory V)
    (hH : ∀ t, HamiltonEquationsAt (freeHamiltonian m) q p t) (t₁ t₂ : ℝ) : p t₁ = p t₂

-- Source line 708
theorem freeHamiltonian_config_affine (m : ℝ) (q p : Trajectory V)
    (hH : ∀ t, HamiltonEquationsAt (freeHamiltonian m) q p t) (t : ℝ) :
    q t = q 0 + t • (m⁻¹ • p 0)

-- Source line 737
theorem harmonicHamiltonian_apply (m k q p t : ℝ) :
    (harmonicHamiltonian m k).ham q p t = p ^ 2 / (2 * m) + (k / 2) * q ^ 2

-- Source line 746
theorem isHamiltonianReduction_harmonic (m k : ℝ) (hm : m ≠ 0) :
    IsHamiltonianReduction (harmonicLagrangian m k)
      (standardLegendre m hm (harmonicPotential k)) (harmonicHamiltonian m k)

-- Source line 752
theorem harmonicHamiltonian_equations_iff (m k : ℝ) (q p : Trajectory ℝ) (t : ℝ) :
    HamiltonEquationsAt (harmonicHamiltonian m k) q p t ↔
      HasDerivAt q (m⁻¹ * p t) t ∧ HasDerivAt p (-(k * q t)) t

-- Source line 765
theorem harmonic_cos_hamiltonEquationsAt (t : ℝ) :
    HamiltonEquationsAt (harmonicHamiltonian 1 1) Real.cos (fun s => -Real.sin s) t

-- Source line 774
theorem harmonic_cos_hamiltonian_conserved (t₁ t₂ : ℝ) :
    hamiltonianAlong (harmonicHamiltonian 1 1) Real.cos (fun s => -Real.sin s) t₁ =
      hamiltonianAlong (harmonicHamiltonian 1 1) Real.cos (fun s => -Real.sin s) t₂

-- Source line 791
theorem exampleGauge_selectsHamiltonianRegime :
    SelectsHamiltonianRegime exampleGauge exampleLagrangianGauge exampleHamiltonianGauge
      (fun s => harmonicPotential (exampleStiffness s)) Real.cos 0 where
  lagrangian

-- Source line 799
theorem example_hamiltonEquations_on_dwell (t : ℝ) :
    HamiltonEquationsAt (exampleHamiltonianGauge 0) Real.cos
      (canonicalMomentum (exampleLagrangianGauge 0) Real.cos (fun s => -Real.sin s)) t

-- Source line 826
theorem momentumMap_degenerate_not_injective (P : PotentialData ℝ) :
    ¬ Function.Injective (momentumMap (degenerateLagrangian P) 0 0)

-- Source line 835
theorem not_nonempty_legendreData_degenerate (P : PotentialData ℝ) :
    ¬ Nonempty (LegendreData (degenerateLagrangian P))

-- Source line 843
theorem nonempty_legendreData_standardLagrangian_iff (m : ℝ) (P : PotentialData ℝ) :
    Nonempty (LegendreData (standardLagrangian m P)) ↔ m ≠ 0

-- Source line 859
theorem no_hamiltonianReduction_of_zero_mass (P : PotentialData ℝ) :
    ¬ ∃ (ℒ : LegendreData (standardLagrangian (0 : ℝ) P)) (H : HamiltonianData ℝ),
        IsHamiltonianReduction (standardLagrangian (0 : ℝ) P) ℒ H

-- Source line 105
theorem hasDerivAt_gen_comp (X : InfinitesimalGenerator V) (q : Trajectory V) {v : V} {t : ℝ}
    (hq : HasDerivAt q v t) :
    HasDerivAt (fun s => X.gen (q s)) (X.genDeriv (q t) v) t

-- Source line 127
theorem noetherQuantity_add_gen (Λ : LagrangianData V) (X Y : InfinitesimalGenerator V)
    (q qdot : Trajectory V) (t : ℝ) {Z : InfinitesimalGenerator V}
    (hZ : Z.gen = fun x => X.gen x + Y.gen x) :
    noetherQuantity Λ Z q qdot t =
      noetherQuantity Λ X q qdot t + noetherQuantity Λ Y q qdot t

-- Source line 137
theorem differentiableAt_noetherQuantity (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) {t : ℝ} {p' : V}
    (hq : HasDerivAt q (qdot t) t)
    (hp : HasDerivAt (canonicalMomentum Λ q qdot) p' t) :
    DifferentiableAt ℝ (noetherQuantity Λ X q qdot) t

-- Source line 170
theorem IsLagrangianSymmetry.on (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) (h : IsLagrangianSymmetry Λ X q qdot) (s : Set ℝ) :
    IsLagrangianSymmetryOn Λ X q qdot s

-- Source line 177
theorem isLagrangianSymmetryAt_constantGenerator_iff (Λ : LagrangianData V) (w : V)
    (q qdot : Trajectory V) (t : ℝ) :
    IsLagrangianSymmetryAt Λ (constantGenerator w) q qdot t ↔
      ⟪Λ.gradPos (q t) (qdot t) t, w⟫ = 0

-- Source line 185
theorem isLagrangianSymmetry_constantGenerator_of_gradPos_zero (Λ : LagrangianData V) (w : V)
    (q qdot : Trajectory V) (h : ∀ t, Λ.gradPos (q t) (qdot t) t = 0) :
    IsLagrangianSymmetry Λ (constantGenerator w) q qdot

-- Source line 199
theorem hasDerivAt_noetherQuantity (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) {t : ℝ} {p' : V}
    (hq : HasDerivAt q (qdot t) t)
    (hp : HasDerivAt (canonicalMomentum Λ q qdot) p' t) :
    HasDerivAt (noetherQuantity Λ X q qdot)
      (⟪p', X.gen (q t)⟫ +
        ⟪canonicalMomentum Λ q qdot t, X.genDeriv (q t) (qdot t)⟫) t

-- Source line 213
theorem hasDerivAt_noetherQuantity_forced (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V) (Q : ForceField V) {t : ℝ}
    (hq : HasDerivAt q (qdot t) t)
    (hEL : EulerLagrangeForcedAt Λ q qdot Q t) :
    HasDerivAt (noetherQuantity Λ X q qdot)
      ((⟪Λ.gradPos (q t) (qdot t) t, X.gen (q t)⟫ +
          ⟪Λ.gradVel (q t) (qdot t) t, X.genDeriv (q t) (qdot t)⟫) +
        ⟪Q t, X.gen (q t)⟫) t

-- Source line 228
theorem hasDerivAt_noetherQuantity_eulerLagrange (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V) {t : ℝ}
    (hq : HasDerivAt q (qdot t) t) (hEL : EulerLagrangeAt Λ q qdot t) :
    HasDerivAt (noetherQuantity Λ X q qdot)
      (⟪Λ.gradPos (q t) (qdot t) t, X.gen (q t)⟫ +
        ⟪Λ.gradVel (q t) (qdot t) t, X.genDeriv (q t) (qdot t)⟫) t

-- Source line 253
theorem noetherConservedAt_of_symmetry (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) {t : ℝ} (hq : HasDerivAt q (qdot t) t)
    (hEL : EulerLagrangeAt Λ q qdot t) (hsym : IsLagrangianSymmetryAt Λ X q qdot t) :
    NoetherConservedAt Λ X q qdot t

-- Source line 262
theorem noetherBalanceAt_of_symmetry (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) (Q : ForceField V) {t : ℝ} (hq : HasDerivAt q (qdot t) t)
    (hEL : EulerLagrangeForcedAt Λ q qdot Q t)
    (hsym : IsLagrangianSymmetryAt Λ X q qdot t) :
    NoetherBalanceAt Λ X q qdot Q t

-- Source line 272
theorem noetherConservedAt_of_balance_zero_force (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V) (Q : ForceField V) {t : ℝ}
    (hbal : NoetherBalanceAt Λ X q qdot Q t) (hQ : Q t = 0) :
    NoetherConservedAt Λ X q qdot t

-- Source line 281
theorem not_noetherConservedAt_of_balance_ne (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V) (Q : ForceField V) {t : ℝ}
    (hbal : NoetherBalanceAt Λ X q qdot Q t) (hQ : (⟪Q t, X.gen (q t)⟫ : ℝ) ≠ 0) :
    ¬ NoetherConservedAt Λ X q qdot t

-- Source line 291
theorem const_on_Ioo_of_hasDerivAt_zero {f : ℝ → ℝ} {a b : ℝ}
    (h : ∀ t ∈ Set.Ioo a b, HasDerivAt f 0 t) {t₁ t₂ : ℝ} (h₁ : t₁ ∈ Set.Ioo a b)
    (h₂ : t₂ ∈ Set.Ioo a b) : f t₁ = f t₂

-- Source line 309
theorem noetherQuantity_const (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hEL : ∀ t, EulerLagrangeAt Λ q qdot t) (hsym : IsLagrangianSymmetry Λ X q qdot)
    (t₁ t₂ : ℝ) :
    noetherQuantity Λ X q qdot t₁ = noetherQuantity Λ X q qdot t₂

-- Source line 321
theorem noetherQuantity_const_on_Ioo (Λ : LagrangianData V) (X : InfinitesimalGenerator V)
    (q qdot : Trajectory V) {a b : ℝ} (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hEL : ∀ t ∈ Set.Ioo a b, EulerLagrangeAt Λ q qdot t)
    (hsym : IsLagrangianSymmetryOn Λ X q qdot (Set.Ioo a b))
    {t₁ t₂ : ℝ} (h₁ : t₁ ∈ Set.Ioo a b) (h₂ : t₂ ∈ Set.Ioo a b) :
    noetherQuantity Λ X q qdot t₁ = noetherQuantity Λ X q qdot t₂

-- Source line 343
theorem canonicalMomentum_component_const_of_translation_symmetry (Λ : LagrangianData V)
    (w : V) (q qdot : Trajectory V) (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hEL : ∀ t, EulerLagrangeAt Λ q qdot t)
    (hsym : ∀ t, ⟪Λ.gradPos (q t) (qdot t) t, w⟫ = 0) (t₁ t₂ : ℝ) :
    ⟪canonicalMomentum Λ q qdot t₁, w⟫ = ⟪canonicalMomentum Λ q qdot t₂, w⟫

-- Source line 355
theorem canonicalMomentum_const_of_translation_symmetry (Λ : LagrangianData V)
    (q qdot : Trajectory V) (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hEL : ∀ t, EulerLagrangeAt Λ q qdot t)
    (hsym : ∀ t, Λ.gradPos (q t) (qdot t) t = 0) (t₁ t₂ : ℝ) :
    canonicalMomentum Λ q qdot t₁ = canonicalMomentum Λ q qdot t₂

-- Source line 378
theorem noetherQuantity_constantGenerator_eq_momentum (D : MechanicalData V) (m : ℝ)
    (P : PotentialData V) (q : Trajectory V) (w : V) (hI : ∀ t, D.inertia t = m) (t : ℝ) :
    noetherQuantity (standardLagrangian m P) (constantGenerator w) q D.velocity t =
      ⟪D.momentum t, w⟫

-- Source line 388
theorem mechanicalMomentum_component_const_of_translation_symmetry (D : MechanicalData V)
    (m : ℝ) (P : PotentialData V) (q : Trajectory V) (w : V) (hI : ∀ t, D.inertia t = m)
    (hq : ∀ t, HasDerivAt q (D.velocity t) t)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q D.velocity t)
    (hsym : ∀ t, ⟪P.gradU (q t), w⟫ = 0) (t₁ t₂ : ℝ) :
    ⟪D.momentum t₁, w⟫ = ⟪D.momentum t₂, w⟫

-- Source line 403
theorem mechanicalMomentum_const_of_free (D : MechanicalData V) (m : ℝ)
    (P : PotentialData V) (q : Trajectory V) (hI : ∀ t, D.inertia t = m)
    (hq : ∀ t, HasDerivAt q (D.velocity t) t)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q D.velocity t)
    (hfree : ∀ t, P.gradU (q t) = 0) (t₁ t₂ : ℝ) :
    D.momentum t₁ = D.momentum t₂

-- Source line 434
theorem isTimeIndependent_standardLagrangian (m : ℝ) (P : PotentialData V) :
    IsTimeIndependent (standardLagrangian m P) where
  lag_const

-- Source line 442
theorem energyFunction_time_invariant (Λ : LagrangianData V) (h : IsTimeIndependent Λ)
    (q v : V) (t t' : ℝ) : energyFunction Λ q v t = energyFunction Λ q v t'

-- Source line 450
theorem energy_conserved_of_timeIndependent (m : ℝ) (P : PotentialData V)
    (q qdot acc : Trajectory V) (hq : ∀ t, HasDerivAt q (qdot t) t)
    (hv : ∀ t, HasDerivAt qdot (acc t) t)
    (hEL : ∀ t, EulerLagrangeAt (standardLagrangian m P) q qdot t) (t₁ t₂ : ℝ) :
    energyAlong (standardLagrangian m P) q qdot t₁ =
      energyAlong (standardLagrangian m P) q qdot t₂

-- Source line 461
theorem energy_eq_kinetic_add_potential (m : ℝ) (P : PotentialData V) (q qdot : Trajectory V)
    (t : ℝ) :
    energyAlong (standardLagrangian m P) q qdot t = kineticEnergy m (qdot t) + P.U (q t)

-- Source line 490
theorem noetherConservedAt_on_dwell (G : AtlasGauge V) (Λg : AtlasLagrangianGauge V)
    (Pot : State → PotentialData V) (Xg : AtlasNoetherGauge V) (σ : Schedule)
    (q v : Trajectory V) {s : State} {t : ℝ} {a : V}
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v))
    (hd : DwellsAt σ s t) (hq : HasDerivAt q (v t) t) (hv : HasDerivAt v a t)
    (hsel : SelectsLagrangianRegime G Λg Pot q s)
    (hsym : IsLagrangianSymmetryAt (Λg s) (Xg s) q v t) :
    NoetherConservedAt (Λg s) (Xg s) q v t

-- Source line 504
theorem selectedNoetherQuantity_const_on_dwell (G : AtlasGauge V)
    (Λg : AtlasLagrangianGauge V) (Pot : State → PotentialData V) (Xg : AtlasNoetherGauge V)
    (σ : Schedule) (q v acc : Trajectory V) {s : State} {a b : ℝ}
    (hEvo : SatisfiesGeneralEvolution (coupled G σ v))
    (hconst : ∀ u ∈ Set.Ioo a b, σ u = s)
    (hq : ∀ t, HasDerivAt q (v t) t) (hv : ∀ t, HasDerivAt v (acc t) t)
    (hsel : SelectsLagrangianRegime G Λg Pot q s)
    (hsym : SelectsNoetherSymmetry Λg Xg q v s (Set.Ioo a b))
    {t₁ t₂ : ℝ} (h₁ : t₁ ∈ Set.Ioo a b) (h₂ : t₂ ∈ Set.Ioo a b) :
    selectedNoetherQuantity Λg Xg q v s t₁ = selectedNoetherQuantity Λg Xg q v s t₂

-- Source line 521
theorem selectedNoetherQuantity_const_on_sampled_window (G : AtlasGauge V)
    (Λg : AtlasLagrangianGauge V) (Pot : State → PotentialData V) (Xg : AtlasNoetherGauge V)
    (q v acc : Trajectory V) {h : ℝ} (hh : 0 < h) (s : ℕ → State) (k : ℕ)
    (hEvo : SatisfiesGeneralEvolution (coupled G (sampledSchedule h s) v))
    (hq : ∀ t, HasDerivAt q (v t) t) (hv : ∀ t, HasDerivAt v (acc t) t)
    (hsel : SelectsLagrangianRegime G Λg Pot q (s k))
    (hsym : SelectsNoetherSymmetry Λg Xg q v (s k)
      (Set.Ioo ((k : ℝ) * h) (((k : ℝ) + 1) * h)))
    {t₁ t₂ : ℝ} (h₁ : t₁ ∈ Set.Ioo ((k : ℝ) * h) (((k : ℝ) + 1) * h))
    (h₂ : t₂ ∈ Set.Ioo ((k : ℝ) * h) (((k : ℝ) + 1) * h)) :
    selectedNoetherQuantity Λg Xg q v (s k) t₁ =
      selectedNoetherQuantity Λg Xg q v (s k) t₂

-- Source line 556
theorem noetherJump_eq_zero_of_gauges_match (Λg : AtlasLagrangianGauge V)
    (Xg : AtlasNoetherGauge V) (q qdot : Trajectory V) (s u : State) (t : ℝ)
    (hΛ : Λg u = Λg s) (hX : Xg u = Xg s) : noetherJump Λg Xg q qdot s u t = 0

-- Source line 564
theorem noetherJump_eq_zero_of_gate_fail (Λg : AtlasLagrangianGauge V)
    (Xg : AtlasNoetherGauge V) (q qdot : Trajectory V) (C : Config) (s : State) (z : Metric)
    (next : State) (t : ℝ) (hstep : Step C s z next)
    (hgate : ∀ u ∈ legalNbhd C s, score C s z u - score C s z s < C.Δ) :
    noetherJump Λg Xg q qdot s next t = 0

-- Source line 573
theorem noether_switch_legal (Λg : AtlasLagrangianGauge V) (Xg : AtlasNoetherGauge V)
    (C : Config) (s : State) (z : Metric) (next : State) (hstep : Step C s z next) :
    cdist s next ≤ C.r ∧
      ((Λg next ≠ Λg s ∨ Xg next ≠ Xg s) →
        next ∈ legalNbhd C s ∧ C.A s next ∧ next ≠ s)

-- Source line 594
theorem selectedNoetherQuantity_match_across_switch (Λg : AtlasLagrangianGauge V)
    (Xg : AtlasNoetherGauge V) (q qdot : Trajectory V) (s u : State) {t₁ tsw t₂ : ℝ}
    (hs : selectedNoetherQuantity Λg Xg q qdot s t₁ =
      selectedNoetherQuantity Λg Xg q qdot s tsw)
    (hmatch : noetherJump Λg Xg q qdot s u tsw = 0)
    (hu : selectedNoetherQuantity Λg Xg q qdot u tsw =
      selectedNoetherQuantity Λg Xg q qdot u t₂) :
    selectedNoetherQuantity Λg Xg q qdot s t₁ =
      selectedNoetherQuantity Λg Xg q qdot u t₂

-- Source line 629
theorem decayingLedger_recovering : IsConstraintRecovering decayingLedger

-- Source line 644
theorem decayingLedger_balance : SatisfiesPhysicalEnergyBalance decayingLedger

-- Source line 648
theorem decayingLedger_strict_decrease (n : ℕ) :
    augmentedEnergy decayingLedger (n + 1) < augmentedEnergy decayingLedger n

-- Source line 664
theorem noether_conservation_and_stability_are_distinct (Λ : LagrangianData V)
    (X : InfinitesimalGenerator V) (q qdot : Trajectory V)
    (hq : ∀ t, HasDerivAt q (qdot t) t) (hEL : ∀ t, EulerLagrangeAt Λ q qdot t)
    (hsym : IsLagrangianSymmetry Λ X q qdot) :
    (∀ t₁ t₂ : ℝ, noetherQuantity Λ X q qdot t₁ = noetherQuantity Λ X q qdot t₂) ∧
      (∀ n : ℕ, augmentedEnergy decayingLedger (n + 1) < augmentedEnergy decayingLedger n) ∧
      (∀ n : ℕ, IsEnergyStableStep decayingLedger n)

-- Source line 690
theorem freeLagrangian_translation_symmetry (m : ℝ) (w : V) (q qdot : Trajectory V) :
    IsLagrangianSymmetry (freeLagrangian m) (constantGenerator w) q qdot

-- Source line 698
theorem freeParticle_momentum_conserved (m : ℝ) (w q₀ v₀ : V) (t₁ t₂ : ℝ) :
    noetherQuantity (freeLagrangian m) (constantGenerator w)
        (fun t => q₀ + t • v₀) (fun _ => v₀) t₁ =
      noetherQuantity (freeLagrangian m) (constantGenerator w)
        (fun t => q₀ + t • v₀) (fun _ => v₀) t₂

-- Source line 714
theorem freeParticle_noetherQuantity_value (m : ℝ) (w q₀ v₀ : V) (t : ℝ) :
    noetherQuantity (freeLagrangian m) (constantGenerator w)
        (fun t => q₀ + t • v₀) (fun _ => v₀) t = ⟪m • v₀, w⟫

-- Source line 720
theorem harmonic_energy_conserved_reuse (t₁ t₂ : ℝ) :
    energyAlong (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t₁ =
      energyAlong (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t₂

-- Source line 732
theorem forced_freeParticle_eulerLagrangeForcedAt (w : V) (t : ℝ) :
    EulerLagrangeForcedAt (freeLagrangian (1 : ℝ)) (fun s => (s ^ 2 / 2) • w)
      (fun s => s • w) (fun _ => w) t

-- Source line 742
theorem forced_freeParticle_balance (w : V) (t : ℝ) :
    HasDerivAt (noetherQuantity (freeLagrangian (1 : ℝ)) (constantGenerator w)
      (fun s => (s ^ 2 / 2) • w) (fun s => s • w)) (‖w‖ ^ 2) t

-- Source line 757
theorem forced_freeParticle_not_conserved (w : V) (hw : w ≠ 0) (t : ℝ) :
    ¬ NoetherConservedAt (freeLagrangian (1 : ℝ)) (constantGenerator w)
      (fun s => (s ^ 2 / 2) • w) (fun s => s • w) t

-- Source line 773
theorem harmonic_dilation_noetherQuantity (t : ℝ) :
    noetherQuantity (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
      (fun s => -Real.sin s) t = -(Real.sin t * Real.cos t)

-- Source line 781
theorem harmonic_dilation_not_symmetry :
    ¬ IsLagrangianSymmetryAt (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
      (fun s => -Real.sin s) 0

-- Source line 788
theorem harmonic_dilation_noetherQuantity_not_const :
    noetherQuantity (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
        (fun s => -Real.sin s) 0 ≠
      noetherQuantity (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
        (fun s => -Real.sin s) (Real.pi / 4)

-- Source line 803
theorem harmonic_dilation_counterexample :
    (∀ t, EulerLagrangeAt (harmonicLagrangian 1 1) Real.cos (fun s => -Real.sin s) t) ∧
      ¬ IsLagrangianSymmetryAt (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
        (fun s => -Real.sin s) 0 ∧
      noetherQuantity (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
          (fun s => -Real.sin s) 0 ≠
        noetherQuantity (harmonicLagrangian 1 1) (dilationGenerator ℝ) Real.cos
          (fun s => -Real.sin s) (Real.pi / 4)

-- Source line 90
theorem hasDerivAt_div (O : MaxwellOperators X S) (F : FieldTrajectory X)
    (t : ℝ) (F' : X) (hF : HasDerivAt F F' t) :
    HasDerivAt (fun s => O.div (F s)) (O.div F') t

-- Source line 96
theorem hasDerivAt_curl (O : MaxwellOperators X S) (F : FieldTrajectory X)
    (t : ℝ) (F' : X) (hF : HasDerivAt F F' t) :
    HasDerivAt (fun s => O.curl (F s)) (O.curl F') t

-- Source line 103
theorem magneticConstraint_hasDerivAt_zero (O : MaxwellOperators X S)
    (D : MaxwellData X S) (t : ℝ) (hDivCurl : DivCurlZero O)
    (hFaraday : SatisfiesFaraday O D) :
    HasDerivAt (magneticConstraint O D) 0 t

-- Source line 114
theorem magneticConstraint_constant (O : MaxwellOperators X S) (D : MaxwellData X S)
    (hDivCurl : DivCurlZero O) (hFaraday : SatisfiesFaraday O D) :
    ∃ c : S, ∀ t, magneticConstraint O D t = c

-- Source line 128
theorem magneticGauss_propagates (O : MaxwellOperators X S) (D : MaxwellData X S)
    (t₀ : ℝ) (hDivCurl : DivCurlZero O) (hFaraday : SatisfiesFaraday O D)
    (hInitial : SatisfiesMagneticGaussAt O D t₀) :
    ∀ t, SatisfiesMagneticGaussAt O D t

-- Source line 141
theorem electricConstraint_hasDerivAt_zero (O : MaxwellOperators X S)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hDivCurl : DivCurlZero O) (hAmpere : SatisfiesAmpereMaxwell O C D)
    (hContinuity : SatisfiesChargeContinuity O D) :
    HasDerivAt (electricConstraint O C D) 0 t

-- Source line 156
theorem electricConstraint_constant (O : MaxwellOperators X S) (C : MaxwellConstants)
    (D : MaxwellData X S) (hDivCurl : DivCurlZero O)
    (hAmpere : SatisfiesAmpereMaxwell O C D)
    (hContinuity : SatisfiesChargeContinuity O D) :
    ∃ c : S, ∀ t, electricConstraint O C D t = c

-- Source line 172
theorem electricGauss_propagates (O : MaxwellOperators X S) (C : MaxwellConstants)
    (D : MaxwellData X S) (t₀ : ℝ) (hDivCurl : DivCurlZero O)
    (hAmpere : SatisfiesAmpereMaxwell O C D)
    (hContinuity : SatisfiesChargeContinuity O D)
    (hInitial : SatisfiesElectricGaussAt O C D t₀) :
    ∀ t, SatisfiesElectricGaussAt O C D t

-- Source line 185
theorem maxwell_constraints_propagate (O : MaxwellOperators X S) (C : MaxwellConstants)
    (D : MaxwellData X S) (t₀ : ℝ) (hDivCurl : DivCurlZero O)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hContinuity : SatisfiesChargeContinuity O D)
    (hMagneticInitial : SatisfiesMagneticGaussAt O D t₀)
    (hElectricInitial : SatisfiesElectricGaussAt O C D t₀) :
    ∀ t, SatisfiesMagneticGaussAt O D t ∧ SatisfiesElectricGaussAt O C D t

-- Source line 229
theorem effectiveFieldDrive_eq_maxwellDrive (O : MaxwellOperators X S)
    (C : MaxwellConstants) (D : MaxwellData X S) (G : GeneralFieldData (X × X))
    (hR : IsMaxwellReduction O C D G) :
    effectiveFieldDrive G = maxwellDrive O C D

-- Source line 236
theorem maxwell_reduction_theorem (O : MaxwellOperators X S) (C : MaxwellConstants)
    (D : MaxwellData X S) (G : GeneralFieldData (X × X))
    (hGeneral : SatisfiesGeneralFieldEvolution G)
    (hReduction : IsMaxwellReduction O C D G) :
    SatisfiesMaxwellEvolution O C D

-- Source line 259
theorem electric_vacuum_wave_equation (O : MaxwellWaveOperators X S)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hVacuum : IsVacuum D)
    (hEvolution : SatisfiesMaxwellEvolution O.toMaxwellOperators C D)
    (hGauss : SatisfiesElectricGaussAt O.toMaxwellOperators C D t)
    (hCurlCurl : CurlCurlIdentity O) :
    HasSecondDerivAt D.electric
      ((waveSpeedSq C) • O.laplacian (D.electric t)) t

-- Source line 310
theorem magnetic_vacuum_wave_equation (O : MaxwellWaveOperators X S)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hVacuum : IsVacuum D)
    (hEvolution : SatisfiesMaxwellEvolution O.toMaxwellOperators C D)
    (hGauss : SatisfiesMagneticGaussAt O.toMaxwellOperators D t)
    (hCurlCurl : CurlCurlIdentity O) :
    HasSecondDerivAt D.magnetic
      ((waveSpeedSq C) • O.laplacian (D.magnetic t)) t

-- Source line 359
theorem newton_lorentz_equation
    (D : ResonantEvolution.NewtonianReduction.MechanicalData X)
    (m q : ℝ) (t : ℝ) (a E B : X) (cross : X → X → X)
    (hEvolution : ResonantEvolution.NewtonianReduction.MechanicalData.SatisfiesGeneralEvolution D)
    (hNewton : ResonantEvolution.NewtonianReduction.IsNewtonianReduction D m)
    (hAccel : ResonantEvolution.NewtonianReduction.HasAccelerationAt D a t)
    (hDrive : http://D.drive t = lorentzForce cross q E B (D.velocity t)) :
    m • a = lorentzForce cross q E B (D.velocity t)

-- Source line 372
theorem charge_continuity_of_ampere_and_gauss
    (O : MaxwellOperators X S) (C : MaxwellConstants) (D : MaxwellData X S)
    (t : ℝ) (ρ' : S) (hDivCurl : DivCurlZero O)
    (hAmpere : SatisfiesAmpereMaxwell O C D)
    (hGauss : ∀ s, SatisfiesElectricGaussAt O C D s)
    (hCharge : HasDerivAt D.charge ρ' t) :
    HasDerivAt D.charge (-O.div (D.current t)) t

-- Source line 429
theorem electromagneticEnergy_nonneg (C : MaxwellConstants) (E B : X) :
    0 ≤ electromagneticEnergy C E B

-- Source line 38
theorem electromagneticEnergy_eq_components (C : MaxwellConstants) (E B : X) :
    electromagneticEnergy C E B = electricEnergy C E + magneticEnergy C B

-- Source line 42
theorem electricEnergy_nonneg (C : MaxwellConstants) (E : X) :
    0 ≤ electricEnergy C E

-- Source line 47
theorem magneticEnergy_nonneg (C : MaxwellConstants) (B : X) :
    0 ≤ magneticEnergy C B

-- Source line 54
theorem electromagneticEnergy_nonneg (C : MaxwellConstants) (E B : X) :
    0 ≤ electromagneticEnergy C E B

-- Source line 59
theorem electromagneticEnergy_eq_zero_iff (C : MaxwellConstants) (E B : X) :
    electromagneticEnergy C E B = 0 ↔ E = 0 ∧ B = 0

-- Source line 83
theorem hasDerivAt_norm_sq (F : ℝ → X) (F' : X) (t : ℝ)
    (hF : HasDerivAt F F' t) :
    HasDerivAt (fun s => ‖F s‖ ^ 2) (2 * inner ℝ (F t) F') t

-- Source line 90
theorem electromagneticEnergy_hasDerivAt
    (O : MaxwellOperators X S) (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D) :
    HasDerivAt (energyTrajectory C D)
      ((1 / http://C.mu) * inner ℝ (D.electric t) (O.curl (D.magnetic t))
        - inner ℝ (D.electric t) (D.current t)
        - (1 / http://C.mu) * inner ℝ (D.magnetic t) (O.curl (D.electric t))) t

-- Source line 131
theorem local_poynting_theorem
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P) :
    HasDerivAt (energyTrajectory C D)
      (-P.fluxDiv (poyntingVector P C (D.electric t) (D.magnetic t))
        - matterPower D t) t

-- Source line 150
theorem local_poynting_vacuum
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P) (hVacuum : IsVacuum D) :
    HasDerivAt (energyTrajectory C D)
      (-P.fluxDiv (poyntingVector P C (D.electric t) (D.magnetic t))) t

-- Source line 165
theorem energy_deriv_zero_of_vacuum_and_zero_flux
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P) (hVacuum : IsVacuum D)
    (hFlux : ZeroNetFluxAt P C D t) :
    HasDerivAt (energyTrajectory C D) 0 t

-- Source line 177
theorem energy_constant_of_vacuum_and_zero_flux
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P) (hVacuum : IsVacuum D)
    (hFlux : ∀ t, ZeroNetFluxAt P C D t) :
    ∀ t, energyTrajectory C D t = energyTrajectory C D 0

-- Source line 194
theorem field_energy_loss_eq_matter_power
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P)
    (hFlux : ZeroNetFluxAt P C D t) :
    HasDerivAt (energyTrajectory C D) (-matterPower D t) t

-- Source line 207
theorem field_matter_total_energy_hasDerivAt_zero
    (C : MaxwellConstants) (D : MaxwellData X S) (matterEnergy : ℝ → ℝ) (t : ℝ)
    (hField : HasDerivAt (energyTrajectory C D) (-matterPower D t) t)
    (hMatter : HasDerivAt matterEnergy (matterPower D t) t) :
    HasDerivAt (fun s => energyTrajectory C D s + matterEnergy s) 0 t

-- Source line 219
theorem magnetic_lorentz_power_zero (cross : X → X → X) (q : ℝ) (v B : X)
    (hCross : CrossOrthogonal cross) :
    inner ℝ v (q • cross v B) = 0

-- Source line 227
theorem lorentz_power_eq_electric_power (cross : X → X → X) (q : ℝ) (E B v : X)
    (hCross : CrossOrthogonal cross) :
    inner ℝ v (lorentzForce cross q E B v) = q * inner ℝ v E

-- Source line 237
theorem ohmic_matterPower (sigma : ℝ) (E : X) :
    inner ℝ E (ohmicCurrent sigma E) = sigma * ‖E‖ ^ 2

-- Source line 241
theorem ohmic_dissipation_nonneg (sigma : ℝ) (E : X) (hsigma : 0 ≤ sigma) :
    0 ≤ inner ℝ E (ohmicCurrent sigma E)

-- Source line 248
theorem field_energy_derivative_nonpos_of_ohmic_current
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (t sigma : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P)
    (hFlux : ZeroNetFluxAt P C D t)
    (hOhm : D.current t = ohmicCurrent sigma (D.electric t))
    (hsigma : 0 ≤ sigma) :
    HasDerivAt (energyTrajectory C D) (-sigma * ‖D.electric t‖ ^ 2) t ∧
      -sigma * ‖D.electric t‖ ^ 2 ≤ 0

-- Source line 59
theorem entropyProduction_nonneg (Θ : ThermalData)
    (hT : PositiveTemperature Θ) (hD : NonnegativeDissipation Θ) (t : ℝ) :
    0 ≤ entropyProduction Θ t

-- Source line 71
theorem entropy_derivative_lower_bound (Θ : ThermalData)
    (hS : SatisfiesEntropyBalance Θ) (hT : PositiveTemperature Θ)
    (hD : NonnegativeDissipation Θ) (t : ℝ) :
    Θ.heatPower t / Θ.temperature t ≤ deriv Θ.entropy t

-- Source line 94
theorem matter_total_energy_balance (M : MatterEnergyData) (t : ℝ)
    (hMech : SatisfiesMechanicalEnergyBalance M)
    (hInternal : SatisfiesInternalEnergyBalance M.thermal) :
    HasDerivAt
      (fun s => M.mechanicalEnergy s + M.thermal.internalEnergy s)
      (M.externalPower t + M.fieldMatterPower t + M.thermal.heatPower t) t

-- Source line 113
theorem field_matter_thermal_total_energy_balance
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (M : MatterEnergyData) (t : ℝ)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P)
    (hFlux : ZeroNetFluxAt P C D t)
    (hPower : M.fieldMatterPower t = matterPower D t)
    (hMech : SatisfiesMechanicalEnergyBalance M)
    (hInternal : SatisfiesInternalEnergyBalance M.thermal) :
    HasDerivAt
      (fun s => energyTrajectory C D s +
        (M.mechanicalEnergy s + M.thermal.internalEnergy s))
      (M.externalPower t + M.thermal.heatPower t) t

-- Source line 136
theorem isolated_total_energy_derivative_zero
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (M : MatterEnergyData)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P)
    (hFlux : ∀ t, ZeroNetFluxAt P C D t)
    (hPower : ∀ t, M.fieldMatterPower t = matterPower D t)
    (hMech : SatisfiesMechanicalEnergyBalance M)
    (hInternal : SatisfiesInternalEnergyBalance M.thermal)
    (hExternal : ∀ t, M.externalPower t = 0)
    (hHeat : ∀ t, M.thermal.heatPower t = 0) :
    ∀ t, HasDerivAt
      (fun s => energyTrajectory C D s +
        (M.mechanicalEnergy s + M.thermal.internalEnergy s)) 0 t

-- Source line 157
theorem isolated_total_energy_constant
    (O : MaxwellOperators X S) (P : PoyntingOperators X)
    (C : MaxwellConstants) (D : MaxwellData X S) (M : MatterEnergyData)
    (hEvolution : SatisfiesMaxwellEvolution O C D)
    (hPoynting : SatisfiesPoyntingIdentity O P)
    (hFlux : ∀ t, ZeroNetFluxAt P C D t)
    (hPower : ∀ t, M.fieldMatterPower t = matterPower D t)
    (hMech : SatisfiesMechanicalEnergyBalance M)
    (hInternal : SatisfiesInternalEnergyBalance M.thermal)
    (hExternal : ∀ t, M.externalPower t = 0)
    (hHeat : ∀ t, M.thermal.heatPower t = 0) :
    ∀ t,
      energyTrajectory C D t + (M.mechanicalEnergy t + M.thermal.internalEnergy t) =
      energyTrajectory C D 0 + (M.mechanicalEnergy 0 + M.thermal.internalEnergy 0)

-- Source line 182
theorem adiabatic_entropy_derivative_nonneg (Θ : ThermalData)
    (hS : SatisfiesEntropyBalance Θ) (hT : PositiveTemperature Θ)
    (hD : NonnegativeDissipation Θ) (hAdiabatic : ∀ t, Θ.heatPower t = 0)
    (t : ℝ) :
    0 ≤ deriv Θ.entropy t

-- Source line 197
theorem resistancePower_nonneg_of_opposing (v R : X)
    (hOpposing : 0 ≤ -inner ℝ v R) :
    0 ≤ resistancePower v R

-- Source line 205
theorem nonnegativeDissipation_of_resistancePower (Θ : ThermalData)
    (v R : ℝ → X)
    (hPower : ∀ t, Θ.dissipatedPower t = resistancePower (v t) (R t))
    (hOpposing : ∀ t, 0 ≤ -inner ℝ (v t) (R t)) :
    NonnegativeDissipation Θ

-- Source line 94
theorem IsNormalized.norm_eq_one {psi : H} (h : IsNormalized psi) : ‖psi‖ = 1

-- Source line 97
theorem http://IsNormalized.ne_zero {psi : H} (h : IsNormalized psi) : psi ≠ 0

-- Source line 103
theorem IsNormalized.inner_self {psi : H} (h : IsNormalized psi) :
    (inner ℂ psi psi : ℂ) = 1

-- Source line 108
theorem isNormalized_iff_inner_self {psi : H} :
    IsNormalized psi ↔ (inner ℂ psi psi : ℂ) = 1

-- Source line 118
theorem isNormalized_norm_inv_smul {psi : H} (h : psi ≠ 0) :
    IsNormalized ((‖psi‖ : ℂ)⁻¹ • psi)

-- Source line 125
theorem exists_isNormalized_smul {psi : H} (h : psi ≠ 0) :
    ∃ c : ℂ, c ≠ 0 ∧ IsNormalized (c • psi)

-- Source line 130
theorem IsNormalized.smul {psi : H} (h : IsNormalized psi) {c : ℂ} (hc : ‖c‖ = 1) :
    IsNormalized (c • psi)

-- Source line 153
theorem expectation_add_op (A B : H →L[ℂ] H) (psi : H) :
    expectation (A + B) psi = expectation A psi + expectation B psi

-- Source line 157
theorem expectation_smul_op (c : ℂ) (A : H →L[ℂ] H) (psi : H) :
    expectation (c • A) psi = c * expectation A psi

-- Source line 161
theorem expectation_id (psi : H) :
    expectation (http://ContinuousLinearMap.id ℂ H) psi = (inner ℂ psi psi : ℂ)

-- Source line 164
theorem IsNormalized.expectation_id {psi : H} (h : IsNormalized psi) :
    expectation (http://ContinuousLinearMap.id ℂ H) psi = 1

-- Source line 172
theorem expectation_conj_eq_self {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    conj (expectation A psi) = expectation A psi

-- Source line 178
theorem expectation_im_eq_zero {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    (expectation A psi).im = 0

-- Source line 183
theorem realExpectation_ofReal_eq {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    ((realExpectation A psi : ℝ) : ℂ) = expectation A psi

-- Source line 190
theorem expectation_mem_range_ofReal {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    expectation A psi ∈ Set.range ((↑) : ℝ → ℂ)

-- Source line 204
theorem http://IsEigenpair.ne_zero {A : H →L[ℂ] H} {lam : ℂ} {psi : H} (h : IsEigenpair A lam psi) :
    psi ≠ 0

-- Source line 207
theorem IsEigenpair.apply_eq {A : H →L[ℂ] H} {lam : ℂ} {psi : H} (h : IsEigenpair A lam psi) :
    A psi = lam • psi

-- Source line 211
theorem isEigenpair_iff_hasEigenvector {A : H →L[ℂ] H} {lam : ℂ} {psi : H} :
    IsEigenpair A lam psi ↔ HasEigenvector (A : H →ₗ[ℂ] H) lam psi

-- Source line 220
theorem IsEigenpair.hasEigenvalue {A : H →L[ℂ] H} {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) : HasEigenvalue (A : H →ₗ[ℂ] H) lam

-- Source line 225
theorem IsEigenpair.mem_eigenspace {A : H →L[ℂ] H} {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) : psi ∈ eigenspace (A : H →ₗ[ℂ] H) lam

-- Source line 230
theorem expectation_of_eigenpair {A : H →L[ℂ] H} {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) :
    expectation A psi = lam * (inner ℂ psi psi : ℂ)

-- Source line 235
theorem expectation_of_eigenpair_normalized {A : H →L[ℂ] H} {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) (hn : IsNormalized psi) : expectation A psi = lam

-- Source line 244
theorem eigenvalue_conj_eq_self {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) : conj lam = lam

-- Source line 254
theorem eigenvalue_isReal {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) : http://lam.im = 0

-- Source line 259
theorem exists_real_eigenvalue {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {lam : ℂ} {psi : H}
    (h : IsEigenpair A lam psi) : ∃ r : ℝ, (r : ℂ) = lam

-- Source line 265
theorem inner_eq_zero_of_eigenpair_ne {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {a b : ℂ} {x y : H}
    (hx : IsEigenpair A a x) (hy : IsEigenpair A b y) (hab : a ≠ b) :
    (inner ℂ x y : ℂ) = 0

-- Source line 278
theorem inner_eq_zero_of_mem_eigenspace_ne {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {a b : ℂ}
    {x y : H} (hx : x ∈ eigenspace (A : H →ₗ[ℂ] H) a) (hy : y ∈ eigenspace (A : H →ₗ[ℂ] H) b)
    (hab : a ≠ b) : (inner ℂ x y : ℂ) = 0

-- Source line 298
theorem mapsTo_eigenspace_self (A : H →L[ℂ] H) (lam : ℂ) :
    ∀ x ∈ eigenspace (A : H →ₗ[ℂ] H) lam, A x ∈ eigenspace (A : H →ₗ[ℂ] H) lam

-- Source line 308
theorem mapsTo_eigenspace_orthogonal {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (lam : ℂ) :
    ∀ x ∈ (eigenspace (A : H →ₗ[ℂ] H) lam)ᗮ, A x ∈ (eigenspace (A : H →ₗ[ℂ] H) lam)ᗮ

-- Source line 323
theorem spectralProjector_idem (A : H →L[ℂ] H) (lam : ℂ) :
    spectralProjector A lam ∘L spectralProjector A lam = spectralProjector A lam

-- Source line 328
theorem spectralProjector_isSelfAdjoint (A : H →L[ℂ] H) (lam : ℂ) :
    IsSelfAdjoint (spectralProjector A lam)

-- Source line 333
theorem spectralProjector_apply_of_mem {A : H →L[ℂ] H} {lam : ℂ} {x : H}
    (hx : x ∈ eigenspace (A : H →ₗ[ℂ] H) lam) : spectralProjector A lam x = x

-- Source line 338
theorem spectralProjector_apply_of_mem_orthogonal {A : H →L[ℂ] H} {lam : ℂ} {x : H}
    (hx : x ∈ (eigenspace (A : H →ₗ[ℂ] H) lam)ᗮ) : spectralProjector A lam x = 0

-- Source line 343
theorem spectralProjector_apply_mem (A : H →L[ℂ] H) (lam : ℂ) (x : H) :
    spectralProjector A lam x ∈ eigenspace (A : H →ₗ[ℂ] H) lam

-- Source line 348
theorem apply_spectralProjector (A : H →L[ℂ] H) (lam : ℂ) (x : H) :
    A (spectralProjector A lam x) = lam • spectralProjector A lam x

-- Source line 353
theorem isEigenpair_spectralComponent {A : H →L[ℂ] H} {lam : ℂ} {psi : H}
    (h : spectralComponent A lam psi ≠ 0) : IsEigenpair A lam (spectralComponent A lam psi)

-- Source line 381
theorem isEigenpair (R : SpectralResolution A n) (i : Fin n) :
    IsEigenpair A ((R.eigenvalue i : ℝ) : ℂ) (R.basis i)

-- Source line 389
theorem expand (R : SpectralResolution A n) (psi : H) :
    ∑ i, R.coeff psi i • R.basis i = psi

-- Source line 394
theorem apply_eq_sum (R : SpectralResolution A n) (psi : H) :
    A psi = ∑ i, (((R.eigenvalue i : ℝ) : ℂ) * R.coeff psi i) • R.basis i

-- Source line 402
theorem sum_normSq_coeff (R : SpectralResolution A n) (psi : H) :
    ∑ i, ‖R.coeff psi i‖ ^ 2 = ‖psi‖ ^ 2

-- Source line 415
theorem sum_normSq_coeff_of_normalized (R : SpectralResolution A n) {psi : H}
    (h : IsNormalized psi) : ∑ i, ‖R.coeff psi i‖ ^ 2 = 1

-- Source line 436
theorem exists_spectralResolution {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) :
    Nonempty (SpectralResolution A (Module.finrank ℂ H))

-- Source line 442
theorem eigenspaces_directSum_isInternal {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) :
    DirectSum.IsInternal fun lam : Eigenvalues (A : H →ₗ[ℂ] H) =>
      eigenspace (A : H →ₗ[ℂ] H) lam

-- Source line 458
theorem SpectralResolution.expectation_eq_sum {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {n : ℕ}
    (R : SpectralResolution A n) (psi : H) :
    expectation A psi = ∑ i, ((R.eigenvalue i : ℝ) : ℂ) * ((‖R.coeff psi i‖ ^ 2 : ℝ) : ℂ)

-- Source line 477
theorem SpectralResolution.realExpectation_eq_sum {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {n : ℕ}
    (R : SpectralResolution A n) (psi : H) :
    realExpectation A psi = ∑ i, R.eigenvalue i * ‖R.coeff psi i‖ ^ 2

-- Source line 496
theorem variance_nonneg (A : H →L[ℂ] H) (psi : H) : 0 ≤ variance A psi

-- Source line 511
theorem centered_isSelfAdjoint {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    IsSelfAdjoint (centered A psi)

-- Source line 524
theorem variance_eq_expectation_centered_sq {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) (psi : H) :
    ((variance A psi : ℝ) : ℂ) = expectation (centered A psi ∘L centered A psi) psi

-- Source line 535
theorem variance_eq_zero_iff {A : H →L[ℂ] H} {psi : H} (hpsi : IsNormalized psi) :
    variance A psi = 0 ↔ IsEigenpair A (expectation A psi) psi

-- Source line 557
theorem mapsTo_eigenspace_of_commute {A B : H →L[ℂ] H} (hAB : A ∘L B = B ∘L A) (lam : ℂ) :
    ∀ x ∈ eigenspace (A : H →ₗ[ℂ] H) lam, B x ∈ eigenspace (A : H →ₗ[ℂ] H) lam

-- Source line 568
theorem apply_isEigenpair_of_commute {A B : H →L[ℂ] H} (hAB : A ∘L B = B ∘L A) {lam : ℂ}
    {psi : H} (h : IsEigenpair A lam psi) (hne : B psi ≠ 0) : IsEigenpair A lam (B psi)

-- Source line 575
theorem commute_directSum_isInternal {A B : H →L[ℂ] H} (hA : IsSelfAdjoint A)
    (hB : IsSelfAdjoint B) (hAB : A ∘L B = B ∘L A) :
    DirectSum.IsInternal fun (i : ℂ × ℂ) =>
      eigenspace (A : H →ₗ[ℂ] H) i.2 ⊓ eigenspace (B : H →ₗ[ℂ] H) i.1

-- Source line 592
theorem unitary_inner_map_map {U : H →L[ℂ] H} (hU : U ∈ unitary (H →L[ℂ] H)) (x y : H) :
    (inner ℂ (U x) (U y) : ℂ) = inner ℂ x y

-- Source line 602
theorem unitary_norm_map {U : H →L[ℂ] H} (hU : U ∈ unitary (H →L[ℂ] H)) (x : H) :
    ‖U x‖ = ‖x‖

-- Source line 610
theorem IsNormalized.unitary_map {U : H →L[ℂ] H} (hU : U ∈ unitary (H →L[ℂ] H)) {psi : H}
    (h : IsNormalized psi) : IsNormalized (U psi)

-- Source line 616
theorem isSelfAdjoint_unitary_conj {U A : H →L[ℂ] H} (hA : IsSelfAdjoint A) :
    IsSelfAdjoint (U * A * star U)

-- Source line 620
theorem expectation_unitary_conj {U A : H →L[ℂ] H} (hU : U ∈ unitary (H →L[ℂ] H)) (psi : H) :
    expectation (U * A * star U) (U psi) = expectation A psi

-- Source line 682
theorem exists_quantumIngredients {A : H →L[ℂ] H} (hA : IsSelfAdjoint A) {psi : H}
    (hpsi : IsNormalized psi) : Nonempty (QuantumIngredients A psi)

-- Source line 706
theorem isNormalized_ket0 : IsNormalized ket0

-- Source line 710
theorem isNormalized_ket1 : IsNormalized ket1

-- Source line 714
theorem inner_ket0_ket1 : (inner ℂ ket0 ket1 : ℂ) = 0

-- Source line 727
theorem pauliZ_isSelfAdjoint : IsSelfAdjoint pauliZ

-- Source line 734
theorem pauliX_isSelfAdjoint : IsSelfAdjoint pauliX

-- Source line 741
theorem diagD_isSelfAdjoint : IsSelfAdjoint diagD

-- Source line 748
theorem pauliZ_ket0 : pauliZ ket0 = (1 : ℂ) • ket0

-- Source line 753
theorem pauliZ_ket1 : pauliZ ket1 = (-1 : ℂ) • ket1

-- Source line 758
theorem pauliX_ket0 : pauliX ket0 = ket1

-- Source line 763
theorem pauliX_ket1 : pauliX ket1 = ket0

-- Source line 768
theorem diagD_ket0 : diagD ket0 = (2 : ℂ) • ket0

-- Source line 773
theorem diagD_ket1 : diagD ket1 = (3 : ℂ) • ket1

-- Source line 778
theorem isEigenpair_pauliZ_ket0 : IsEigenpair pauliZ 1 ket0

-- Source line 781
theorem isEigenpair_pauliZ_ket1 : IsEigenpair pauliZ (-1) ket1

-- Source line 799
theorem isNormalized_psiPlus : IsNormalized psiPlus

-- Source line 805
theorem coeff_psiPlus (i : Fin 2) :
    pauliZResolution.coeff psiPlus i = ((Real.sqrt 2)⁻¹ : ℝ)

-- Source line 812
theorem normSq_coeff_psiPlus (i : Fin 2) :
    ‖pauliZResolution.coeff psiPlus i‖ ^ 2 = 1 / 2

-- Source line 822
theorem realExpectation_pauliZ_psiPlus : realExpectation pauliZ psiPlus = 0

-- Source line 829
theorem expectation_pauliZ_ket0 : expectation pauliZ ket0 = 1

-- Source line 835
theorem pauliZ_comm_diagD : pauliZ ∘L diagD = diagD ∘L pauliZ

-- Source line 848
theorem commuting_example_directSum_isInternal :
    DirectSum.IsInternal fun (i : ℂ × ℂ) =>
      eigenspace (pauliZ : H2 →ₗ[ℂ] H2) i.2 ⊓ eigenspace (diagD : H2 →ₗ[ℂ] H2) i.1

-- Source line 853
theorem ket1_ne_neg_ket1 : ket1 ≠ (-1 : ℂ) • ket1

-- Source line 867
theorem pauliX_not_comm_pauliZ : pauliX ∘L pauliZ ≠ pauliZ ∘L pauliX

-- Source line 883
theorem isEigenpair_iScal : IsEigenpair iScal Complex.I ket0

-- Source line 887
theorem eigenvalue_iScal_not_real : (Complex.I).im ≠ 0

-- Source line 890
theorem expectation_iScal_not_real : (expectation iScal ket0).im ≠ 0

-- Source line 898
theorem iScal_not_isSelfAdjoint : ¬ IsSelfAdjoint iScal

-- Source line 80
theorem IsQuantumState.norm_eq_one {psi : H} (h : IsQuantumState psi) : ‖psi‖ = 1

-- Source line 84
theorem http://IsQuantumState.ne_zero {psi : H} (h : IsQuantumState psi) : psi ≠ 0

-- Source line 89
theorem IsQuantumState.inner_self {psi : H} (h : IsQuantumState psi) :
    (inner ℂ psi psi : ℂ) = 1

-- Source line 93
theorem isQuantumState_iff_isNormalized {psi : H} : IsQuantumState psi ↔ IsNormalized psi

-- Source line 118
theorem hbar_ne_zero : Q.hbar ≠ 0

-- Source line 120
theorem hbar_ne_zero' : (Q.hbar : ℂ) ≠ 0

-- Source line 124
theorem inner_op_left (x y : H) : (inner ℂ (Q.op x) y : ℂ) = inner ℂ x (Q.op y)

-- Source line 131
theorem generator_apply (x : H) : Q.generator x = (-Complex.I / (Q.hbar : ℂ)) • Q.op x

-- Source line 149
theorem SchrodingerAt.hasDerivAt {Q : QuantumHamiltonian H} {psi : ℝ → H} {t : ℝ}
    (h : SchrodingerAt Q psi t) :
    HasDerivAt psi ((-Complex.I / (Q.hbar : ℂ)) • Q.op (psi t)) t

-- Source line 153
theorem SchrodingerAt.differentiableAt {Q : QuantumHamiltonian H} {psi : ℝ → H} {t : ℝ}
    (h : SchrodingerAt Q psi t) : DifferentiableAt ℝ psi t

-- Source line 158
theorem schrodingerAt_iff {Q : QuantumHamiltonian H} {psi : ℝ → H} {t : ℝ} {d : H}
    (hd : HasDerivAt psi d t) :
    SchrodingerAt Q psi t ↔ (Complex.I * (Q.hbar : ℂ)) • d = Q.op (psi t)

-- Source line 205
theorem expectationAlong_apply (A : H →L[ℂ] H) (psi : ℝ → H) (t : ℝ) :
    expectationAlong A psi t = inner ℂ (psi t) (A (psi t))

-- Source line 209
theorem realExpectationAlong_eq_re (A : H →L[ℂ] H) (psi : ℝ → H) (t : ℝ) :
    realExpectationAlong A psi t = (expectationAlong A psi t).re

-- Source line 216
theorem commutator_apply (A B : H →L[ℂ] H) (x : H) :
    commutator A B x = A (B x) - B (A x)

-- Source line 224
theorem commutator_antisymm (A B : H →L[ℂ] H) : commutator A B = -commutator B A

-- Source line 228
theorem commutator_eq_zero_iff_comm {A B : H →L[ℂ] H} :
    commutator A B = 0 ↔ A ∘L B = B ∘L A

-- Source line 237
theorem hasDerivAt_inner {f g : ℝ → H} {f' g' : H} {t : ℝ}
    (hf : HasDerivAt f f' t) (hg : HasDerivAt g g' t) :
    HasDerivAt (fun s => (inner ℂ (f s) (g s) : ℂ))
      ((inner ℂ f' (g t) : ℂ) + inner ℂ (f t) g') t

-- Source line 246
theorem hasDerivAt_inner_eq_zero {Q : QuantumHamiltonian H} {phi psi : ℝ → H} {t : ℝ}
    (hphi : SchrodingerAt Q phi t) (hpsi : SchrodingerAt Q psi t) :
    HasDerivAt (fun s => (inner ℂ (phi s) (psi s) : ℂ)) 0 t

-- Source line 262
theorem hasDerivAt_inner_self_eq_zero {Q : QuantumHamiltonian H} {psi : ℝ → H} {t : ℝ}
    (h : SchrodingerAt Q psi t) :
    HasDerivAt (fun s => (inner ℂ (psi s) (psi s) : ℂ)) 0 t

-- Source line 268
theorem hasDerivAt_normSq_eq_zero {Q : QuantumHamiltonian H} {psi : ℝ → H} {t : ℝ}
    (h : SchrodingerAt Q psi t) : HasDerivAt (fun s => ‖psi s‖ ^ 2) 0 t

-- Source line 281
theorem inner_const_of_isSchrodingerEvolution {Q : QuantumHamiltonian H} {phi psi : ℝ → H}
    (hphi : IsSchrodingerEvolution Q phi) (hpsi : IsSchrodingerEvolution Q psi) (t₁ t₂ : ℝ) :
    (inner ℂ (phi t₁) (psi t₁) : ℂ) = inner ℂ (phi t₂) (psi t₂)

-- Source line 289
theorem norm_const_of_isSchrodingerEvolution {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (h : IsSchrodingerEvolution Q psi) (t₁ t₂ : ℝ) : ‖psi t₁‖ = ‖psi t₂‖

-- Source line 299
theorem isQuantumState_of_isSchrodingerEvolution {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (h : IsSchrodingerEvolution Q psi) {t₀ : ℝ} (h0 : IsQuantumState (psi t₀)) (t : ℝ) :
    IsQuantumState (psi t)

-- Source line 307
theorem norm_const_on_Icc {Q : QuantumHamiltonian H} {psi : ℝ → H} {a b : ℝ}
    (h : SchrodingerOn Q psi (Set.Icc a b)) {t : ℝ} (ht : t ∈ Set.Icc a b) :
    ‖psi t‖ = ‖psi a‖

-- Source line 326
theorem schrodinger_unique {Q : QuantumHamiltonian H} {phi psi : ℝ → H}
    (hphi : IsSchrodingerEvolution Q phi) (hpsi : IsSchrodingerEvolution Q psi) {t₀ : ℝ}
    (h0 : phi t₀ = psi t₀) : phi = psi

-- Source line 344
theorem IsPropagator.inner_map_map {Q : QuantumHamiltonian H} {U : ℝ → (H →L[ℂ] H)}
    (hU : IsPropagator Q U) (t : ℝ) (x y : H) :
    (inner ℂ (U t x) (U t y) : ℂ) = inner ℂ x y

-- Source line 351
theorem IsPropagator.norm_map {Q : QuantumHamiltonian H} {U : ℝ → (H →L[ℂ] H)}
    (hU : IsPropagator Q U) (t : ℝ) (x : H) : ‖U t x‖ = ‖x‖

-- Source line 361
theorem IsPropagator.isQuantumState {Q : QuantumHamiltonian H} {U : ℝ → (H →L[ℂ] H)}
    (hU : IsPropagator Q U) (t : ℝ) {psi : H} (h : IsQuantumState psi) :
    IsQuantumState (U t psi)

-- Source line 371
theorem hasDerivAt_expectationAlong {Q : QuantumHamiltonian H} {psi : ℝ → H}
    {A : ℝ → (H →L[ℂ] H)} {A' : H →L[ℂ] H} {t : ℝ}
    (hpsi : SchrodingerAt Q psi t) (hA : HasDerivAt A A' t) :
    HasDerivAt (fun s => (inner ℂ (psi s) (A s (psi s)) : ℂ))
      ((Complex.I / (Q.hbar : ℂ)) * (inner ℂ (psi t) (commutator Q.op (A t) (psi t)) : ℂ)
        + inner ℂ (psi t) (A' (psi t))) t

-- Source line 397
theorem hasDerivAt_expectationAlong_const {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (A : H →L[ℂ] H) {t : ℝ} (hpsi : SchrodingerAt Q psi t) :
    HasDerivAt (expectationAlong A psi)
      ((Complex.I / (Q.hbar : ℂ)) * (inner ℂ (psi t) (commutator Q.op A (psi t)) : ℂ)) t

-- Source line 408
theorem expectationAlong_const_of_commutator_zero {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) {A : H →L[ℂ] H} (hA : commutator Q.op A = 0)
    (t₁ t₂ : ℝ) : expectationAlong A psi t₁ = expectationAlong A psi t₂

-- Source line 417
theorem expectationAlong_const_of_comm {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) {A : H →L[ℂ] H} (hA : Q.op ∘L A = A ∘L Q.op)
    (t₁ t₂ : ℝ) : expectationAlong A psi t₁ = expectationAlong A psi t₂

-- Source line 423
theorem realExpectationAlong_const_of_commutator_zero {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) {A : H →L[ℂ] H} (hA : commutator Q.op A = 0)
    (t₁ t₂ : ℝ) : realExpectationAlong A psi t₁ = realExpectationAlong A psi t₂

-- Source line 432
theorem energy_const {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) (t₁ t₂ : ℝ) :
    expectationAlong Q.op psi t₁ = expectationAlong Q.op psi t₂

-- Source line 438
theorem realEnergy_const {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) (t₁ t₂ : ℝ) :
    realExpectationAlong Q.op psi t₁ = realExpectationAlong Q.op psi t₂

-- Source line 458
theorem hasDerivAt_phaseFactor (Q : QuantumHamiltonian H) (E t : ℝ) :
    HasDerivAt (fun s => phaseFactor Q E s)
      ((-Complex.I * (E : ℂ) / (Q.hbar : ℂ)) * phaseFactor Q E t) t

-- Source line 476
theorem isSchrodingerEvolution_phaseSolution {Q : QuantumHamiltonian H} {E : ℝ} {psi₀ : H}
    (h : Q.op psi₀ = ((E : ℝ) : ℂ) • psi₀) : IsSchrodingerEvolution Q (phaseSolution Q E psi₀)

-- Source line 490
theorem eq_phaseSolution_of_eigen {Q : QuantumHamiltonian H} {E : ℝ} {psi₀ : H} {psi : ℝ → H}
    (h : Q.op psi₀ = ((E : ℝ) : ℂ) • psi₀) (hpsi : IsSchrodingerEvolution Q psi)
    (h0 : psi 0 = psi₀) : psi = phaseSolution Q E psi₀

-- Source line 521
theorem isSchrodingerEvolution_spectralSolution (Q : QuantumHamiltonian H)
    (R : SpectralResolution Q.op n) (psi₀ : H) :
    IsSchrodingerEvolution Q (spectralSolution Q R psi₀)

-- Source line 555
theorem eq_spectralSolution {Q : QuantumHamiltonian H} {R : SpectralResolution Q.op n}
    {psi₀ : H} {psi : ℝ → H} (hpsi : IsSchrodingerEvolution Q psi) (h0 : psi 0 = psi₀) :
    psi = spectralSolution Q R psi₀

-- Source line 564
theorem coeff_sum_smul_basis {A : H →L[ℂ] H} (R : SpectralResolution A n) (c : Fin n → ℂ)
    (i : Fin n) : R.coeff (∑ j, c j • R.basis j) i = c i

-- Source line 577
theorem coeff_spectralSolution (Q : QuantumHamiltonian H) (R : SpectralResolution Q.op n)
    (psi₀ : H) (t : ℝ) (i : Fin n) :
    R.coeff (spectralSolution Q R psi₀ t) i
      = phaseFactor Q (R.eigenvalue i) t * R.coeff psi₀ i

-- Source line 585
theorem normSq_coeff_spectralSolution (Q : QuantumHamiltonian H) (R : SpectralResolution Q.op n)
    (psi₀ : H) (t : ℝ) (i : Fin n) :
    ‖R.coeff (spectralSolution Q R psi₀ t) i‖ ^ 2 = ‖R.coeff psi₀ i‖ ^ 2

-- Source line 592
theorem normSq_coeff_const_of_isSchrodingerEvolution {Q : QuantumHamiltonian H}
    {R : SpectralResolution Q.op n} {psi : ℝ → H} (hpsi : IsSchrodingerEvolution Q psi)
    (t₁ t₂ : ℝ) (i : Fin n) :
    ‖R.coeff (psi t₁) i‖ ^ 2 = ‖R.coeff (psi t₂) i‖ ^ 2

-- Source line 601
theorem norm_spectralSolution (Q : QuantumHamiltonian H) (R : SpectralResolution Q.op n)
    (psi₀ : H) (t : ℝ) : ‖spectralSolution Q R psi₀ t‖ = ‖psi₀‖

-- Source line 612
theorem IsSchrodingerEvolution.add {Q : QuantumHamiltonian H} {phi psi : ℝ → H}
    (hphi : IsSchrodingerEvolution Q phi) (hpsi : IsSchrodingerEvolution Q psi) :
    IsSchrodingerEvolution Q (fun t => phi t + psi t)

-- Source line 619
theorem IsSchrodingerEvolution.smul {Q : QuantumHamiltonian H} {psi : ℝ → H} (c : ℂ)
    (hpsi : IsSchrodingerEvolution Q psi) : IsSchrodingerEvolution Q (fun t => c • psi t)

-- Source line 640
theorem quantumBracket_antisymm (Q : QuantumHamiltonian H) (A B : H →L[ℂ] H) :
    quantumBracket Q A B = -quantumBracket Q B A

-- Source line 644
theorem quantumBracket_add_left (Q : QuantumHamiltonian H) (A B C : H →L[ℂ] H) :
    quantumBracket Q (A + B) C = quantumBracket Q A C + quantumBracket Q B C

-- Source line 651
theorem quantumBracket_add_right (Q : QuantumHamiltonian H) (A B C : H →L[ℂ] H) :
    quantumBracket Q A (B + C) = quantumBracket Q A B + quantumBracket Q A C

-- Source line 660
theorem quantumBracket_isSelfAdjoint {Q : QuantumHamiltonian H} {A B : H →L[ℂ] H}
    (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B) : IsSelfAdjoint (quantumBracket Q A B)

-- Source line 678
theorem hasDerivAt_expectationAlong_quantumBracket {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (A : H →L[ℂ] H) {t : ℝ} (hpsi : SchrodingerAt Q psi t) :
    HasDerivAt (expectationAlong A psi) (expectation (quantumBracket Q Q.op A) (psi t)) t

-- Source line 690
theorem poisson_quantumBracket_structural_analogy {V : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [CompleteSpace V] (Q : QuantumHamiltonian H) (A B : H →L[ℂ] H)
    (f g : ResonantEvolution.HamiltonianReduction.Observable V) (q p : V) :
    (quantumBracket Q A B = -quantumBracket Q B A ∧ quantumBracket Q A A = 0) ∧
      (ResonantEvolution.HamiltonianReduction.poissonBracket f g q p
          = -ResonantEvolution.HamiltonianReduction.poissonBracket g f q p ∧
        ResonantEvolution.HamiltonianReduction.poissonBracket f f q p = 0)

-- Source line 748
theorem extractAlong_eq_comp (E : QuantumExtractor H) (psi : ℝ → H) :
    extractAlong E psi = E.extract ∘ psi

-- Source line 753
theorem isSchrodingerEvolution_of_extract {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (E : QuantumExtractor H) (h : IsSchrodingerEvolution Q psi) :
    IsSchrodingerEvolution Q psi ∧ extractAlong E psi = fun t => E.extract (psi t)

-- Source line 760
theorem observation_energy_const {Q : QuantumHamiltonian H} {A : Observable H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) (t₁ t₂ : ℝ) :
    (quantumObservation Q A (psi t₁)).energy = (quantumObservation Q A (psi t₂)).energy

-- Source line 767
theorem hasDerivAt_observation_observable {Q : QuantumHamiltonian H} (A : Observable H)
    {psi : ℝ → H} {t : ℝ} (hpsi : SchrodingerAt Q psi t) :
    HasDerivAt (fun s => (quantumObservation Q A (psi s)).observable)
      (quantumObservation Q A (psi t)).observableRate t

-- Source line 791
theorem isQuantumReduction_of {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (hpsi : IsSchrodingerEvolution Q psi) {t₀ : ℝ} (h0 : IsQuantumState (psi t₀)) :
    IsQuantumReduction Q psi where
  selfAdjoint

-- Source line 799
theorem IsQuantumReduction.norm_const {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (h : IsQuantumReduction Q psi) (t₁ t₂ : ℝ) : ‖psi t₁‖ = ‖psi t₂‖

-- Source line 803
theorem http://IsQuantumReduction.energy_const {Q : QuantumHamiltonian H} {psi : ℝ → H}
    (h : IsQuantumReduction Q psi) (t₁ t₂ : ℝ) :
    realExpectationAlong Q.op psi t₁ = realExpectationAlong Q.op psi t₂

-- Source line 862
theorem effectiveState_quantum (Q : QuantumHamiltonian H) (A : Observable H)
    (U : H →L[ℂ] H) (M : MDCFOperator) (Δ : Scale) (cfg : Config) (psi : H) :
    effectiveState (quantumUpdate U) (quantumCurvatureExtractor Q A) M Δ () cfg psi
      = M.assign Δ cfg (quantumCurvature (quantumObservation Q A (U psi)))

-- Source line 868
theorem quantumUpdate_isQuantumState {Q : QuantumHamiltonian H} {Uf : ℝ → (H →L[ℂ] H)}
    (hU : IsPropagator Q Uf) (dt : ℝ) {psi : H} (h : IsQuantumState psi) :
    IsQuantumState (show H from (quantumUpdate (Uf dt)).update psi)

-- Source line 879
theorem mdcfStep_of_quantum {Q : QuantumHamiltonian H} {Uf : ℝ → (H →L[ℂ] H)}
    (hU : IsPropagator Q Uf) (dt : ℝ) (A : Observable H) (M : MDCFOperator) (Δ : Scale)
    (cfg : Config) (m : ℝ) (s : State) (z : Metric) {psi : H} (hpsi : IsQuantumState psi)
    (h : ResolvedAssignment cfg s z m
      (effectiveState (quantumUpdate (Uf dt)) (quantumCurvatureExtractor Q A) M Δ () cfg psi)) :
    IsQuantumState (Uf dt psi) ∧
      AdmissibleAssignment cfg s
        (effectiveState (quantumUpdate (Uf dt)) (quantumCurvatureExtractor Q A) M Δ () cfg psi) ∧
      MDCFStep (quantumUpdate (Uf dt)) (quantumCurvatureExtractor Q A) M Δ () cfg m s z psi
        (mdcfCommitted (quantumUpdate (Uf dt)) (quantumCurvatureExtractor Q A) M Δ () cfg s z
          psi)

1. Tensor and metric algebra
----------------------------

outer_symm
MetricPoint.inverse'
MetricPoint.raise_lower
MetricPoint.lower_raise
MetricPoint.pair_lower
MetricPoint.traceWith_outer_lower
eta_symm
eta_inverse
lorentzSignature_eta

2. Curvature and Einstein tensor
--------------------------------

Spacetime.einstein_eq
Spacetime.ricci_symm
Spacetime.einstein_symm
vacuumSource_isVacuum
satisfiesEFE_zero_lambda
einstein_zero_of_vacuum

3. Conservation
---------------

einstein_implies_source_conservation
vacuum_sourceConserved

4. Contractions and observer decomposition
-------------------------------------------

contract2_smul
contract2_outer
contractRight_smul
contractRight_outer
traceWith_smul
traceWith_add
traceWith_sub
traceWith_metric
traceWith_outer
pair_uCov_self
traceWith_outer_uCov
source_decomposition
momentumDensity_orthogonal
spatialStress_orthogonal
spatialProjector_orthogonal
traceWith_spatialProjector
spatialStress_symm

5. Dust and perfect fluids
--------------------------

dust_energyDensity
dust_momentumDensity
dust_spatialStress
dust_pressure
dust_trace
perfectFluid_energyDensity
perfectFluid_momentumDensity
perfectFluid_spatialStress
perfectFluid_pressure

6. Minkowski and observer witnesses
------------------------------------

restU_unit
boostU_unit
nullPlus_energyDensity
nullPlus_momentumDensity
nullMinus_momentumDensity
nullMinus_energyDensity
same_energyDensity_not_same_source
energyDensity_observer_dependent
dust_boosted_momentumDensity_ne_zero

7. Electromagnetic stress-energy
--------------------------------

traceWith_emFirst
emStressEnergy_traceless
constElectricF_antisymm
constElectric_fieldInvariant
constElectric_energyDensity
constElectric_spatialStress_yy
emSource_not_dust

8. Non-injectivity of scalar observations
------------------------------------------

energyDensity_not_injective
trace_not_injective

9. Curvature and plane-wave witnesses
--------------------------------------

kappaDefault_ne_zero
waveRiemann_ricci
waveRiemann_scalar
waveSpacetime_einstein
waveH_symm
waveH_trace
nullCovPlus_null
nullCovMinus_null
waveH_trans_plus
waveH_trans_minus
curvedVacuum_einstein
vacuum_not_flat

10. Stress trace and pressure
-----------------------------

raise_uCov
traceWith_outer_comm
spatialStress_trace
pressure_eq

11. GR observation surface
--------------------------

extract_preservesObservables

12. Reduction loss ledger
-------------------------

obsEquiv_refl
obsEquiv_symm
obsEquiv_trans
nullDustState_lawful
nullDustState'_lawful
nullDust_scalar
nullDust'_scalar
nullPlus_trace
nullMinus_trace
nullPlus_momentumNormSq
nullMinus_momentumNormSq
extractor_collision
extract_not_faithful
extract_faithfulOn_dust
minkowskiDustState_lawful_iff

13. Generic-adapter boundary
----------------------------

grSourceSystem_hasSolution
naiveScalarAdapter_not_faithful
no_certifiedAdapter_naiveScalar

14. K-plane and MDCF firewall
-----------------------------

grToKPlane_not_injective
grMDCF_assignment_not_curvature_identity

15. Weak-field surface
----------------------

weakField_poisson
dust_source00

16. GR histories
----------------

extractAlong_eq
lawfulHistory_preserved
nullDustHistory_lawful
histories_not_determined_by_observation

17. Capability separations
--------------------------

observablePreserved_not_faithful
conservation_needs_bianchi
dust_not_universal

18. Non-vacuity witnesses
-------------------------

witness_vacuum
witness_dust
witness_momentum
witness_stress

1. Quantum-side scalar readout
------------------------------

quantumEnergyScalar_eq_observation_energy
quantumEnergyAlong_eq
quantumEnergyAlong_const

2. Source descriptors
---------------------

grDescriptor_reconstructs
grDescriptor_observer_dependent

3. Available quantum exports
----------------------------

energyExport_not_exportsMomentum
energyExport_not_exportsStress
energyExport_scalarFactored

4. Calibration firewall
-----------------------

calibration_injective

5. Layered correspondence relations
------------------------------------

http://QuantumCorrespondsAt.energy
quantumCorrespondsOn_at
globallyQuantumCorresponds_at
energyCorrespondsOn_at
globallyEnergyCorresponds_at
descriptor_correspondence_unique_source

6. Restricted GR source classes
--------------------------------

dustLikeAt_dustSource
nullDustPlus_outerSource
dustLikeAt_param
nullDustPlus_param
dustLike_quantum_source_reconstruction
nullDust_quantum_source_reconstruction
dust_class_load_bearing

7. Direct cross-theory theorems
--------------------------------

schrodinger_source_parameter_transport
schrodinger_nullDust_source_transport
schrodinger_dustLike_source_transport
nullDust_correspondence_einstein
dustLike_correspondence_einstein
quantum_correspondence_source_conserved
correspondence_conservation_needs_bianchi

8. Non-vacuous benchmark and level promotions
----------------------------------------------

benchmarkPsi_isSchrodingerEvolution
benchmarkPsi_isQuantumState
benchmarkPsi_energy
benchmark_quantum_nullDust_correspondence
benchmark_einstein
energyDensity_vacuum
psiPlus_energy
ket0_energy
correspondsAt_not_correspondsOn
correspondsOn_not_globallyCorresponds

9. Quantum state to quantum descriptor loss
--------------------------------------------

idOp_selfAdjoint
expectation_idOp
variance_idOp
ket0_ne_smul_ket1
native_quantum_observation_not_injective
energyExport_not_injective

10. Quantum descriptor to GR source loss
-----------------------------------------

scalar_correspondence_underdetermines_source
no_source_reconstruction_from_energy_channel
no_momentum_reconstruction_from_energy_channel
energyExport_no_descriptor_correspondence_of_momentum
no_descriptor_correspondence_nullDust
energy_channel_blind_to_stress
em_outside_scalar_reading

11. GR source to geometry loss
------------------------------

zero_correspondence_not_flat
correspondence_does_not_determine_geometry
same_readouts_different_riemann
correspondence_not_efe_solutionhood

12. MDCF and K-plane projection tests
-------------------------------------

projections_agree
shared_projection_not_geometry
kplane_projection_blind_to_nullDust_amplitude
loss_is_in_the_readout_not_the_calibration
projection_agreement_not_correspondence

13. Dynamics and backreaction firewall
---------------------------------------

no_scalarMediatedResponse
quantum_side_unconstrained_by_gr

14. Load-bearing hypothesis audit
---------------------------------

jumpPsi_zero
jumpPsi_one
jumpPsi_energy_zero
jumpPsi_energy_one
quantum_evolution_hypothesis_load_bearing
gr_hypotheses_load_bearing

1. Native geometry and potential foundations
--------------------------------------------
recoveryRegion_subset_recoveryCorridor
not_mem_legalNbhd_of_forbidden
adjacent_deterministicStepState
unitParams_pos
potential_goodMetric
potential_zeroMetric
potential_coldMetric
coh_term_le_potential
cdist_succ_one

2. Stall witness and legacy strict-descent audit
------------------------------------------------
succ_ne_self
stallConfig_valid
stall_score_const
stall_step_eq_self
stall_hysteresis
stall_succ_legal
stall_recoveryEdgeAvailable
coldMetric_mem_corridor
coldMetric_not_mem_basin
stall_no_strict_descent
legacy_claim_one_insufficient

3. Repaired corridor descent and finite-time basin entry
--------------------------------------------------------
descent_of_dominant_recovery_edge
corridor_strict_descent
descent_iterate
exists_basin_entry_time
mem_stableBasin_of_potential_le

4. Basin stability and switching audit
--------------------------------------
switchConfig_valid
switch_score_eq
switch_legalNbhd
switch_isBestCandidate_iff
switch_hysteresis
switch_best_succ
switch_step
goodMetric_mem_basin
basin_escalation_counterexample
legacy_claim_three_insufficient
basin_drift_nonpos_of_stabilizing
potential_le_of_nonincreasing
lyapunov_stability_in_basin
hysteresis_does_not_bound_switching

5. Bounded-input audit and repaired potential bound
---------------------------------------------------
bounded_inputs_do_not_bound_potential
momentum_runaway_under_bounded_inputs
potential_le_of_bounded_inputs