costGradient_linear_add
plain-language theorem explainer
The free cost-gradient extension is additive on finitely supported ledger configurations: the image of a sum equals the sum of the images. Anyone assembling T2 (cost-gradient functoriality under superposition) cites this as the addition half of linearity. The proof is a one-line appeal to the LinearMap additivity of the free extension constructed by Finsupp.lift.
Claim. Let $g$ send density labels to finitely supported complex gravity configurations. Write $\hat{g}$ for the unique $\mathbb{C}$-linear extension of $g$ to finitely supported complex combinations of density labels. Then for all such combinations $x,y$, $\hat{g}(x+y)=\hat{g}(x)+\hat{g}(y)$.
background
This module anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel: T1 (ledger superposition on the eight-tick signal carrier) and T2 (cost-gradient functoriality under superposition). T2 says any classical map from definite density configurations to gravity configurations extends uniquely to a $\mathbb{C}$-linear operator on the free modules they generate; the physical reading is that the cost-gradient response in a matter-plus-gravity channel must be that linear extension, not a nonlinear classical readout.
The upstream definition builds that extension by the universal property of free linear maps: given $g$ from density labels into finitely supported complex gravity data, Finsupp.lift produces a canonical $\mathbb{C}$-linear map $\hat{g}$ with $\hat{g}|\alpha\rangle = g\alpha$ on basis elements. Because the result is packaged as a LinearMap, additivity and scalar homogeneity are already part of the structure; this declaration records the addition law explicitly.
No new Recognition Science axioms are introduced; the argument reuses the foundation modules on the recognition operator, Schrödinger derivation, and forced complex structure.
proof idea
One-line term proof. The free extension is already a LinearMap over $\mathbb{C}$, so its built-in map_add field applied to the two configurations yields the identity. No separate algebraic expansion or induction on support is required.
why it matters
Inside T2, linearity splits into addition and scalar multiplication; the doc-comment states this addition clause is recorded explicitly for use in T3. Together with the companion scalar-multiplication statement and the basis-identity for the free extension, it makes the cost-gradient response a genuine $\mathbb{C}$-linear functor on superposed ledger states rather than a pointwise classical readout.
That is the mathematical half of the paper's claim that coherent superpositions of density configurations carry a unique linear gravity channel. The module ties this to T1: once the eight-tick recognition update preserves the Hilbert structure on Signal8, the gravity side must extend linearly if the joint matter-plus-channel dynamics is to stay inside the same linear framework. The theorem itself is unconditional; only the physical identification of the classical map $g$ with a cost-gradient is tagged MODEL.
No downstream dependents are wired in the current graph, so this lemma is presently a named building block rather than a leaf of a larger proved chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.