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.
Analytic potentials on a finite phase torus
Definition
Let be a nonempty finite set and with its angular charts and flat metric. A real-valued function on is real analytic if, in an angular chart around each point, it equals a real power series in the angular coordinates that converges absolutely on some open polydisc about that point. A potential here means a real-valued function on .
For a smooth potential, a critical point is a point at which all first angular partial derivatives vanish. At a critical point its Hessian is the bilinear form represented in angular coordinates by the matrix of second partial derivatives. The angular transition maps are locally translations, so this matrix is unchanged between angular charts.
Every finite real linear combination of the functions , , is a real analytic potential. The expression uses any real representatives of the phases.
Definition references
Facts & Assumptions
Angular charts cover and their transition maps are locally translations by elements of ; the flat metric is Euclidean in these charts (Finite phase tori, local lifts and the flat metric).
For real , , , and cosine is -periodic (Phasors, trigonometric identities and periodic derivatives).
The complex exponential has the absolutely convergent series for every complex , and (The complex exponential by its power series, exp(z+w)=exp z exp w, and the complex exponential extends the real exponential).
A real analytic germ is represented locally by an absolutely convergent real multivariable power series; the intrinsic critical Hessian is the bilinear form represented by the second partial derivatives in a smooth chart (Real analytic germs in several variables, The intrinsic Hessian of a smooth function at a critical point).
For and , , where is the binomial coefficient viewed in (The binomial theorem in ℝ: (x+y)ⁿ = ∑_k<n+1 iotaC(n, k) xᵏ y^ n-k).
Justification
Given: A finite nonempty , a smooth real potential when discussing its critical points, and finitely many real coefficients and ordered pairs of vertices for the cosine combination.
Goal: Verify that the definitions are independent of angular choices and that the stated cosine combination is real analytic.
1.1 By [F1], on a sufficiently small connected neighborhood of an overlap the two angular coordinate systems differ by a constant lattice vector. Substituting this translation into a convergent power series only changes its center, so the local analytic condition is independent of the angular chart. The first and second partial derivatives are unchanged under such a translation. Thus the condition that all first derivatives vanish is independent of the angular chart, and at a critical point the displayed matrix represents the intrinsic Hessian from [F4]. Periodicity in [F2] makes each cosine of a phase difference independent of the chosen representatives. [F1, F2, F4, algebra]
2.1 Fix a chart point with coordinates and write nearby coordinates as . For distinct , [F2] and [F3] give . Expanding each finite power by [F5] gives a real power series in after taking real parts. In degree , the sum of absolute monomial factors is by [F5]; taking real parts after multiplication by the unit-modulus factor cannot increase this bound by [F2]. The sum of the absolute values of all its terms is bounded by , which converges by [F3]. Thus it is an absolutely convergent multivariable power series on every bounded polydisc; its coefficients in the other coordinates are zero. If , the term is the constant . A finite real linear combination remains such a series on a common polydisc, proving the assertion by [F4]. [F2, F3, F4, F5, algebra] ∎
Depends on
- Finite phase tori, local lifts and the flat metric
- Phasors, trigonometric identities and periodic derivatives
- Real analytic germs in several variables
- The intrinsic Hessian of a smooth function at a critical point
- The complex exponential by its power series
- exp(z+w)=exp z exp w, and the complex exponential extends the real exponential
- The binomial theorem in ℝ: (x+y)ⁿ = ∑_k<n+1 iotaC(n, k) xᵏ y^ n-k
Used by · 5
Dependency tree · 2 levels
Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.