costGradient_linear_unique
plain-language theorem explainer
Any two complex-linear maps between finitely supported complex functions that agree on Dirac basis vectors agree everywhere. Gravity-channel authors cite this as the uniqueness half of free linear extension for cost-gradient response. The proof extends agreement from unit spikes to scalar multiples by linearity, then applies the standard Finsupp linear-hom extension lemma.
Claim. Let $\iota$ and $\kappa$ be types with decidable equality on $\iota$. If $f_1,f_2:(\iota\to_0\mathbb{C})\to_{\mathbb{C}}(\kappa\to_0\mathbb{C})$ are $\mathbb{C}$-linear maps such that $f_1(e_\alpha)=f_2(e_\alpha)$ for every basis spike $e_\alpha=\mathrm{single}(\alpha,1)$, then $f_1=f_2$.
background
The module Gravity IV anchors two load-bearing theorems from Gravity from Recognition IV: The Quantum Channel. T1 treats the recognition state space as a complex Hilbert carrier whose one-tick update is linear and inner-product preserving, so coherent superpositions of ledger configurations are physical. T2 concerns cost-gradient functoriality under superposition: any classical map from density configurations to gravity configurations extends uniquely to a $\mathbb{C}$-linear operator on the free modules they generate.
Here the free modules are finitely supported functions $\iota\to_0\mathbb{C}$ and $\kappa\to_0\mathbb{C}$. The Dirac spikes $\mathrm{single}(\alpha,1)$ form the canonical basis. The universal property of free linear extension splits into existence (an explicit linear extension of a basis assignment) and uniqueness (any two linear maps agreeing on that basis coincide). This declaration is the uniqueness half.
No new Recognition Science axioms enter: the argument is pure Mathlib linear algebra on Finsupp modules over $\mathbb{C}$, reused alongside the Schrödinger derivation and recognition-operator foundations already in the stack.
proof idea
Apply Finsupp.lhom_ext' to reduce equality of linear maps to equality after composition with each left-single embedding $\alpha\mapsto\mathrm{lsingle},\alpha$. For fixed $\alpha$, apply LinearMap.ext on the scalar $c\in\mathbb{C}$.
The key algebraic identity is $\mathrm{single}(\alpha,c)=c\cdot\mathrm{single}(\alpha,1)$, proved by pointwise case split on whether the index equals $\alpha$. Homogeneity of both maps plus the hypothesis that they agree on unit spikes then yields agreement on every scaled spike. Simplifying the compositions with lsingle finishes the goal.
No Recognition-specific lemmas are invoked; the proof is a short tactic walk through standard free-module uniqueness.
why it matters
This is the uniqueness clause of T2 (cost-gradient functoriality under superposition). Downstream it is packaged as the unique_on_basis field of the canonical costGradientFunctoriality witness, alongside the explicit extension and basis-agreement facts. Together those three fields form the T2 master witness: existence, agreement on basis, and uniqueness.
Physically, the claim forces the cost-gradient response in any linear extension of the ledger update from matter alone to matter-plus-gravitational-channel to be the unique free linear extension, not a nonlinear classical readout. The mathematical theorem is unconditional; the physical reading is tagged MODEL in the module doc.
In the broader Recognition chain this sits under Gravity IV rather than the T0–T8 forcing spine, but it inherits the complex structure forced upstream and the linear recognition update from T1 in the same module. It closes the uniqueness gap so superposition of density configurations cannot spawn ambiguous gravitational channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.