ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A two-rotor model with units: dimensionless normalisation, Diophantine measure and the conditional KAM family

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited from the positive-measure supplier.

The dimensionless model. On the phase space $R^{2} \times T^{2}$ with angular variables $θ_{1}, θ_{2}$ read modulo $2 π$ and coupling $ε > 0$ , consider the Hamiltonian $H (I, θ) : = \frac{1}{2} (I_{1}^{2} + I_{2}^{2}) + ε \cos θ_{1} \cos θ_{2}, I = (I_{1}, I_{2}) \in R^{2},$ so that $h (I) = \frac{1}{2} (I_{1}^{2} + I_{2}^{2})$ and $F (I, θ) = ε \cos θ_{1} \cos θ_{2}$ . This is the standard dimensionless model of two rotors with uncoupled kinetic terms and a cosine interaction, and is a worked instance of Positive-measure families of invariant Lagrangian tori for nondegenerate real analytic Hamiltonians: persistence for $ε \leq c α^{2}$ . The example is conditional mathematics: nothing below asserts that any physical rotor is governed by this model, and no empirical quantity, measurement or statistical inference occurs.

The physical reading with units. Let $E_{u n i t} > 0$ be an energy unit. For an illustrative model, take $q = (q_{1}, q_{2}) \in T^{2}$ as angular coordinates in radians (dimensionless) and $p = (p_{1}, p_{2}) \in R^{2}$ as their conjugate angular momenta, with dimension energy times time. Let $I > 0$ be the common moment of inertia, with dimension energy times time squared, and let $λ > 0$ be an interaction energy. Adopt the Hamiltonian model $H_{p h y s} (p, q) = \frac{p_{1}^{2} + p_{2}^{2}}{2 I} + λ \cos q_{1} \cos q_{2} .$ With the action unit $J_{0} : = (I E_{u n i t})^{1 / 2}$ and the time unit $t_{0} : = I / J_{0}$ (so that $I = J_{0}^{2} / E_{u n i t} = J_{0} t_{0}$ ), the substitutions $p = J_{0} I$ , $t = t_{0} u$ , $λ = ε E_{u n i t}$ identify $H_{p h y s} / E_{u n i t}$ with the dimensionless $H$ above, and the frequency $ν$ of a torus of $H$ corresponds to rotation of the torus parameter with physical frequencies $ν_{j} / t_{0} = ν_{j} J_{0} / I$ ; the physical angles are obtained through the torus embedding.

Data. Let $α > 0$ and use dimension $n = 2$ and Diophantine exponent $τ : = 2$ . Take $K : = [1, 2]^{2} \subseteq R^{2}$ , $U : = C^{2}$ , $r_{0} : = 1 / 10$ , $Ω : = (1.1, 1.9)^{2}$ , $C^{*} : = [1.2, 1.8]^{2}$ and strip width $s_{0} > 0$ with $0 < σ_{0} \leq \min (1, s_{0} / 24)$ . Then $D h (I) = I$ is the identity, so the inverse frequency map is $b (ν) = ν$ , $K$ is the closed square of side $1$ and $C^{*} + (B_{r_{0}} \cap R^{2}) \subseteq K$ ; the Hessian is $D^{2} h = I_{2}$ , so $M_{2} = 2$ . For real $t$ write $\cosh t : = (e^{t} + e^{- t}) / 2$ and $\sinh t : = (e^{t} - e^{- t}) / 2$ . The perturbation has complex sup-norm $∣ F ∣ = ε \cosh (s_{0})^{2}$ on the strip of width $s_{0}$ if $F (I, θ) = ε \cos θ_{1} \cos θ_{2}$ is evaluated there.

Facts & Assumptions

Given: The Axiom of Countable Choice, $α > 0$ , and the dimensionless Hamiltonian $H = \frac{1}{2} (I_{1}^{2} + I_{2}^{2}) + ε \cos θ_{1} \cos θ_{2}$ with $ε > 0$ , the data $K, U, r_{0}, Ω, C^{*}, s_{0}, σ_{0}$ of the example, and the positive physical data $E_{u n i t}, I, λ$ .

[L1]

The KAM theorem Positive-measure families of invariant Lagrangian tori for nondegenerate real analytic Hamiltonians: persistence for $ε \leq c α^{2}$ : for its fixed analytic data there is $c > 0$ such that for $0 < α < c$ and perturbation sup-norm $0 < ε_{K A M} \leq c α^{2}$ the Diophantine set $Ω_{α, τ}$ in $C^{*}$ has positive measure and every $ν \in Ω_{α, τ}$ carries an invariant Lagrangian torus of $H$ with frequency $ν$ , with the closeness bounds of its clause 3. Here the rotor amplitude is $ε$ , while $ε_{K A M} = ε \cosh (s_{0})^{2}$ is its complex-strip sup-norm.

[L2]

For $α > 0$ , the slab estimate Small-divisor slabs and the positive measure of the Diophantine set: the resonance covering has measure $O (α)$ gives, for $n = 2$ , $τ = 2$ and half-width $R$ , a resonant-set bound $2^{2} 2^{1} 4^{2} R α \sum_{m \geq 1} m^{- 2}$ . Its slicing proof also applies to a cube centred at $a$ : the orthogonal image of the cube lies in the radius- $\sqrt{2} R$ ball centred at the image of $a$ , so its transverse projection has length at most $2 \sqrt{2} R$ , while the resonance slab has thickness $2 α ∣ k ∣_{1}^{- 2} / ∣ k ∣_{2}$ independent of that centre. This is also the translated-cube argument in Positive-measure families of invariant Lagrangian tori for nondegenerate real analytic Hamiltonians: persistence for $ε \leq c α^{2}$ fact [F5]. Closed faces do not change the projection or slicing bounds. Finally $\sum_{m \geq 1} m^{- 2} \leq 2$ , since $m^{- 2} \leq 1 / (m (m - 1))$ for $m \geq 2$ and the finite sums of the latter terms are $1 - 1 / N \to 1$ .

[L3]

On complex angles define $\cos z : = (e^{i z} + e^{- i z}) / 2$ and $\sin z : = (e^{i z} - e^{- i z}) / (2 i)$ ; Euler's formula identifies their restrictions to real angles with the real trigonometric functions. Trigonometric and exponential calculus: $\cos$ and $\sin$ are $2 π$ -periodic with $\cos^{'} = - \sin$ , $\sin^{'} = \cos$ , and the addition formula gives $∣ \cos (x + i y) ∣^{2} = \cos^{2} x \cosh^{2} y + \sin^{2} x \sinh^{2} y \leq \cosh^{2} y$ for real $x, y$ (The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[L4]

Rescaling of an autonomous system: if $t = t_{0} u$ and $p = J_{0} I$ then $\frac{d}{d u} = \frac{d t}{d u} \frac{d}{d t} = t_{0} \frac{d}{d t}$ by the chain rule, and $q \mapsto q$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , First-order systems, initial value problems, and solutions on intervals).

[L5]

Notation of the KAM framework: $B_{r}$ , $S_{s}$ , $O_{h}$ , $D_{r, s, h}$ , the label set $Ω_{α, τ}$ and the sup-norms (Analytic KAM data: angular tori, action-angle neighbourhoods, Fourier cutoffs and Diophantine frequency labels, Open ball, closed ball and sphere in a metric space).

Proof

technique · direct; write the dimensionless normalisation, check the data of the KAM theorem with explicit constants, estimate the Diophantine measure arithmetically, and translate the conclusion back to physical units

1.1givenL3L5algebra

Data check. For $h (I) = \frac{1}{2} (I_{1}^{2} + I_{2}^{2})$ one has $D h (I) = I$ , $D^{2} h = I_{2}$ , so $b (ν) = ν$ on $Ω^{'} = C^{2}$ and $∣ I^{T} D^{2} h I ∣ \leq 2 ∣ I ∣_{\infty}^{2}$ , hence $M_{2} = 2$ on $U = C^{2}$ . Moreover $b (Ω) + (B_{r_{0}} \cap R^{2}) = (1, 2)^{2} \subseteq K = [1, 2]^{2}$ , and $C^{*} = [1.2, 1.8]^{2}$ is a compact cube at distance $1 / 10$ from $\partial Ω$ . The perturbation $F (I, θ) = ε \cos θ_{1} \cos θ_{2}$ is holomorphic and $2 π$ -periodic, is conjugation-symmetric by its exponential formula, and by [L3] its sup-norm on the strip of width $s_{0}$ is at most $ε \cosh (s_{0})^{2}$ . Thus the fixed analytic data of [L1] are met, with the positive perturbation bound $ε_{K A M} = ε \cosh (s_{0})^{2}$ .

2.1step 1.1L2algebra

Diophantine measure with explicit constants. For $n = 2$ , $τ = 2$ and the square $C^{*}$ of side $3 / 5$ (half-width $R = 3 / 10$ ), [L2] bounds the resonant set in $C^{*}$ by $2^{2} 2^{1} 4^{2} \cdot (3 / 10) \cdot 2 α = 8 \cdot 16 \cdot (3 / 5) α = (384 / 5) α$ , since $\sum_{m} m^{- 2} \leq 2$ ; the square has measure $9 / 25$ , so the Diophantine set in $C^{*}$ has measure at least $9 / 25 - (384 / 5) α > 0$ whenever $α < (9 / 25) \cdot (5 / 384) = 3 / 640$ .

3.1step 2.1L1algebra

Conditional KAM conclusion. By [L1] with the data of step 1.1 there is a constant $c > 0$ (depending on $σ_{0}, s_{0}$ and the fixed square $C^{*}$ through the theorem) such that if $0 < α < \min (c, 3 / 640)$ and $0 < ε \cosh (s_{0})^{2} \leq c α^{2}$ , then the Diophantine set of step 2.1 has positive measure and each of its frequencies $ν$ carries an invariant Lagrangian torus of $H$ with frequency $ν$ , with the closeness bounds of [L1]; in particular this is a positive-measure family, and the action and angle bounds of clause 3 show the perturbed tori remain close to the unperturbed tori $I = ν$ .

4.1step 3.1L4algebra∎

Units restored. Let the positive physical data $E_{u n i t}, I, λ$ be given and put $J_{0} = (I E_{u n i t})^{1 / 2}$ , $t_{0} = I / J_{0}$ ; with $p = J_{0} I$ , $t = t_{0} u$ and $ε = λ / E_{u n i t} > 0$ the equations $p_{j}^{'} = - \partial_{q_{j}} H_{p h y s}$ , $q_{j}^{'} = \partial_{p_{j}} H_{p h y s}$ become the dimensionless Hamilton equations for $H$ (by [L4] and the identities $t_{0} J_{0} / I = 1$ , $t_{0} λ / J_{0} = λ / E_{u n i t} = ε$ ), and $H_{p h y s} / E_{u n i t} = H$ ; hence the conditional conclusion of step 3.1 holds whenever $0 < α < \min (c, 3 / 640)$ and $0 < λ \leq E_{u n i t} c α^{2} / \cosh (s_{0})^{2}$ . The action unit $J_{0}$ has dimension energy times time and $t_{0}$ has dimension time; the torus with frequency $ν$ then has linear parameter phase with physical frequencies $ν_{j} / t_{0} = ν_{j} J_{0} / I$ ; its physical angles are obtained from that phase by the torus embedding.

Remarks

What the example does and does not show. It exhibits the standard two-rotor model, verifies the hypotheses of the measure theorem with explicit constants, and restores units. It produces no dynamical measurement, no numerical integration and no claim of physical applicability; the tightness or sharpness of the constants is not asserted.
The complex sup-norm. The factor $\cosh (s_{0})^{2}$ records that the theorem's hypotheses are sup-norms over the complex strip, not over the real torus; absorbing it into the threshold changes a constant and nothing else.

A two-rotor model with units: dimensionless normalisation, Diophantine measure and the conditional KAM family

Example

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources