Shell-analytic suspended Hamiltonian interfaces for corrected resonant KAM persistence

Definition

frame_2026_kam_interfaces

by ShouqiaoWang · Aug 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

almost-periodic-functionsdynamical-systemshamiltonian-systemsinvariant-torikam-theorysmall-divisorssymplectic-geometry

This bundle gives concrete semantics to the corrected resonant KAM target. It defines finite internal points and tori, the infinite product external-angle torus, real and complex $\ell^1$ external actions, the full suspended phase, finitely supported external Fourier modes, their pairings and lengths, spatial-shell weights, admissibility, minimum support weights, and weighted action norms. A spatial structure covers every lattice site and carries a genuine minimizing support envelope, so elementary modes exist and the nonresonance quantifier is nonempty. An approximation function includes its lower bound, monotonicity, normalization, decreasing logarithmic ratio, subexponential limit, and Brjuno-type integrability.

A resonance frame records the primitive resonance subgroup and a determinant-one integer basis $K_0=(K_1,K_2)$ . The bundle defines adapted angles, the original-angle reconstruction, the resonant set $K_2^{\mathsf T}\nabla N=0$ , and the reduced frequency $K_1^{\mathsf T}\nabla N$ . The perturbation is shell-indexed rather than collapsed by mode; its coefficient bounds use a uniform inner analytic supremum and an outer weighted shell sum. Reality, complex-neighborhood analyticity, and convergence of the actual Fourier evaluation are explicit. The averaged potential is its literal zero external/fast coefficient, and criticality and the Hessian are computed from Fréchet derivatives.

The corrected hypothesis package requires positive dimensions, a bounded closed parameter region, analytic $N$ , a nonempty nondegenerate resonant locus, nonempty positive-measure trims in the reduced-frequency chart, full derivative twist, an analytic lower-Lipschitz reduced-frequency diffeomorphism, nondegeneracy of every retained critical point, external nonresonance, and the shell-analytic perturbation class. The suspended Hamiltonian $\langle\omega,J\rangle+N+\epsilon P$ , its canonical vector field, and every convergence or differentiability guard are defined directly.

Persistent embeddings take values in the full suspended phase. Scalar angle and internal coordinates have shell Fourier expansions, while the entire $J$ component has one weighted- $\ell^1$ -valued expansion equal to its Fourier series. Local canonical transformations have explicit source and target neighborhoods, inverses, tangents, and preservation of the full suspended two-form on cylinder directions. Invariance is the coordinatewise Hamilton equation along the rigid $(\omega,\Omega(y))$ translation, and closeness controls all angle coordinates, the external-action norm, and all internal actions. None of analyticity, criticality, Hamiltonian flow, symplecticity, invariance, or persistence is an arbitrary model-supplied predicate.

Definition code

import Mathlib

/-!
# Concrete interfaces for almost-periodic resonant KAM persistence

The perturbation is represented by its Fourier coefficients in the external
almost-periodic angles and in the adapted internal angles.  The averaged
Hamiltonian, its critical points and Hessian, the canonical Hamiltonian vector
field, analytic almost-periodic embeddings, and the standard symplectic form
are definitions, not model-supplied predicates.

We use the suspended Hamiltonian

`H ε θ J x y = ⟨ω,J⟩ + N y + ε P θ x y ε`

on the genuine `ℓ¹` external-action phase space.  Invariance is stated in all
external and internal canonical coordinates.
-/

noncomputable section

namespace KAMInterfaces

open Filter MeasureTheory Set
open scoped BigOperators Topology Gradient

abbrev Point (d : ℕ) := Fin d → ℝ
abbrev ComplexPoint (d : ℕ) := Fin d → ℂ
abbrev LatticePoint (d : ℕ) := Fin d → ℤ
abbrev PhaseAngle (m : ℕ) := Fin m → Real.Angle
abbrev ExternalAngle := ℤ → Real.Angle
abbrev ExternalAction := lp (fun _ : ℤ => ℝ) 1
abbrev ComplexExternalAction := lp (fun _ : ℤ => ℂ) 1
abbrev TorusPoint (n : ℕ) := ExternalAngle × PhaseAngle n
abbrev FiniteMode := ℤ →₀ ℤ
abbrev CanonicalPhase (d : ℕ) := PhaseAngle d × Point d
abbrev PhaseVector (d : ℕ) := Point d × Point d
abbrev SuspendedPhase (d : ℕ) :=
  (ExternalAngle × ExternalAction) × CanonicalPhase d
abbrev ExternalCylinderVector := ℤ →₀ ℝ
abbrev SuspendedCylinderVector (d : ℕ) :=
  (ExternalCylinderVector × ExternalAction) × PhaseVector d
abbrev SuspendedPhaseVector (d : ℕ) :=
  ((ℤ → ℝ) × ExternalAction) × PhaseVector d

/-- Coordinatewise complexification of a real `ℓ¹` external action. -/
noncomputable def complexifyExternalAction
    (J : ExternalAction) : ComplexExternalAction :=
  ⟨fun j => (J j : ℂ), by
    apply memℓp_gen
    simpa using (lp.memℓp J).summable_of_one.norm⟩

/-- The canonical inclusion of a real finite-dimensional point in its
complexification. -/
def complexifyPoint {d : ℕ} (x : Point d) : ComplexPoint d :=
  fun i => (x i : ℂ)

/-- A genuine complex neighborhood of a real parameter set. -/
def complexTube {d : ℕ} (G : Set (Point d)) (radius : ℝ) : Set (ComplexPoint d) :=
  {z | ∃ y ∈ G, dist z (complexifyPoint y) < radius}

/-- A complex neighborhood of the real perturbation interval `[-1,1]`. -/
def complexEpsilonTube (radius : ℝ) : Set ℂ :=
  {z | ∃ epsilon ∈ Set.Icc (-1 : ℝ) 1, dist z (epsilon : ℂ) < radius}

/-- The elementary Fourier mode supported at one external frequency. -/
def unitMode (j : ℤ) : FiniteMode :=
  Finsupp.single j 1

/-- Pairing of a finite-support external mode with a real frequency vector. -/
def modePairing (k : FiniteMode) (ω : ℤ → ℝ) : ℝ :=
  k.sum fun j coefficient => (coefficient : ℝ) * ω j

/-- The external Fourier length. -/
def modeL1 (k : FiniteMode) : ℕ :=
  k.sum fun _ coefficient => coefficient.natAbs

/-- Pairing of a finite-dimensional integer mode with lifted angles. -/
def latticePairing {d : ℕ} (k : LatticePoint d) (x : Point d) : ℝ :=
  ∑ j, (k j : ℝ) * x j

/-- The finite-dimensional Fourier length. -/
def latticeL1 {d : ℕ} (k : LatticePoint d) : ℕ :=
  ∑ j, (k j).natAbs

/-- The source's concrete weight of a finite spatial set. -/
def spatialSetWeight (spatialExponent : ℝ) (A : Finset ℤ) : ℝ :=
  1 + ∑ j ∈ A,
    Real.rpow (Real.log (1 + (j.natAbs : ℝ))) spatialExponent

/-- A source spatial structure, including a chosen witness for the printed
minimum `[[k]] = min{[A] : supp k ⊆ A ∈ S}`.  The witness is constrained to
be a genuine minimizer, so it cannot change the small-divisor condition. -/
structure SpatialStructure where
  sets : Set (Finset ℤ)
  spatialExponent : ℝ
  spatialExponent_gt_two : 2 < spatialExponent
  covers : ∀ j : ℤ, ∃ A, A ∈ sets ∧ j ∈ A
  union_mem_of_intersects :
    ∀ {A B}, A ∈ sets → B ∈ sets → (A ∩ B).Nonempty → A ∪ B ∈ sets
  supportEnvelope : FiniteMode → Finset ℤ
  supportEnvelope_mem :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) → supportEnvelope k ∈ sets
  support_subset_envelope :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) → k.support ⊆ supportEnvelope k
  supportEnvelope_minimal :
    ∀ k, (∃ A, A ∈ sets ∧ k.support ⊆ A) →
      ∀ A, A ∈ sets → k.support ⊆ A →
        spatialSetWeight spatialExponent (supportEnvelope k) ≤
          spatialSetWeight spatialExponent A

/-- The modes `ℤ^ℤ_S` occurring in the source: finite modes whose support is
contained in a member of the spatial structure. -/
def SpatialStructure.IsAdmissible (S : SpatialStructure) (k : FiniteMode) : Prop :=
  ∃ A, A ∈ S.sets ∧ k.support ⊆ A

/-- Every elementary external mode is admissible, because a spatial structure
covers every lattice site.  Thus the nonresonance quantifier cannot be empty. -/
theorem SpatialStructure.unitMode_admissible (S : SpatialStructure) (j : ℤ) :
    S.IsAdmissible (unitMode j) := by
  rcases S.covers j with ⟨A, hA, hj⟩
  refine ⟨A, hA, ?_⟩
  intro i hi
  have hji : j = i := by simpa [unitMode] using hi
  simpa [hji] using hj

/-- The source weight `[[k]]`, evaluated at the constrained minimizing shell. -/
def modeSpatialWeight (S : SpatialStructure) (k : FiniteMode) : ℝ :=
  spatialSetWeight S.spatialExponent (S.supportEnvelope k)

/-- The source's individual-site weight `[j]`, obtained from the constrained
minimum shell containing the unit mode at `j`. -/
def siteSpatialWeight (S : SpatialStructure) (j : ℤ) : ℝ :=
  modeSpatialWeight S (unitMode j)

/-- Weighted external actions from the source phase norm
`sum_j |J_j| exp(w[j])`. -/
def HasWeightedExternalAction (S : SpatialStructure) (w : ℝ)
    (J : ExternalAction) : Prop :=
  Summable fun j : ℤ => ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- Weighted summability for a complex `ℓ¹` action coefficient. -/
def HasWeightedComplexExternalAction (S : SpatialStructure) (w : ℝ)
    (J : ComplexExternalAction) : Prop :=
  Summable fun j : ℤ => ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- The actual weighted `ℓ¹` norm of a complex action coefficient.  Every use
below is paired with `HasWeightedComplexExternalAction`, so the `tsum` fallback
is excluded. -/
noncomputable def weightedComplexExternalActionNorm (S : SpatialStructure)
    (w : ℝ) (J : ComplexExternalAction) : ℝ :=
  ∑' j : ℤ, ‖J j‖ * Real.exp (w * siteSpatialWeight S j)

/-- The character of the infinite product torus associated to a finite mode. -/
def externalCharacter (k : FiniteMode) (θ : ExternalAngle) : ℂ :=
  k.prod fun j coefficient => ((θ j).toCircle : ℂ) ^ coefficient

/-- The character of a finite torus associated to an integer lattice point. -/
def finiteCharacter {d : ℕ} (k : LatticePoint d) (x : PhaseAngle d) : ℂ :=
  ∏ j, ((x j).toCircle : ℂ) ^ k j

/-- A subgroup of a free abelian group is primitive (saturated). -/
def IsPrimitive {d : ℕ} (g : AddSubgroup (LatticePoint d)) : Prop :=
  ∀ (q : ℕ), q ≠ 0 → ∀ z, q • z ∈ g → z ∈ g

/-- A primitive rank-`m` resonance lattice with a chosen unimodular frame. -/
structure ResonanceFrame (n m : ℕ) where
  g : AddSubgroup (LatticePoint (n + m))
  K₀ : Matrix (Fin (n + m)) (Fin (n + m)) ℤ
  det_one : K₀.det = 1
  generated_by_resonant_columns :
    g = AddSubgroup.closure
      (Set.range fun j : Fin m =>
        fun i : Fin (n + m) => K₀ i (Fin.natAdd n j))

/-- The complementary columns of a resonance frame. -/
def ResonanceFrame.K₁ {n m : ℕ} (K : ResonanceFrame n m) :
    Matrix (Fin (n + m)) (Fin n) ℤ :=
  fun i j => K.K₀ i (Fin.castAdd m j)

/-- The resonant columns of a resonance frame. -/
def ResonanceFrame.K₂ {n m : ℕ} (K : ResonanceFrame n m) :
    Matrix (Fin (n + m)) (Fin m) ℤ :=
  fun i j => K.K₀ i (Fin.natAdd n j)

/-- Lifted adapted angle coordinates `(ψ, φ) = K₀ᵀ x`. -/
def ResonanceFrame.adaptedLift {n m : ℕ} (K : ResonanceFrame n m)
    (x : Point (n + m)) : Point n × Point m :=
  (fun j => ∑ i, (K.K₁ i j : ℝ) * x i,
   fun j => ∑ i, (K.K₂ i j : ℝ) * x i)

/-- Adapted torus coordinates `(ψ, φ) = K₀ᵀ x`. -/
def ResonanceFrame.adaptedAngles {n m : ℕ} (K : ResonanceFrame n m)
    (x : PhaseAngle (n + m)) : PhaseAngle n × PhaseAngle m :=
  (fun j => ∑ i, (K.K₁ i j) • x i,
   fun j => ∑ i, (K.K₂ i j) • x i)

/-- Recover the original torus angle from `(ψ, φ)`.  Since `det K₀ = 1`,
`adjugate K₀` is its integer inverse. -/
def ResonanceFrame.originalAngles {n m : ℕ} (K : ResonanceFrame n m)
    (ψ : PhaseAngle n) (φ : PhaseAngle m) : PhaseAngle (n + m) :=
  let q : PhaseAngle (n + m) := Fin.append ψ φ
  fun i => ∑ a, (K.K₀.adjugate a i) • q a

/-- `K₁ᵀ` applied to the internal frequency. -/
def reducedFrequency {n m : ℕ} (K : ResonanceFrame n m)
    (internalFrequency : Point (n + m) → Point (n + m)) :
    Point (n + m) → Point n :=
  fun y j => ∑ i, (K.K₁ i j : ℝ) * internalFrequency y i

/-- The internal resonant surface `K₂ᵀ ∇N(y)=0`. -/
def resonantSet {n m : ℕ} (K : ResonanceFrame n m)
    (G : Set (Point (n + m)))
    (internalFrequency : Point (n + m) → Point (n + m)) :
    Set (Point (n + m)) :=
  {y | y ∈ G ∧
    ∀ j : Fin m,
      ∑ i, (K.K₂ i j : ℝ) * internalFrequency y i = 0}

/-- An analytic bijection with analytic inverse and a uniform lower Lipschitz
bound on the source. -/
def IsAnalyticDiffeomorphismOn {d e : ℕ}
    (f : Point d → Point e) (source : Set (Point d))
    (target : Set (Point e)) : Prop :=
  AnalyticOnNhd ℝ f source ∧
    Set.BijOn f source target ∧
    ∃ inverse : Point e → Point d,
      AnalyticOnNhd ℝ inverse target ∧
      Set.MapsTo inverse target source ∧
      (∀ x ∈ source, inverse (f x) = x) ∧
      (∀ z ∈ target, f (inverse z) = z) ∧
      ∃ twist : ℝ, 0 < twist ∧
        ∀ x ∈ source, ∀ y ∈ source,
          twist * dist x y ≤ dist (f x) (f y)

/-- Approximation-function conditions used in the small-divisor estimates. -/
structure ApproximationFunction where
  toFun : ℝ → ℝ
  one_le : ∀ t, 0 ≤ t → 1 ≤ toFun t
  monotone : MonotoneOn toFun (Set.Ici 0)
  at_zero : toFun 0 = 1
  ratio_antitone :
    AntitoneOn (fun t => Real.log (toFun t) / t) (Set.Ioi 0)
  subexponential :
    Tendsto (fun t => Real.log (toFun t) / t) atTop (𝓝 0)
  brjuno_integrable :
    MeasureTheory.IntegrableOn
      (fun t => Real.log (toFun t) / t ^ 2) (Set.Ioi 0)

instance : CoeFun ApproximationFunction (fun _ => ℝ → ℝ) :=
  ⟨ApproximationFunction.toFun⟩

/-- The source nonresonance condition, quantified over exactly the nonzero
external modes admitted by the spatial structure. -/
def StronglyNonresonant (S : SpatialStructure) (ω : ℤ → ℝ) (γ : ℝ)
    (Δ : ApproximationFunction) : Prop :=
  0 < γ ∧
    ∀ k : FiniteMode, k ≠ 0 → S.IsAdmissible k →
      |modePairing k ω| ≥
        γ / (Δ (modeSpatialWeight S k) * Δ (modeL1 k : ℝ))

/-- A Fourier mode of the perturbation in `(θ, ψ, φ)`. -/
abbrev PerturbationMode (n m : ℕ) :=
  FiniteMode × LatticePoint n × LatticePoint m

/-- Shell-indexed Fourier data for a perturbation.  The first index is the
spatial shell `A ∈ S`; it is deliberately not collapsed to the minimum-weight
support of the total Fourier mode.  Coefficients are defined on complex
parameter variables so that the source's complex-neighborhood analyticity can
be stated literally. -/
structure FourierPerturbation (n m : ℕ) where
  coefficient :
    Finset ℤ → PerturbationMode n m → ComplexPoint (n + m) → ℂ → ℂ

/-- Total Fourier length of a perturbation mode. -/
def perturbationModeL1 {n m : ℕ} (mode : PerturbationMode n m) : ℕ :=
  modeL1 mode.1 + latticeL1 mode.2.1 + latticeL1 mode.2.2

/-- Evaluation of the perturbation on real lifts of the torus angles. -/
def FourierPerturbation.evaluateLifted {n m : ℕ}
    (P : FourierPerturbation n m) (θ : ℤ → ℝ)
    (ψ : Point n) (φ : Point m) (y : Point (n + m)) (ε : ℝ) : ℝ :=
  (∑' shellMode : Finset ℤ × PerturbationMode n m,
    P.coefficient shellMode.1 shellMode.2 (complexifyPoint y) (ε : ℂ) *
      Complex.exp (Complex.I *
        (modePairing shellMode.2.1 θ + latticePairing shellMode.2.2.1 ψ +
          latticePairing shellMode.2.2.2 φ))).re

/-- The source's shell Banach class for a real analytic almost-periodic
perturbation.  A single bound for each shell controls the angular Fourier norm
uniformly throughout one complex neighborhood, and the spatially weighted sum
of those shell bounds is finite.  Keeping the shell index prevents replacing
`sum_A ‖P_A‖ exp(m[A])` by the weaker minimum-envelope norm of a collapsed
coefficient. -/
def FourierPerturbation.IsRealAnalyticAlmostPeriodicOn {n m : ℕ}
    (P : FourierPerturbation n m) (S : SpatialStructure)
    (G : Set (Point (n + m))) : Prop :=
  ∃ angleWidth spatialWidth parameterWidth : ℝ,
    0 < angleWidth ∧ 0 < spatialWidth ∧ 0 < parameterWidth ∧
    ∃ shellBound : Finset ℤ → ℝ,
    (∀ A, 0 ≤ shellBound A) ∧
    (∀ A, A ∉ S.sets → shellBound A = 0) ∧
    Summable (fun A : Finset ℤ =>
      shellBound A * Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
    (∀ A mode,
      ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        ∀ y ε, P.coefficient A mode y ε = 0) ∧
    (∀ A mode,
      DifferentiableOn ℂ
        (fun z : ComplexPoint (n + m) × ℂ =>
          P.coefficient A mode z.1 z.2)
        (complexTube G parameterWidth ×ˢ complexEpsilonTube parameterWidth)) ∧
    (∀ A mode, ∀ y ∈ complexTube G parameterWidth,
      ∀ ε ∈ complexEpsilonTube parameterWidth,
        ‖P.coefficient A mode y ε‖ *
          Real.exp (angleWidth * (perturbationModeL1 mode : ℝ)) ≤ shellBound A) ∧
    (∀ A, ∀ y ∈ complexTube G parameterWidth,
      ∀ ε ∈ complexEpsilonTube parameterWidth,
        Summable (fun mode : PerturbationMode n m =>
          ‖P.coefficient A mode y ε‖)) ∧
    (∀ A mode, ∀ y ∈ G, ∀ ε ∈ Set.Icc (-1 : ℝ) 1,
      P.coefficient A (-mode.1, -mode.2.1, -mode.2.2)
          (complexifyPoint y) (ε : ℂ) =
        star (P.coefficient A mode (complexifyPoint y) (ε : ℂ))) ∧
    /- Requiring analyticity of the actual uniformly convergent sum records the
    source's analytic shell function and prevents `fderiv` fallback. -/
    (∀ theta : ℤ → ℝ,
      AnalyticOnNhd ℝ
        (fun z : (Point n × Point m) × (Point (n + m) × ℝ) =>
          P.evaluateLifted theta z.1.1 z.1.2 z.2.1 z.2.2)
        ((Set.univ ×ˢ Set.univ) ×ˢ (G ×ˢ Set.Icc (-1 : ℝ) 1))) ∧
    /- The zero fast/external Fourier coefficient used for `h_0` is likewise
    required to be the actual analytic averaged potential. -/
    AnalyticOnNhd ℝ
      (fun z : Point m × Point (n + m) =>
        (∑' shellMode : Finset ℤ × LatticePoint m,
          P.coefficient shellMode.1 (0, 0, shellMode.2)
              (complexifyPoint z.2) 0 *
            Complex.exp (Complex.I * latticePairing shellMode.2 z.1)).re)
      (Set.univ ×ˢ G)

/-- The averaged perturbation `h₀(φ,y)`: the zero external and zero fast-angle
Fourier coefficient, evaluated at `ε = 0`. -/
def averagedPotentialLift {n m : ℕ} (P : FourierPerturbation n m)
    (φ : Point m) (y : Point (n + m)) : ℝ :=
  (∑' shellMode : Finset ℤ × LatticePoint m,
    P.coefficient shellMode.1 (0, 0, shellMode.2) (complexifyPoint y) 0 *
      Complex.exp (Complex.I * latticePairing shellMode.2 φ)).re

/-- A torus angle represented by its standard real representative. -/
def phaseAngleLift {m : ℕ} (φ : PhaseAngle m) : Point m :=
  fun j => (φ j).toReal

/-- Coordinate gradient on `ℝᵈ`, using the actual Fréchet derivative and the
standard coordinate vectors.  This avoids importing an inner product whose
norm would conflict with the product norm on `Fin d → ℝ`. -/
def coordinateGradient {d : ℕ} (f : Point d → ℝ) (x : Point d) : Point d :=
  fun j => fderiv ℝ f x (Pi.single j 1)

/-- Criticality of the explicitly averaged Hamiltonian. -/
def IsAveragedCritical {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Prop :=
  coordinateGradient (fun u : Point m => averagedPotentialLift P u y)
    (phaseAngleLift φ) = 0

/-- The Hessian matrix of the explicitly averaged Hamiltonian. -/
def averagedCriticalHessian {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Matrix (Fin m) (Fin m) ℝ :=
  let D := fderiv ℝ
    (fun u : Point m =>
      coordinateGradient (fun v : Point m => averagedPotentialLift P v y) u)
    (phaseAngleLift φ)
  fun i j => D (Pi.single j 1) i

/-- The internal frequency is the actual Euclidean gradient of `N`. -/
def internalFrequency {d : ℕ} (N : Point d → ℝ) : Point d → Point d :=
  coordinateGradient N

/-- Concrete data for one almost-periodically perturbed integrable Hamiltonian. -/
structure Model (n m : ℕ) where
  frame : ResonanceFrame n m
  parameterRegion : Set (Point (n + m))
  integrableHamiltonian : Point (n + m) → ℝ
  externalFrequency : ℤ → ℝ
  perturbation : FourierPerturbation n m
  approximation : ApproximationFunction
  divisorConstant : ℝ
  spatialStructure : SpatialStructure

/-- The perturbation evaluated in the original physical angles. -/
def Model.perturbationValue {n m : ℕ} (M : Model n m)
    (θ : ExternalAngle) (x : PhaseAngle (n + m))
    (y : Point (n + m)) (ε : ℝ) : ℝ :=
  let adapted := M.frame.adaptedLift (fun i => (x i).toReal)
  M.perturbation.evaluateLifted (fun j => (θ j).toReal)
    adapted.1 adapted.2 y ε

/-- The literal non-autonomous Hamiltonian `N + ε P`. -/
def Model.hamiltonian {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ExternalAngle) (z : CanonicalPhase (n + m)) : ℝ :=
  M.integrableHamiltonian z.2 + ε * M.perturbationValue θ z.1 z.2 ε

/-- The same Hamiltonian on real lifts of all angle variables. -/
def Model.hamiltonianLifted {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ℤ → ℝ) (z : Point (n + m) × Point (n + m)) : ℝ :=
  let adapted := M.frame.adaptedLift z.1
  M.integrableHamiltonian z.2 +
    ε * M.perturbation.evaluateLifted θ adapted.1 adapted.2 z.2 ε

/-- The canonical Hamiltonian vector field `(∂H/∂y, -∂H/∂x)`, computed on
real lifts of the physical angle torus. -/
def Model.hamiltonianVectorField {n m : ℕ} (M : Model n m) (ε : ℝ)
    (θ : ExternalAngle) (z : CanonicalPhase (n + m)) : PhaseVector (n + m) :=
  let θLift : ℤ → ℝ := fun j => (θ j).toReal
  let xLift : Point (n + m) := fun j => (z.1 j).toReal
  (coordinateGradient
      (fun y => M.hamiltonianLifted ε θLift (xLift, y)) z.2,
    -coordinateGradient
      (fun x => M.hamiltonianLifted ε θLift (x, z.2)) xLift)

/-- An associated nondegenerate relative equilibrium is an actual critical
point of the averaged perturbation with nonzero Hessian determinant. -/
def IsAssociatedNondegenerateCritical {n m : ℕ} (P : FourierPerturbation n m)
    (φ : PhaseAngle m) (y : Point (n + m)) : Prop :=
  IsAveragedCritical P φ y ∧ (averagedCriticalHessian P φ y).det ≠ 0

/-- The paper's set `O₀(g,G)` of resonant parameters which admit at least one
associated nondegenerate relative equilibrium. -/
def nondegenerateResonantSet {n m : ℕ} (M : Model n m) : Set (Point (n + m)) :=
  {y | y ∈ resonantSet M.frame M.parameterRegion
      (internalFrequency M.integrableHamiltonian) ∧
    ∃ φ, IsAssociatedNondegenerateCritical M.perturbation φ y}

/-- The reduced-frequency image of `O₀(g,G)`.  Boundary distance must be
measured in this `n`-dimensional chart: the ambient boundary of the resonant
surface in `ℝ^(n+m)` would contain the whole surface and make every positive
trim empty. -/
def nondegenerateReducedFrequencyDomain {n m : ℕ} (M : Model n m) :
    Set (Point n) :=
  reducedFrequency M.frame (internalFrequency M.integrableHamiltonian) ''
    nondegenerateResonantSet M

/-- The source trim in reduced-frequency coordinates. -/
def trimmedReducedFrequencyDomain {n m : ℕ} (M : Model n m) (ξ : ℝ) :
    Set (Point n) :=
  {Omega | Omega ∈ nondegenerateReducedFrequencyDomain M ∧
    ξ ≤ Metric.infDist Omega (frontier (nondegenerateReducedFrequencyDomain M))}

/-- Pullback of the reduced-frequency trim to the resonant parameter surface. -/
def trimmedNondegenerateResonantSet {n m : ℕ} (M : Model n m) (ξ : ℝ) :
    Set (Point (n + m)) :=
  {y | y ∈ nondegenerateResonantSet M ∧
    reducedFrequency M.frame (internalFrequency M.integrableHamiltonian) y ∈
      trimmedReducedFrequencyDomain M ξ}

/-- Corrected hypotheses for the concrete KAM target. -/
structure CorrectedHypotheses {n m : ℕ} (M : Model n m) where
  n_pos : 0 < n
  m_pos : 0 < m
  primitive : IsPrimitive M.frame.g
  parameterRegion_closed : IsClosed M.parameterRegion
  parameterRegion_bounded : Bornology.IsBounded M.parameterRegion
  integrableHamiltonian_analytic :
    AnalyticOnNhd ℝ M.integrableHamiltonian M.parameterRegion
  nondegenerate_resonant_nonempty : (nondegenerateResonantSet M).Nonempty
  trimRadius : ℝ
  trimRadius_pos : 0 < trimRadius
  trimmed_measurable :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      MeasurableSet (trimmedNondegenerateResonantSet M ξ)
  trimmed_compact :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      IsCompact (trimmedNondegenerateResonantSet M ξ)
  reduced_frequency_positive_measure :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      0 < MeasureTheory.volume (trimmedReducedFrequencyDomain M ξ)
  /-- The missing Kolmogorov twist used verbatim in Lemma 3.2: because `K₀`
  is unimodular, injectivity of the full Hessian is equivalent to
  nonsingularity of `K₀ᵀ Hess(N) K₀`. -/
  integrableHamiltonian_twist_on_trimmed :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      ∀ y ∈ trimmedNondegenerateResonantSet M ξ,
      Function.Injective
        (fderiv ℝ (internalFrequency M.integrableHamiltonian) y)
  reduced_frequency_diffeomorphism :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      IsAnalyticDiffeomorphismOn
        (reducedFrequency M.frame (internalFrequency M.integrableHamiltonian))
        (trimmedNondegenerateResonantSet M ξ)
        (trimmedReducedFrequencyDomain M ξ)
  /-- Printed assumption (A1), restricted to the retained compact trim: every
  critical point which the conclusion quantifies over is nondegenerate.  On
  the compact critical locus analyticity then supplies the uniform gap used by
  one common `epsilonZero`; no numerical gap is inserted as separate data. -/
  all_retained_critical_points_nondegenerate :
    ∀ ξ, 0 < ξ → ξ ≤ trimRadius →
      ∀ y ∈ trimmedNondegenerateResonantSet M ξ, ∀ φ,
        IsAveragedCritical M.perturbation φ y →
          (averagedCriticalHessian M.perturbation φ y).det ≠ 0
  external_nonresonance :
    StronglyNonresonant M.spatialStructure M.externalFrequency
      M.divisorConstant M.approximation
  perturbation_analytic :
    M.perturbation.IsRealAnalyticAlmostPeriodicOn
      M.spatialStructure M.parameterRegion

/-- The rigid translation with external frequency `ω` and reduced internal
frequency `Ω`. -/
def torusTranslation {n : ℕ} (external : ℤ → ℝ)
    (internal : Point n) (t : ℝ) (q : TorusPoint n) : TorusPoint n :=
  (fun j => q.1 j + (t * external j : Real.Angle),
   fun j => q.2 j + (t * internal j : Real.Angle))

/-- The standard suspended resonant torus
`T^ℤ × Tⁿ(φ) × {J=0} × {y}` in the coordinates `(θ,J,x,y)`. -/
def standardSuspendedEmbedding {n m : ℕ} (M : Model n m)
    (y : Point (n + m)) (φ : PhaseAngle m)
    (q : TorusPoint n) : SuspendedPhase (n + m) :=
  ((q.1, 0), (M.frame.originalAngles q.2 φ, y))

/-- A Fourier mode for an almost-periodic torus embedding. -/
abbrev EmbeddingMode (n : ℕ) := FiniteMode × LatticePoint n

/-- Total length of an embedding Fourier mode. -/
def embeddingModeL1 {n : ℕ} (mode : EmbeddingMode n) : ℕ :=
  modeL1 mode.1 + latticeL1 mode.2

/-- One scalar coordinate has a source-style shell expansion at fixed analytic
widths.  Shell bounds are uniform in the torus variables and summable with the
actual `[A]` weight. -/
def HasShellFourierExpansion {n : ℕ} (S : SpatialStructure)
    (angleWidth spatialWidth : ℝ) (f : TorusPoint n → ℂ) : Prop :=
  ∃ coefficient : Finset ℤ → EmbeddingMode n → ℂ,
    ∃ shellBound : Finset ℤ → ℝ,
      (∀ A, 0 ≤ shellBound A) ∧
      (∀ A, A ∉ S.sets → shellBound A = 0) ∧
      Summable (fun A : Finset ℤ =>
        shellBound A *
          Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
      (∀ A mode, ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        coefficient A mode = 0) ∧
      (∀ A, Summable fun mode : EmbeddingMode n =>
        ‖coefficient A mode‖) ∧
      (∀ A mode,
        ‖coefficient A mode‖ *
          Real.exp (angleWidth * (embeddingModeL1 mode : ℝ)) ≤ shellBound A) ∧
      ∀ q,
        f q = ∑' shellMode : Finset ℤ × EmbeddingMode n,
          coefficient shellMode.1 shellMode.2 *
            externalCharacter shellMode.2.1 q.1 *
            finiteCharacter shellMode.2.2 q.2

/-- One unified weighted-`ℓ¹`-valued shell expansion for the full external
action component.  The coefficient majorant uses the source's inner supremum
norm, while the additional weighted absolute summability explicitly guards
the Banach-valued Fourier `tsum`. -/
def HasWeightedActionShellFourierExpansion {n : ℕ} (S : SpatialStructure)
    (angleWidth spatialWidth actionWeight : ℝ)
    (f : TorusPoint n → ExternalAction) : Prop :=
  ∃ coefficient : Finset ℤ → EmbeddingMode n → ComplexExternalAction,
    ∃ shellBound : Finset ℤ → ℝ,
      (∀ A, 0 ≤ shellBound A) ∧
      (∀ A, A ∉ S.sets → shellBound A = 0) ∧
      Summable (fun A : Finset ℤ =>
        shellBound A *
          Real.exp (spatialWidth * spatialSetWeight S.spatialExponent A)) ∧
      (∀ A mode, ¬ (A ∈ S.sets ∧ mode.1.support ⊆ A) →
        coefficient A mode = 0) ∧
      (∀ A mode,
        HasWeightedComplexExternalAction S actionWeight (coefficient A mode)) ∧
      (∀ A mode,
        weightedComplexExternalActionNorm S actionWeight (coefficient A mode) *
            Real.exp (angleWidth * (embeddingModeL1 mode : ℝ)) ≤
          shellBound A) ∧
      Summable (fun shellMode : Finset ℤ × EmbeddingMode n =>
        weightedComplexExternalActionNorm S actionWeight
          (coefficient shellMode.1 shellMode.2)) ∧
      (∀ q : TorusPoint n, Summable fun shellMode : Finset ℤ × EmbeddingMode n =>
        (externalCharacter shellMode.2.1 q.1 *
          finiteCharacter shellMode.2.2 q.2) •
            coefficient shellMode.1 shellMode.2) ∧
      (∀ q : TorusPoint n, HasWeightedExternalAction S actionWeight (f q)) ∧
      ∀ q : TorusPoint n,
        complexifyExternalAction (f q) =
          ∑' shellMode : Finset ℤ × EmbeddingMode n,
            (externalCharacter shellMode.2.1 q.1 *
              finiteCharacter shellMode.2.2 q.2) •
                coefficient shellMode.1 shellMode.2

/-- Every coordinate of the full suspended embedding has an actual
shell-indexed analytic almost-periodic expansion, including the external
angles and their conjugate actions. -/
def IsRealAnalyticAlmostPeriodicSuspendedEmbedding {n d : ℕ}
    (S : SpatialStructure) (ι : TorusPoint n → SuspendedPhase d) : Prop :=
  ∃ angleWidth spatialWidth actionWeight : ℝ,
    0 < angleWidth ∧ 0 < spatialWidth ∧
    0 ≤ actionWeight ∧ actionWeight < spatialWidth ∧
    (∀ j : ℤ, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => (((ι q).1.1 j).toCircle : ℂ))) ∧
    HasWeightedActionShellFourierExpansion S angleWidth spatialWidth actionWeight
      (fun q => (ι q).1.2) ∧
    (∀ i : Fin d, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => (((ι q).2.1 i).toCircle : ℂ))) ∧
    ∀ i : Fin d, HasShellFourierExpansion S angleWidth spatialWidth
      (fun q => ((ι q).2.2 i : ℂ))

/-- A line in the suspended phase in a finitely supported external direction
and an arbitrary finite-dimensional internal direction. -/
def suspendedCylinderPath {d : ℕ} (z : SuspendedPhase d)
    (v : SuspendedCylinderVector d) (t : ℝ) : SuspendedPhase d :=
  ((fun j => z.1.1 j + (t * v.1.1 j : Real.Angle),
    z.1.2 + t • v.1.2),
   (fun i => z.2.1 i + (t * v.2.1 i : Real.Angle),
    fun i => z.2.2 i + t * v.2.2 i))

/-- Coordinatewise derivative of a suspended transformation on cylinder
directions.  Circle derivatives recover angular velocities canonically. -/
noncomputable def suspendedTransformationTangent {d : ℕ}
    (F : SuspendedPhase d → SuspendedPhase d) (z : SuspendedPhase d)
    (v : SuspendedCylinderVector d) : SuspendedPhaseVector d :=
  let curve := fun t => F (suspendedCylinderPath z v t)
  let image := F z
  ((fun j =>
      (star (((image.1.1 j).toCircle : ℂ)) *
        deriv (fun t => (((curve t).1.1 j).toCircle : ℂ)) 0).im,
    deriv (fun t => (curve t).1.2) 0),
   (fun i =>
      (star (((image.2.1 i).toCircle : ℂ)) *
        deriv (fun t => (((curve t).2.1 i).toCircle : ℂ)) 0).im,
    deriv (fun t => (curve t).2.2) 0))

/-- The coordinate curves used above are genuinely differentiable, preventing
the total `deriv` operator from falling back to zero. -/
def CylinderDifferentiableOn {d : ℕ}
    (F : SuspendedPhase d → SuspendedPhase d) (U : Set (SuspendedPhase d)) : Prop :=
  ∀ z ∈ U, ∀ v : SuspendedCylinderVector d,
    (∀ j, DifferentiableAt ℝ
      (fun t => (((F (suspendedCylinderPath z v t)).1.1 j).toCircle : ℂ)) 0) ∧
    DifferentiableAt ℝ
      (fun t => (F (suspendedCylinderPath z v t)).1.2) 0 ∧
    (∀ i, DifferentiableAt ℝ
      (fun t => (((F (suspendedCylinderPath z v t)).2.1 i).toCircle : ℂ)) 0) ∧
    DifferentiableAt ℝ (fun t => (F (suspendedCylinderPath z v t)).2.2) 0

/-- Summability of the infinite external part of the canonical two-form. -/
def ExternalSymplecticSummable {d : ℕ}
    (u v : SuspendedPhaseVector d) : Prop :=
  Summable fun j : ℤ =>
    u.1.1 j * v.1.2 j - u.1.2 j * v.1.1 j

/-- The full suspended canonical form
`Σ dθⱼ∧dJⱼ + Σ dxᵢ∧dyᵢ`.  Every use below carries the explicit summability
guard for its infinite first series. -/
noncomputable def suspendedCanonicalSymplecticForm {d : ℕ}
    (u v : SuspendedPhaseVector d) : ℝ :=
  (∑' j : ℤ, (u.1.1 j * v.1.2 j - u.1.2 j * v.1.1 j)) +
    ∑ i, (u.2.1 i * v.2.2 i - u.2.2 i * v.2.1 i)

/-- Inclusion of cylinder directions into the ambient coordinate tangent. -/
def suspendedCylinderVectorToPhaseVector {d : ℕ}
    (v : SuspendedCylinderVector d) : SuspendedPhaseVector d :=
  ((fun j => v.1.1 j, v.1.2), v.2)

/-- A local change of suspended canonical coordinates with an actual inverse
on open source and target neighborhoods. -/
structure LocalSuspendedTransformation (d : ℕ) where
  source : Set (SuspendedPhase d)
  target : Set (SuspendedPhase d)
  source_open : IsOpen source
  target_open : IsOpen target
  toFun : SuspendedPhase d → SuspendedPhase d
  invFun : SuspendedPhase d → SuspendedPhase d
  mapsTo : Set.MapsTo toFun source target
  invMapsTo : Set.MapsTo invFun target source
  left_inverse : ∀ z ∈ source, invFun (toFun z) = z
  right_inverse : ∀ z ∈ target, toFun (invFun z) = z
  continuous_to : ContinuousOn toFun source
  continuous_inv : ContinuousOn invFun target

/-- Preservation of the full suspended canonical form on all cylinder
directions, by the derivative of the concrete local transformation. -/
def LocalSuspendedTransformation.IsSymplectic {d : ℕ}
    (F : LocalSuspendedTransformation d) : Prop :=
  CylinderDifferentiableOn F.toFun F.source ∧
    ∀ z ∈ F.source, ∀ u v : SuspendedCylinderVector d,
      ExternalSymplecticSummable
        (suspendedTransformationTangent F.toFun z u)
        (suspendedTransformationTangent F.toFun z v) ∧
      suspendedCanonicalSymplecticForm
          (suspendedTransformationTangent F.toFun z u)
          (suspendedTransformationTangent F.toFun z v) =
        suspendedCanonicalSymplecticForm
          (suspendedCylinderVectorToPhaseVector u)
          (suspendedCylinderVectorToPhaseVector v)

/-- The perturbed suspended torus is the image of the standard one under an
actual local symplectic coordinate change. -/
def IsSymplecticallyConjugateSuspendedEmbedding {n m : ℕ} (M : Model n m)
    (y : Point (n + m)) (φ : PhaseAngle m)
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  ∃ F : LocalSuspendedTransformation (n + m),
    Set.range (standardSuspendedEmbedding M y φ) ⊆ F.source ∧
      F.IsSymplectic ∧
      (∀ z ∈ F.source, (F.toFun z).1.1 = z.1.1) ∧
      ∀ q, ι q = F.toFun (standardSuspendedEmbedding M y φ q)

/-- The formal suspended Hamiltonian
`⟨ω,J⟩ + N(y) + εP(θ,x,y,ε)`. -/
noncomputable def Model.suspendedHamiltonian {n m : ℕ} (M : Model n m) (ε : ℝ)
    (z : SuspendedPhase (n + m)) : ℝ :=
  (∑' j : ℤ, M.externalFrequency j * z.1.2 j) +
    M.hamiltonian ε z.1.1 z.2

/-- The formal external pairing is a genuine convergent series at this point. -/
def Model.SuspendedHamiltonianDefined {n m : ℕ} (M : Model n m)
    (z : SuspendedPhase (n + m)) : Prop :=
  Summable fun j : ℤ => M.externalFrequency j * z.1.2 j

/-- Vary one external angle along its standard circle coordinate. -/
def externalAngleLine (θ : ExternalAngle) (j : ℤ) (s : ℝ) : ExternalAngle :=
  fun k => θ k + (if k = j then (s : Real.Angle) else 0)

/-- The raw external-action component `-∂θ H`. -/
noncomputable def Model.externalActionVelocityRaw {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : ℤ → ℝ :=
  fun j => -deriv
    (fun s => M.hamiltonian ε (externalAngleLine z.1.1 j s) z.2) 0

/-- The external-action velocity belongs to the source phase space `ℓ¹`. -/
def Model.ExternalActionVelocityDefined {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : Prop :=
  Memℓp (M.externalActionVelocityRaw ε z) 1

/-- Package the actual external-action velocity in `ℓ¹`; every use in the
invariance predicate carries `ExternalActionVelocityDefined`, excluding the
fallback branch. -/
noncomputable def Model.externalActionVelocity {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) : ExternalAction :=
  by
    classical
    exact if h : M.ExternalActionVelocityDefined ε z then
      ⟨M.externalActionVelocityRaw ε z, h⟩
    else 0

/-- The canonical Hamiltonian vector field of the suspended Hamiltonian.  Its
external components are `θdot=ω` and `Jdot=-∂θ P`; the finite components are
the actual `(∂y H,-∂x H)` defined above. -/
noncomputable def Model.suspendedHamiltonianVectorField {n m : ℕ}
    (M : Model n m) (ε : ℝ) (z : SuspendedPhase (n + m)) :
    SuspendedPhaseVector (n + m) :=
  ((M.externalFrequency, M.externalActionVelocity ε z),
   M.hamiltonianVectorField ε z.1.1 z.2)

/-- The rigid almost-periodic orbit solves every coordinate of the concrete
suspended Hamilton equation. -/
def IsSuspendedHamiltonianInvariantTorus {n m : ℕ} (M : Model n m) (ε : ℝ)
    (y : Point (n + m))
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  let Ω := reducedFrequency M.frame
    (internalFrequency M.integrableHamiltonian) y
  ∀ q t,
    let translated := torusTranslation M.externalFrequency Ω t q
    let z := ι translated
    let thetaLift : ℤ → ℝ := fun j => (z.1.1 j).toReal
    let xLift : Point (n + m) := fun j => (z.2.1 j).toReal
    let X := M.suspendedHamiltonianVectorField ε z
    M.SuspendedHamiltonianDefined z ∧
      M.ExternalActionVelocityDefined ε z ∧
      (∀ j, DifferentiableAt ℝ
        (fun s => M.hamiltonian ε (externalAngleLine z.1.1 j s) z.2) 0) ∧
      DifferentiableAt ℝ
        (fun y => M.hamiltonianLifted ε thetaLift (xLift, y)) z.2.2 ∧
      DifferentiableAt ℝ
        (fun x => M.hamiltonianLifted ε thetaLift (x, z.2.2)) xLift ∧
      (∀ j,
        HasDerivAt
          (fun s =>
            (((ι (torusTranslation M.externalFrequency Ω s q)).1.1 j).toCircle : ℂ))
          (Complex.I * (X.1.1 j : ℂ) * (((z.1.1 j).toCircle : ℂ))) t) ∧
      HasDerivAt
        (fun s => (ι (torusTranslation M.externalFrequency Ω s q)).1.2)
        X.1.2 t ∧
      (∀ j,
        HasDerivAt
          (fun s =>
            (((ι (torusTranslation M.externalFrequency Ω s q)).2.1 j).toCircle : ℂ))
          (Complex.I * (X.2.1 j : ℂ) * (((z.2.1 j).toCircle : ℂ))) t) ∧
      HasDerivAt
        (fun s => (ι (torusTranslation M.externalFrequency Ω s q)).2.2)
        X.2.2 t

/-- Coordinatewise uniform closeness of the full suspended torus to the
standard one, including the external actions omitted by a non-autonomous
physical-only formulation. -/
def SuspendedCloseToUnperturbed {n m : ℕ} (M : Model n m)
    (rate : ℝ → ℝ) (ε : ℝ) (y : Point (n + m)) (φ : PhaseAngle m)
    (ι : TorusPoint n → SuspendedPhase (n + m)) : Prop :=
  ∀ q,
    (∀ j, dist ((ι q).1.1 j) (q.1 j) ≤ rate ε) ∧
    ‖(ι q).1.2‖ ≤ rate ε ∧
    (∀ i, dist ((ι q).2.1 i) (M.frame.originalAngles q.2 φ i) ≤ rate ε) ∧
    ∀ i, |(ι q).2.2 i - y i| ≤ rate ε

end KAMInterfaces

/-! ## The complete corrected persistence proposition -/

namespace KAMMainCorrected

open Filter MeasureTheory Set
open scoped Topology
open KAMInterfaces

/-- Corrected headline persistence problem for the actual suspended
Hamiltonian `⟨ω,J⟩ + N + epsilon P`.  The radius `ξ` is quantified outside the
smallness threshold, exactly as in Theorem 2.7. -/
def PoincareTreshchevPersistenceProblem {n m : ℕ} (M : Model n m) : Prop :=
  ∀ hypotheses : CorrectedHypotheses M,
    ∀ ξ : ℝ, 0 < ξ → ξ ≤ hypotheses.trimRadius →
      ∃ epsilonZero : ℝ, 0 < epsilonZero ∧ epsilonZero ≤ 1 ∧
      ∃ closenessRate : ℝ → ℝ,
        (∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
          0 ≤ closenessRate epsilon) ∧
        Tendsto closenessRate (𝓝[>] 0) (𝓝 0) ∧
        ∃ Lambda : ℝ → Set (Point (n + m)),
          (∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
            IsClosed (Lambda epsilon) ∧
            MeasurableSet (Lambda epsilon) ∧
            (Lambda epsilon).Nonempty ∧
            Lambda epsilon ⊆ trimmedNondegenerateResonantSet M ξ) ∧
          Tendsto
            (fun epsilon => MeasureTheory.volume
              ((reducedFrequency M.frame
                (internalFrequency M.integrableHamiltonian)) ''
                (trimmedNondegenerateResonantSet M ξ \ Lambda epsilon)))
            (𝓝[>] 0) (𝓝 0) ∧
          ∀ epsilon, 0 < epsilon → epsilon ≤ epsilonZero →
            ∀ y ∈ Lambda epsilon, ∀ phi,
              IsAssociatedNondegenerateCritical M.perturbation phi y →
                ∃ embedding : TorusPoint n → SuspendedPhase (n + m),
                  Topology.IsEmbedding embedding ∧
                  IsRealAnalyticAlmostPeriodicSuspendedEmbedding
                    M.spatialStructure embedding ∧
                  IsSymplecticallyConjugateSuspendedEmbedding
                    M y phi embedding ∧
                  IsSuspendedHamiltonianInvariantTorus M epsilon y embedding ∧
                  SuspendedCloseToUnperturbed
                    M closenessRate epsilon y phi embedding

end KAMMainCorrected

Source

Yuan Zhang, Wen Si, and Jianguo Si, Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations, Discrete and Continuous Dynamical Systems 52 (2026), 32–69, Theorem 2.7 on journal p. 39, with Definitions 2.2–2.4, equations (5)–(7), and the full twist/parameter reduction used in Lemma 3.2 on pp. 41–43: https://doi.org/10.3934/dcds.2026043

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

Definitions.KAMInterfaces / definition bundle

KAMInterfaces.Point. For $d\in\mathbb N$ , a point is a function $\operatorname{Fin}(d)\to\mathbb R$ . When $d=0$ , this is the one-element empty-coordinate space.

KAMInterfaces.ComplexPoint. For $d\in\mathbb N$ , a complex point is a function $\operatorname{Fin}(d)\to\mathbb C$ ; for $d=0$ , it has only the empty function.

KAMInterfaces.LatticePoint. For $d\in\mathbb N$ , a lattice point is a function $\operatorname{Fin}(d)\to\mathbb Z$ ; for $d=0$ , it has only the zero/empty function.

KAMInterfaces.PhaseAngle. For $m\in\mathbb N$ , a phase angle is an $m$ -tuple of real circle angles. At $m=0$ , there is a unique tuple.

KAMInterfaces.ExternalAngle. An external angle is an arbitrary integer-indexed family of real circle angles; no decay or regularity is imposed.

KAMInterfaces.ExternalAction. An external action is a real integer-indexed $\ell^1$ sequence.

KAMInterfaces.ComplexExternalAction. A complex external action is a complex integer-indexed $\ell^1$ sequence.

KAMInterfaces.TorusPoint. A torus point of internal dimension $n$ is a pair consisting of an external angle and an $n$ -tuple of internal circle angles.

KAMInterfaces.FiniteMode. A finite external mode is a finitely supported integer-valued function on $\mathbb Z$ .

KAMInterfaces.CanonicalPhase. A canonical phase point of dimension $d$ is a pair $(x,y)$ with $x$ a $d$ -tuple of circle angles and $y\in\mathbb R^d$ .

KAMInterfaces.PhaseVector. A finite-dimensional phase vector is a pair of points in $\mathbb R^d$ .

KAMInterfaces.SuspendedPhase. A suspended phase point of dimension $d$ is $((\theta,J),(x,y))$ , where $\theta$ is an arbitrary integer-indexed circle angle, $J$ is a real $\ell^1$ sequence, $x$ is a $d$ -tuple of circle angles, and $y\in\mathbb R^d$ .

KAMInterfaces.ExternalCylinderVector. An external cylinder direction is a finitely supported real function on $\mathbb Z$ .

KAMInterfaces.SuspendedCylinderVector. A suspended cylinder direction is $((v_\theta,v_J),(v_x,v_y))$ , where $v_\theta$ is finitely supported, $v_J\in\ell^1(\mathbb Z,\mathbb R)$ , and $v_x,v_y\in\mathbb R^d$ .

KAMInterfaces.SuspendedPhaseVector. A suspended phase vector has the same components except that its external-angle component is an arbitrary function $\mathbb Z\to\mathbb R$ , rather than a finitely supported one.

KAMInterfaces.complexifyExternalAction. This sends a real $\ell^1$ action $J$ to the complex $\ell^1$ action with coordinates $J_j$ viewed in $\mathbb C$ .

KAMInterfaces.complexifyPoint. This sends $x\in\mathbb R^d$ to the same coordinate vector in $\mathbb C^d$ .

KAMInterfaces.complexTube. For $G\subseteq\mathbb R^d$ and $r\in\mathbb R$ , this is the set of $z\in\mathbb C^d$ for which some $y\in G$ satisfies $d(z,y)<r$ , using the coerced real point. It is empty if $G$ is empty or $r\le0$ .

KAMInterfaces.complexEpsilonTube. For $r\in\mathbb R$ , this is the set of $z\in\mathbb C$ lying at distance $<r$ from some real $\epsilon\in[-1,1]$ . It is empty when $r\le0$ .

KAMInterfaces.unitMode. For $j\in\mathbb Z$ , this is the finitely supported integer mode equal to $1$ at $j$ and $0$ elsewhere.

KAMInterfaces.modePairing. For a finite mode $k$ and arbitrary real frequency family $\omega$ , this is the finite sum $\langle k,\omega\rangle=\sum_j k_j\omega_j$ .

KAMInterfaces.modeL1. This is the natural number $|k|_1=\sum_j|k_j|$ , where only the finite support contributes.

KAMInterfaces.latticePairing. For $k\in\mathbb Z^d$ and $x\in\mathbb R^d$ , this is $\sum_{j\in\operatorname{Fin}(d)}k_jx_j$ ; at $d=0$ , it is $0$ .

KAMInterfaces.latticeL1. For $k\in\mathbb Z^d$ , this is $\sum_j|k_j|$ as a natural number; at $d=0$ , it is $0$ .

KAMInterfaces.spatialSetWeight. For a real exponent $p$ and finite $A\subset\mathbb Z$ , this is

[A]_p=1+\sum_{j\in A}\bigl(\log(1+|j|)\bigr)^p,

where the power is the total real-power operation and $|j|$ is first taken as a natural number. The definition itself permits every real $p$ , although a spatial structure later requires $p>2$ .

KAMInterfaces.SpatialStructure. A spatial structure supplies a set $\mathcal S$ of finite subsets of $\mathbb Z$ , an exponent $p>2$ , coverage of every $j\in\mathbb Z$ by at least one $A\in\mathcal S$ , and closure under $A\cup B$ whenever $A,B\in\mathcal S$ intersect. It also supplies a total envelope $E(k)$ for every finite mode. Only when $k$ is supported in some member of $\mathcal S$ , the laws require $E(k)\in\mathcal S$ , $\operatorname{supp}k\subseteq E(k)$ , and $[E(k)]_p\le[A]_p$ for every $A\in\mathcal S$ containing $\operatorname{supp}k$ . For inadmissible $k$ , the envelope is unconstrained.

KAMInterfaces.SpatialStructure.IsAdmissible. A finite mode $k$ is admissible for $\mathcal S$ exactly when there exists $A\in\mathcal S$ with $\operatorname{supp}k\subseteq A$ .

KAMInterfaces.SpatialStructure.unitMode_admissible. For every spatial structure and every $j\in\mathbb Z$ , the unit mode at $j$ is admissible.

KAMInterfaces.modeSpatialWeight. This assigns every finite mode $k$ the real number $[E(k)]_p$ . For admissible modes it is the minimum permitted shell weight by the structure laws; for inadmissible modes it still has a value but that value is unconstrained.

KAMInterfaces.siteSpatialWeight. The site weight of $j$ is the preceding mode weight of the unit mode at $j$ ; unit-mode admissibility makes the envelope constraints apply.

KAMInterfaces.HasWeightedExternalAction. For a spatial structure $S$ , real $w$ , and real $\ell^1$ sequence $J$ , this says that

\sum_{j\in\mathbb Z}|J_j|e^{w[j]_S}

is summable. The definition allows negative, zero, or positive $w$ .

KAMInterfaces.HasWeightedComplexExternalAction. This is the same weighted summability condition for a complex $\ell^1$ sequence $J$ .

KAMInterfaces.weightedComplexExternalActionNorm. This is the total infinite sum

\sum_{j\in\mathbb Z}|J_j|e^{w[j]_S}.

As a raw total sum it takes the library fallback value when the family is not summable; predicates that use it below separately demand the corresponding summability.

KAMInterfaces.externalCharacter. For a finite mode $k$ and external angle $\theta$ , this is the finite product $\prod_j(\theta_j^{\circ})^{k_j}\in\mathbb C$ , where $\theta_j^\circ$ is the unit-circle representative. Integer, including negative, powers are used.

KAMInterfaces.finiteCharacter. For $k\in\mathbb Z^d$ and a $d$ -tuple of circle angles $x$ , this is $\prod_j(x_j^\circ)^{k_j}$ ; at $d=0$ , it is $1$ .

KAMInterfaces.IsPrimitive. An additive subgroup $g\le\mathbb Z^d$ is primitive when, for every natural $q\ne0$ and every $z\in\mathbb Z^d$ , $qz\in g$ implies $z\in g$ .

KAMInterfaces.ResonanceFrame. For $n,m\in\mathbb N$ , a resonance frame consists of a subgroup $g\le\mathbb Z^{n+m}$ and an integer $(n+m)\times(n+m)$ matrix $K_0$ with determinant exactly $1$ , such that $g$ equals the additive subgroup generated by the last $m$ columns of $K_0$ . Primitivity is not a field of this structure; it is imposed later. At $m=0$ , $g$ is forced to be the subgroup generated by the empty range.

KAMInterfaces.ResonanceFrame.K₁. This is the $(n+m)\times n$ matrix consisting of the first $n$ columns of $K_0$ .

KAMInterfaces.ResonanceFrame.K₂. This is the $(n+m)\times m$ matrix consisting of the last $m$ columns of $K_0$ .

KAMInterfaces.ResonanceFrame.adaptedLift. For a real lifted angle $x\in\mathbb R^{n+m}$ , this returns $(\psi,\phi)=(K_1^Tx,K_2^Tx)\in\mathbb R^n\times\mathbb R^m$ .

KAMInterfaces.ResonanceFrame.adaptedAngles. For a torus angle $x$ , this returns circle angles $(\psi,\phi)$ , whose coordinates are the integer linear combinations given by $K_1^T$ and $K_2^T$ .

KAMInterfaces.ResonanceFrame.originalAngles. For $\psi\in\mathbb T^n$ and $\phi\in\mathbb T^m$ , append them and apply the transpose-indexed adjugate formula

x_i=\sum_a\operatorname{adj}(K_0)_{a i}\,q_a.

The definition is total; the frame law $\det K_0=1$ makes the adjugate the integer inverse relevant to this formula.

KAMInterfaces.reducedFrequency. Given an internal-frequency map $\nu:\mathbb R^{n+m}\to\mathbb R^{n+m}$ , this is $y\mapsto K_1^T\nu(y)\in\mathbb R^n$ .

KAMInterfaces.resonantSet. This is the set of $y\in G$ satisfying $K_2^T\nu(y)=0$ coordinatewise. If $m=0$ , the equations are vacuous and the set is $G$ .

KAMInterfaces.IsAnalyticDiffeomorphismOn. A map $f:\mathbb R^d\to\mathbb R^e$ has this property from a source set $A$ to a target set $B$ when it is real analytic on a neighborhood of $A$ , maps $A$ bijectively onto $B$ , and there exists a total inverse map analytic on a neighborhood of $B$ , mapping $B$ into $A$ , inverse to $f$ on both sets. In addition, there is a real $\tau>0$ such that $\tau\,d(x,y)\le d(f(x),f(y))$ for all $x,y\in A$ . Empty source and target make all pointwise and Lipschitz clauses vacuous and can satisfy this predicate.

KAMInterfaces.ApproximationFunction. An approximation function is a total $\Delta:\mathbb R\to\mathbb R$ satisfying: $\Delta(t)\ge1$ for $t\ge0$ ; monotonicity on $[0,\infty)$ ; $\Delta(0)=1$ ; antitonicity of $t\mapsto\log(\Delta(t))/t$ on $(0,\infty)$ ; convergence of that ratio to $0$ as $t\to+\infty$ ; and integrability of $\log(\Delta(t))/t^2$ over $(0,\infty)$ . Its values at negative arguments are otherwise unconstrained.

KAMInterfaces approximation-function coercion. This declaration makes an approximation-function structure callable as its underlying real function $\Delta(t)$ ; it adds no proposition.

KAMInterfaces.StronglyNonresonant. For $S,\omega,\gamma,\Delta$ , this says $\gamma>0$ and, for every nonzero admissible finite mode $k$ ,

|\langle k,\omega\rangle| \ge \frac{\gamma} {\Delta([k]_S)\Delta(|k|_1)}.

Every unit mode is among the admissible nonzero modes, so the universal condition is not indexed by an empty class. No internal frequency enters this condition.

KAMInterfaces.PerturbationMode. A perturbation mode is a triple $(k,\ell,r)$ with $k$ a finitely supported external integer mode, $\ell\in\mathbb Z^n$ , and $r\in\mathbb Z^m$ .

KAMInterfaces.FourierPerturbation. A perturbation is raw coefficient data $P_{A,k,\ell,r}(y,\epsilon)\in\mathbb C$ for every finite shell $A\subset\mathbb Z$ , every perturbation mode, every $y\in\mathbb C^{n+m}$ , and every $\epsilon\in\mathbb C$ . The structure itself imposes no support, convergence, reality, or analyticity.

KAMInterfaces.perturbationModeL1. The length of $(k,\ell,r)$ is $|k|_1+|\ell|_1+|r|_1$ .

KAMInterfaces.FourierPerturbation.evaluateLifted. For arbitrary real lifts $\theta,\psi,\phi$ , real $y$ , and real $\epsilon$ , this is the real part of

\sum_{A,k,\ell,r}P_{A,k,\ell,r}(y,\epsilon) e^{i(\langle k,\theta\rangle+\langle\ell,\psi\rangle+\langle r,\phi\rangle)}.

It is a total infinite sum; absent a summability condition, its fallback behavior can collapse a nonsummable series.

KAMInterfaces.FourierPerturbation.IsRealAnalyticAlmostPeriodicOn. This says that there exist positive real widths $a,s,\rho$ and shell bounds $B_A\ge0$ such that $B_A=0$ outside $S.\mathrm{sets}$ , $\sum_A B_Ae^{s[A]_S}$ is summable, and every coefficient is identically zero unless $A\in S.\mathrm{sets}$ and the external support of its mode is contained in $A$ . Every individual coefficient is complex differentiable on the product of the complex $\rho$ -tube about $G$ and the complex $\rho$ -tube about $[-1,1]$ , and throughout that product

|P_{A,\mu}(y,\epsilon)|e^{a|\mu|_1}\le B_A.

For every $A$ and every such $y,\epsilon$ , the absolute coefficient sum over all modes is summable. For all $A,\mu$ , all real $y\in G$ , and all real $\epsilon\in[-1,1]$ , negating all three mode components conjugates the coefficient. For every arbitrary real external lift $\theta:\mathbb Z\to\mathbb R$ , the actually summed real evaluation is real analytic on a neighborhood of all $(\psi,\phi)$ and of $G\times[-1,1]$ . Finally, the actually summed zero-external, zero-fast-angle coefficient at $\epsilon=0$ is analytic on a neighborhood of $\mathbb R^m\times G$ . If $G=\varnothing$ , the tube-dependent clauses are vacuous, although the global shell support and summability clauses remain.

KAMInterfaces.averagedPotentialLift. This is the real part of

h_0(\phi,y)= \sum_{A,r}P_{A,(0,0,r)}(y,0)e^{i\langle r,\phi\rangle}.

As a raw total sum it has fallback behavior if nonsummable; the preceding analytic-class predicate separately controls this sum.

KAMInterfaces.phaseAngleLift. This replaces each circle angle by its standard chosen real representative.

KAMInterfaces.coordinateGradient. For a total $f:\mathbb R^d\to\mathbb R$ , its coordinate-gradient value at $x$ has $j$ -th coordinate equal to the Fréchet derivative of $f$ at $x$ applied to the $j$ -th standard basis vector. The Fréchet derivative is total and is $0$ at nondifferentiable points.

KAMInterfaces.IsAveragedCritical. A circle angle $\phi$ is averaged-critical at $y$ when the coordinate gradient in the lifted $\phi$ variables of the explicit averaged sum equals the zero vector. At $m=0$ , this equality is automatic.

KAMInterfaces.averagedCriticalHessian. This is the $m\times m$ matrix obtained by Fréchet differentiating the preceding coordinate-gradient map at the standard lift of $\phi$ and applying it to coordinate vectors. Without differentiability, the total derivative can fall back to zero.

KAMInterfaces.internalFrequency. For $N:\mathbb R^d\to\mathbb R$ , this is the coordinate-gradient map $y\mapsto\nabla N(y)$ , with the same derivative fallback at nondifferentiable points.

KAMInterfaces.Model. A model of dimensions $n,m$ contains a resonance frame, an arbitrary parameter set $G\subseteq\mathbb R^{n+m}$ , an arbitrary real function $N$ , an arbitrary real external-frequency family $\omega_j$ , raw Fourier perturbation coefficients, an approximation function, a real divisor constant, and a spatial structure. The structure itself imposes no relation among these fields.

KAMInterfaces.Model.perturbationValue. At external and physical circle angles $(\theta,x)$ , action $y$ , and parameter $\epsilon$ , this lifts the angles by their standard representatives, applies $K_1^T$ and $K_2^T$ to the physical lift, and evaluates the perturbation Fourier sum there.

KAMInterfaces.Model.hamiltonian. This is the finite physical Hamiltonian

H_\epsilon(\theta,x,y)=N(y)+\epsilon P(\theta,x,y,\epsilon).

It has no external-action variable.

KAMInterfaces.Model.hamiltonianLifted. On real lifts $\theta,x$ , this is the same expression, with $K_1^Tx,K_2^Tx$ inserted into the explicit perturbation evaluation.

KAMInterfaces.Model.hamiltonianVectorField. At $(\theta,x,y)$ , this is $(\partial_yH,-\partial_xH)$ , computed via coordinate Fréchet derivatives of the lifted Hamiltonian. The raw definition can use zero derivative fallbacks; the invariance predicate later separately requires differentiability at every sampled point.

KAMInterfaces.IsAssociatedNondegenerateCritical. A pair $(\phi,y)$ is associated and nondegenerate when $\phi$ is an averaged critical circle angle at $y$ and the explicit averaged Hessian at $(\phi,y)$ has nonzero determinant. For $m=0$ , the critical condition is automatic and the empty-matrix determinant convention governs nondegeneracy.

KAMInterfaces.nondegenerateResonantSet. This is the set of $y\in G$ satisfying $K_2^T\nabla N(y)=0$ for which there exists at least one circle angle $\phi$ that is averaged critical and has nonzero averaged Hessian determinant.

KAMInterfaces.nondegenerateReducedFrequencyDomain. This is the image of the preceding set under $y\mapsto K_1^T\nabla N(y)$ .

KAMInterfaces.trimmedReducedFrequencyDomain. For real $\xi$ , this consists of those $\Omega$ in the reduced-frequency image for which

\xi\le \operatorname{infDist}\bigl(\Omega,\operatorname{frontier}(\mathcal O)\bigr),

where $\mathcal O$ is that image. The definition is total for every $\xi$ , including nonpositive values and empty frontiers; later hypotheses use only positive $\xi$ .

KAMInterfaces.trimmedNondegenerateResonantSet. This is the subset of the nondegenerate resonant set whose reduced frequency belongs to the preceding $\xi$ -trimmed domain.

KAMInterfaces.CorrectedHypotheses. For a model $M$ , an inhabitant supplies proofs that $n>0$ , $m>0$ , the resonance subgroup is primitive, $G$ is closed and bounded, and $N$ is real analytic on a neighborhood of $G$ . It requires the nondegenerate resonant set to be nonempty and supplies a trim radius $r_*>0$ . For every $0<\xi\le r_*$ , the pulled-back trimmed resonant set must be measurable and compact; the reduced-frequency trimmed domain must have strictly positive $n$ -dimensional Lebesgue volume; at every retained $y$ , the Fréchet derivative of $y\mapsto\nabla N(y)$ must be injective; the reduced-frequency map must be an analytic diffeomorphism, in the explicit analytic/bijective/inverse/lower-Lipschitz sense, from the pulled-back trim onto its reduced domain; and every averaged critical $\phi$ at every retained $y$ must have nonzero Hessian determinant. Finally, the external frequency must satisfy the explicit strong nonresonance inequality with the model’s divisor constant and approximation function, and the perturbation must satisfy the full shell-indexed analytic almost-periodic predicate. Since the reduced trim has positive measure for each allowed $\xi$ , those reduced trims are nonempty.

KAMInterfaces.torusTranslation. For external frequency $\omega$ , internal frequency $\Omega$ , time $t$ , and torus point $q=(\theta,\psi)$ , this is

(\theta_j+t\omega_j,\ \psi_i+t\Omega_i)

with all additions taken as circle-angle additions.

KAMInterfaces.standardSuspendedEmbedding. For $M,y,\phi$ , this sends $q=(\theta,\psi)$ to

((\theta,0),(\operatorname{originalAngles}_M(\psi,\phi),y)).

KAMInterfaces.EmbeddingMode. An embedding Fourier mode is a pair consisting of a finitely supported external integer mode and an internal lattice point in $\mathbb Z^n$ .

KAMInterfaces.embeddingModeL1. Its length is the sum of the external and internal $\ell^1$ lengths.

KAMInterfaces.HasShellFourierExpansion. For fixed $S,a,s$ and scalar $f$ on the torus, this asserts the existence of coefficients $c_{A,\mu}$ and bounds $B_A\ge0$ . Bounds vanish off $S.\mathrm{sets}$ , $\sum_AB_Ae^{s[A]_S}$ is summable, and coefficients vanish unless $A\in S.\mathrm{sets}$ and the external support of $\mu$ lies in $A$ . For every shell $A$ , $\sum_\mu|c_{A,\mu}|$ is summable, and

|c_{A,\mu}|e^{a|\mu|_1}\le B_A.

For every torus point $q$ , $f(q)$ equals the total sum of $c_{A,\mu}$ times the external and finite characters. This raw predicate does not itself require $a$ or $s$ to be positive.

KAMInterfaces.HasWeightedActionShellFourierExpansion. For an external-action-valued $f$ , this asserts complex $\ell^1$ -valued coefficients $c_{A,\mu}$ and shell bounds with the same nonnegativity, shell support, spatially weighted summability, and mode-support rules. Every coefficient is summable with action weight $w$ ; its weighted action norm times $e^{a|\mu|_1}$ is at most $B_A$ ; the weighted norms are summable over all shell-mode pairs; and, at every torus point, the corresponding Banach-valued character series is summable. Each real output $f(q)$ itself has weighted action summability, and its coordinatewise complexification equals that series. The raw predicate allows arbitrary $a,s,w$ .

KAMInterfaces.IsRealAnalyticAlmostPeriodicSuspendedEmbedding. A suspended embedding $\iota$ has this property when there exist $a,s,w\in\mathbb R$ with $a>0$ , $s>0$ , $0\le w<s$ , such that every external-angle coordinate after passage to its complex unit-circle value has a scalar shell expansion; the full external-action component has one weighted action shell expansion; every finite internal-angle circle coordinate has a scalar shell expansion; and every finite action coordinate, viewed in $\mathbb C$ , has a scalar shell expansion. This predicate alone does not assert injectivity or topological embedding.

KAMInterfaces.suspendedCylinderPath. Starting at $z=((\theta,J),(x,y))$ in a cylinder direction $v$ , this path adds $tv_{\theta,j}$ to every external angle, adds $t v_J$ in $\ell^1$ , adds $tv_{x,i}$ to each internal angle, and adds $tv_{y,i}$ to each finite action.

KAMInterfaces.suspendedTransformationTangent. For a total transformation $F$ , point $z$ , and cylinder direction $v$ , this differentiates $F(z+tv)$ at $t=0$ . Each angular velocity is extracted as the imaginary part of the conjugate of the output circle value times the derivative of that circle value; the action components are ordinary derivatives in their Banach spaces. All derivative operators are total and can return fallback zero without differentiability.

KAMInterfaces.CylinderDifferentiableOn. A transformation $F$ has this property on $U$ when, for every $z\in U$ and every cylinder direction $v$ , all external circle-coordinate curves, the external $\ell^1$ -action curve, all finite circle-coordinate curves, and the finite-action curve are differentiable at $0$ . If $U$ is empty, the condition is vacuous.

KAMInterfaces.ExternalSymplecticSummable. For phase vectors $u,v$ , this says the integer-indexed family $u_{\theta,j}v_{J,j}-u_{J,j}v_{\theta,j}$ is summable.

KAMInterfaces.suspendedCanonicalSymplecticForm. This is

\sum_{j\in\mathbb Z}(u_{\theta,j}v_{J,j}-u_{J,j}v_{\theta,j}) +\sum_{i\in\operatorname{Fin}(d)}(u_{x,i}v_{y,i}-u_{y,i}v_{x,i}).

The first total sum has fallback behavior if it is not summable; every symplectic use below explicitly demands summability of the output pair.

KAMInterfaces.suspendedCylinderVectorToPhaseVector. This includes a cylinder direction into a phase vector by viewing its finitely supported external-angle component as an arbitrary real family and leaving every other component unchanged.

KAMInterfaces.LocalSuspendedTransformation. Such a transformation supplies open source and target subsets of suspended phase space, total forward and inverse functions, proofs that they map the designated sets into one another and are mutual inverses there, and continuity of both maps on their respective sets. The structure itself does not require differentiability or symplecticity. Both sets can be empty, making the pointwise conditions vacuous.

KAMInterfaces.LocalSuspendedTransformation.IsSymplectic. This requires cylinder differentiability of the forward map on its source and, for every source point and every two cylinder directions, summability of the external part of the two output tangent vectors and equality of the full suspended canonical form on the output tangents with that on the included input directions. It says nothing at points outside the source.

KAMInterfaces.IsSymplecticallyConjugateSuspendedEmbedding. An embedding $\iota$ is symplectically conjugate to the standard torus for $M,y,\phi$ when there exists a local suspended transformation $F$ whose source contains the entire range of the standard embedding, which is symplectic in the preceding cylinder sense, fixes every external-angle component pointwise throughout its source, and satisfies $\iota(q)=F(\iota_0(q))$ for every $q$ . Since the standard torus has points, the source in such a witness cannot be empty.

KAMInterfaces.Model.suspendedHamiltonian. At $z=((\theta,J),(x,y))$ , this is

\mathcal H_\epsilon(z)=\sum_{j\in\mathbb Z}\omega_jJ_j+H_\epsilon(\theta,x,y).

The external pairing is a total infinite sum and may use its fallback value when nonsummable.

KAMInterfaces.Model.SuspendedHamiltonianDefined. At $z$ , this says the family $j\mapsto\omega_jJ_j$ is summable, excluding the preceding fallback there.

KAMInterfaces.externalAngleLine. This varies a single external angle $j$ by a real circle increment $s$ and leaves every other external angle fixed.

KAMInterfaces.Model.externalActionVelocityRaw. Its $j$ -th coordinate is minus the derivative at $s=0$ of the physical Hamiltonian under the preceding variation of $\theta_j$ . The derivative is total and can be zero by fallback at a nondifferentiable point.

KAMInterfaces.Model.ExternalActionVelocityDefined. This says that the entire raw external-action velocity belongs to real $\ell^1(\mathbb Z)$ .

KAMInterfaces.Model.externalActionVelocity. If the preceding $\ell^1$ membership holds, this packages the raw family with that proof as an external action; otherwise, it returns the zero $\ell^1$ sequence.

KAMInterfaces.Model.suspendedHamiltonianVectorField. This is the phase vector

((\omega,\dot J),(\partial_yH,-\partial_xH)),

where $\dot J$ is the packaged external action velocity and the finite components are the explicit coordinate-gradient Hamiltonian vector field.

KAMInterfaces.IsSuspendedHamiltonianInvariantTorus. Fix $M,\epsilon,y,\iota$ , put $\Omega=K_1^T\nabla N(y)$ , and quantify over every torus point $q$ and every $t\in\mathbb R$ . Let $z=\iota(T_tq)$ , where $T_t$ translates with frequencies $(\omega,\Omega)$ , and let $X$ be the explicit suspended Hamiltonian vector field at $z$ . The predicate requires the external Hamiltonian pairing and raw external-action velocity to be defined at $z$ ; differentiability at $0$ of every one-coordinate external-angle variation of $H$ ; and differentiability of the lifted Hamiltonian in its finite action and angle variables at the sampled point. It then requires, at time $t$ , the derivative of every external output circle coordinate along $s\mapsto\iota(T_sq)$ to equal $iX_{\theta,j}$ times that circle value; the derivative of the external $\ell^1$ -action curve to equal $X_J$ ; the analogous derivative identity for every internal circle coordinate; and the derivative of the finite-action curve to equal $X_y$ . Thus every displayed coordinate equation holds for all $q,t$ ; no merely almost-everywhere notion is used.

KAMInterfaces.SuspendedCloseToUnperturbed. For every torus point $q$ , this requires each external output angle to be within $\operatorname{rate}(\epsilon)$ of $q$ ’s external angle, the norm of the full external-action output to be at most that rate, each finite output angle to be within that rate of the corresponding original angle determined by $(q_{\rm int},\phi)$ , and each finite action coordinate to differ from $y$ in absolute value by at most that rate. The raw definition does not require the rate to be nonnegative, though the persistence problem does so for the positive perturbations it uses.

KAMMainCorrected.PoincareTreshchevPersistenceProblem. For a model $M$ , this proposition universally quantifies over every inhabitant $h$ of CorrectedHypotheses $M$ , and then over every real $0<\xi\le h.r_*$ . It requires a real $\epsilon_0$ with $0<\epsilon_0\le1$ , a single rate $r:\mathbb R\to\mathbb R$ that is nonnegative for every $0<\epsilon\le\epsilon_0$ and tends to $0$ as $\epsilon\to0^+$ , and a family $\Lambda_\epsilon\subseteq\mathbb R^{n+m}$ . For every $0<\epsilon\le\epsilon_0$ , $\Lambda_\epsilon$ must be closed, measurable, nonempty, and contained in the $\xi$ -trimmed nondegenerate resonant set. The $n$ -dimensional Lebesgue volume of the reduced-frequency image of the removed set

\bigl(\operatorname{trim}_\xi M\bigr)\setminus\Lambda_\epsilon

must tend to $0$ as $\epsilon\to0^+$ . For every such $\epsilon$ , every $y\in\Lambda_\epsilon$ , and every circle angle $\phi$ , if $(\phi,y)$ is an averaged critical point with nonzero averaged Hessian determinant, then there exists a torus map $\iota$ that is a topological embedding, has all the shell-indexed analytic almost-periodic coordinate expansions, is the image of the standard suspended torus under a local symplectic transformation fixing external angles, satisfies every coordinate of the explicit suspended Hamilton equation under the rigid frequency translation, and obeys the full coordinatewise closeness bounds with rate $r(\epsilon)$ . Membership of $y$ in the nondegenerate resonant set guarantees at least one associated nondegenerate $\phi$ , so the final implication cannot be vacuous for every $\phi$ at a retained $y$ . The threshold, rate, and $\Lambda$ may depend on $M,h,\xi$ ; an embedding may additionally depend on $\epsilon,y,\phi$ . Nothing is asserted for $\epsilon\le0$ or $\epsilon>\epsilon_0$ . If CorrectedHypotheses $M$ is empty, the outer universal quantifier makes the entire proposition vacuously true; for an actual hypothesis inhabitant, $r_*>0$ ensures that admissible positive $\xi$ exist.

Human review

Endorsed by Shuze Chen · Aug 27, 2026
Endorsed by ShouqiaoWang · Aug 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph