IndisputableMonolith.Gravity.LedgerSuperposition

   1import Mathlib
   2import IndisputableMonolith.Foundation.RecognitionOperator
   3import IndisputableMonolith.Foundation.SchrodingerDerivation
   4import IndisputableMonolith.Foundation.ComplexStructureForcing
   5
   6/-!
   7# Gravity IV: Ledger Superposition (Theorem 1) and Cost-Gradient Functoriality (Theorem 2)
   8
   9This module supplies the formal anchors for two of the four load-bearing
  10theorems of the paper *Gravity from Recognition IV: The Quantum Channel*:
  11
  12* **T1 (Ledger Superposition).**
  13  The recognition state space `Signal8` is a complex Hilbert carrier;
  14  the one-tick recognition update `cyclic_shift` is `ℂ`-linear and
  15  preserves the canonical `inner8` inner product. Therefore coherent
  16  superpositions of definite ledger configurations are physical states
  17  and are preserved by the recognition update.
  18
  19* **T2 (Cost-Gradient Functoriality Under Superposition).**
  20  Any classical map `g : DensityConfig → GravityConfig` extends uniquely
  21  to a `ℂ`-linear operator on the free `ℂ`-modules generated by the
  22  basis sets, by the universal property of free linear extension. The
  23  physical content is the identification: in any extension of the
  24  linear ledger update from matter alone to matter-plus-gravitational-channel,
  25  the cost-gradient response must be the unique linear extension, not a
  26  nonlinear classical readout. The mathematical theorem is unconditional;
  27  the physical interpretation is tagged MODEL.
  28
  29All proofs reuse `Foundation.SchrodingerDerivation`,
  30`Foundation.RecognitionOperator`, and `Foundation.ComplexStructureForcing`
  31without introducing new RS-internal axioms.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Gravity
  36namespace LedgerSuperposition
  37
  38open IndisputableMonolith.Spectral
  39
  40noncomputable section
  41
  42/-- Local abbreviation: the eight-tick analytic signal carrier
  43`Fin 8 → ℂ`, identified with the canonical
  44`Foundation.ComplexStructureForcing.Signal8`. -/
  45abbrev Signal8 : Type :=
  46  IndisputableMonolith.Foundation.ComplexStructureForcing.Signal8
  47
  48/-- Local abbreviation: the canonical Hermitian inner product on
  49`Signal8`. -/
  50abbrev inner8 (f g : Signal8) : ℂ :=
  51  IndisputableMonolith.Foundation.ComplexStructureForcing.inner8 f g
  52
  53/-! ## Theorem 1: Ledger Superposition -/
  54
  55/-- **T1.i (Linearity).** The recognition update is `ℂ`-linear: it maps
  56linear combinations of ledger configurations to the corresponding linear
  57combinations of evolved configurations. This is
  58`SchrodingerDerivation.schrodinger_linear` repackaged in the ledger
  59superposition language. -/
  60theorem ledger_superposition_preserved
  61    (ψ φ : Signal8) (a b : ℂ) :
  62    cyclic_shift (a • ψ + b • φ) =
  63      a • cyclic_shift ψ + b • cyclic_shift φ :=
  64  IndisputableMonolith.Foundation.SchrodingerDerivation.schrodinger_linear ψ φ a b
  65
  66/-- **T1.i (Finite-sum form).** For a finite family of definite ledger
  67configurations `L : ι → Signal8` and amplitudes `c : ι → ℂ` indexed by a
  68finite set, the recognition update commutes with the finite linear
  69combination. This is the explicit superposition principle for ledger
  70configurations: `R̂ Σ c_α |L_α⟩ = Σ c_α R̂ |L_α⟩`. -/
  71theorem ledger_superposition_finite_sum
  72    {ι : Type*} (s : Finset ι) (c : ι → ℂ) (L : ι → Signal8) :
  73    cyclic_shift (∑ α ∈ s, c α • L α) =
  74      ∑ α ∈ s, c α • cyclic_shift (L α) := by
  75  classical
  76  induction s using Finset.induction_on with
  77  | empty =>
  78      ext t
  79      simp [cyclic_shift]
  80  | @insert α s hα ih =>
  81      have hsum :
  82          (∑ β ∈ insert α s, c β • L β)
  83            = c α • L α + ∑ β ∈ s, c β • L β := by
  84        simp [Finset.sum_insert hα]
  85      rw [hsum,
  86          IndisputableMonolith.Foundation.SchrodingerDerivation.cyclic_shift_add,
  87          IndisputableMonolith.Foundation.SchrodingerDerivation.cyclic_shift_smul,
  88          ih]
  89      simp [Finset.sum_insert hα]
  90
  91/-- **T1.iii (Inner-product preservation).** The recognition update
  92preserves the canonical `inner8` Hermitian inner product. The proof is
  93direct from the definitions of `inner8` and `cyclic_shift`: the cyclic
  94shift permutes the eight summands without changing the value of the
  95sum. -/
  96theorem recognition_update_inner_preserved (f g : Signal8) :
  97    inner8 (cyclic_shift f) (cyclic_shift g) = inner8 f g := by
  98  show IndisputableMonolith.Foundation.ComplexStructureForcing.inner8
  99      (cyclic_shift f) (cyclic_shift g)
 100      = IndisputableMonolith.Foundation.ComplexStructureForcing.inner8 f g
 101  unfold IndisputableMonolith.Foundation.ComplexStructureForcing.inner8 cyclic_shift
 102  rw [Fin.sum_univ_eight, Fin.sum_univ_eight]
 103  simp
 104  ring
 105
 106/-- **T1.iii (Norm preservation).** As a corollary of inner-product
 107preservation, the recognition update preserves the `inner8`-norm
 108squared. -/
 109theorem recognition_update_norm_preserved (f : Signal8) :
 110    inner8 (cyclic_shift f) (cyclic_shift f) = inner8 f f :=
 111  recognition_update_inner_preserved f f
 112
 113/-- **T1 master.** A complete witness that the recognition update is a
 114`ℂ`-linear, inner-product-preserving operator on the ledger Hilbert
 115carrier. This is the formal content of "ledger superpositions are
 116physical and are preserved by recognition evolution." -/
 117structure LedgerSuperpositionTheorem where
 118  /-- (i) Linearity on pairs. -/
 119  linearity :
 120    ∀ (ψ φ : Signal8) (a b : ℂ),
 121      cyclic_shift (a • ψ + b • φ) =
 122        a • cyclic_shift ψ + b • cyclic_shift φ
 123  /-- (i) Linearity on finite sums. -/
 124  linearity_sum :
 125    ∀ {ι : Type} (s : Finset ι) (c : ι → ℂ) (L : ι → Signal8),
 126      cyclic_shift (∑ α ∈ s, c α • L α) =
 127        ∑ α ∈ s, c α • cyclic_shift (L α)
 128  /-- (iii) Inner-product preservation. -/
 129  inner_preserved :
 130    ∀ f g : Signal8,
 131      inner8 (cyclic_shift f) (cyclic_shift g) = inner8 f g
 132  /-- (iii) Norm preservation. -/
 133  norm_preserved :
 134    ∀ f : Signal8, inner8 (cyclic_shift f) (cyclic_shift f) = inner8 f f
 135
 136/-- The canonical inhabitant of `LedgerSuperpositionTheorem`. -/
 137def ledgerSuperpositionTheorem : LedgerSuperpositionTheorem where
 138  linearity := ledger_superposition_preserved
 139  linearity_sum := fun s c L => ledger_superposition_finite_sum s c L
 140  inner_preserved := recognition_update_inner_preserved
 141  norm_preserved := recognition_update_norm_preserved
 142
 143theorem ledgerSuperpositionTheorem_inhabited :
 144    Nonempty LedgerSuperpositionTheorem :=
 145  ⟨ledgerSuperpositionTheorem⟩
 146
 147/-! ## Theorem 2: Cost-Gradient Functoriality Under Superposition
 148
 149The mathematical content is the universal property of free `ℂ`-modules:
 150any function on a basis extends uniquely to a `ℂ`-linear map on the free
 151`ℂ`-module generated by that basis. We package this as a generic
 152`linear_extension` theorem, applicable to any `DensityConfig → GravityConfig`
 153classical mass-density-to-cost-gradient map.
 154
 155The physical interpretation that this linear extension *is* the
 156gravitational response operator on the ledger Hilbert span is a modeling
 157step (tagged MODEL in the paper); the mathematical extension is
 158unconditional.
 159-/
 160
 161/-- The cost-gradient map seen as a function on definite ledger
 162configurations indexed by `ι` (mass densities), valued in
 163`Signal8`-spans indexed by `κ` (gravity configurations). In the BMV
 164two-mass two-branch setup, `ι = κ = Fin 4` indexing the four definite
 165branch states {LL, LR, RL, RR}. -/
 166abbrev DensityConfig (ι : Type*) := ι
 167abbrev GravityConfig (κ : Type*) := κ
 168
 169/-- Free `ℂ`-module on a finite basis, used for the BMV two-qubit setup.
 170We identify `ι →₀ ℂ` with the finite `ℂ`-linear span of basis vectors
 171`{|α⟩ : α ∈ ι}`. -/
 172abbrev FreeC (ι : Type*) [DecidableEq ι] := ι →₀ ℂ
 173
 174/-- **T2 (universal property of free linear extension).** Given any
 175classical map `g : ι → (κ →₀ ℂ)` from definite densities to definite
 176gravity configurations (or `ℂ`-combinations thereof), there exists a
 177canonical `ℂ`-linear map `ĝ : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ)` extending `g` in
 178the sense that `ĝ |α⟩ = g α` for every basis element `α : ι`. -/
 179def costGradientLinearExtension {ι κ : Type*} [DecidableEq ι]
 180    (g : ι → (κ →₀ ℂ)) : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ) :=
 181  Finsupp.lift (κ →₀ ℂ) ℂ ι g
 182
 183/-- **T2 (basis identity).** The linear extension agrees with the
 184classical map on basis elements. -/
 185theorem costGradient_linear_basis {ι κ : Type*} [DecidableEq ι]
 186    (g : ι → (κ →₀ ℂ)) (α : ι) :
 187    costGradientLinearExtension g (Finsupp.single α (1 : ℂ)) = g α := by
 188  simp [costGradientLinearExtension]
 189
 190/-- **T2 (linearity, addition).** The cost-gradient extension respects
 191addition; this is automatic because the extension is a `LinearMap`, but
 192the statement is recorded explicitly for use in T3. -/
 193theorem costGradient_linear_add {ι κ : Type*} [DecidableEq ι]
 194    (g : ι → (κ →₀ ℂ)) (x y : ι →₀ ℂ) :
 195    costGradientLinearExtension g (x + y) =
 196      costGradientLinearExtension g x + costGradientLinearExtension g y :=
 197  (costGradientLinearExtension g).map_add x y
 198
 199/-- **T2 (linearity, scalar multiplication).** -/
 200theorem costGradient_linear_smul {ι κ : Type*} [DecidableEq ι]
 201    (g : ι → (κ →₀ ℂ)) (a : ℂ) (x : ι →₀ ℂ) :
 202    costGradientLinearExtension g (a • x) =
 203      a • costGradientLinearExtension g x :=
 204  (costGradientLinearExtension g).map_smul a x
 205
 206/-- **T2 (uniqueness).** Any two `ℂ`-linear maps that agree on the
 207finsupp basis agree everywhere. This is the uniqueness half of the
 208universal property. -/
 209theorem costGradient_linear_unique {ι κ : Type*} [DecidableEq ι]
 210    (f₁ f₂ : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ))
 211    (h : ∀ α : ι, f₁ (Finsupp.single α (1 : ℂ)) = f₂ (Finsupp.single α (1 : ℂ))) :
 212    f₁ = f₂ := by
 213  apply Finsupp.lhom_ext'
 214  intro α
 215  apply LinearMap.ext
 216  intro c
 217  have h1 : Finsupp.single α c = c • Finsupp.single α (1 : ℂ) := by
 218    ext β
 219    by_cases hβ : β = α <;> simp [hβ]
 220  have hα := h α
 221  have step :
 222      f₁ (Finsupp.single α c) = f₂ (Finsupp.single α c) := by
 223    rw [h1, f₁.map_smul, f₂.map_smul, hα]
 224  show (f₁.comp (Finsupp.lsingle (R := ℂ) α)) c
 225        = (f₂.comp (Finsupp.lsingle (R := ℂ) α)) c
 226  simp [Finsupp.lsingle, step]
 227
 228/-- **T2 master witness.** The complete content of cost-gradient
 229functoriality under superposition: existence (the explicit linear
 230extension), agreement on basis, and uniqueness. -/
 231structure CostGradientFunctoriality (ι κ : Type) [DecidableEq ι] where
 232  /-- Existence: the linear extension itself. -/
 233  extend : (ι → (κ →₀ ℂ)) → ((ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ))
 234  /-- Basis agreement: extension agrees with classical map on basis. -/
 235  basis_agreement :
 236    ∀ (g : ι → (κ →₀ ℂ)) (α : ι),
 237      extend g (Finsupp.single α (1 : ℂ)) = g α
 238  /-- Uniqueness on basis. -/
 239  unique_on_basis :
 240    ∀ (f₁ f₂ : (ι →₀ ℂ) →ₗ[ℂ] (κ →₀ ℂ)),
 241      (∀ α : ι, f₁ (Finsupp.single α (1 : ℂ)) = f₂ (Finsupp.single α (1 : ℂ))) →
 242        f₁ = f₂
 243
 244/-- The canonical inhabitant of `CostGradientFunctoriality`. -/
 245def costGradientFunctoriality (ι κ : Type) [DecidableEq ι] :
 246    CostGradientFunctoriality ι κ where
 247  extend := costGradientLinearExtension
 248  basis_agreement := costGradient_linear_basis
 249  unique_on_basis := costGradient_linear_unique
 250
 251theorem costGradientFunctoriality_inhabited (ι κ : Type) [DecidableEq ι] :
 252    Nonempty (CostGradientFunctoriality ι κ) :=
 253  ⟨costGradientFunctoriality ι κ⟩
 254
 255end
 256
 257end LedgerSuperposition
 258end Gravity
 259end IndisputableMonolith
 260