ExampleConstruction: AI-adaptedVerification: AI-adapted

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 trapped one-label model: the compact energy sublevel of the radial quartic potential is invariant with finite phase volume, so the recurrence theorem applies, while the free model's energy sublevels are unbounded and the hypothesis fails

Physical scope

A declared-data check in dimensionless normalized coordinates of the page's recurrence theorem on a trapped one-label, three-dimensional Cartesian model: for the unit-mass radial quartic potential U(x)=||x||^4/4 the six-dimensional phase-space energy sublevel {E<=E1}, E1>0, is compact with finite dimensionless coordinate volume bounded by 512 E1^(9/4), invariant under the flow by energy conservation and compact continuation, so the recurrence theorem gives almost-everywhere infinite returns; in contrast the dimensionless free model U=0 has unbounded energy sublevels and each nonzero-velocity trajectory eventually exits every bounded set, showing the finite-volume hypothesis is not automatic. No SI quantity, measurement or empirical comparison is asserted.

Example

Declared model data. Use dimensionless normalized position, velocity, mass, time and energy coordinates; this is a dimensionless model computation and no SI units are assigned. Take one label in the flat Cartesian presentation of Poincare recurrence for the model's Hamiltonian flow on a bounded invariant set of finite phase volume: almost every state of any Borel subset returns to it infinitely often with $N = 1$ : the configuration domain is $Q : = R^{3}$ , the mass is $m : = 1$ so that $M = I_{3}$ and $W = Q \times R^{3}$ with coordinates $(x, v)$ , and the radial quartic potential is $U (x) : = \frac{1}{4} ∥ x ∥_{2}^{4},$ a $C^{\infty}$ datum of The mechanical first-order field, Lagrangian and energy of a configuration-dependent kinetic metric in a chart with field $G (x, v) = (v, - ∥ x ∥_{2}^{2} x)$ and energy $E (x, v) = \frac{1}{2} ∥ v ∥_{2}^{2} + \frac{1}{4} ∥ x ∥_{2}^{4}$ . For $E_{1} > 0$ put $A_{E_{1}} : = {(x, v) \in W : E (x, v) \leq E_{1}} .$

Assertions to check. (i) $A_{E_{1}}$ is a nonempty compact Borel subset of $W$ with $λ_{6} (A_{E_{1}}) \leq (2 (4 E_{1})^{1 / 4})^{3} (2 \sqrt{2 E_{1}})^{3} = 512 E_{1}^{9 / 4} < \infty$ ; (ii) the flow of the model maps $A_{E_{1}}$ onto itself for every real time, so the hypotheses of Poincare recurrence for the model's Hamiltonian flow on a bounded invariant set of finite phase volume: almost every state of any Borel subset returns to it infinitely often are met and for every Borel $E \subseteq A_{E_{1}}$ almost every state of $E$ returns to $E$ infinitely often; (iii) for the flat model $U \equiv 0$ the energy sublevels are unbounded, the phase measure of $W$ is infinite, and each nonzero-velocity free motion eventually exits every bounded set (hence visits a fixed bounded set at only finitely many integer times), so the finite-volume hypothesis is not automatic.

Facts & Assumptions

Given: the data $N = 1$ , $M = I_{3}$ , $U (x) = ∥ x ∥_{2}^{4} / 4$ , its field and energy; the sublevel $A_{E_{1}}$ ; the flat comparison data $U \equiv 0$ with field $G_{0} (x, v) = (v, 0)$ .

[L1]

Recurrence (Poincare recurrence for the model's Hamiltonian flow on a bounded invariant set of finite phase volume: almost every state of any Borel subset returns to it infinitely often): for an autonomous potential presentation with a bounded invariant Borel set $A$ whose compact closure lies in the phase domain and whose flow is defined for all real times on $A$ , phase volume is preserved on its Borel subsets by finite local covers and time subdivision; almost every state of every Borel $E \subseteq A$ returns to $E$ infinitely often at integer times. The theorem assumes ${A C}_{ω}$ , inherited from the phase-volume result.

[L2]

Energy conservation and compact continuation (Energy is conserved along solutions of the mechanical system with a configuration-dependent kinetic metric, Compact continuation for locally Lipschitz ODEs: a solution whose graph stays in a compact subset of the domain near a finite endpoint extends past it): the energy of the mechanical system is constant along every maximal solution, and a solution whose graph stays in a compact subset of the state domain cannot reach a finite forward or backward endpoint.

[L3]

Borel and Lebesgue vocabulary (The Borel sigma-algebra of a topological space, Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ ): closed sets are Borel, and the Lebesgue measure of a box in $R^{6}$ is the product of its side lengths.

Verification

technique · direct

1.1givenL3algebra

Compactness and phase volume: $E$ is continuous and $A_{E_{1}} = E^{- 1} ((- \infty, E_{1}])$ is closed; if $(x, v) \in A_{E_{1}}$ then $\frac{1}{4} ∥ x ∥_{2}^{4} \leq E_{1}$ and $\frac{1}{2} ∥ v ∥_{2}^{2} \leq E_{1}$ , so $∥ x ∥_{2} \leq (4 E_{1})^{1 / 4}$ and $∥ v ∥_{2} \leq \sqrt{2 E_{1}}$ ; hence $A_{E_{1}}$ is contained in the box of side lengths $2 (4 E_{1})^{1 / 4}$ (three position coordinates) and $2 \sqrt{2 E_{1}}$ (three velocity coordinates), is bounded and closed, therefore compact, and by [L3] has $λ_{6} (A_{E_{1}}) \leq (2 (4 E_{1})^{1 / 4})^{3} (2 \sqrt{2 E_{1}})^{3} = 512 E_{1}^{9 / 4} < \infty$ ; it is nonempty because $(0, 0) \in A_{E_{1}}$ .

2.1step 1.1givenL2algebra

Invariance: along a maximal solution of the quartic model the energy is constant by [L2], so the solution stays in $A_{E_{1}}$ ; because $A_{E_{1}}$ is compact and contained in the state domain $W$ , [L2] also shows the solution is defined for all times, and applying the same argument to the reversed motion gives $Φ_{t} (A_{E_{1}}) \supseteq A_{E_{1}}$ as well; hence $Φ_{t} (A_{E_{1}}) = A_{E_{1}}$ for every $t \in R$ .

3.1step 1.1step 2.1L1

Recurrence conclusion: $A_{E_{1}}$ is a bounded Borel set of finite measure with closure in the flow domain and is invariant by step 2.1; [L1] therefore gives, for every Borel $E \subseteq A_{E_{1}}$ , that almost every state of $E$ returns to $E$ at infinitely many positive integer times.

4.1step 1.1givenL1algebra∎

Failure of the hypothesis for the flat model: for $U \equiv 0$ , $E_{0} (x, v) = \frac{1}{2} ∥ v ∥_{2}^{2}$ and the sublevel ${E_{0} \leq E_{1}} = R^{3} \times {v : ∥ v ∥_{2} \leq \sqrt{2 E_{1}}}$ is unbounded, indeed it meets every translate of the velocity ball in the position directions; the phase domain $W = R^{6}$ has infinite Lebesgue measure, so [L1]'s boundedness and finite-measure hypotheses fail. For the motion through $(0, e_{1})$ , $x (t) = t e_{1}$ : if a fixed bounded phase set has $∥ x ∥_{2} \leq R$ on it, this trajectory can be in the set only for $0 \leq t \leq R$ . It eventually exits and makes only finitely many integer-time visits; this does not claim that no finite return occurs. The finite-volume hypothesis is a genuine restriction.

Remarks

What the check establishes. The radial quartic model is trapped: every energy sublevel is compact and invariant, so recurrence applies to every positive energy level in the flat $N = 1$ Cartesian presentation for which the theorem is stated. This realizes the hypothesis of Poincare recurrence for the model's Hamiltonian flow on a bounded invariant set of finite phase volume: almost every state of any Borel subset returns to it infinitely often on declared data and shows that the theorem is not vacuous. The conclusion is almost-everywhere in phase volume, gives no return time and says nothing about the flat model beyond the failure of its hypotheses.
Choice assumption. The check inherits the countable-choice assumption of [L1] through the cited theorem; no further choice is used.
Units. The coordinates and measure here are dimensionless. To give the model a physical-unit interpretation one would have to specify compatible length, mass, time and energy scales and restore them in both the potential and phase-volume bound; this example does not make that identification (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework).

A trapped one-label model: the compact energy sublevel of the radial quartic potential is invariant with finite phase volume, so the recurrence theorem applies, while the free model's energy sublevels are unbounded and the hypothesis fails

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources