Vec4
plain-language theorem explainer
A bare four-component real vector (t,x,y,z) used as the coordinate carrier for the module’s minimal metric interface. Anyone proving light-cone identities from RS units cites it as the domain of the Minkowski pairing. There is no proof: it is a plain structure with four ℝ fields.
Claim. A four-vector is a tuple $v = (t,x,y,z)$ with $t,x,y,z \in \mathbb{R}$, written componentwise as time and three spatial coordinates.
background
The module MetricFromUnitsCert is a non-scaffold milestone on the Ledger ⇒ Metric bridge. It defines a minimal 4D metric interface (symmetric bilinear evaluation), instantiates Minkowski form at a speed parameter $c$, and proves the null condition for the RS anchor $(\tau_0,\ell_0,0,0)$ from the cone-bound identity $c\cdot\tau_0=\ell_0$. No Relativity/Geometry imports are used.
Vec4 is the coordinate type on which that interface acts. Downstream, Metric4 packages an evaluation map Vec4 → Vec4 → ℝ plus a symmetry axiom; minkowskiEval implements signature $(-c^2,+1,+1,+1)$; normSq is the induced quadratic form $g(v,v)$. Anchors are extracted from RSUnits as the vector $(\tau_0,\ell_0,0,0)$.
proof idea
No proof body. The declaration is a four-field structure on ℝ (time plus three spatial components). Downstream definitions pattern-match on the fields; lemmas such as minkowskiEval_symm unfold the bilinear form and close by ring.
why it matters
Vec4 is the carrier type for the entire MetricFromUnitsCert stack. Metric4, minkowskiEval, minkowskiEval_symm, normSq, and anchorsVec all take or return it. The module’s goal is the light-cone/null identity for the RS anchor under Minkowski evaluation, a first concrete step from ledger units toward a metric without importing a full relativity geometry library. In the broader Recognition framework this sits under verification of the units-to-geometry bridge (c from RS units, eight-tick and D=3 already forced upstream), not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.