costGradient_linear_basis
plain-language theorem explainer
The free ℂ-linear extension of a classical cost-gradient map agrees with that map on standard basis vectors. Anyone assembling T2 (cost-gradient functoriality under superposition) cites this basis identity. The proof is a one-line simplification that unfolds the extension definition.
Claim. Let $\iota,\kappa$ be types with decidable equality on $\iota$, and let $g:\iota\to(\kappa\to_0\mathbb{C})$ be any classical map into finitely supported complex configurations. Then the free $\mathbb{C}$-linear extension of $g$ satisfies $\widehat{g}(e_\alpha)=g(\alpha)$ for every basis index $\alpha\in\iota$, where $e_\alpha$ is the standard basis vector (unit mass at $\alpha$).
background
This module anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel. T1 treats the eight-tick recognition register Signal8 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 the cost-gradient channel: any classical map from density configurations to gravity configurations extends uniquely to a ℂ-linear operator on the free modules they generate.
The free module is realized by finitely supported functions $\kappa\to_0\mathbb{C}$. The linear extension is the unique LinearMap that interpolates a classical assignment $g$ on basis elements. Recognition cost itself appears upstream in several guises (J-cost on ratios, multiset totals under ratio weights, derived costs of multiplicative recognizers); here only the linear-algebraic skeleton of the gradient response is needed.
No new RS-internal axioms are introduced: the argument reuses the complex structure and recognition-operator foundations already forced earlier in the chain.
proof idea
Term-mode one-liner. Unfolding costGradientLinearExtension makes the claim definitional: by construction the free linear extension evaluates on Finsupp.single α 1 to the classical value g α. A single simp closes the goal. No external lemmas beyond the definition are required.
why it matters
This is the basis-agreement clause of T2 (cost-gradient functoriality under superposition). Downstream it is packaged as basis_agreement inside the canonical inhabitant of CostGradientFunctoriality, together with the extension map and the uniqueness-on-basis lemma. Physically, once the ledger update is extended from matter alone to a matter-plus-gravitational channel, the cost-gradient response must be this unique linear extension rather than a nonlinear classical readout; the mathematical identity is unconditional, while the physical reading is MODEL-tagged.
In the broader Recognition framework the result sits under the complex Hilbert carrier forced for the eight-tick register (T7 octave structure, complex structure forcing). It does not itself invoke J-uniqueness, φ, or the mass ladder, but it is the linear-algebraic hinge that lets classical gravity configurations ride on superposed ledger states without breaking ℂ-linearity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.