Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

Worked change of adapted chart with a rotation, a boost and a spatial shift

Example

Take V=R4 with coordinates (t,x1,x2,x3), τ(t,x1,x2,x3)=t, so that K={0}×R3 with the standard inner product g, and take A=V as an affine space over itself. Let the first adapted chart be the standard one, o=0, u=e0, (e1,e2,e3) the standard basis of K. Let the second adapted chart be

o′=e2,u′=e0+e1,e1′=e2,e2′=−e1,e3′=e3,

which is adapted: τ(u′)=1, and (e1′,e2′,e3′) is a positively oriented g-orthonormal basis of K.

For a point with first coordinates (t,x1,x2,x3), equating the two expansions gives t′=t, x2=x1′+1 and x1=t′−x2′, that is

x1′=x2−1,x2′=t−x1,x3′=x3,

which is the transformation x′=Rx+vt+a of Transformation between adapted charts and its kinematic consequences with b=0,

R=(010−100001),v=(010),a=(−100).

The matrix R satisfies RTR=I3 and det⁡R=1, so R∈SO(3).

Facts & Assumptions

Given: The two adapted charts displayed above, a point p with first coordinates (t,x1,x2,x3), and the map γ:R→A, γ(s)=(s,s,2s,0) in the first coordinates.

[L1]

Adapted coordinates are unique: the coefficients in p=o+tu+∑ixiei and in the primed expansion are uniquely determined (Existence and uniqueness of adapted coordinates, and the affine structure of simultaneous slices).

[L2]

Two adapted charts are related by t′=t+b and x′=Rx+vt+a with R∈O(3), and R∈SO(3) when both bases are positively oriented (Transformation between adapted charts and its kinematic consequences, The orthogonal group O(3) and the rotation group SO(3)).

Verification

technique · direct; substitute the chart data and check the displays
1.1givenalgebra

The matrix R has rows (0,1,0), (−1,0,0), (0,0,1), so RTR has entries: first diagonal 02+(−1)2+02=1, second diagonal 12+02+02=1, third diagonal 1, and off-diagonal entries 0⋅1+(−1)⋅0+0⋅0=0, 0⋅0+(−1)⋅0+0⋅1=0, 1⋅0+0⋅0+0⋅1=0; hence RTR=I3, and det⁡R=0⋅(0⋅1−0⋅0)−1⋅((−1)⋅1−0⋅0)+0=1, so R∈SO(3).

2.1step 1.1L1L2algebra

For the point p with first coordinates (t,x1,x2,x3) the direct substitution p=o′+t′u′+∑ixi′ei′ reads (t,x1,x2,x3)=(t′, t′−x2′, 1+x1′, x3′), whose unique solution is t′=t, x1′=x2−1, x2′=t−x1, x3′=x3; comparison with x′=Rx+vt+a gives Rx+vt+a=(x2,−x1,x3)+(0,t,0)+(−1,0,0)=(x2−1, t−x1, x3), so the transformation law of the lemma holds in this chart pair with the displayed b,v,a,R.

3.1step 2.1L2algebra∎

For the curve γ(s)=(s,s,2s,0), with first coordinate representative x(s)=(s,2s,0), the second representative is y(s)=(2s−1, s−s, 0)=(2s−1,0,0) by step 2.1, so y′(s)=(2,0,0) and Rx′(s)+v=R(1,2,0)+(0,1,0)=(2,−1,0)+(0,1,0)=(2,0,0); also x′′=0 and y′′=0, and R⋅0=0. This verifies y′=Rx′+v and y′′=Rx′′ in the worked case.

Remarks

  • The shift a=(−1,0,0) is the coordinate vector of o−o′=−e2 in the primed spatial basis. The change from u to u′=u+e1 supplies the boost v=(0,1,0); since b=0, it adds no constant shift.

  • The matrix R is the change-of-basis matrix from (e1,e2,e3) to (e1′,e2′,e3′), and its determinant is 1 because both bases are positively oriented. Had one of the two bases been negatively oriented, the same computation would give det⁡R=−1 and R∈O(3)∖SO(3).

Depends on

Dependency tree · 2 levels

Sources