ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

Number statistics of a single declared mode: sharp, Poisson and geometric preparations

Physical scope

A conditional computation of the count statistics of three declared preparations of one normalisable mode: the sharp count of an n-quanta mode state, the Poisson count law of the mode-coherent preparation, and the geometric count law of a declared effective-mode-energy Gibbs-type preparation. The example is conditional on P1, P2 and the adopted radiation model, declares its mode-energy parameter explicitly, records no measurement, no sampling model and no temperature identification, and asserts no thermalisation.

Example

Adopt the state and composition postulate P1, the observable and probability postulate P2 (State and composition postulate P1: Hilbert spaces, preparations and composite systems, Observable and probability postulate P2: self-adjoint observables, spectral probability and finite unsharp outcomes), the radiation extension postulate (Radiation extension of the framework: transverse mode and photon assignments), the radiation sector definition The radiation sector of the framework: modes and the number, energy and momentum assignments and the declared ideal counting model The declared ideal counting, energy-window and analyser detection models of the radiation sector. Assume the Axioms of Countable Choice, Dependent Choice and Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The Axiom of Choice). Fix a unit mode vector $φ \in h$ with coordinate representatives in $m^{3 / 2}$ under $d^{3} k$ by clause (b) of The radiation sector of the framework: modes and the number, energy and momentum assignments; write $U = U_{φ}$ for the fixed-mode isometry of The fixed-mode isometry of Fock space and the transfer of number and ladder operators and let the dimensionless label $z \in C$ and a declared effective mode energy $E_{0} > 0$ in joules (equivalently a declared effective frequency $ω_{0} = E_{0} / ℏ > 0$ in $s^{- 1}$ ) be given parameters of this example. The example compares the count statistics of the following three declared preparations of the mode subspace, all read with the declared ideal total-number detector:

(a) The $n$ -quanta mode state. For $n \in N$ , the pure preparation of the ray of $U e_{n} = φ^{\otimes n}$ .

(b) The mode-coherent state. The pure preparation of the ray of $U ψ_{z}$ , with dimensionless coherent-state label $z$ and $ψ_{z} = e^{- ∣ z ∣^{2} / 2} \sum_{m} \frac{z^{m}}{\sqrt{m!}} e_{m}$ .

(c) The declared effective-energy mode preparation. For a parameter $β > 0$ in $J^{- 1}$ , the density operator $ρ_{β, E_{0}} : = (1 - q) \sum_{n \in N} q^{n} T_{U e_{n}, U e_{n}}, q : = e^{- β E_{0}} \in (0, 1),$ the transfer to the mode subspace of the single-mode weights of Single-mode thermal trace with its parameter $ω$ set equal to the declared effective energy $E_{0}$ . This is a declared conditional preparation of the model, not a derivation from any radiation-matter interaction and not a statement that the mode is in thermal equilibrium.

The example computes the count law, mean and variance of the three preparations. It compares (b) and (c) at equal positive mean, and includes (a) in that comparison when the common mean is a positive integer and $n$ is chosen equal to it.

Verification

Given: The declared mode data: unit $φ \in h$ , the isometry $U$ , dimensionless label $z \in C$ , energy $E_{0} > 0$ joules, inverse-energy parameter $β > 0$ in $J^{- 1}$ , and the three preparations (a)-(c).

[L1] Mode transfer and number law. $U e_{m} = φ^{\otimes m}$ are orthonormal unit vectors with $N U e_{m} = m U e_{m}$ , the count law of a preparation of $U e_{m}$ is $δ_{m}$ , the count law of the mode-coherent preparation is $e^{- ∣ z ∣^{2}} \frac{∣ z ∣^{2 n}}{n!}$ with mean and variance $∣ z ∣^{2}$ , and $∥ ψ_{z} ∥ = 1$ (Number and energy statistics of a declared mode: number states, coherent states and the continuum thermal limitation clauses (a),(b), The fixed-mode isometry of Fock space and the transfer of number and ladder operators clauses (a),(b), Fixed-mode number law clause (b)).

[L2] Single-mode weights. For the one-mode Fock space with orthonormal family $(e_{n})$ , the weights $w_{n} : = e^{- β ω n}$ satisfy $\sum_{n} w_{n} = (1 - e^{- β ω})^{- 1}$ and $\sum_{n} n w_{n} = e^{- β ω} (1 - e^{- β ω})^{- 2}$ , and $ρ_{β} = G_{β} / Z (β)$ is a density operator whose number expectation is $(e^{β ω} - 1)^{- 1}$ (Single-mode thermal trace clauses (b),(c),(d)).

[L3] Geometric series. For $q \in [0, 1)$ one has $\sum_{n \geq 0} q^{n} = (1 - q)^{- 1}$ ; for nonnegative double series the order of summation may be interchanged (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, Tonelli's theorem for double series of nonnegative extended real numbers).

[L4] States. The rank-one operators $T_{u, u}$ of unit vectors are states, and a trace-norm convergent convex combination of states with weights $(1 - q) q^{n}$ , $\sum_{n} (1 - q) q^{n} = 1$ , is a state (The state space: density operators, pure and mixed states, and purity, Density operators and scalar spectral probability).

[L5] Free-energy multiplier calculus, products and logarithm. The free energy is the self-adjoint direct sum of the sector multipliers $ε_{n} = \sum_{i} ε (k_{i})$ , with the exact multiplication domains (Transverse continuum free Fock Hamiltonian, clauses (a)-(c)). The symmetric transverse sector embeddings and projections are constructed in Total momentum multipliers on transverse symmetric Fock sectors, proof1.1-2.1; scalar multiplier spectral PVMs are inverse-image indicators (Spectral measure of a real L2 multiplication operator, clauses (b),(c)), and the regular spectral representation of a self-adjoint operator is unique (CC spectral calculus on an arbitrary complex Hilbert space by compatible vector-local Cayley subspaces, Statement). Finite product tensor inner products are the Euclidean product integrals (Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b}), Statement). The real logarithm is the inverse of the real exponential, which is strictly increasing with value one at zero (The natural logarithm as the inverse of the exponential function, The exponential function is strictly increasing, Statement).

Proof technique: direct; read the count law off the sector projections for (a) and (b), sum the geometric weights in (c), and compare the resulting means and variances.

Given: The data of the Example and [L1]-[L4].

1.1L1algebra

[Sharp preparation] For the preparation (a) the count law is $p_{m} = δ_{m n}$ by [L1]; its mean is $n$ and its variance $0$ .

1.2L1algebra

[Coherent preparation] For the preparation (b) the count law is Poisson by [L1], with mean and variance $∣ z ∣^{2}$ ; for $z = 0$ it is the sharp law $δ_{0}$ .

1.3L2L4algebra

[Effective-energy preparation is a state] By [L2] the weights satisfy $\sum_{n} q^{n} = (1 - q)^{- 1}$ with $q = e^{- β E_{0}}$ , so $(1 - q) \sum_{n} q^{n} = 1$ and the series defining $ρ_{β, E_{0}}$ converges in trace norm; since each $T_{U e_{n}, U e_{n}}$ is a state, the convex combination is a state by [L4]. Its count law is $p_{n} = tr (ρ_{β, E_{0}} Π_{n}) = (1 - q) q^{n}$ by the declared detector law and the orthogonality of the mode vectors.

1.4L3algebra

[Geometric moments] Put $p_{n} = (1 - q) q^{n}$ with $0 < q < 1$ . By [L3], $\sum_{n \geq 1} n q^{n} = \sum_{k \geq 1} \sum_{n \geq k} q^{n} = \sum_{k \geq 1} \frac{q^{k}}{1 - q} = \frac{q}{(1 - q)^{2}}$ , and likewise $\sum_{n \geq 2} n (n - 1) q^{n} = 2 \sum_{k \geq 2} (k - 1) \frac{q^{k}}{1 - q} = \frac{2 q^{2}}{(1 - q)^{3}}$ . Hence the mean, second moment and variance of the count law are $\sum_{n} n p_{n} = \frac{q}{1 - q} = \frac{1}{e^{β E_{0}} - 1}, \sum_{n} n^{2} p_{n} = \frac{q (1 + q)}{(1 - q)^{2}}, Var = \frac{q}{(1 - q)^{2}} = \frac{e^{β E_{0}}}{(e^{β E_{0}} - 1)^{2}},$ the variance formula from $\sum n^{2} p_{n} = 2 \sum_{n \geq 2} (\binom{n}{2}) q^{n} (1 - q) + \sum n p_{n}$ combined with the two sums above; in particular the variance equals $m (m + 1)$ for the mean $m = (e^{β E_{0}} - 1)^{- 1}$ .

1.5L5algebra

[Sector and Fock bounded Gibbs multipliers] For any $β > 0$ , let $G_{β} = e^{- β H_{f}}$ and $a_{β} = ⟨ e^{- β ε} φ, φ ⟩$ . In the embedding and projection $I_{n}, R_{n}$ of [L5], the indicators $1_{ε_{n}^{- 1} (B)}$ commute with the pointwise transverse projection and all polarization-aware permutations because $ε_{n}$ is scalar and symmetric. They therefore restrict to a regular sector PVM: its scalar measures are the finite-component push-forwards. Its identity-function integral has exactly the maximal sector domain of $T_{n}$ and the same multiplication action, by bounded truncations and the integrable squared tail. Spectral uniqueness in [L5] identifies it with the spectral PVM of $T_{n}$ . Its direct-sum PVM has the identity integral $H_{f}$ on the stated square-sum domain, by sector truncation and spectral truncation; uniqueness identifies the full PVM too. Bounded spectral approximation now gives $G_{β} ∣_{n} = M_{e^{- β ε_{n}}} = M_{\prod_{i} e^{- β ε (k_{i})}}$ , including the vacuum value one.

2.1step 1.1step 1.2step 1.4algebra

[Comparison at equal mean] Choose $z$ with $∣ z ∣^{2} = m : = (e^{β E_{0}} - 1)^{- 1} > 0$ . By steps 1.2 and 1.4, the coherent and effective-energy preparations then have the same mean $m$ and variances $m$ and $m (m + 1) > m$ . A number-state preparation has mean $n \in N$ and variance $0$ by step 1.1, so it shares this positive mean exactly when $m$ is a positive integer and $n = m$ ; in that case all three variances differ. If $m$ is not an integer, no number state has that mean. Every comparison uses the same declared ideal counting model.

2.2step 1.5L1L5algebra

[Compression matrix coefficients] Since $ε (k) > 0$ off the null point zero, $0 < a_{β} < 1$ . The finite-product integral of [L5] gives $⟨ G_{β} U e_{n}, U e_{n} ⟩ = a_{β}^{n}$ , including the vacuum value one, and different sectors have zero matrix coefficients. Because $(e_{n})$ is complete and the compression is bounded, $U^{*} G_{β} U = diag (a_{β}^{n})$ .

3.1step 1.1step 1.2step 1.3step 1.4step 2.1

[Concluding comparison] The computations show: the $n$ -quanta mode state has the sharp count $n$ ; the mode-coherent state has the Poisson count law with mean and variance $∣ z ∣^{2}$ ; and the declared effective-energy preparation with parameter $E_{0} > 0$ has the geometric law with mean $1 / (e^{β E_{0}} - 1)$ and variance $m (m + 1)$ . The parameter $E_{0}$ is declared; it is not derived from $φ$ , because no normalisable mode vector has sharp energy. No measurement, sampling model or temperature identification occurs, and the comparison is a comparison of the declared conditional models, which is the announced computation.

4.1step 2.2L2L3L5algebra∎

[Normalization and effective scale] By [L2] and [L3], it is positive trace class with trace $(1 - a_{β})^{- 1}$ and normalized geometric weights $(1 - a_{β}) a_{β}^{n}$ . Put $ε_{e f f} (β) = - β^{- 1} \log a_{β}$ ; [L5] gives $ε_{e f f} (β) > 0$ and $e^{- β ε_{e f f} (β)} = a_{β}$ . This proves the fixed- $β$ compression formula, without identifying the independently declared $E_{0}$ with this generally $β$ -dependent value or claiming an invariant mode or a full continuum Gibbs state.

Remarks

Independent effective-energy assignment and Gibbs compression. The example independently declares $E_{0}$ ; a normalisable mode is not an eigenmode of the free energy, so the free Hamiltonian does not restrict to $E_{0} N^{'}$ on this mode subspace. Nevertheless a compression of its bounded Gibbs operator is possible. Put $a_{β} : = ⟨ e^{- β ε} φ, φ ⟩$ . Since $0 < e^{- β ε (k)} < 1$ off the null set ${k = 0}$ and $∥ φ ∥ = 1$ , $0 < a_{β} < 1$ . The sector multiplier representation of Transverse continuum free Fock Hamiltonian gives $e^{- β T_{n}} = M_{\prod_{i} e^{- β ε (k_{i})}}$ on the symmetric transverse sector. Its pairing on $φ^{\otimes n}$ is $a_{β}^{n}$ by the finite-product inner-product integral of Euclidean L² product unitary: L²(R^a)⊗̂L²(R^b) ≅ L²(R^{a+b}), and different sectors have zero cross pairing. Hence $U^{*} e^{- β H_{f}} U$ is the diagonal operator with entries $a_{β}^{n}$ ; its trace is $(1 - a_{β})^{- 1}$ and its normalization gives the geometric weights $(1 - a_{β}) a_{β}^{n}$ . At each fixed $β$ these correspond to the effective scale $ε_{e f f} (β) = - β^{- 1} \log a_{β} > 0$ , with the real logarithm of The natural logarithm as the inverse of the exponential function; positivity follows because the exponential is strictly increasing with $\exp (0) = 1$ (The exponential function is strictly increasing). The scale is generally dependent on $β$ . This is compression and normalization of a positive operator, not a normalized Gibbs state of the full continuum or an invariant free-energy mode. The full Gibbs operator remains non-trace-class by clause (e) of Number and energy statistics of a declared mode: number states, coherent states and the continuum thermal limitation; no thermalisation or temperature identification follows.
Counts are model quanta. All three laws are laws of the declared ideal total-number detector; a laboratory photon-counting comparison would require a declared counter response, efficiency and sampling model, and reported data. None is supplied or assumed here.

Number statistics of a single declared mode: sharp, Poisson and geometric preparations

Example

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources