Golden Observer Beatty Route

Abstract

The golden observer exponent has sqrt-five drift and exactly two golden step sizes.

Theorem 1.1 (The golden observer has sqrt-five drift and two golden distances).

$$\begin{gathered} (\forall v\in \mathbb{N}, \\ \mathrm{beta}\left(v\right)=\sqrt{5}\times v+r\left(v\right)\wedge r\left(v\right)=\phi -1-\mathrm{fract}\left(v+1\times \phi \right)\wedge \\ r\left(v\right)\in (\phi -2,\phi -1]\wedge \mathrm{beta}\left(v+1\right)-\mathrm{beta}\left(v\right)\in \left\{\phi ,{\phi }^2\right\}\wedge \\ (\mathrm{beta}\left(v+1\right)-\mathrm{beta}\left(v\right)=\phi ⟺\mathrm{beatty}\left(v+1\right)-\mathrm{beatty}\left(v\right)=1))\wedge \\ \mathrm{beta}\left(2\right)-\mathrm{beta}\left(1\right)=\phi . \end{gathered}$$

Proof. Machine-checked in Lean as D5/S1/Deficit/Beatty/GoldenObserverRoute.golden_observer_route_w_c1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here phi=(1+sqrt(5))/2, psi=1-phi, beatty(v)=floor((v+1)phi)-1, beta(v)=beatty(v)-v psi, and r is the displayed fractional remainder. These four definitions are transcribed from the frozen Hearts module; the proof module does not import that frontier.

Splitting a real number into its integer floor and fractional part gives the drift formula and the left-open, right-closed remainder window. The floor increment lies between one and two because 1<phi<2. Subtracting psi then turns those two integer increments into phi and phi squared, respectively.

This is the Appendix III correction of W-C1. The superseded distance pair involving sqrt(5)+phi-2 and sqrt(5)+phi-1 is not asserted. The final equality records the requested beta(2)-beta(1)=phi anchor.

Pinned Mathlib and the repository were searched before proving. Mathlib supplies the floor, fractional-part, and golden-ratio component laws, but neither source contains this observer-specific conjunction.

References

• Truth anchor: D5/S1/Deficit/Beatty/GoldenObserverRoute.golden_observer_route_w_c1