vec4_three
plain-language theorem explainer
The index-3 slot of the named four-vector constructor equals its fourth real argument. Anyone evaluating null probes or quadratic forms on Fin 4 cites this simp fact. The proof is a one-line rewrite that unfolds the nested if-chain and discharges three decidable inequalities.
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(3)=d$.
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.
Four-vectors are coded as maps $\mathrm{Fin},4\to\mathbb{R}$. The constructor vec4 packages four reals into such a map by a nested if-chain on the index: slot 0 gets $a$, slot 1 gets $b$, slot 2 gets $c$, and every remaining index (here only 3) gets $d$. This lemma is the component projection at index 3.
proof idea
One-line wrapper. Rewrite by the definition of the four-vector constructor, then apply if_neg three times. Each negation is discharged by decide on the concrete inequalities $3\neq 0$, $3\neq 1$, $3\neq 2$ in Fin 4, leaving the final else-branch $d$.
why it matters
Component projections for the named four-vector are the elementary scaffolding of the Clausius-to-Einstein hinge. Null probes, the Minkowski quadratic form, and the pointwise-equality-implies-null-cut lemma all evaluate vectors at concrete Fin-4 indices; this simp lemma keeps those evaluations definitionally clean.
No downstream theorem currently lists it as a direct dependency, and the module deliberately stays clear of the refuted ledger-deficit bridge: it does not build horizons, identify heat with stress-energy, or fix the free scalar. Within Recognition Science gravity work it is pure linear-algebra hygiene supporting the algebraic shape of the Einstein equation from all-null Clausius balance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.