ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Grand condensate variance remains macroscopic

Physical scope

The grand-ensemble ground-mode variance and tail at a fixed positive excess density above the ideal critical density, as a direct instance of the linked theorem. It makes no canonical or interacting-gas claim.

Example

In the three-dimensional ideal Bose grand ensemble at fixed density $ρ > ρ_{c}$ , put $ρ_{0} = ρ - ρ_{c} > 0$ . The ground-mode mean is asymptotic to $ρ_{0} V$ , but ${Var}_{L} (N_{0} / V) \to ρ_{0}^{2}$ , and for every $x > 0$ in m $^{- 3}$ its density tail satisfies $P_{L} (N_{0} / V \geq x) \to e^{- x / ρ_{0}}$ . Thus the condensate density does not concentrate at its mean limit in this grand ensemble.

Verification

Given: ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), $V = L^{3}$ in m $^{3}$ , $ρ_{0} > 0$ in m $^{- 3}$ , $x > 0$ in m $^{- 3}$ , and the grand geometric ground-mode law in Dimension-restricted fixed-mean-density Bose condensation.

[F1] Dimension-restricted fixed-mean-density Bose condensation, Statement: $E_{L} N_{0} / V \to ρ_{0}$ , ${Var}_{L} (N_{0} / V) \to ρ_{0}^{2}$ , and $P_{L} (N_{0} / V \geq x) \to e^{- x / ρ_{0}}$ .

1.1givenF1algebra

The linked theorem gives $E_{L} N_{0} = ρ_{0} V + o (V)$ . Substitution into the geometric variance ${\overset{ˉ}{n}}_{0, L} (1 + {\overset{ˉ}{n}}_{0, L})$ and division by $V^{2}$ gives limit $ρ_{0}^{2}$ .

2.1givenF1algebra∎

At $x = 2 ρ_{0}$ , $P_{L} (N_{0} / V \geq 2 ρ_{0}) \to e^{- 2} > 0$ . Every such event differs from the limiting mean density $ρ_{0}$ by at least $ρ_{0}$ , so convergence in probability to $ρ_{0}$ is impossible. This conclusion is specific to the grand preparation; a fixed-number state has $N_{0}$ constrained by total number.

Depends on

Dependency tree · 2 levels

Sources

David Tong, Statistical Physics, §3.5.3, Bose condensation and grand-canonical fluctuations