Closing the normalization induction from one step

This file reduces the all-orders classical normalization principle to a single reusable closure theorem. Once every jointly analytic first integral can be normalized once—preserving joint analyticity and the first-integral equation—classical choice and primitive recursion construct all orders automatically.

def LeanPool.PoincareThreeBody.ClassicalNormalizationStep : Prop

The one-step statement needed from the Poincaré-set obstruction and analytic Hadamard division.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.PoincareThreeBody.ClassicalZerothCoefficientPrinciple : Prop

Celestial-mechanics half of one normalization step: the mass-zero coefficient of every analytic first integral is a globally analytic function of the Kepler Hamiltonian.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.PoincareThreeBody.JointAnalyticMassDivisionPrinciple : Prop

Analytic half of one normalization step: division by the mass coordinate preserves joint analyticity after the zeroth coefficient has been cancelled on the actual mass-zero domain.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.PoincareThreeBody.MassZeroAnalyticDivisionPrinciple : Prop

Pointwise form of analytic Hadamard division on the only nontrivial slice. Ordinary division already handles every point with nonzero mass, so this is equivalent to the global joint-analytic division principle above.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PoincareThreeBody.jointAnalyticMassDivisionPrinciple_iff_massZero : JointAnalyticMassDivisionPrinciple ↔ MassZeroAnalyticDivisionPrinciple

Parameterized analytic division is reduced exactly to the removable mass-zero slice.

theorem LeanPool.PoincareThreeBody.classicalNormalizationStep_of_zerothCoefficient_of_massDivision (hcoefficient : ClassicalZerothCoefficientPrinciple) (hdivision : JointAnalyticMassDivisionPrinciple) : ClassicalNormalizationStep

The functional-dependence and analytic-division halves together give the reusable one-step closure theorem; preservation of the first-integral equation is already formal.

structure LeanPool.PoincareThreeBody.NormalizationState (δ : ℝ) : Type

A jointly analytic first integral, bundled so a normalization step can be iterated.

• family : ℝ → PhaseSpace → ℝ

  The parameterized phase-space function at the current normalization stage.

• analytic : IsJointlyAnalytic δ self.family
• firstIntegral : IsFirstIntegralFamily δ self.family

noncomputable def LeanPool.PoincareThreeBody.selectedEnergy (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (current : NormalizationState δ) : ℝ → ℝ

The energy function selected for one normalization state.

Equations

• LeanPool.PoincareThreeBody.selectedEnergy hstep hδ current = Classical.choose ⋯

theorem LeanPool.PoincareThreeBody.selectedEnergy_spec (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (current : NormalizationState δ) : (∀ (energy : ℝ), AnalyticAt ℝ (selectedEnergy ⋯ hδ current) energy) ∧ (∀ (state : PhaseSpace), (0, state) ∈ collisionFree → current.family 0 state = selectedEnergy ⋯ hδ current (hamiltonian 0 state)) ∧ IsJointlyAnalytic δ (domainMassNormalizedCandidate current.family (selectedEnergy ⋯ hδ current)) ∧ IsFirstIntegralFamily δ (domainMassNormalizedCandidate current.family (selectedEnergy ⋯ hδ current))

noncomputable def LeanPool.PoincareThreeBody.nextNormalizationState (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (current : NormalizationState δ) : NormalizationState δ

Apply one selected normalization step to a bundled state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PoincareThreeBody.normalizationStateSequence (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (initial : NormalizationState δ) : ℕ → NormalizationState δ

The recursively selected sequence of analytic first integrals.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.PoincareThreeBody.normalizationStateSequence hstep hδ initial 0 = initial

noncomputable def LeanPool.PoincareThreeBody.normalizationEnergySequence (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (initial : NormalizationState δ) (n : ℕ) : ℝ → ℝ

The energy function selected at each recursive stage.

Equations

• LeanPool.PoincareThreeBody.normalizationEnergySequence hstep hδ initial n = LeanPool.PoincareThreeBody.selectedEnergy ⋯ hδ (LeanPool.PoincareThreeBody.normalizationStateSequence ⋯ hδ initial n)

theorem LeanPool.PoincareThreeBody.normalizationStateSequence_family_eq_iterated (hstep : ClassicalNormalizationStep) {δ : ℝ} (hδ : 0 < δ) (initial : NormalizationState δ) (n : ℕ) : (normalizationStateSequence ⋯ hδ initial n).family = iteratedMassNormalization initial.family (normalizationEnergySequence ⋯ hδ initial) n

The recursively bundled family agrees with the explicit iteration used by the all-orders endpoint.

theorem LeanPool.PoincareThreeBody.classicalNormalizationPrinciple_of_step (hstep : ClassicalNormalizationStep) : ClassicalNormalizationPrinciple

A one-step normalization closure theorem supplies the complete all-orders principle.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_classicalNormalizationStep (hstep : ClassicalNormalizationStep) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

Thus the exact challenge theorem follows from the one-step closure theorem.

theorem LeanPool.PoincareThreeBody.nonintegrability_of_zerothCoefficient_of_massDivision (hcoefficient : ClassicalZerothCoefficientPrinciple) (hdivision : JointAnalyticMassDivisionPrinciple) : ¬∃ (δ : ℝ), 0 < δ ∧ ∃ (F : ℝ → PhaseSpace → ℝ), IsJointlyAnalytic δ F ∧ IsFirstIntegralFamily δ F ∧ IsIndependentSomewhere δ F

Final decomposition of the exact theorem into its two remaining reusable inputs.