costGradient_linear_smul
plain-language theorem explainer
The free ℂ-linear extension of a classical density-to-gravity map is homogeneous: ĝ(a·x) = a·ĝ(x) for every scalar a and finitely supported ledger state x. Cite this for the scalar half of T2 cost-gradient functoriality under superposition in Gravity IV. Proof is a one-line appeal to LinearMap.map_smul on the Finsupp lift.
Claim. Let $g:\iota\to(\kappa\to_0\mathbb{C})$ be any classical map from density labels to finitely supported complex gravity configurations. Write $\hat g$ for its free $\mathbb{C}$-linear extension on finitely supported ledger states. Then for every $a\in\mathbb{C}$ and every $x\in(\iota\to_0\mathbb{C})$, $\hat g(a\cdot x)=a\cdot\hat g(x)$.
background
Gravity IV anchors two load-bearing theorems. T1 makes the recognition carrier Signal8 a complex Hilbert space whose one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of definite ledger configurations are physical. T2 concerns cost-gradient functoriality: any classical map from definite density configurations to gravity configurations extends uniquely to a ℂ-linear operator on the free modules those bases generate.
The extension itself is costGradientLinearExtension g, defined as Finsupp.lift of g, hence a map $(\iota\to_0\mathbb{C})\to_{\ell[\mathbb{C}]}(\kappa\to_0\mathbb{C})$. By construction it agrees with g on basis elements (the basis-identity sibling). The present statement is scalar homogeneity of that operator.
The module reuses Foundation.SchrodingerDerivation, RecognitionOperator, and ComplexStructureForcing and introduces no new RS-internal axioms. The mathematical theorem is unconditional; the physical reading that the gravitational channel must use this linear extension rather than a nonlinear classical readout is tagged MODEL.
proof idea
One-line term proof. The definition of the free extension is already a LinearMap (Finsupp.lift), so it exposes the structure field map_smul. Instantiating that field at the scalar a and the finsupp vector x yields the identity at once. No case split, no induction, no extra lemmas.
why it matters
This is the scalar-multiplication clause of T2 (linearity) in Gravity from Recognition IV: The Quantum Channel. Paired with the additivity sibling it completes the statement that the cost-gradient response on superposed ledger states is exactly the unique free linear extension of the classical map, not an ad-hoc nonlinear readout.
Parent packaging in-module includes the universal-property definition of the extension, its basis identity, and the LedgerSuperpositionTheorem cluster for T1. The graph currently lists no external used-by edges, so the lemma is a local T2 building block. Framework contact is indirect: complex structure forcing and the eight-tick Hilbert carrier (foundation imports tied to T7/T8) supply the ℂ-linear setting; the argument itself is pure free-module algebra and does not invoke J-uniqueness, the RCL, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.