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.
Worked change of adapted chart with a rotation, a boost and a spatial shift
Example
Take with coordinates , , so that with the standard inner product , and take as an affine space over itself. Let the first adapted chart be the standard one, , , the standard basis of . Let the second adapted chart be
which is adapted: , and is a positively oriented -orthonormal basis of .
For a point with first coordinates , equating the two expansions gives , and , that is
which is the transformation of Transformation between adapted charts and its kinematic consequences with ,
The matrix satisfies and , so .
Facts & Assumptions
Given: The two adapted charts displayed above, a point with first coordinates , and the map , in the first coordinates.
Adapted coordinates are unique: the coefficients in and in the primed expansion are uniquely determined (Existence and uniqueness of adapted coordinates, and the affine structure of simultaneous slices).
Two adapted charts are related by and with , and when both bases are positively oriented (Transformation between adapted charts and its kinematic consequences, The orthogonal group and the rotation group ).
Verification
The matrix has rows , , , so has entries: first diagonal , second diagonal , third diagonal , and off-diagonal entries , , ; hence , and , so .
For the point with first coordinates the direct substitution reads , whose unique solution is , , , ; comparison with gives , so the transformation law of the lemma holds in this chart pair with the displayed .
For the curve , with first coordinate representative , the second representative is by step 2.1, so and ; also and , and . This verifies and in the worked case.
Remarks
-
The shift is the coordinate vector of in the primed spatial basis. The change from to supplies the boost ; since , it adds no constant shift.
-
The matrix is the change-of-basis matrix from to , and its determinant is because both bases are positively oriented. Had one of the two bases been negatively oriented, the same computation would give and .