Suppose the symmetric partial sums converge at a fixed point. Group positive and negative frequencies together, let $S_n$ be the resulting partial sums and set $w(x)=(\sin x/x{)}^2$, with $w(0)=1$. Summation by parts expresses the weighted sum as ${\sum }_{n\ge 0}{S}_n[w(nk)-w((n+1)k)]$, where $k=|h|/2$. The total variation of these weights is at most ${\int }_0^{\infty }|w^{\prime }(x)|dx<\infty$, independently of $k$, and each fixed difference tends to zero. Subtract the limiting value of $S_n$ and split into a finite prefix and a uniformly small tail to prove convergence to that value. This is a regular summation method even though the sinc-squared weights need not decrease monotonically.

If the symmetric partial sums of ${\sum }_{r\in \mathbb{Z}}{a}_r{e}^{irt}$ tend to zero at every point outside a finite set, then all coefficients vanish. Almost-everywhere convergence first gives $a_{\pm n}\to 0$. The twice-integrated series $F(t)=a_0{t}^2/2-{\sum }_{r\ne 0}{a}_r{e}^{irt}/r^2$ is continuous. Riemann summation of a convergent trigonometric series makes its symmetric second derivative zero away from the exceptional points, so it is affine on each intervening interval. Sinc-squared summation of a sequence tending to zero makes its symmetric first-order quotient zero everywhere, removing all possible affine corners. The globally affine function differs from a periodic function by $a_0{t}^2/2$, forcing $a_0=0$; periodicity then makes it constant, and integration against each nonzero frequency gives $a_r=0$.

The complex exponential functions $e^{int}$, for integers $n$, are orthogonal under the normalized integral inner product over a complete period. If $n=m$, the integrand $e^{i(n-m)t}$ is one; otherwise its antiderivative has equal endpoint values, giving zero. For the real modes, ${\int }_{-\pi }^{\pi }{\cos }^2(nt)dt={\int }_{-\pi }^{\pi }{\sin }^2(nt)dt=\pi$ for $n\ge 1$, while every mixed sine-cosine integral and every unequal-frequency pairing vanishes.

This makes the coefficient formulas useful: multiply a trigonometric polynomial by one mode and integrate, and all other modes cancel. For $f(x)=1/2+\cos x+\frac{1}{2}\sin (2x)$, integration against $\cos x$ gives $\pi$, and against $\sin (2x)$ gives $\pi /2$, recovering $a_1=1$ and $b_2=1/2$. Division by the squared norm of the mode supplies the normalization. A full period matters; truncating the integration interval generally destroys these cancellations.

For real noninteger $\lambda$, the periodic extension from $[-\pi ,\pi ]$ has the displayed Fourier series, obtained by the product-to-sum identity in the sine coefficient integral. It equals the original function in the open interval and zero at the periodic endpoint jumps. At $\lambda =1/2$, Parseval's identity gives ${\sum }_{n\ge 1}{n}^2/(4n^2-1{)}^2={\pi }^2/64$. Integer frequencies instead already belong to the ordinary sine basis and should not be substituted into the removable coefficient singularities without taking limits.

The Gibbs phenomenon is the persistent overshoot near a jump discontinuity in ordinary truncated Fourier series. For this square wave, retain $M$ nonzero odd modes:As $M$ grows, the first peak approaches the jump while its height tends to approximately $1.17897974$. This is an excess of about $0.17898$ above the upper level $1$, or $8.949\%$ of the jump size $2$. The narrower region does not imply a vanishing maximum error. At the jump itself every $Q_M(0)=0$. These observations are compatible with pointwise convergence and $L^2$ convergence but exclude uniform convergence to the discontinuous square wave. ^[ref].

For this particular sum, its derivative is $Q_M^{\prime }(x)=(2/\pi )\sin (2Mx)/\sin x$ away from multiples of $\pi$, so the first positive peak is exactly at $x=\pi /(2M)$. There,This is a midpoint Riemann sum tending to $2\mathrm{Si}(\pi )/\pi$, where $\mathrm{Si}$ is the sine integral. It gives a short explanation of the nonzero limiting excess.

The phenomenon matters whenever a sharp boundary is represented by a limited set of Fourier harmonics: a visible ripple can be a property of the approximation rather than an oscillation in the original profile. Josiah Willard Gibbs reported the phenomenon in his 1899 letter “Fourier's Series” in Nature, volume 59, page 606. This is a documented historical report, without a claim of first discovery. ^[ref].

A square wave alternates between two constant levels for equal halves of a period. Choose a $2\pi$-periodic function equal to $1$ on $(0,\pi )$ and $-1$ on $(-\pi ,0)$, with value zero at the jumps. Its odd function symmetry makes the mean and every cosine Fourier coefficient vanish. Directly integrating the two constant pieces givesThus only odd sine Fourier harmonics occur, with amplitudes decreasing like the reciprocal of their frequency multiplier. Every finite Fourier partial sum is smooth, yet their pointwise limit has jumps. At those jumps the Fourier series converges to zero, the midpoint of the two levels, regardless of which value we assign to the original function there.

This example explains how smooth components can encode sharp transitions. Increasing the number of Fourier harmonics narrows the transition region, but also produces the persistent overshoot described by the Gibbs phenomenon. The illustrated square wave and coefficient calculation are mathematical constructions, not measurements of a physical device.

A frequency spectrum describes the frequency components of a function. A Fourier series supplies discrete Fourier coefficients; the Fourier transform of an integrable function supplies a continuous, generally complex-valued description. An amplitude plot shows magnitudes and omits wave phases, so it need not determine the original function. In the example with three Fourier harmonics above, the one-sided amplitude plot has heights $1$, $1/2$, and $1/4$. The corresponding complex Fourier coefficients at positive and negative frequencies each have half those heights: $\cos (2\pi \nu t)=(e^{2\pi i\nu t}+e^{-2\pi i\nu t})/2$.

The spacetime coordinates of an event combine into a four-vector $X^a=(ct,x,y,z)$ under Lorentz transformations between inertial frames sharing an origin. For a massive particle, differentiation with respect to proper time gives its four-velocity. Under a spacetime translation, positions acquire an additive offset, while displacement four-vectors transform linearly under the Lorentz part.

The four-force is the proper time derivative of four-momentum. For constant rest mass and coordinate three-force $\mathbf{F}=d\mathbf{p}/dt$, its components are $K^{\mu }=\gamma (\mathbf{F}\cdot \mathbf{v}/c,\mathbf{F})$ in the convention $p^{\mu }=(E/c,\mathbf{p})$. Thus it packages the power transfer and three-force into one Lorentz-covariant vector.

For a particle of rest mass $m$,

An observer with future-directed unit velocity $u^{\mu }$ measures particle energy $E=-u_{\mu }{p}^{\mu }$ and spatial physical momentum given by the orthogonal projection of its four-momentum in the displayed formula. With signature $(-+++)$ and $p_{\mu }{p}^{\mu }=-m^2$, its squared magnitude is $p_{\perp \mu }{p}_{\perp }^{\mu }=E^2-m^2$. Components in the observer's orthonormal spatial frame agree with $\gamma m\mathbf{v}$. They differ in general from coordinate canonical momentum components. For a comoving observer in flat FRW, a conserved conventional spatial comoving covector has locally measured magnitude divided by the scale factor.

The supercurrent is the spinor-valued Noether current of rigid supersymmetry. Its spatial integral is a supercharge. Localizing the supersymmetry parameter produces ${\partial }_{\mu }\overline{ϵ}{S}^{\mu }$ in the variation of the action; a gravitino coupling cancels this term and starts the Noether gauging procedure.

The Super-Poincaré group combines Lorentz transformations and supertranslations. Its even part acts by spin-group transformations and ordinary spacetime translations; odd parameters generate the supercharges. Their graded commutator closes on translations through the Super-Poincaré algebra. A superspace tensor built from invariant coframes and Lorentz-invariant contractions is invariant under the full group.

A deterministic interpretation with a definite particle configuration guided by the wavefunction. The latter obeys the Time-dependent Schrödinger equation, while the particle follows the guidance equation. A Born rule distribution of initial positions is preserved by quantum equilibrium equivariance. The guidance law restricts admissible initial velocities, even when trajectories are rewritten as a second-order force equation.

A superselection rule partitions a representation into sectors between which the specified observable algebra has no matrix elements. Relative phases between vectors in different sectors cannot be detected by those observables, so a coherent vector spanning sectors and its sector-diagonal mixture define the same observable state. The restriction is relative to the observable algebra; it is not by itself a physical wave-function collapse. Infinite-system phases can yield disjoint representations and emergent superselection sectors even though each finite system permits global connecting operators.

The EPR argument uses correlations of an entangled state and a locality assumption to challenge the completeness of the quantum description. Its Einstein–Podolsky–Rosen criterion of reality identifies quantities predictable with certainty without disturbing a distant system as elements of physical reality.

Conformance of compiled machine code to the behaviour of the code model used to justify it. Binary correctness can extend formal verification across the compilation step; the result applies to the particular compiled artifact and its assumptions.

A mathematically precise description of permitted behaviour. A formal specification for the microkernel file-read example's service could relate an authorized request to the exact returned bytes; a formal specification of its microkernel's IPC need only describe the protected transport operation. They state different obligations.

For the summation loop verification, require a nonnegative integer input $n$ and a returned value $s$ satisfying $2s=n(n+1)$. The formal specification describes what answer is acceptable without requiring this particular loop: another implementation may satisfy the same contract. State separately whether partial correctness or total correctness is required. A Hoare triple packages the precondition, the program and the postcondition; Hoare logic supplies rules for establishing such claims.

Precision alone does not ensure a useful requirement. The postcondition $s\ge 0$ permits returning zero for every nonnegative integer input; it does not specify the intended triangular number. Conversely, an impossible precondition permits no starts, making a universal correctness claim vacuous. Check both that intended inputs are admitted and that admitted outputs express the intended task.

An abstract family of languages is a family of formal languages containing a nonempty language and closed under finite union, concatenation of formal languages, positive closure of a formal language, nonerasing monoid homomorphisms between free word monoids, inverse homomorphisms, and intersection with regular languages. Here positive closure means $L^{+}={\bigcup }_{n\ge 1}{L}^n$, and nonerasing means that the homomorphism maps every alphabet letter to a nonempty word.

A full abstract family of languages allows arbitrary word homomorphisms, including ones that erase letters. This distinction matters: erasing an unbounded amount of a computation or derivation can change the resources needed to recognize the image language. The regular languages and context-free languages are full abstract families. In particular, the closure axioms say that if $L$ is context-free and $R$ is regular, then $L\cap R$ is context-free; they do not assert closure under intersection of two arbitrary context-free languages. The framework collects the common constructions without identifying the different language classes.^[ref]

In a formal grammar, terminal symbols are symbols of completed words; a nonterminal symbol is an auxiliary symbol that may be replaced by a production. The two alphabets are disjoint.