vec4_two

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. Local Clausius balance on all null cuts therefore has the algebraic shape of the Einstein equation, with the metric term free.

Four-vectors appear as finite null probes. The helper vec4 packages four reals into a map Fin 4 → ℝ by nested if-then-else on the index: index 0 yields the first argument, 1 the second, 2 the third, and otherwise the fourth. Component lemmas such as this one turn those nested conditionals into simp-normal form so later quadratic-form identities stay readable.

One-line wrapper. Rewrite by the definition of the four-vector map, then discharge the two false branches i = 0 and i = 1 with decide (since the concrete index is 2) and the remaining true branch i = 2 with rfl. No external lemmas beyond the definition itself.

Component extraction is the lowest layer of the finite null-probe calculus used throughout the Clausius–Einstein bridge. Without simp lemmas for each index, every later identity about quadratic contractions on Minkowski-null directions would carry nested if-noise. The module deliberately stops short of horizons, heat–flux identification, continuum focusing, or fixing the free scalar; this lemma only clears the algebraic bookkeeping those later steps would need. No downstream consumers are recorded yet; the lemma sits ready for the null-cut and quadratic-form arguments in the same file.