Metric4
plain-language theorem explainer
Minimal 4D metric interface: a real bilinear pairing on spacetime 4-vectors that is required only to be symmetric. Downstream Minkowski constructions and the quadratic form (norm squared) are typed against this record. There is no proof body; it is a structure definition packaging the evaluation map with its symmetry axiom.
Claim. A 4D metric is a pair $(g,\mathrm{symm})$ where $g:V_4\times V_4\to\mathbb{R}$ is a real-valued evaluation on 4-vectors $V_4=\{(t,x,y,z)\}$ and $\mathrm{symm}$ asserts $g(v,w)=g(w,v)$ for all $v,w\in V_4$.
background
The module is a non-scaffold milestone on the Ledger ⇒ Metric bridge: define a thin 4D metric interface, instantiate Minkowski with speed parameter $c$, and prove the light-cone/null condition for the RS anchor $(\tau_0,\ell_0,0,0)$ via $c\cdot\tau_0=\ell_0$. No Relativity/Geometry imports are used.
Four-vectors are the plain record $V_4$ with real components $(t,x,y,z)$. The metric interface keeps only what the certificate needs: an evaluation pairing $g(v,w)\in\mathbb{R}$ and the symmetry law $g(v,w)=g(w,v)$. Full bilinearity, nondegeneracy, and Lorentz signature are not part of this type; they appear later when Minkowski is plugged in.
proof idea
No proof. The declaration is a structure: a field eval of type $V_4\to V_4\to\mathbb{R}$ together with a field symm asserting symmetry of that pairing. Instantiation (e.g. Minkowski at speed $c$) supplies both fields; lemmas such as symmetry of the Minkowski evaluator discharge symm by unfolding and ring.
why it matters
This is the typed carrier for the module's Minkowski instance and induced quadratic form. Downstream, the Minkowski metric at speed $c$ is built as { eval := minkowskiEval c, symm := minkowskiEval_symm c }, and normSq g v := g.eval v v is the quadratic form used for null/light-cone checks on the RS anchor vector $(\tau_0,\ell_0,0,0)$.
In the Recognition framework this is the first concrete step of the Ledger ⇒ Metric checklist: units and the cone-bound identity $c\cdot\tau_0=\ell_0$ determine a Minkowski pairing without importing a full differential-geometry stack. It sits under verification of metric structure forced by RS units (with $c=1$ in RS-native units), not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.