Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated
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 boost family on the spacelike pair (11,13,0,0): simultaneity at b=11/13 and both time orders

Example

Worked computation in the chart x of an inertial frame of an affine Minkowski space (Oriented time-oriented affine Minkowski space (the spacetime primitives), Inertial frames and inertial charts of the affine Minkowski model) with η0=diag⁡(−1,1,1,1). Let p:=x−1(0,0,0,0) and q:=x−1(11,13,0,0); then D:=x(q)−x(p)=(11,13,0,0) has η(D,D)=−112+132=−121+169=48>0, so q−p is spacelike and ∣D0∣=11<13=∣Ds∣, in accordance with clause (a) of Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign.

(a) Simultaneity at b0=11/13. With e:=Ds/∣Ds∣=e1 and b0:=D0/∣Ds∣=11/13, so that ∣b0∣<1, the chart xb0 of the inertial frame built from the passive boost B(b0e1) by clause (d) of the same lemma satisfies xb00(q)−xb00(p)=γb0(11−1113⋅13)=0,γb0=(1−121169)−1/2=1348: the two events are simultaneous in that frame.

(b) Below b0: positive time difference. With b=3/5 one has γb=(1−9/25)−1/2=5/4 and xb0(q)−xb0(p)=54(11−35⋅13)=54⋅165=4>0.

(c) Above b0: negative time difference. With b=12/13 one has γb=(1−144/169)−1/2=13/5 and xb0(q)−xb0(p)=135(11−1213⋅13)=135(−1)=−135<0.

(d) The spatial separation in the three frames. The boost in the (0,1)-plane acts by x′0=γ(x0−bx1), x′1=γ(x1−bx0) (The passive Lorentz boost with parameter beta), so the spatial difference of the pair in the boosted chart is xb1(q)−xb1(p)=γb(13−11b). It equals 48 for b=b0, 8 for b=3/5 and 37/5 for b=12/13; in each case it is nonzero and ∣xb0(q)−xb0(p)∣<∣xb1(q)−xb1(p)∣. The displacement stays spacelike because a boost is a Lorentz map and preserves η (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups, Linear and affine Lorentz maps, and the Lorentz group), so the three charts are charts of three inertial frames related to x by passive boosts and the time-order sign of a spacelike-separated pair is an artifact of the chart, not of the pair. No physical synchronization procedure is asserted; simultaneity means equality of the chart's time coordinate.

Facts & Assumptions

Given: An inertial frame with chart x and η0=diag⁡(−1,1,1,1), the events p=x−1(0,0,0,0) and q=x−1(11,13,0,0), the displacement D=(11,13,0,0) with spatial part Ds=(13,0,0) and Euclidean norm ∣Ds∣=13.

[L1]

For a spacelike pair the lemma gives ∣D0∣<∣Ds∣ in every inertial chart, and for every ∣b∣<1 the chart xb of the inertial frame with ordered basis ea′=B(be)−1ea, where e=Ds/∣Ds∣, satisfies xb0(q)−xb0(p)=γb(D0−b∣Ds∣) with γb=(1−b2)−1/2 (Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign).

[L2]

For β=be1 with ∣b∣<1 the passive boost acts in coordinates by x′0=γ(x0−bx1), x′1=γ(x1−bx0), x′2=x2, x′3=x3, with γ=(1−b2)−1/2>0 (The passive Lorentz boost with parameter beta).

[L3]

A vector v is spacelike exactly when η(v,v)>0; a linear Lorentz map preserves η, hence preserves the causal character of every nonzero vector, and the boosts are proper orthochronous Lorentz maps (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups, Linear and affine Lorentz maps, and the Lorentz group).

[L4]

In a fixed inertial frame the spatial coordinates carry the Euclidean norm ∣(u1,u2,u3)∣=(u1)2+(u2)2+(u3)2 (The Euclidean spatial structure and cross product of an inertial frame).

Verification

technique · direct
1.1givenL3L4algebra

The displacement is D=(11,13,0,0), so η(D,D)=−121+169=48>0, the pair is spacelike, and ∣D0∣=11<13=∣Ds∣.

2.1step 1.1L1algebra

With b0=11/13 one has ∣b0∣<1, and the chart of clause (d) of [L1] gives xb00(q)−xb00(p)=γb0(11−(11/13)13)=0 with γb0=(1−121/169)−1/2=(48/169)−1/2=13/48>0; this is (a).

2.2step 1.1L1algebra

With b=3/5 one has ∣b∣<1, γb=(1−9/25)−1/2=(16/25)−1/2=5/4 and xb0(q)−xb0(p)=(5/4)(11−(3/5)13)=(5/4)(16/5)=4>0; this is (b).

2.3step 1.1L1algebra

With b=12/13 one has ∣b∣<1, γb=(1−144/169)−1/2=(25/169)−1/2=13/5 and xb0(q)−xb0(p)=(13/5)(11−(12/13)13)=(13/5)(−1)=−13/5<0; this is (c).

3.1step 1.1step 2.1step 2.2step 2.3L2L3algebra

The spatial difference in the boosted chart is xb1(q)−xb1(p)=γb(13−11b) by [L2] applied to D, and the three values are γb0(13−121/13)=(13/48)(48/13)=48, (5/4)(13−33/5)=(5/4)(32/5)=8 and (13/5)(13−132/13)=(13/5)(37/13)=37/5, all nonzero; the corresponding time differences are 0, 4 and −13/5, so ∣xb0(q)−xb0(p)∣<∣xb1(q)−xb1(p)∣ holds in all three charts, and the spacelike character is preserved because η(Bv,Bv)=η(v,v) by [L3]; this is (d).

4.1step 3.1step 2.1step 2.2step 2.3L1∎

By [L1] the three charts xb0, x3/5 and x12/13 are charts of inertial frames related to x by passive boosts, and steps 2.1, 2.2 and 2.3 give time differences 0, 4 and −13/5; hence the time order of the spacelike-separated pair (p,q) is simultaneity for b0=11/13, positive for 3/5<b0 and negative for 12/13>b0, and is therefore an artifact of the inertial chart and not a property of the pair. Only equality of the chart's time coordinate is used for simultaneity, and no choice principle is used.

Depends on

Dependency tree · 2 levels

Sources