Alphabeta Math
LemmaStatement: 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.

The maximal distributional domain of a geometric Dirac operator is H1

Statement

Assume full AC. Let M be closed, Riemannian, and of even dimension n≥2. Let DV be the formally symmetric geometric Dirac operator of Graded Hermitian Clifford modules and geometric Dirac operators, and let P=DV2 have the Lichnerowicz form of Lichnerowicz formula for a geometric Dirac operator. Then dom⁡(D‾V)=H1(M,V)={u∈L2:DVu∈L2 distributionally}, its graph norm is equivalent to the H1 norm, smooth sections are a core, and D‾V is selfadjoint.

Facts & Assumptions

Given: Full AC, closed compact M, the module and operator above, and the compact L2 and Sobolev spaces.

[F1]

The Lichnerowicz formula says P=∇∗∇+R0, where R0=scal⁡/4+c(FV/S) is a smooth bounded endomorphism (Lichnerowicz formula for a geometric Dirac operator).

[F2]

For a formally symmetric Laplace-type bundle operator on compact boundaryless M, (P+λ):H2→L2 is an isomorphism for sufficiently large λ>0, its inverse B maps L2→H2 and is selfadjoint, and smooth data are preserved (Compact Laplace-type bundle operators: regularity and shifted parametrices).

[F3]

P has a smooth finite-dimensional kernel, closed range, and a Green inverse; the exact H2 domain and higher regularity are as in Compact Laplace-type operators: smooth kernel, closed range and Green inverse.

[F4]

The geometric Dirac operator is globally defined and formally symmetric on closed M under Countable Choice (The geometric Dirac operator is globally well defined and formally symmetric).

[A1]

Full AC supplies the choice assumptions of [F2]–[F4] (The Axiom of Choice).

Proof

Given: The hypotheses in the Statement.

1.1F1F3F4given

For smooth u, formal symmetry [F4] and integration of [F1] against u give ∥Du∥22=∥∇u∥22+⟨R0u,u⟩. Since R0 is bounded and the connection Sobolev norm is equivalent to a finite-chart H1 norm, this gives ∥u∥H1≤C(∥Du∥2+∥u∥2). Smooth density extends the estimate to H1, while the first-order local formula gives ∥Du∥2≤C∥u∥H1. Thus the graph norm is equivalent to H1, and smooth sections are dense in that graph norm.

1.2F2F3F4givenalgebra

Let B=(P+λ)−1 from [F2]. It maps L2→H2, so DB:L2→H1 is bounded. On smooth h, D(Bh)=B(Dh): both solve (P+λ)z=Dh because D commutes with D2 on smooth sections and the solution is unique. Density extends the symmetry identity ⟨DBf,h⟩=⟨f,DBh⟩ to f,h∈L2.

2.1F2F4step 1.2

Suppose u∈L2 and Du=f∈L2 distributionally. Then (P+λ)u=Df+λu distributionally. Test against Bh for smooth h: formal symmetry gives ⟨u,h⟩=⟨f,DBh⟩+λ⟨u,Bh⟩=⟨DBf+λBu,h⟩, using step 1.2 and selfadjointness of B. Hence u=DBf+λBu as distributions. The first term is in H1 by the bounded map DB, and the second is in H2 by [F2]; therefore u∈H1. Conversely every H1 section has Du∈L2 by the first-order local formula, so the maximal distributional domain equals H1.

3.1A1F2F3F4step 1.1step 2.1algebra∎

The closure of smooth D has domain H1 by step 1.1, so its closure is contained in the maximal distributional operator. If u∈dom⁡(D∗), then the distribution Du equals the L2 vector D∗u by the definition of adjoint testing against smooth sections. Step 2.1 gives u∈H1, and formal symmetry plus density shows D∗u=Du. Thus D∗=D‾; the closure is selfadjoint. No compact-resolvent theorem for a general first-order operator is assumed. Full AC supplies the choice assumptions of [F2]–[F4] as recorded in [A1].

Depends on

Used by

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources