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 geometric Dirac operator is globally well defined and formally symmetric

Statement

Assume Countable Choice. For a supplied graded Hermitian Clifford module and compatible connection as in Graded Hermitian Clifford modules and geometric Dirac operators, the local expression DV=∑ic(ei)∇eiV is independent of oriented orthonormal frame, is a smooth globally defined first-order differential operator, and is formally symmetric on a closed M.

Facts & Assumptions

Given: Countable Choice, a smooth oriented Riemannian manifold, a graded Hermitian Clifford module V, and a supplied graded Hermitian Clifford connection ∇V.

[F1]

The Clifford relation, odd action and skew-Hermitian condition are exactly those in Graded Hermitian Clifford modules and geometric Dirac operators.

[F2]

A Clifford connection obeys ∇XV(c(ξ)v)=c(∇XLCξ)v+c(ξ)∇XVv (Graded Hermitian Clifford modules and geometric Dirac operators, Complex-linear and metric-compatible bundle connections).

[F3]

On a closed Riemannian manifold of dimension n≥1, the integral of the divergence of a smooth vector field is zero under countable choice (Riemannian divergence theorem).

[A1]

This proof uses only ACω through [F3]; it is declared in The Axiom of Countable Choice (ACω).

Proof

Given: The stated module, connection and closed manifold.

1.1F1F2givenalgebra

On an overlap let ei′=∑jaijej be a change of oriented orthonormal frame, so A=(aij) is orthogonal. The dual coframe changes by the same orthogonal coefficient matrix with the corresponding inverse convention, while ∇ei′=∑kaik∇ek. Therefore ∑ic(e′i)∇ei′=∑i,j,kaijaikc(ej)∇ek=∑jc(ej)∇ej by ∑iaijaik=δjk. Each chart expression has smooth coefficients, and these overlap equalities glue them to one global first-order operator.

2.1A1F1F2F3step 1.1∎

If dim⁡M=0, the defining sum for DV is empty, so DV=0 is formally symmetric. Now suppose dim⁡M≥1. Define the complex vector field Y=∑i⟨c(ei)u,v⟩ei for smooth sections u,v. At any chosen point take a local orthonormal frame with ∇LCei=0 there. Using [F2], metric compatibility and ∇ei=0 at that point gives div⁡Y=⟨DVu,v⟩−⟨u,DVv⟩: the second term has this sign because c(ei)∗=−c(ei) and the Hermitian pairing is linear in its first variable. Since this is a pointwise identity independent of the chosen normal frame, it holds globally. Apply [F3] to real and imaginary parts of Y and integrate to get ∫M⟨DVu,v⟩=∫M⟨u,DVv⟩. Thus DV is formally symmetric. Oddness follows termwise because each c(ei) is odd and ∇ preserves grading.

Depends on

Used by

Cited to discharge well-definedness by Graded Hermitian Clifford modules and geometric Dirac operators.

Dependency tree · two levels

34 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