Gravity Ledger Superposition Cost Gradient Linear Basis

The linear extension

The declaration costGradient_linear_basis is a theorem in the machine-checked library of formal theorems used by Recognition Science. It states a precise fact about a construction called the linear extension. One can have a rule that assigns a value to each basic item in a collection. The linear extension is the unique way to extend that rule to all finite combinations of those items, so that combining items combines their values in an additive way. The theorem says that this extended rule agrees with the original rule on each basic item: if you apply the extension to a single basic item, you get exactly the value the original rule assigned to it.

This is a standard and unconditional result in linear algebra. It is the universal property of free modules: any map from a basis set extends uniquely to a linear map on the whole space. The theorem is proved in the framework's library without introducing new axioms specific to Recognition Science. It is a formal statement about the mathematics of linear extension, and it holds for any choice of the underlying sets.

In Recognition Science, this theorem is used in a physical model. The framework models a discrete ledger of recognition events, a record of events that the universe keeps. The theorem is part of a broader claim about how the cost-gradient response, the way the cost of a configuration changes, must behave when matter and a gravitational channel are considered together. The physical content is an identification: in any extension of the linear ledger update from matter alone to matter-plus-gravitational-channel, the cost-gradient response must be the unique linear extension, not a nonlinear classical readout. This identification is a modeling choice, not a proved physical law.

The theorem itself does not claim that the physical identification is correct. It does not say that gravity is linear, or that a nonlinear response is impossible. It only establishes the mathematical fact that a linear extension exists and is unique. The physical interpretation, that this linear extension is the right way to describe the cost-gradient response, is explicitly tagged as a model in the framework's own documentation. The theorem is a tool; the model is a decision about how to use it.

/-- **T2 (basis identity).** The linear extension agrees with the
classical map on basis elements. -/
theorem costGradient_linear_basis {ι κ : Type*} [DecidableEq ι]
    (g : ι → (κ →₀ ℂ)) (α : ι) :
    costGradientLinearExtension g (Finsupp.single α (1 : ℂ)) = g α := by
  simp [costGradientLinearExtension]

/-- **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]

/-- The canonical inhabitant of `CostGradientFunctoriality`. -/
def costGradientFunctoriality (ι κ : Type) [DecidableEq ι] :
    CostGradientFunctoriality ι κ where
  extend := costGradientLinearExtension
  basis_agreement := costGradient_linear_basis
  unique_on_basis := costGradient_linear_unique

What this page does not claim

The theorem does not prove that the physical identification is correct. The theorem does not imply that gravity is linear. The theorem does not rule out nonlinear cost-gradient responses.

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: