costGradientLinearExtension
plain-language theorem explainer
Canonical free ℂ-linear extension of a classical map from density labels to finitely supported gravity configurations. Anyone citing T2 (cost-gradient functoriality under superposition) uses this operator: it is the unique linear map agreeing with the classical readout on basis states. The body is a one-line application of Mathlib's free-module lift Finsupp.lift.
Claim. Given index types $\iota$ and $\kappa$ (with decidable equality on $\iota$) and a classical map $g:\iota\to(\kappa\to_0\mathbb{C})$ from definite density labels to finitely supported complex gravity configurations, there is a canonical $\mathbb{C}$-linear map $\hat g:(\iota\to_0\mathbb{C})\to_\ell(\kappa\to_0\mathbb{C})$ extending $g$ on basis elements: $\hat g\,|\alpha\rangle=g(\alpha)$ for every $\alpha\in\iota$.
background
Gravity IV formalizes two load-bearing claims of the paper Gravity from Recognition IV: The Quantum Channel. T1 treats the recognition carrier Signal8 as a complex Hilbert space whose one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of definite ledger states are physical. T2 concerns the cost-gradient channel that couples matter densities to gravity configurations.
The classical side is a map $g$ from density labels $\iota$ into finitely supported complex configurations on gravity labels $\kappa$ (written $\kappa\to_0\mathbb{C}$). Superpositions live in the free ℂ-module $\iota\to_0\mathbb{C}$ of finitely supported formal combinations of density labels. The universal property of free modules supplies a unique ℂ-linear extension of any set-map out of the basis.
The module reuses Foundation.SchrodingerDerivation, RecognitionOperator, and ComplexStructureForcing; no new RS-internal axioms are introduced. Physical reading of the extension as the forced cost-gradient response is tagged MODEL; the linear-algebra statement itself is unconditional.
proof idea
One-line definitional wrapper. The body is exactly Mathlib's Finsupp.lift (κ →₀ ℂ) ℂ ι g, which is the standard free-module universal property: any function from the index type ι into a ℂ-module (here the finitely supported maps κ →₀ ℂ) extends uniquely to a ℂ-linear map out of ι →₀ ℂ. No custom tactics or RS lemmas are invoked; the type signature already records that the result is a LinearMap.
why it matters
This definition is the constructive core of T2 (cost-gradient functoriality under superposition). Downstream, costGradientFunctoriality packages it as the extend field of the CostGradientFunctoriality structure, together with basis agreement and uniqueness. The sibling lemmas costGradient_linear_basis, costGradient_linear_add, and costGradient_linear_smul discharge the three elementary identities needed later (basis identity, additivity, scalar homogeneity), the last two recorded explicitly for use in T3.
Framework role: once T1 has made superpositions of ledger states physical, any extension of the linear ledger update from matter alone to a matter-plus-gravitational channel must send the cost-gradient response through this unique linear extension rather than a nonlinear classical readout. That is the mathematical content of T2; the physical identification remains MODEL-tagged. It sits downstream of the complex structure forcing that supplies the ℂ-module structure on the recognition carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.