Poisson algebra for coefficient normalization

Subtracting a differentiable function of the Hamiltonian preserves the first-integral equation, as does multiplication by a scalar. Combined with the exact off-zero formula for dslope, this shows that the mass-normalized candidate remains a first integral for nonzero mass wherever the zeroth coefficient cancellation holds locally in phase space.

theorem LeanPool.PoincareThreeBody.poissonBracket_comp_self_eq_zero {observable : PhaseSpace → ℝ} {scalarFunction : ℝ → ℝ} {state : PhaseSpace} (hobservable : DifferentiableAt ℝ observable state) (hscalar : DifferentiableAt ℝ scalarFunction (observable state)) : poissonBracket (fun (candidate : PhaseSpace) => scalarFunction (observable candidate)) observable state = 0

A differentiable scalar function of an observable Poisson-commutes with that observable.

theorem LeanPool.PoincareThreeBody.poissonBracket_sub_left {first second observable : PhaseSpace → ℝ} {state : PhaseSpace} (hfirst : DifferentiableAt ℝ first state) (hsecond : DifferentiableAt ℝ second state) : poissonBracket (fun (candidate : PhaseSpace) => first candidate - second candidate) observable state = poissonBracket first observable state - poissonBracket second observable state

The Poisson bracket is additive in its first argument at differentiability points.

theorem LeanPool.PoincareThreeBody.poissonBracket_const_mul_left {first observable : PhaseSpace → ℝ} {state : PhaseSpace} (hfirst : DifferentiableAt ℝ first state) (scalar : ℝ) : poissonBracket (fun (candidate : PhaseSpace) => scalar * first candidate) observable state = scalar * poissonBracket first observable state

Multiplying the first argument by a constant multiplies its Poisson bracket by that constant.

theorem LeanPool.PoincareThreeBody.poissonBracket_normalizationResidual_eq_zero {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} {mass : ℝ} {state : PhaseSpace} (hcandidate : DifferentiableAt ℝ (F mass) state) (hhamiltonian : DifferentiableAt ℝ (hamiltonian mass) state) (henergyFunction : DifferentiableAt ℝ energyFunction (hamiltonian mass state)) (hcommutes : poissonBracket (F mass) (hamiltonian mass) state = 0) : poissonBracket (normalizationResidual F energyFunction mass) (hamiltonian mass) state = 0

Subtracting a differentiable function of the Hamiltonian preserves Poisson commutation.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.normalizationResidual_poissonBracket_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {z : ℝ × PhaseSpace} (hz : z ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian z.1 z.2)) : poissonBracket (normalizationResidual F energyFunction z.1) (hamiltonian z.1) z.2 = 0

Under the challenge hypotheses, the normalization residual is a first integral at every domain point where the chosen energy function is analytic.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.normalizationResidual_div_mass_poissonBracket_eq_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {mass : ℝ} (_hmass : mass ≠ 0) {state : PhaseSpace} (hdomain : (mass, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian mass state)) : poissonBracket (fun (candidate : PhaseSpace) => normalizationResidual F energyFunction mass candidate / mass) (hamiltonian mass) state = 0

At nonzero mass, division of the normalization residual by mass preserves its first-integral equation.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.massNormalizedCandidate_poissonBracket_eq_zero_of_ne {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {mass : ℝ} (hmass : mass ≠ 0) {state : PhaseSpace} (hdomain : (mass, state) ∈ parameterDomain δ) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian mass state)) (hcancel : ∀ᶠ (candidate : PhaseSpace) in nhds state, F 0 candidate = energyFunction (hamiltonian 0 candidate)) : poissonBracket (massNormalizedCandidate F energyFunction mass) (hamiltonian mass) state = 0

If the zeroth residual vanishes on a phase neighborhood, then the dslope-normalized candidate Poisson-commutes with the Hamiltonian at every nonzero mass in the domain.

theorem LeanPool.PoincareThreeBody.continuousAt_poissonBracket_curry {first second : ℝ × PhaseSpace → ℝ} {mass : ℝ} {state : PhaseSpace} (hfirst : ContDiffAt ℝ 1 first (mass, state)) (hsecond : ContDiffAt ℝ 1 second (mass, state)) : ContinuousAt (fun (candidateMass : ℝ) => poissonBracket (fun (candidate : PhaseSpace) => first (candidateMass, candidate)) (fun (candidate : PhaseSpace) => second (candidateMass, candidate)) state) mass

A Poisson bracket formed from two jointly C¹ mass/phase families varies continuously with mass at a fixed phase point.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.massNormalizedCandidate_poissonBracket_eq_zero_at_mass_zero {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) {state : PhaseSpace} (hcollision : (0, state) ∈ collisionFree) (henergyFunction : AnalyticAt ℝ energyFunction (hamiltonian 0 state)) (hcancel : ∀ᶠ (candidate : PhaseSpace) in nhds state, F 0 candidate = energyFunction (hamiltonian 0 candidate)) (hnormalized : ContDiffAt ℝ 1 (Function.uncurry (massNormalizedCandidate F energyFunction)) (0, state)) : poissonBracket (massNormalizedCandidate F energyFunction 0) (hamiltonian 0) state = 0

Once joint C¹ regularity of the removable quotient is available, its off-zero first-integral equation extends continuously to mass zero. This isolates the joint analytic Hadamard-division lemma needed to iterate Poincaré's normalization.

theorem LeanPool.PoincareThreeBody.IsFirstIntegralFamily.domainMassNormalizedCandidate_isFirstIntegralFamily {δ : ℝ} {F : ℝ → PhaseSpace → ℝ} {energyFunction : ℝ → ℝ} (hδ : 0 < δ) (hanalytic : IsJointlyAnalytic δ F) (hfirstIntegral : IsFirstIntegralFamily δ F) (henergy : ∀ (energy : ℝ), AnalyticAt ℝ energyFunction energy) (hcancel : ∀ (state : PhaseSpace), (0, state) ∈ collisionFree → F 0 state = energyFunction (hamiltonian 0 state)) (hnormalized : IsJointlyAnalytic δ (domainMassNormalizedCandidate F energyFunction)) : IsFirstIntegralFamily δ (domainMassNormalizedCandidate F energyFunction)

Joint analyticity of the domain-correct removable quotient upgrades the pointwise normalization algebra to a first-integral family on the whole parameter domain.