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.

The unit cylinder shift: explicit local generating function, loop integral and global failure

Example

Take the cylinder $C = (R / Z) \times R$ with the shift $Φ (θ, I) = (θ, I + 1)$ , i.e. $a = 1$ in The symplectic shift of the cylinder changes $λ$ by the closed, non-exact form $a d θ$ and has no global generating function, and with the descended forms $λ_{C}, ω_{C}$ of that proposition. Then:

$Φ^{*} λ_{C} = λ_{C} + d θ_{C}$ and $Φ^{*} ω_{C} = ω_{C}$ ;
the loop $γ (t) = π (t, 0)$ , $t \in [0, 1]$ , satisfies $\int_{0}^{1} d θ_{C} (γ^{'} (t)) d t = 1 \neq 0$ , confirming that $d θ_{C}$ is not exact on $C$ ;
on the chart ${θ \in (0, 1)}$ the second-kind generating function $S (θ, P) = θ P - θ$ generates the shift; globally no such $C^{1}$ function exists.

Facts & Assumptions

Given: The cylinder $C$ , the shift $Φ$ , the descended forms and the loop $γ$ .

[F1]

The proposition The symplectic shift of the cylinder changes $λ$ by the closed, non-exact form $a d θ$ and has no global generating function establishes clauses 1 and 2 in general form for $a \neq 0$ ; for $a = 1$ the identities read $Φ^{*} λ_{C} - λ_{C} = d θ_{C}$ and $\int_{0}^{1} d θ_{C} (γ^{'} (t)) d t = 1$ . [F1]

[F2]

The second-kind relations and the local chart (Generating functions of the first and second kind for a local canonical map): for $θ$ in an open interval of length one, $S (θ, P) = θ P - θ$ satisfies $S_{θ} = P - 1$ , $S_{P} = θ$ and $S_{θ P} = 1$ , so it generates the map that sends $(θ, I)$ with $I = P - 1$ to $(Q, P) = (θ, I + 1)$ ; on the chart $S$ is a $C^{\infty}$ function.

Verification

technique · direct; specialise the general identities to $a=1$, compute the loop integral, and check the generating relations on a chart

1.1F1

Clause 1 is [F1] specialised to $a = 1$ : $Φ^{*} λ_{C} = λ_{C} + d θ_{C}$ and $Φ^{*} ω_{C} = ω_{C}$ ; clause 2 is the same proposition's non-exactness statement, whose proof integrates $d θ_{C}$ along $γ$ to $1$ .

2.1F1F2algebra∎

Clause 3: on the chart $θ \in (0, 1)$ the derivatives of [F2] satisfy the second-kind relations $p = S_{θ} = P - 1$ and $Q = S_{P} = θ$ with $S_{θ P} = 1 \neq 0$ ; the generated map is $(θ, I) \mapsto (θ, I + 1)$ , which is the shift, so $S$ generates $Φ$ on the chart. Globally, The symplectic shift of the cylinder changes $λ$ by the closed, non-exact form $a d θ$ and has no global generating function clause 3 (with $a = 1$ ) excludes any global $C^{1}$ generating function: a $1$ -periodic lift $\hat{S}$ would satisfy ${\hat{S}}_{P} = θ + m$ for a constant integer $m$ and ${\hat{S}}_{θ} = P - 1$ , hence $\hat{S} (θ, P) = θ P + m P + c (θ)$ with $c^{'} = - 1$ , so $c (1) - c (0) = - 1 \neq 0$ by the fundamental theorem of calculus, contradicting the periodicity $c (1) = c (0)$ .

The unit cylinder shift: explicit local generating function, loop integral and global failure

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources