Machine-rendered statements

The three headline targets of the development, each on its own page. Every result is machine-translated from the Lean 4 / Mathlib source by the project tool (lean_track latex), which walks the delaborated syntax tree of each declaration. The content is verbatim; only the presentation is editorial — leading universal quantifiers and type ascriptions are factored out (free variables are implicitly universally quantified: $x$ ranges over spacetime points, indices $\mu,\nu$ over $\{0,1,2,3\}$, $v$ over tangent vectors), each statement leads with the author’s explanation, the conclusion follows in display math, the load-bearing hypotheses are shown, and routine conditions are summarized by count. To explore the full dependency network behind these results, see the theorem browser.

GR field equations

Target 3 — QIQT-H’s conditional, free-field Einstein-form equation  (15 statements)

Born rule

Target 1 — the Born rule: reductions and a no-go  (13 statements)

Lorentz covariance

Target 2 — Lorentz covariance of the selection  (11 statements)