vec4
plain-language theorem explainer
Named-component constructor for real 4-vectors as maps Fin 4 → ℝ. Gravity analysts cite it when building finite Minkowski-null probes and checking Lorentz TT conditions on the null axis. The body is a four-way case split on the Fin index.
Claim. For $a,b,c,d \in \mathbb{R}$, the four-vector with components $(a,b,c,d)$ is the function $v:\mathrm{Fin}\,4\to\mathbb{R}$ with $v(0)=a$, $v(1)=b$, $v(2)=c$, and $v(3)=d$.
background
The module isolates the finite-dimensional linear algebra behind Jacobson's thermodynamic route to Einstein: if two symmetric quadratic forms agree on every Minkowski-null direction, their difference is a scalar multiple of the metric. That algebraic hinge is kept independent of continuum horizons, heat-flux identifications, and conservation laws that would fix the free scalar.
Four-vectors here are plain maps Fin 4 → ℝ. The Minkowski pairing and null-cone tests live on that type. Named components make null probes (e.g. lightlike axes and their transverse companions) readable in later TT-decomposition lemmas without index gymnastics.
proof idea
Pure definition: a single lambda with nested equality tests on the Fin 4 index, returning the four real arguments in order. No lemmas, no tactics.
why it matters
This is the standard way the gravity analysis builds concrete null probes. Downstream, nullAxisAux is exactly vec4 1 (-1) 0 0; its Minkowski self-dot and cross-dot with the null-axis wave are proved by unfolding and simplifying through this constructor. The same pattern feeds Euclidean momentum-squared checks, Lorentz-transverse projector counterexamples on the null axis, and the TT-cross / TT-plus certificates that certify Lorentz TT structure. Without a named four-vector sugar, those finite null-axis calculations would be opaque Fin-case walls. It sits inside the Clausius–Einstein algebraic hinge, not the refuted ledger-deficit bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.