The Orthogonal Witness Theoremthe OG theorem · de Sitter as the closed universe

A sphere that breathes

Let the whole of space be a three-sphere $S^3$, and let it live inside a flat hyperspace $H^4 = \mathbb{R}^4$ as the set of points at distance $a$ from the origin. Let $a$ change with time. We witness that motion through time — three dimensions of space, plus one of time — and the question is how much room it takes to hold the whole thing as a single object, and who could stand where to see it.

This is not a new toy. A three-sphere of radius $a(t)$ carried by a flat $\mathbb{R}^4$, breathing in time, is exactly the closed Friedmann–Lemaître universe — the cosmology of positive spatial curvature, written

where $d\Omega_3^2$ is the round metric on the unit three-sphere. The intuition that "four dimensions plus time make five" turns out to be precise, and the precise version is the theorem of this chapter.

The breathing sphere is de Sitter space

Choose the de Sitter radius $a(\tau)=\ell\cosh(\tau/\ell)$. Then the breathing three-sphere is not merely like a hypersurface in five dimensions — it is the unit hyperboloid of five-dimensional Minkowski space $\mathbb{R}^{1,4}$, under the explicit map

The constraint holds identically, using $|\omega|^2=1$ and $\cosh^2-\sinh^2=1$:

Pull the flat Minkowski metric $\eta=\mathrm{diag}(-1,1,1,1,1)$ back through this map. The differentials are $dX^0=\cosh\tfrac{\tau}{\ell}\,d\tau$ and $dX^i=\sinh\tfrac{\tau}{\ell}\,\omega^i\,d\tau + \ell\cosh\tfrac{\tau}{\ell}\,d\omega^i$; since $\sum_i\omega^i d\omega^i=\tfrac12 d(|\omega|^2)=0$ and $\sum_i(d\omega^i)^2=d\Omega_3^2$,

That is the closed FRW line element exactly, with scale factor $a(\tau)=\ell\cosh(\tau/\ell)$. The pullback carries no error term — verified here by exact symbolic computation, the difference against the target metric being the zero matrix.

Three, four, five — and the seat above

The witness that certifies is a level, not a dimension

There is a second, honest theorem in the neighbourhood, and it is the one that makes the word witness earn its keep — but it is not geometric. To certify the truth of the history, rather than merely embed it, you cannot stand inside it. This is not Gödel (who is about a system proving its own consistency); it is Tarski's undefinability of truth: no predicate internal to a theory can decide that theory's own truth, and the truth-witness lives in a strictly stronger metalanguage.

Its quantum instantiation is real physics: the Frauchiger–Renner (2018) and Local Friendliness (2020) no-go theorems prove that an observer cannot be consistently modelled as a subsystem of the very quantum state they measure. The witness is never inside the wavefunction it collapses. That is the rigorous version of "the witness sits outside" — and it is a strict meta-level, not a further axis of space.

What the theorem does and does not say

The whole result lives or dies on not welding two different steps into one seductive sentence. There is a +1 spatial dimension, from three to four to five — real, forced, orthogonal, and proven by the embedding. And there is a +1 meta-level, the vantage that certifies — real, forced, but not a dimension at all. "A six-dimensional observer proves the five-dimensional universe" fuses them, and that specific sentence is false: for maximally symmetric de Sitter the five-dimensional ambient already contains the completed history, so nothing geometric forces a sixth dimension.

The checkable core of Leg 1

The full tensor pullback is an assertion about manifolds; its scalar heart, however, is finite real algebra and sits inside a proof assistant cleanly. We set the hyperboloid constraint, the proper-time identity $g_{\tau\tau}=-1$, and the de Sitter throat $a(\tau)\ge\ell$ — the sphere never collapses to a point; it bounces at radius $\ell$.

-- de Sitter scale factor and the timelike ambient coordinate
noncomputable def a  (ℓ τ : ℝ) : ℝ := ℓ * Real.cosh (τ / ℓ)
noncomputable def X0 (ℓ τ : ℝ) : ℝ := ℓ * Real.sinh (τ / ℓ)

-- Leg 1 · the image lies on the unit hyperboloid  −(X⁰)² + a² = ℓ²
theorem on_hyperboloid (ℓ τ : ℝ) :
    -(X0 ℓ τ) ^ 2 + (a ℓ τ) ^ 2 = ℓ ^ 2 := by
  have h : Real.cosh (τ / ℓ) ^ 2 - Real.sinh (τ / ℓ) ^ 2 = 1 :=
    Real.cosh_sq_sub_sinh_sq (τ / ℓ)
  have expand : -(X0 ℓ τ)^2 + (a ℓ τ)^2
      = ℓ^2 * (Real.cosh (τ/ℓ)^2 - Real.sinh (τ/ℓ)^2) := by
    simp only [X0, a]; ring
  rw [expand, h]; ring

-- Leg 1 · τ is proper time: the τ–τ metric component is −1
theorem proper_time (τ ℓ : ℝ) :
    -(Real.cosh (τ / ℓ)) ^ 2 + (Real.sinh (τ / ℓ)) ^ 2 = -1 := by
  have h := Real.cosh_sq_sub_sinh_sq (τ / ℓ)
  linarith

-- Leg 1 · the throat: for ℓ ≥ 0 the radius never drops below ℓ (a bounce)
theorem radius_has_throat (ℓ τ : ℝ) (hℓ : 0 ≤ ℓ) : ℓ ≤ a ℓ τ := by
  have h : (1 : ℝ) ≤ Real.cosh (τ / ℓ) := Real.one_le_cosh (τ / ℓ)
  have hprod : 0 ≤ ℓ * (Real.cosh (τ / ℓ) - 1) := mul_nonneg hℓ (by linarith)
  simp only [a]; nlinarith [hprod]

-- the witness direction is the normal bundle: codimension exactly one
theorem witness_codimension : 5 - 4 = 1 := rfl

The first-person witness — the space of possibility — is developed on its own terms in the companion chapter of the Omega book. Here the theorem stands alone; there the seat is taken.

1. de Sitter, W. (1917). On the curvature of space. Proc. KNAW 20. (The hyperboloid $-(X^0)^2+\sum(X^i)^2=\ell^2$ in $\mathbb{R}^{1,4}$.)
2. Hawking, S. W. & Ellis, G. F. R. (1973). The Large Scale Structure of Space-Time. Cambridge University Press. (de Sitter and closed FRW geometry.)
3. Nash, J. (1956). The imbedding problem for Riemannian manifolds. Ann. of Math. 63. (Isometric embedding and codimension.)
4. Tarski, A. (1936). Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1. (Undefinability of truth.)
5. Frauchiger, D. & Renner, R. (2018). Quantum theory cannot consistently describe the use of itself. Nature Communications 9, 3711.
6. Bong, K.-W. et al. (2020). A strong no-go theorem on the Wigner's friend paradox (Local Friendliness). Nature Physics 16, 1199–1205.