costGradientFunctoriality
plain-language theorem explainer
Canonical T2 witness packaging free ℂ-linear extension of classical density-to-gravity maps, basis agreement, and uniqueness on the finsupp basis. Gravity-from-Recognition readers cite it as the inhabited Cost-Gradient Functoriality structure. Construction is a three-field assembly of the already-proved extension, basis identity, and uniqueness lemmas.
Claim. For index types $\iota$ and $\kappa$ with decidable equality on $\iota$, there is a cost-gradient functoriality witness: a map sending each classical $g:\iota\to(\kappa\to_0\mathbb{C})$ to a $\mathbb{C}$-linear operator $\hat g:(\iota\to_0\mathbb{C})\to_{\ell[\mathbb{C}]}(\kappa\to_0\mathbb{C})$ that agrees with $g$ on basis vectors $\lvert\alpha\rangle$, and any two linear maps agreeing on the basis are identical.
background
Module Gravity IV anchors two load-bearing results of Gravity from Recognition IV: The Quantum Channel. T1 (Ledger Superposition) makes Signal8 a complex Hilbert carrier whose one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of ledger configurations are physical. T2 (Cost-Gradient Functoriality Under Superposition) is the companion: any classical map from definite density configurations to gravity configurations extends uniquely to a ℂ-linear operator on the free modules they generate.
The master witness structure records three pieces: an explicit free linear extension (via Finsupp.lift), agreement of that extension with the classical map on basis elements, and uniqueness of any two ℂ-linear maps that agree on the finsupp basis. The physical reading is that, 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 mathematics is unconditional, the interpretation tagged MODEL.
Upstream, the extension is the free-module universal property, the basis identity is a one-line simplification of that lift, and uniqueness is Finsupp.lhom_ext'.
proof idea
Pure structure inhabitant. The extend field is set to the free linear extension costGradientLinearExtension (i.e. Finsupp.lift). The basis_agreement field is discharged by the already-proved basis identity theorem. The unique_on_basis field is discharged by the uniqueness theorem that any two ℂ-linear maps agreeing on singles are equal. No new reasoning; three prior results are wired into the three structure fields.
why it matters
This is the canonical T2 package in the Gravity IV module. Downstream, costGradientFunctoriality_inhabited simply wraps it to obtain Nonempty (CostGradientFunctoriality ι κ), the inhabitedness form used as a theorem-shaped anchor. Together with T1 (ledger superposition preserved by the recognition update), it supplies the formal half of the paper's claim that gravitational response under superposition is forced to be the unique linear extension of the classical cost-gradient map. No new RS axioms are introduced; the argument reuses Foundation Schrödinger derivation, RecognitionOperator, and ComplexStructureForcing. It does not itself touch the forcing chain T0–T8 or the RCL, but it is the gravity-side consequence of the complex Hilbert structure those foundations enable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.