vec4_one
plain-language theorem explainer
Evaluating a named four-vector at Fin-index 1 returns its second real component. Anyone assembling finite Minkowski-null probes in the Clausius–Einstein algebraic hinge will cite this simp fact. The proof is a one-line rewrite through the piecewise definition of the four-vector.
Claim. For all $a,b,c,d\in\mathbb{R}$, if $v:\mathrm{Fin}\,4\to\mathbb{R}$ is the four-vector with components $(a,b,c,d)$, then $v(1)=b$.
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 left free.
A four-vector with named components is the basic probe object. It is the map $\mathrm{Fin},4\to\mathbb{R}$ sending $0\mapsto a$, $1\mapsto b$, $2\mapsto c$, and otherwise $d$. Index-1 access is the second spatial (or first non-time) slot in that ordering, used when building null directions and quadratic contractions against the Minkowski form.
proof idea
One-line wrapper: unfold the piecewise definition of the four-vector, discharge the $i\neq 0$ branch by decide, then take the $i=1$ branch by reflexivity. No external lemmas beyond the definition itself.
why it matters
This is local plumbing for the algebraic Clausius-to-Einstein hinge. Downstream null-cut and quadratic-contraction lemmas need reliable component extraction under simp; the sibling zero/two/three accessors play the same role for the other slots. The module deliberately stays independent of any ledger-deficit bridge: it does not build horizons, identify heat with stress-energy, or fix the free metric scalar. Within Recognition Science gravity work it supports only the finite linear-algebra step that makes an all-null Clausius balance look like Einstein's equation up to that scalar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.