Golden Observer Events and Null Directions

Abstract

Golden observer events and their genuine tangents recover two fixed null directions.

Theorem 1.1 (Observer events and tangents recover the golden null basis).

$$\begin{gathered} letuPlus=\mathrm{pair}\left(\phi ,1\right); \\ letuMinus=\mathrm{pair}\left({\phi }^{\prime },1\right); \\ letQ(w)=\mathrm{fst}{\left(w\right)}^2-\mathrm{fst}\left(w\right)\cdot \mathrm{snd}\left(w\right)-\mathrm{snd}{\left(w\right)}^2; \\ leth\left(eta\right)=\mathrm{pair}\left(\frac{\exp \left(eta\right)\cdot \phi -\exp \left(-eta\right)\cdot {\phi }^{\prime }}{\mathrm{sqrt}\left(5\right)},\frac{\exp \left(eta\right)-\exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\right); \\ let\mathrm{tangent}\left(eta\right)=\mathrm{pair}\left(\frac{\exp \left(eta\right)\cdot \phi +\exp \left(-eta\right)\cdot {\phi }^{\prime }}{\mathrm{sqrt}\left(5\right)},\frac{\exp \left(eta\right)+\exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\right); \\ \left(\left(\forall v\in \mathrm{Prod}\left(\mathrm{Real}\left(\right),\mathrm{Real}\left(\right)\right),\exists !a,b\in \mathrm{Real}\left(\right),v=a\cdot uPlus+b\cdot uMinus\wedge \left(\forall a\in \mathrm{Real}\left(\right),b\in \mathrm{Real}\left(\right),Q\left(a\cdot uPlus+b\cdot uMinus\right)=-5\cdot a\cdot b\right)\right)\wedge \left(Q\left(uPlus\right)=0\wedge Q\left(uMinus\right)=0\right)\right)\wedge \left(\forall eta\in \mathrm{Real}\left(\right),\left(\left(\left(\left(\left(\left(h\left(eta\right)=\frac{\exp \left(eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uPlus+-\frac{\exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uMinus\wedge \mathrm{tangent}\left(eta\right)=\frac{\exp \left(eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uPlus+\frac{\exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uMinus\right)\wedge \mathrm{HasDerivAt}\left(h,\mathrm{tangent}\left(eta\right),eta\right)\right)\wedge Q\left(h\left(eta\right)\right)=1\right)\wedge h\left(eta\right)+\mathrm{tangent}\left(eta\right)=\frac{2\cdot \exp \left(eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uPlus\right)\wedge \mathrm{tangent}\left(eta\right)-h\left(eta\right)=\frac{2\cdot \exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\cdot uMinus\right)\wedge 0<\frac{2\cdot \exp \left(eta\right)}{\mathrm{sqrt}\left(5\right)}\right)\wedge 0<\frac{2\cdot \exp \left(-eta\right)}{\mathrm{sqrt}\left(5\right)}\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/HyperbolicTransport/ObserverEventNullDirections.golden_observer_event_null_directions (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two vectors (phi,1) and (phi-prime,1) form a basis of the real plane. Every vector therefore has unique coefficients in this basis, and the golden Lorentz form of a combination is exactly -5ab.

The displayed event and tangent are defined from positive exponential amplitudes divided by sqrt(5). The proof establishes sqrt(5)>0 internally, differentiates both event coordinates, and proves that the event remains on the unit Lorentz hyperbola.

Adding the tangent to the event cancels the conjugate direction; subtracting the event from the tangent cancels the future direction. The remaining amplitudes are strictly positive for every rapidity.

At zero rapidity all eight event laws give a concrete satisfying witness. Replacing the genuine tangent there by the zero vector falsifies the future-null identity, so the derivative clauses are not vacuous.

References

• Truth anchor: D5/S3/Observer/HyperbolicTransport/ObserverEventNullDirections.golden_observer_event_null_directions