Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passverified 2026-10-22 (gpt-6.1-sol)
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.

A conical helicity packet has reduced axial spin projection

Example

Let θ(k)=arccos⁡(kz/∣k∣)∈[0,π]. For σ∈{+1,−1}, θ0∈[0,π], and 0<δ≤π, a normalized helicity-σ packet of angular width δ is a vector f∈HTν with ∥f∥ν=1, Pσf=f almost everywhere, and f(k)=0 almost everywhere unless ∣θ(k)−θ0∣≤δ. Such packets exist for every θ0 and δ. Each satisfies ∣⟨f,Sz′f⟩ν−ℏσcos⁡θ0∣≤ℏδ. Consequently, for any sequence 0<δm≤π with δm↓0 and normalized helicity-σ packets fm of widths δm, ⟨fm,Sz′fm⟩ν→ℏσcos⁡θ0. The exact cone Cθ0:={k∈M:θ(k)=θ0} is ν-null. Therefore every g∈HTν that vanishes ν-almost everywhere on M∖Cθ0 is the zero element, and no such g can be normalized.

Facts & Assumptions

Given: The Axiom of Choice, ℏ>0, the transverse one-photon Hilbert space, helicity projectors, and projected spin operator Sz′.

[A1]

Assume the Axiom of Choice, as in the rotation and Fock suppliers. The Axiom of Choice

[F1]

The helicity spaces are the ranges of the orthogonal rank-one projectors Pσ(n) on the transverse fibers; each line has smooth local unit sections, and HTν uses dν=d3k/(2∣k∣). Transverse one-photon space and helicity projectors

[F2]

For normalized helicity-σ f, the projected-spin expectation is ⟨f,Sz′f⟩ν=ℏσ∫Mcos⁡θ(k)∣f(k)∣2 dν(k). Second-quantized total rotations and helicity counts

[F3]

Cosine is 1-Lipschitz: ∣cos⁡u−cos⁡v∣≤∣u−v∣ for all real u,v. Sine and cosine are 1-Lipschitz on R

[F4]

In spherical coordinates on S2, the polar surface element is dΩ=sin⁡θ dθ dϕ, and dν=(r/2) dr dΩ, r=∣k∣. The surface factor follows from ∣∂θn×∂ϕn∣=sin⁡θ. Polar coordinates decompose Lebesgue measure into r^{n-1} dr d sigma Agreement with the existing polar sphere measure

[F5]

Fubini applies to the product radial and angular measures, which are sigma-finite. Fubini's theorem for L^1 functions on a sigma-finite product

[F6]

A nonzero smooth bump supported in a coordinate ball exists; translation and rescaling give compact radial and angular cutoffs. A smooth bump between concentric Euclidean balls

[F7]

Full Choice implies Countable Choice, the bundle supplier's hypothesis [F1], and is also the stated hypothesis of the Fock supplier [F2]. AC implies DC implies countable choice The Axiom of Countable Choice (ACω)

[F8]

Under Countable Choice, every coordinate box, including a degenerate box with a zero side length, is Lebesgue measurable with measure equal to the product of its side lengths. In particular singletons in R and R2 and bounded rectangles contained in a coordinate line in R2 have measure zero. A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included

Verification

Given: [A1], [F1]–[F8], θ0∈[0,π], 0<δ≤π, and σ∈{+1,−1}.

1.1A1F1F4F6F7givenconstruct

By [F7], full Choice supplies Countable Choice to the bundle definition [F1]. The set {n∈S2:∣θ(n)−θ0∣<δ} is a nonempty open angular neighborhood of a direction with polar angle θ0. Choose a smaller coordinate ball whose closure lies in that neighborhood and in a trivializing patch for the helicity line from [F1]. Let uσ be its smooth unit section, choose a nonzero smooth bump χ supported in the ball by [F6], and choose a nonzero smooth radial bump η supported in 1<r<2. The field f~(k)=η(r)χ(n(k))uσ(n(k)), extended by zero outside the patch, is smooth, compactly supported away from k=0, transverse, and satisfies Pσf~=f~. It is nonzero on an open set of positive dν measure by [F4], so 0<∥f~∥ν<∞; normalizing it gives a packet of width δ. Repeating for each δm with 0<δm≤π proves the asserted existence of sequences.

1.2A1F2F3givenalgebra

Under the full-Choice hypothesis [A1], the Fock supplier [F2] gives the projected-spin expectation formula; with ∥f∥ν=1 it yields ∣⟨f,Sz′f⟩ν−ℏσcos⁡θ0∣=ℏ∣∫M(cos⁡θ(k)−cos⁡θ0)∣f(k)∣2 dν(k)∣. On the support of f, [F3] bounds ∣cos⁡θ−cos⁡θ0∣≤∣θ−θ0∣≤δ. Taking the absolute value inside the integral and using normalization gives the claimed bound ℏδ.

2.1step 1.2algebra

For any sequence 0<δm≤π with δm↓0, step 1.2 gives ∣⟨fm,Sz′fm⟩ν−ℏσcos⁡θ0∣≤ℏδm→0, so the expectations converge to ℏσcos⁡θ0.

3.1F1F4F5F7F8givenalgebra∎

Put Eθ0={n∈S2:θ(n)=θ0}. If 0<θ0<π, cover this latitude by two overlapping azimuth-coordinate charts. In each chart its coordinate preimage lies in a bounded rectangle {θ0}×[a,b], which is Lebesgue null by [F8]; the chart-area formula sin⁡θ dθ dϕ in [F4] therefore gives zero surface measure. If θ0=0 or π, Eθ0 is a single pole. A smooth regular sphere chart centered at that pole has a singleton preimage, null in R2 by [F8]; integrating the chart area density over that singleton again gives zero surface measure by the chart-measure identification in [F4]. Thus Eθ0 is surface-null for every stated θ0. For each integer m≥2, the annulus 1/m≤r≤m has finite ν-measure by [F1] and [F4], so the cone indicator restricted to it is integrable. The polar decomposition in [F4] and Fubini [F5] give ν(Cθ0∩{1/m≤r≤m})=∫1/mmr2 dr∫S21Eθ0 dΩ=0. These annuli cover M, so countable subadditivity gives ν(Cθ0)=0. If g∈HTν vanishes ν-almost everywhere on M∖Cθ0, its squared norm is the sum of the integrals of ∣g∣2 over that complement and the null cone, both zero. Hence ∥g∥ν=0 and g is the zero Hilbert-space element; in particular it cannot be normalized. This is the exact null-cone conclusion in the Example.

Depends on

Dependency tree · 2 levels

Sources