ExampleConstruction: AI-adaptedVerification: 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.

Position-bin probabilities of a Gaussian packet

Physical scope

A finite model computation of position-bin probabilities in the spinless massive-particle model: for a normalized Gaussian packet in the first coordinate and an arbitrary normalized transverse factor, the probability that the first position coordinate lies in a Borel bin is the Gaussian integral over that bin, and the probability of an exact value is zero while every bin of positive length gets positive probability with the stated elementary bounds. The item is conditional on the model's postulates, uses no measured data and asserts no apparatus behaviour.

Example

Work in the spinless massive-particle model of P5, that is $H = L^{2} (R^{3}; C)$ with position operators $Q_{j}$ (Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators, Position and momentum operators on Euclidean L2), fix a width $σ > 0$ in metres, and let $ψ_{σ} (t) : = (2 π σ^{2})^{- 1 / 4} e^{- t^{2} / (4 σ^{2})} (t \in R),$ the Gaussian packet of width $σ$ . Let $φ \in L^{2} (R^{2}; C)$ satisfy $\int_{R^{2}} ∣ φ ∣^{2} = 1$ and put $ψ (x) : = ψ_{σ} (x_{1}) φ (x_{2}, x_{3}) (x \in R^{3}),$ so that $ψ \in H$ is a unit vector and the preparation $[ψ]$ is a state of the model. Then:

(i) The probability that the first coordinate $Q_{1}$ lies in a Borel set $B \subseteq R$ is $μ_{ψ}^{Q_{1}} (B) = \int_{B} ∣ ψ_{σ} (t) ∣^{2} d t = \frac{1}{\sqrt{2 π σ^{2}}} \int_{B} e^{- t^{2} / (2 σ^{2})} d t,$ independently of the transverse factor $φ$ ; the law has density $∣ ψ_{σ} ∣^{2}$ and $μ_{ψ}^{Q_{1}} (R) = 1$ .

(ii) For every $λ \in R$ the probability of the exact value $λ$ is zero, $μ_{ψ}^{Q_{1}} ({λ}) = 0$ , while for every $a < b$ the bin $(a, b]$ has positive probability with the explicit bounds $\frac{b - a}{\sqrt{2 π σ^{2}}} \exp (- \frac{\max {∣ a ∣, ∣ b ∣}^{2}}{2 σ^{2}}) \leq μ_{ψ}^{Q_{1}} ((a, b]) \leq \frac{b - a}{\sqrt{2 π σ^{2}}} .$ In particular these bounds hold when $0 \leq a < b$ . In the symmetric case $a = - δ$ , $b = δ$ with $δ > 0$ , the probability satisfies $\sqrt{\frac{2}{π e}} \leq μ_{ψ}^{Q_{1}} ((- σ, σ]) \leq \sqrt{\frac{2}{π}}, 0 < μ_{ψ}^{Q_{1}} ((- δ, δ]) \leq \frac{2 δ}{\sqrt{2 π σ^{2}}} .$ In particular a single recorded event localized in a bin of positive length is possible in the model, while an event at an exact coordinate value has probability zero.

(iii) For each $j \in {1, 2, 3}$ the same formulas hold for $Q_{j}$ in the unit product preparation $ψ^{(j)} (x) : = ψ_{σ} (x_{j}) φ (x_{⊥})$ , where $x_{⊥}$ lists the other two coordinates in increasing index order. For the original preparation $ψ = ψ^{(1)}$ , the laws of $Q_{2}$ and $Q_{3}$ are the marginals of $∣ φ ∣^{2}$ and need not be Gaussian. The width and bin endpoints are model parameters read in metres.

The computation is the framework's own outcome law applied to an explicit state; it records no measurement, no apparatus response and no empirical data.

Facts & Assumptions

Given: The spinless massive-particle model of P5 with $H = L^{2} (R^{3}; C)$ and position operators $Q_{j}$ (Kinematics and massive-particle model postulate P5: Newtonian frames and one-particle operators, Position and momentum operators on Euclidean L2); the outcome-law reading of Assigned sharp observables and the outcome law of the framework; a width $σ > 0$ ; a unit vector $φ \in L^{2} (R^{2}; C)$ ; the Gaussian packet $ψ_{σ}$ and state $ψ = ψ_{σ} \otimes φ$ ; a bin $(a, b] \subseteq R$ ; the Axiom of Countable Choice and the Axiom of Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The Axiom of Choice).

[F1]

Gaussian integrals. $\int_{R} e^{- u^{2}} d u = \sqrt{π}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ ); for $c > 0$ the $C^{1}$ substitution $u = t / \sqrt{2 c}$ gives $\int_{R} e^{- t^{2} / (2 c)} d t = \sqrt{2 π c}$ .

[F2]

Position law of the model. For the spinless massive model and a unit vector $ψ$ , the law of $Q_{j}$ is $μ_{ψ}^{Q_{j}} (B) = \int_{x_{j}^{- 1} (B)} ∣ ψ (x) ∣^{2} d x$ , with density $f_{j} (t) = \int_{R^{2}} ∣ ψ (x_{⊥}, t) ∣^{2} d x_{⊥}$ and $μ_{ψ}^{Q_{j}} ({λ}) = 0$ for every $λ$ (Position and momentum outcome laws and the Born density of the massive particle model clauses (b) and (d)).

[F3]

Iterated integrals and monotonicity. For product-measurable nonnegative functions on $σ$ -finite spaces the integral may be iterated (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product); for nonnegative measurable $f \leq g$ one has $\int f \leq \int g$ and $\int_{A} f \leq \int_{B} f$ for $A \subseteq B$ , directly from the supremum definition of the nonnegative integral (The nonnegative Lebesgue integral, Integral over a measurable subset); and $t \mapsto e^{- t^{2} / (2 σ^{2})}$ is continuous, hence Borel measurable (Continuous functions on Euclidean spaces are Borel measurable).

[F4]

The product state is a unit vector. $ψ = ψ_{σ} \otimes φ$ is the almost-everywhere product of an $L^{2}$ function of $x_{1}$ and an $L^{2}$ function of $(x_{2}, x_{3})$ , hence lies in $L^{2} (R^{3}; C)$ (The space $L^{p} (μ)$ as the quotient by null functions,); Tonelli [F3] and the normalizations of $ψ_{σ}$ and $φ$ give $∥ ψ ∥^{2} = 1$ , and $∣ ψ ∣^{2}$ is the product $∣ ψ_{σ} (x_{1}) ∣^{2} ∣ φ (x_{2}, x_{3}) ∣^{2}$ because the modulus of a product is the product of the moduli (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F5]

States. The pure preparation of the unit vector $ψ$ is the state $T_{ψ, ψ}$ of the model, and the outcome law is read as in Assigned sharp observables and the outcome law of the framework clause (b).

Verification

technique · direct; normalize the Gaussian packet and compute the position-bin probabilities, their bounds and the exact-value probability

1.1givenF1F3F4F5algebra

[Normalization of the Gaussian packet] With $c = σ^{2}$ in [F1], $\int_{R} e^{- t^{2} / (2 σ^{2})} d t = \sqrt{2 π σ^{2}}$ . Therefore $\int_{R} ∣ ψ_{σ} (t) ∣^{2} d t = (2 π σ^{2})^{- 1 / 2} \sqrt{2 π σ^{2}} = 1$ , since $∣ ψ_{σ} (t) ∣^{2} = (2 π σ^{2})^{- 1 / 2} e^{- t^{2} / (2 σ^{2})}$ by [F4]; consequently $\int_{R^{3}} ∣ ψ ∣^{2} d x = (\int_{R} ∣ ψ_{σ} ∣^{2}) (\int_{R^{2}} ∣ φ ∣^{2}) = 1$ by Tonelli [F3], so $ψ$ is a unit vector and $[ψ]$ is a pure preparation of the model by [F5].

2.1givenstep 1.1F2F3F4algebra

[The position law and its density] By [F2] the law of $Q_{1}$ in the preparation $[ψ]$ is $μ_{ψ}^{Q_{1}} (B) = \int_{x_{1}^{- 1} (B)} ∣ ψ ∣^{2} d x$ ; writing the integrand as $∣ ψ_{σ} (x_{1}) ∣^{2} ∣ φ (x_{2}, x_{3}) ∣^{2}$ by [F4] and iterating the integral by Tonelli [F3], $\int_{x_{1}^{- 1} (B)} ∣ ψ ∣^{2} d x = (\int_{B} ∣ ψ_{σ} (t) ∣^{2} d t) (\int_{R^{2}} ∣ φ ∣^{2}) = \int_{B} ∣ ψ_{σ} (t) ∣^{2} d t$ , which is clause (i) with density $f_{1} (t) = ∣ ψ_{σ} (t) ∣^{2}$ .

3.1givenstep 1.1step 2.1F1F2F3algebra∎

[Exact values and bin bounds] By [F2] (the atomless clause of the position law) $μ_{ψ}^{Q_{1}} ({λ}) = 0$ for every $λ$ , so no exact coordinate value carries probability. For any finite $a < b$ , put $M : = \max {∣ a ∣, ∣ b ∣}$ . Every $t \in [a, b]$ satisfies $∣ t ∣ \leq M$ , and therefore $\frac{1}{\sqrt{2 π σ^{2}}} e^{- M^{2} / (2 σ^{2})} \leq ∣ ψ_{σ} (t) ∣^{2} \leq \frac{1}{\sqrt{2 π σ^{2}}}$ . Integrating these inequalities over $(a, b]$ and using the position law in [F2] and monotonicity [F3] gives the two displayed bounds. Their lower bound is strictly positive because $a < b$ and $σ > 0$ , so every bin of positive length receives positive probability, including bins crossing the origin and bins with negative endpoints. For the symmetric bin $(- σ, σ]$ , the substitution $u = t / σ$ in step 2.1 gives $μ_{ψ}^{Q_{1}} ((- σ, σ]) = \frac{1}{\sqrt{2 π}} \int_{- 1}^{1} e^{- u^{2} / 2} d u$ , and since $e^{- 1 / 2} \leq e^{- u^{2} / 2} \leq 1$ on $[- 1, 1]$ , monotonicity [F3] yields $\sqrt{2 / (π e)} \leq μ_{ψ}^{Q_{1}} ((- σ, σ]) \leq \sqrt{2 / π}$ . Permuting the selected coordinate in the product state repeats steps 1.1 and 2.1 with $x_{j}$ in place of $x_{1}$ , proving (iii); the other two marginals of the original state come from $∣ φ ∣^{2}$ by [F2] and Tonelli [F3]. The final upper bound for $(- δ, δ]$ is the general upper estimate with $a = - δ$ , $b = δ$ ; its lower estimate is positive for every $δ > 0$ .

Remarks

The transverse factor $φ$ enters the computation only through its total mass $\int ∣ φ ∣^{2} = 1$ ; the first-coordinate law of a product state is independent of the transverse profile, while a state that is not a product can correlate the coordinates and change the marginal, as the general density formula $f_{j} (t) = \int_{R^{2}} ∣ ψ (x_{⊥}, t) ∣^{2} d x_{⊥}$ of Position and momentum outcome laws and the Born density of the massive particle model shows.
The bounds are deliberately elementary: they neither sharpen the Gaussian integral nor claim an error analysis. They are finite checks of the model's law, not measured frequencies, and no apparatus resolution, binning procedure or count is asserted.

Position-bin probabilities of a Gaussian packet

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources