CostGradientFunctoriality
plain-language theorem explainer
Packages the three clauses of cost-gradient functoriality under superposition: a classical map on basis labels extends to a unique ℂ-linear operator between free finitely supported modules. Cited by anyone invoking T2 of Gravity from Recognition IV (the quantum channel). As a structure, it is pure interface; the canonical inhabitant supplies the concrete extension and uniqueness proofs.
Claim. For index types $\iota$ and $\kappa$ (with decidable equality on $\iota$), cost-gradient functoriality is the data of (i) an extension map sending any family $g:\iota\to(\kappa\to_0\mathbb{C})$ to a $\mathbb{C}$-linear map $(\iota\to_0\mathbb{C})\to_{\ell}(\kappa\to_0\mathbb{C})$, (ii) agreement of that extension with $g$ on Dirac basis vectors $e_\alpha$, and (iii) uniqueness: any two linear maps that agree on all $e_\alpha$ are identical.
background
The module Gravity IV anchors two load-bearing results of Gravity from Recognition IV: The Quantum Channel. T1 treats the eight-component recognition carrier as a complex Hilbert space whose one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of ledger configurations are physical. T2 addresses the gravitational readout: any classical map from density configurations to gravity configurations must lift uniquely through free linear extension when the ledger is allowed to superpose.
Finitely supported functions $\iota\to_0\mathbb{C}$ are the free ℂ-module on the basis ${e_\alpha}$. A classical assignment $g$ on basis labels therefore determines at most one linear operator on superpositions; the structure records existence of that extension, pointwise agreement on basis vectors, and the uniqueness clause that forces the lift. The physical reading (MODEL-tagged) is that the cost-gradient response in any matter-plus-gravity channel cannot be a nonlinear classical readout once superposition is admitted.
No new RS-internal axioms are introduced; the construction reuses the complex structure and recognition-operator foundations already forced upstream.
proof idea
No proof body: this is a structure definition bundling three fields. extend is the existence witness (a map from classical families to linear operators). basis_agreement requires the extension to recover $g\alpha$ on each Dirac mass $Finsupp.single,\alpha,1$. unique_on_basis is the free-module uniqueness statement: linear maps determined by their values on the standard basis coincide. Concrete inhabitants are supplied downstream by wiring an explicit free linear extension together with its basis and uniqueness lemmas.
why it matters
This is the T2 master witness named in the module doc: the complete formal content of cost-gradient functoriality under superposition. Downstream, the canonical inhabitant fills the three fields with the explicit free linear extension and its basis/uniqueness proofs, and the inhabited theorem records Nonempty of the structure for any index pair.
In the paper chain, T2 sits beside T1 (ledger superposition). Together they justify treating gravitational cost-gradient response as the unique linear channel on superposed ledger states rather than a classical nonlinear map. The mathematical claim is unconditional; only the physical identification is MODEL-tagged. Framework-wise it sits in the gravity layer that consumes the forced complex structure and recognition update, without reopening T5–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.