evalAt
plain-language theorem explainer
The i-th coordinate functional on the eight-component complex signal space, as a ℂ-linear map. Gravity Track 2.C proofs that factor the joint matter-channel substrate cite it as the basic readout that peels one tensor factor. Definition is a one-line alias of Mathlib coordinate projection.
Claim. For each index $i \in \{0,\ldots,7\}$, the evaluation map $v \mapsto v(i)$ is a $\mathbb{C}$-linear functional $\mathrm{Signal}_8 \to_{\mathbb{C}} \mathbb{C}$, where $\mathrm{Signal}_8 = (\mathrm{Fin}\,8 \to \mathbb{C})$.
background
Track 2.C lifts the single-factor amplitude-linear dichotomy on Signal8 to the joint matter-plus-channel substrate JointSubstrate := Signal8 ⊗[ℂ] Signal8. Here Signal8 is the eight-tick complex amplitude space (the RS octave period $2^3$), so states are functions Fin 8 → ℂ.
Coordinate evaluation is the elementary linear functional that reads one tick. The module builds pure-tensor factorizations of joint operators and needs a linear way to contract one factor against a fixed coordinate of the other. Mathlib supplies LinearMap.proj on product/function spaces; this definition names that projection in the gravity channel vocabulary.
(The depends-on edges to unrelated proj maps in cosmology and quotient-selection are name collisions, not mathematical inputs.)
proof idea
One-line definition: bind the Mathlib coordinate projection LinearMap.proj i at the given tick index. No proof obligations; the type Signal8 →ₗ[ℂ] ℂ is exactly that of the i-th component map on Fin 8 → ℂ.
why it matters
Local scaffolding for the joint-substrate lift. Downstream, extractFirst i and extractSecond i compose this functional with TensorProduct.map and the left/right unitors to pull one pure-tensor factor out of JointSubstrate, scaled by the i-th coordinate of the other factor. Those extractors feed the Track 2.C theorems: if a joint operator factorizes on pure tensors and the channel (resp. matter) side is nontrivial at some coordinate, the matter (resp. channel) response is amplitude-linear; under bilateral nontriviality both sides are; and a density-only channel response collapses to zero when matter coupling is nontrivial.
That last step is the binary-tensor closure of paper IV T2 under the joint model. Full upgrade from MODEL to THEOREM still needs the joint recognition operator to be ℂ-linear via the Schrödinger-linearity lift. The eight-tick index set is the T7 octave landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.