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.
Tetrads, Lorentz connections and spin interfaces — model 2
Statement
Assume . Let with standard coordinates , metric for , time orientation , and the standard orientation. The Cartesian tetrad on all of is , with dual coframe . Connections below are smooth affine connections on . Define the positive-definite form and its orientation-preserving orthogonal group . Let and consider the constant Lorentz boost
It belongs to but not to . Consequently, for any set and map , no satisfies as matrices. With , the Lorentzian covering sends to in the Hermitian matrix model. In the Cartesian tetrad, zero is the connection matrix of the unique torsion-free metric-compatible affine connection, and the Clifford interface uses the Lorentzian matrix , not .
Statement references
Facts & Assumptions
Given: The explicitly specified Minkowski manifold, coordinates, tetrad, quadratic forms, comparison group, and nonzero real boost parameter from the Statement. All coframes and connections are defined on .
Assume (The Axiom of Countable Choice ()); maps with codomain are comparison data only.
Local Lorentz tetrad and connection: Lorentz coframes use , with and .
Torsion-free tetrad equivalence to Levi-Civita: zero torsion and -skewness give the unique metric-selected Levi-Civita connection.
Lorentzian spin-lift interface: the Lorentzian spin group is and its structure map targets the oriented time-oriented frame bundle through .
The Lorentzian spin double cover from Hermitian matrices: the action on Hermitian matrices preserves and covers .
Local spin-connection Clifford compatibility: under its stated local matrix hypotheses, the Clifford identity uses and ; it does not assert compatibility with a separately supplied group representation.
Verification
Put and . Multiplying the upper-left block gives , because and the off-diagonal time-space terms cancel. The determinant of that block is , the remaining block is identity, and is future timelike since . Hence . For the Euclidean form, however, for , so . Thus is not in the image of any map with codomain .
Write . Its eigenvalues are and , so . Pauli multiplication gives , , and for ; thus its Hermitian action is exactly . By [F4] it is the Lorentzian spin lift, consistent with the target group in [F3].
On the Cartesian tetrad , , so gives zero torsion and is -skew. By [F2] it induces the unique Levi-Civita connection. The boost is constant on spacetime, so also has and its transformed connection is by [F1]; the torsion remains zero. The local matrix identity from [F5] uses the same ; it does not identify this operator as one induced by a group representation. Thus the Euclidean orthogonal comparison group does not supply this Lorentzian interface.