vec4_zero
plain-language theorem explainer
The zeroth component of the named four-vector (a,b,c,d) is a. Anyone writing finite Minkowski-null probes in the Clausius–Einstein algebra cites this as a simp fact. The proof is a one-line unfolding of the piecewise definition of the four-vector.
Claim. For all real $a,b,c,d$, if $v:\mathrm{Fin}\,4\to\mathbb{R}$ is the four-vector with components $(a,b,c,d)$, then $v(0)=a$.
background
The module isolates the finite-dimensional linear algebra behind Jacobson's thermodynamic route to Einstein's equation: equality of two symmetric quadratic forms on every Minkowski-null direction fixes their difference only up to a scalar multiple of the metric. An all-null local Clausius balance therefore has the algebraic shape of the Einstein equation, with the metric term free.
To state those null probes concretely one needs a four-vector with named components. The definition vec4 a b c d is the map $\mathrm{Fin},4\to\mathbb{R}$ sending $0\mapsto a$, $1\mapsto b$, $2\mapsto c$, and everything else to $d$. This lemma records the $i=0$ case of that piecewise definition.
proof idea
One-line wrapper: simp [vec4] unfolds the definition and discharges the i = 0 branch, yielding the component $a$.
why it matters
The lemma is local infrastructure for the algebraic Clausius-to-Einstein hinge. Downstream null-cut and quadratic-form identities (e.g. pointwise equality of forms on null directions implying difference proportional to the metric) need clean component access on $\mathrm{Fin},4$. It does not itself touch the forcing chain (T0–T8), RCL, or the free scalar in front of the metric; it only makes the finite null probes readable. The module is deliberately independent of the refuted ledger-deficit-to-signed-hinge bridge and does not construct horizons or identify heat with stress-energy flux.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.