Gravity Ledger Superposition Cost Gradient Linear Unique

The linear extension

In mathematics, a linear map is determined by what it does to a set of basis vectors. If you know how a transformation acts on each basis element, you know how it acts on every possible combination of them. The theorem costGradient_linear_unique states this principle for a specific class of maps: any two complex-linear operators that agree on every basis vector are identical. The proof is a direct application of the universal property of free linear extension, a standard result in algebra.

Within the Recognition Science framework, the theorem carries physical content. The framework models physical states as a ledger, a discrete record of recognition events. The theorem concerns the cost gradient, the rate at which the ledger's cost changes as its entries vary. The framework proves that when the ledger update is extended from matter alone to matter plus a gravitational channel, the cost-gradient response must be the unique linear extension of the classical map, not a nonlinear readout. This is a functoriality result: the extension respects the algebraic structure of the underlying spaces.

The mathematical theorem is unconditional and machine-checked in the framework's library of formal theorems. The physical interpretation, however, is explicitly tagged as a model choice, not a proved fact about nature. The theorem does not prove that gravity is linear, nor that the cost gradient is linear in reality. It proves that if one accepts the framework's modeling assumptions, then the linear extension is the only possible extension consistent with those assumptions.

The result does not claim that nonlinear classical readouts are impossible, only that they are not the unique extension forced by the framework's structure. It also does not claim that the linear extension is physically realized; that would require additional empirical input. The theorem is a statement about mathematical uniqueness within a specified algebraic setting.

/-- **T2 (uniqueness).** Any two `ℂ`-linear maps that agree on the
finsupp basis agree everywhere. This is the uniqueness half of the
universal property. -/
theorem costGradient_linear_unique {ι κ : Type*} [DecidableEq ι]
    (f₁ f₂ : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ))
    (h : ∀ α : ι, f₁ (Finsupp.single α (1 : ℂ)) = f₂ (Finsupp.single α (1 : ℂ))) :
    f₁ = f₂ := by
  apply Finsupp.lhom_ext'
  intro α
  apply LinearMap.ext
  intro c
  have h1 : Finsupp.single α c = c • Finsupp.single α (1 : ℂ) := by
    ext β
    by_cases hβ : β = α <;> simp [hβ]
  have hα := h α
  have step :
      f₁ (Finsupp.single α c) = f₂ (Finsupp.single α c) := by
    rw [h1, f₁.map_smul, f₂.map_smul, hα]
  show (f₁.comp (Finsupp.lsingle (R := ℂ) α)) c
        = (f₂.comp (Finsupp.lsingle (R := ℂ) α)) c
  simp [Finsupp.lsingle, step]

/-- **T2 master witness.** The complete content of cost-gradient
functoriality under superposition: existence (the explicit linear
extension), agreement on basis, and uniqueness. -/
structure CostGradientFunctoriality (ι κ : Type) [DecidableEq ι] where
  /-- Existence: the linear extension itself. -/
  extend : (ι → (κ →₀ ℂ)) → ((ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ))
  /-- Basis agreement: extension agrees with classical map on basis. -/
  basis_agreement :
    ∀ (g : ι → (κ →₀ ℂ)) (α : ι),
      extend g (Finsupp.single α (1 : ℂ)) = g α
  /-- Uniqueness on basis. -/
  unique_on_basis :
    ∀ (f₁ f₂ : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ)),
      (∀ α : ι, f₁ (Finsupp.single α (1 : ℂ)) = f₂ (Finsupp.single α (1 : ℂ))) →
        f₁ = f₂

What this page does not claim

The theorem does not prove that gravity is linear in physical reality. The theorem does not claim that the linear extension is the physically realized cost gradient. The theorem does not rule out nonlinear classical readouts as a modeling choice.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/LedgerSuperposition.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: