Physics theoremStatement: Literature-sourcedProof: 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.

Exact Tonks hard-rod pressure and convergent virial series

Physical scope

Finite-N one-dimensional classical hard rods of common length a>=0 with L>Na and quadratic momenta; the Euclidean Lebesgue product and Jordan-volume calculations assume ACω; exact thermodynamic and virial statements only for this Tonks model, not an all-fluid cluster expansion.

Statement

Assume ${A C}_{ω}$ as defined in The Axiom of Countable Choice ( ${A C}_{ω}$ ) for the Euclidean Lebesgue product and Jordan-volume identifications below. Use the natural logarithm $\log$ of The natural logarithm as the inverse of the exponential function. Let $N \geq 1$ , let $a \geq 0$ be a hard-rod length in metres, and let $L > N a$ be the one-dimensional box length in metres. Rod centers are $x_{i} \in [a / 2, L - a / 2]$ with $∣ x_{i} - x_{j} ∣ \geq a$ for $i \neq j$ . Let each rod have mass $m > 0$ kg, momentum $p_{i} \in R$ in kg m s $^{- 1}$ , and Hamiltonian $H = \sum_{i = 1}^{N} p_{i}^{2} / (2 m)$ on the allowed configuration set, with infinite energy outside it. Adopt the reference $d x d p / (N! h_{0}^{N})$ , where $h_{0} > 0$ is a fixed action in J s, and canonical inverse temperature $β > 0$ in J $^{- 1}$ . Put $λ = h_{0} \sqrt{β / (2 π m)}$ . Then $Z_{N} = \frac{(L - N a)^{N}}{N! λ^{N}}, U = E H = \frac{N}{2 β}, p_{1 D} : = - {(\frac{\partial F}{\partial L})}_{N, a, m, β, h_{0}} = \frac{N}{β (L - N a)}, F = - β^{- 1} \log Z_{N} .$ Here $p_{1 D}$ is the one-dimensional force conjugate to length and has units N; it is not a three-dimensional pressure. With number density $ρ = N / L$ , the exact equation is $β p_{1 D} = \frac{ρ}{1 - a ρ} = \sum_{j = 1}^{\infty} a^{j - 1} ρ^{j}, a ρ < 1.$ After the first $M \geq 1$ terms, the exact nonnegative remainder (strictly positive when $a > 0$ ) is $ρ (a ρ)^{M} / (1 - a ρ)$ , bounded by $ρ r^{M} / (1 - r)$ whenever $a ρ \leq r < 1$ . At fixed $ρ > 0$ with $a ρ < 1$ , as $N, L \to \infty$ with $N / L = ρ$ , $\lim \frac{β F}{N} = \log ⁣ (\frac{ρ λ}{1 - a ρ}) - 1,$ with finite-size excess between $0$ and $(1 + \log N) / N$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , $N \geq 1$ , $a \geq 0$ , $L > N a$ , $m > 0$ , $β > 0$ , and the hard-core position set and Hamiltonian in the Statement.

[F1]

Declared example preparations and thermodynamic interpretation: for each specified model with finite positive partition function, the canonical density is $Z^{- 1} e^{- β H}$ relative to its fixed reference, and $F = - β^{- 1} \log Z$ is the adopted free-energy definition.

[F2]

Gaussian, gamma and beta product integrals: for $m, β > 0$ , $\int_{R} e^{- β p^{2} / (2 m)} d p = \sqrt{2 π m / β}$ and the normalized Gaussian has second moment $m / β$ ; the positive gamma integral is finite.

[F3]

Change of variables for an injective $C^{1}$ map on a compact Jordan set: an injective $C^{1}$ map with nonzero Jacobian on an open neighborhood of a compact Jordan set obeys the compact Jordan change-of-variables formula.

[F4]

The natural logarithm as the inverse of the exponential function defines $\log$ on positive reals; Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm makes it continuous and increasing with the product and quotient laws, and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t gives $\log^{'} (x) = 1 / x$ and $\log x = \int_{1}^{x} d t / t$ . Finite iteration of the product law gives the integer-power identity.

[F5]

Under ${A C}_{ω}$ , Euclidean Lebesgue measure is the product of its coordinate factors, boxes have the product of their side lengths as measure, and bounded Jordan sets are Lebesgue measurable with measure equal to their Jordan content (On Borel subsets of R^{m+n}, the product lambda_m times lambda_n agrees with lambda_{m+n}, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, Lebesgue outer measure is at most Jordan outer content, and a bounded Jordan measurable set is Lebesgue measurable with Lebesgue measure equal to its Jordan content).

[F6]

Tonelli factors nonnegative product integrals and Fubini factors absolutely integrable signed product integrals on sigma-finite measure spaces (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product, Fubini's theorem for L^1 functions on a sigma-finite product).

[F7]

A bounded set is Jordan measurable when its boundary has content zero, and, for $m \geq 1$ , a continuous graph over a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero, The graph of a continuous function on a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ ).

[F8]

The Gaussian moments in [F2] are improper Riemann integrals; on bounded intervals they agree with Lebesgue integrals under ${A C}_{ω}$ , and monotone convergence passes nonnegative truncations to the full line (Riemann–Lebesgue comparison for distribution test integrands, Monotone convergence for the integral).

[F9]

A closed bounded subset of $R^{N}$ is compact, in particular each closed box and the ordered simplex below (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[A1]

The finite hard-core configuration rule and indistinguishable-classical-particle reference convention are the adopted Tonks model assumptions; no interaction beyond hard exclusion is included.

Proof

1.1givenF2F5F6F8algebra

The single-rod momentum Lebesgue integral is $\int_{R} e^{- β p^{2} / (2 m)} d p = \sqrt{2 π m / β}$ by [F2] and [F8]. By [F5] and Tonelli [F6], the $N$ momentum factors integrate to the product of these integrals. Dividing by $h_{0}^{N}$ gives $λ^{- N}$ .

1.2givenF2F8algebra

By [F2] and the bounded Riemann-to-Lebesgue agreement in [F8], each normalized scalar momentum Gaussian has second moment $m / β$ . Thus the mean kinetic energy of each rod is $1 / (2 β)$ and the total mean is $U = N / (2 β)$ .

1.3givenA1F3F5F7F9algebra

Put $ℓ = L - N a > 0$ . For $N = 1$ , the allowed position set is $[a / 2, L - a / 2]$ , whose Lebesgue measure is $L - a = ℓ$ directly by the box formula [F5]; no graph theorem is needed. For $N \geq 2$ , the allowed labelled position set is a finite union of closed bounded ordering polytopes in $[a / 2, L - a / 2]^{N}$ , hence compact by [F9]. Its boundary is contained in finitely many box faces and contact hyperplanes $x_{i} - x_{j} = \pm a$ , each contained in a graph of an affine function over a sufficiently large closed nondegenerate $(N - 1)$ -dimensional coordinate rectangle, so [F7] makes it Jordan measurable. Fix one label ordering $π$ and sort its centers as $x_{π (1)} \leq \dots \leq x_{π (N)}$ . On that sector set $y_{i} = x_{π (i)} - a / 2 - (i - 1) a$ ; the hard-core inequalities become the closed bounded, hence compact, ordered simplex $S_{ℓ} : = {0 \leq y_{1} \leq \dots \leq y_{N} \leq ℓ}$ by [F9]. Its boundary is contained in the box faces and finitely many tie hyperplanes, each contained in such an affine graph over a nondegenerate $(N - 1)$ -dimensional rectangle; [F7] therefore makes $S_{ℓ}$ Jordan measurable. The affine permutation map has absolute determinant $1$ , so [F3] preserves Jordan volume. The $N!$ coordinate permutations of $S_{ℓ}$ partition $[0, ℓ]^{N}$ up to the tie hyperplanes, which have content zero by [F7]; their equal volumes sum to $ℓ^{N}$ , hence each simplex has volume $ℓ^{N} / N!$ . The $N!$ labelled order sectors cover the allowed set and overlap only on the stated content-zero contact hyperplanes. Therefore its Jordan content is $ℓ^{N}$ , and [F5] gives the full labelled position Lebesgue measure $ℓ^{N}$ .

2.1F1F5F6step 1.1step 1.3algebra

The reference measure divides the position-momentum integral by $N! h_{0}^{N}$ . Product Lebesgue measure and Tonelli [F5, F6] separate the position measure $ℓ^{N}$ from step 1.3 and the momentum integral from step 1.1. Thus $Z_{N} = ℓ^{N} / (N! λ^{N})$ .

3.1F1F4step 2.1algebra

By the product, quotient and integer-power laws in [F4], $F = - β^{- 1} [N \log ((L - N a) / λ) - \log N!]$ , using the logarithm derivative in [F4] at fixed $N, a, β$ gives $p_{1 D} = N / [β (L - N a)]$ . Substituting $ρ = N / L$ yields $β p_{1 D} = ρ / (1 - a ρ)$ .

4.1step 3.1algebra

At $a = 0$ , the virial series has first term $ρ$ and all higher terms zero, so its remainder after any $M \geq 1$ terms is zero. For $0 \leq a ρ < 1$ , the finite geometric identity $\sum_{j = 1}^{M} (a ρ)^{j - 1} = (1 - (a ρ)^{M}) / (1 - a ρ)$ gives the stated virial partial sum and exact remainder after multiplication by $ρ$ . If $a ρ \leq r < 1$ , then $(a ρ)^{M} / (1 - a ρ) \leq r^{M} / (1 - r)$ , proving the uniform bound.

5.1F4step 2.1algebra∎

At fixed $ρ > 0$ , $L - N a = N (1 / ρ - a) > 0$ , so the laws in [F4] give $\frac{β F}{N} = - \log ((L - N a) / λ) + \frac{\log N!}{N} .$ For each integer $k = 1, \dots, N - 1$ , monotonicity of $\log$ bounds its integral on $[k, k + 1]$ between $\log k$ and $\log (k + 1)$ . Summing gives $\int_{1}^{N} \log x d x \leq \log N! \leq \int_{1}^{N} \log x d x + \log N .$ For $N = 1$ the sums and integral are empty and zero. Since [F4] gives $(x \log x - x)^{'} = \log x$ , the integral is $N \log N - N + 1$ . Hence $\log N! = N \log N - N + ϵ_{N}$ with $1 \leq ϵ_{N} \leq 1 + \log N$ . Substitution and [F4] cancel $\log N$ , yielding $\frac{β F}{N} = \log ⁣ (\frac{ρ λ}{1 - a ρ}) - 1 + \frac{ϵ_{N}}{N} .$ The excess is nonnegative and at most $(1 + \log N) / N$ . Finally, $\log N = \int_{1}^{N} d x / x \leq \int_{1}^{N} d x / \sqrt{x} = 2 (\sqrt{N} - 1)$ , so that upper bound tends to zero and proves the stated thermodynamic limit.

Remarks

The infinite virial series is the geometric expansion of this exact one-dimensional hard-rod equation of state. It is not a formal or convergent cluster expansion for arbitrary fluids, attractions, dimensions, or interactions.

Exact Tonks hard-rod pressure and convergent virial series

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources