IndisputableMonolith.Gravity.MacroscopicLedger

   1import Mathlib
   2import IndisputableMonolith.Gravity.LedgerSuperposition
   3
   4/-!
   5# Gravity IV, Track 2.A: Macroscopic Ledger Hilbert Carrier (THEOREM)
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom).
   8
   9This module discharges Track 2.A of the master plan: it upgrades the
  10"macroscopic ledger Hilbert carrier" from a definition / CONDITIONAL
  11THEOREM in paper IV to a Lean theorem that the recognition update extends
  12canonically and `ℂ`-linearly from the single-site `Signal8` carrier
  13(`LedgerSuperposition`) to a finite tensor product over an arbitrary
  14finite indexing set of sites.
  15
  16## Construction
  17
  18Given a finite indexing set `ι` of sites, the macroscopic ledger Hilbert
  19carrier is the `ι`-fold `PiTensorProduct` over `ℂ` of single-site
  20`Signal8` factors:
  21
  22```
  23def MacroscopicLedger : Type :=
  24  ⨂[ℂ] _ : ι, Signal8
  25```
  26
  27The recognition update on each factor is the linearization of
  28`cyclic_shift` (proved `ℂ`-linear in `LedgerSuperposition`); the
  29macroscopic recognition update is `PiTensorProduct.map` applied
  30factor-wise. By the universal property of `PiTensorProduct.map`, the
  31result is automatically `ℂ`-linear and acts on pure tensors `⨂ᵢ ψᵢ` by
  32`⨂ᵢ cyclic_shift ψᵢ`.
  33
  34## Why this matters
  35
  36Paper IV's Theorem 1 (Ledger Superposition) is unconditional for the
  37single-site carrier. The macroscopic claim — that ledger superpositions
  38of multi-site configurations are physical and preserved by recognition —
  39needs the same theorem at the tensor-product level. Track 2.A converts
  40that claim from CONDITIONAL THEOREM to STRUCTURAL THEOREM.
  41
  42## What this does *not* do
  43
  44This module formalises macroscopic ledger superposition at the
  45amplitude-linear level (the universal property of the tensor product).
  46It does not yet force the *physical* identification of the macroscopic
  47recognition update with the gravitational-channel response operator;
  48that is Track 2.C ("Force C2 from substrate"), which converts T2's MODEL
  49tag to THEOREM by ruling out classical-mediator extensions on the joint
  50matter-plus-channel Hilbert space.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Gravity
  55namespace MacroscopicLedger
  56
  57/-- Local abbreviation: the eight-tick analytic signal carrier, identified
  58with the canonical `Foundation.ComplexStructureForcing.Signal8`. -/
  59abbrev Signal8 : Type :=
  60  IndisputableMonolith.Foundation.ComplexStructureForcing.Signal8
  61
  62/-- Local abbreviation: the one-tick recognition update on `Signal8`. -/
  63abbrev cyclic_shift : Signal8 → Signal8 :=
  64  IndisputableMonolith.Spectral.cyclic_shift
  65
  66open scoped TensorProduct
  67
  68noncomputable section
  69
  70/-! ## §1. Single-site recognition update as a `ℂ`-linear map -/
  71
  72/-- The single-site recognition update `cyclic_shift` packaged as a
  73`ℂ`-linear endomorphism of `Signal8`. Linearity (additivity and scalar
  74homogeneity) is from `cyclic_shift_add` and `cyclic_shift_smul`
  75in `Foundation.SchrodingerDerivation`. -/
  76def cyclicShiftLinear : Signal8 →ₗ[ℂ] Signal8 where
  77  toFun := cyclic_shift
  78  map_add' v w :=
  79    IndisputableMonolith.Foundation.SchrodingerDerivation.cyclic_shift_add v w
  80  map_smul' c v :=
  81    IndisputableMonolith.Foundation.SchrodingerDerivation.cyclic_shift_smul c v
  82
  83@[simp] theorem cyclicShiftLinear_apply (ψ : Signal8) :
  84    cyclicShiftLinear ψ = cyclic_shift ψ := rfl
  85
  86/-- The single-site update is `ℂ`-linear (paired with the
  87`LedgerSuperposition` superposition theorem). -/
  88theorem cyclicShiftLinear_map_add (ψ φ : Signal8) :
  89    cyclicShiftLinear (ψ + φ) = cyclicShiftLinear ψ + cyclicShiftLinear φ :=
  90  cyclicShiftLinear.map_add ψ φ
  91
  92theorem cyclicShiftLinear_map_smul (c : ℂ) (ψ : Signal8) :
  93    cyclicShiftLinear (c • ψ) = c • cyclicShiftLinear ψ :=
  94  cyclicShiftLinear.map_smul c ψ
  95
  96/-! ## §2. The macroscopic ledger carrier as a `PiTensorProduct` -/
  97
  98variable {ι : Type} [Fintype ι] [DecidableEq ι]
  99
 100/-- The macroscopic ledger Hilbert carrier over a finite indexing set
 101`ι` of sites: the `ι`-fold `PiTensorProduct` over `ℂ` of single-site
 102`Signal8` factors. The index type is in `Type` (universe 0) to keep the
 103universe constraints simple; `Fin n`, `Finset.univ`, and any concrete
 104finite site set fit. -/
 105abbrev MacroscopicLedger (ι : Type) [Fintype ι] [DecidableEq ι] : Type :=
 106  ⨂[ℂ] _ : ι, Signal8
 107
 108/-- The macroscopic recognition update on the ledger Hilbert carrier:
 109the `PiTensorProduct.map` of the single-site `cyclicShiftLinear` on each
 110factor. By construction this is `ℂ`-linear. -/
 111noncomputable def MacroscopicShift :
 112    MacroscopicLedger ι →ₗ[ℂ] MacroscopicLedger ι :=
 113  PiTensorProduct.map (fun _ : ι => cyclicShiftLinear)
 114
 115/-! ## §3. Action on pure tensors -/
 116
 117/-- Action of the macroscopic recognition update on a pure tensor
 118configuration: `R̂_macro (⨂ᵢ ψᵢ) = ⨂ᵢ R̂ ψᵢ`. -/
 119theorem MacroscopicShift_tprod (ψ : ι → Signal8) :
 120    MacroscopicShift (PiTensorProduct.tprod ℂ ψ) =
 121      PiTensorProduct.tprod ℂ (fun i => cyclic_shift (ψ i)) := by
 122  unfold MacroscopicShift
 123  rw [PiTensorProduct.map_tprod]
 124  rfl
 125
 126/-! ## §4. Linearity and superposition preservation -/
 127
 128/-- **Linearity.** The macroscopic recognition update is `ℂ`-linear
 129(by construction, since `PiTensorProduct.map` returns a `LinearMap`).
 130This restates the universal property explicitly. -/
 131theorem MacroscopicShift_map_add (Ψ Φ : MacroscopicLedger ι) :
 132    MacroscopicShift (Ψ + Φ) = MacroscopicShift Ψ + MacroscopicShift Φ :=
 133  MacroscopicShift.map_add Ψ Φ
 134
 135theorem MacroscopicShift_map_smul (c : ℂ) (Ψ : MacroscopicLedger ι) :
 136    MacroscopicShift (c • Ψ) = c • MacroscopicShift Ψ :=
 137  MacroscopicShift.map_smul c Ψ
 138
 139/-- **Macroscopic ledger superposition.** For a finite family of
 140macroscopic ledger configurations `Ψ : κ → MacroscopicLedger ι` and
 141amplitudes `c : κ → ℂ` indexed by a finite set, the macroscopic
 142recognition update commutes with the finite linear combination. This is
 143the explicit superposition principle for multi-site ledger
 144configurations. -/
 145theorem MacroscopicShift_finite_sum
 146    {κ : Type*} (s : Finset κ) (c : κ → ℂ) (Ψ : κ → MacroscopicLedger ι) :
 147    MacroscopicShift (∑ α ∈ s, c α • Ψ α) =
 148      ∑ α ∈ s, c α • MacroscopicShift (Ψ α) := by
 149  classical
 150  induction s using Finset.induction_on with
 151  | empty => simp
 152  | @insert α s hα ih =>
 153    rw [Finset.sum_insert hα, Finset.sum_insert hα,
 154        MacroscopicShift_map_add, MacroscopicShift_map_smul, ih]
 155
 156/-! ## §5. Master certificate -/
 157
 158/-- **MACROSCOPIC LEDGER HILBERT CARRIER CERTIFICATE.**
 159
 160Five clauses establishing that the macroscopic ledger Hilbert carrier
 161is a `ℂ`-linear extension of the single-site recognition update:
 162
 1631. `single_site_linear`: the single-site recognition update
 164   `cyclicShiftLinear` is a `ℂ`-linear map `Signal8 →ₗ[ℂ] Signal8`.
 1652. `tensor_action`: on a pure tensor configuration, the macroscopic
 166   update acts factor-wise.
 1673. `additive`: the macroscopic update is additive.
 1684. `scalar_homogeneous`: the macroscopic update is scalar-homogeneous.
 1695. `finite_superposition`: the macroscopic update commutes with finite
 170   linear combinations (the superposition principle for multi-site
 171   ledger configurations).
 172
 173This discharges Track 2.A of the master plan: the macroscopic ledger
 174Hilbert carrier is now a STRUCTURAL THEOREM rather than a definition or
 175CONDITIONAL THEOREM. -/
 176structure MacroscopicLedgerTheorem (ι : Type) [Fintype ι] [DecidableEq ι] where
 177  /-- (1) Single-site update is a linear map. -/
 178  single_site_linear :
 179    ∀ (ψ φ : Signal8) (a b : ℂ),
 180      cyclicShiftLinear (a • ψ + b • φ) =
 181        a • cyclicShiftLinear ψ + b • cyclicShiftLinear φ
 182  /-- (2) Pure-tensor action: factor-wise. -/
 183  tensor_action :
 184    ∀ (ψ : ι → Signal8),
 185      MacroscopicShift (PiTensorProduct.tprod ℂ ψ) =
 186        PiTensorProduct.tprod ℂ (fun i => cyclic_shift (ψ i))
 187  /-- (3) Macroscopic update is additive. -/
 188  additive :
 189    ∀ (Ψ Φ : MacroscopicLedger ι),
 190      MacroscopicShift (Ψ + Φ) = MacroscopicShift Ψ + MacroscopicShift Φ
 191  /-- (4) Macroscopic update is scalar-homogeneous. -/
 192  scalar_homogeneous :
 193    ∀ (c : ℂ) (Ψ : MacroscopicLedger ι),
 194      MacroscopicShift (c • Ψ) = c • MacroscopicShift Ψ
 195  /-- (5) Macroscopic update commutes with finite superposition. -/
 196  finite_superposition :
 197    ∀ {κ : Type*} (s : Finset κ) (c : κ → ℂ) (Ψ : κ → MacroscopicLedger ι),
 198      MacroscopicShift (∑ α ∈ s, c α • Ψ α) =
 199        ∑ α ∈ s, c α • MacroscopicShift (Ψ α)
 200
 201/-- The macroscopic ledger theorem is verified. -/
 202noncomputable def macroscopicLedgerTheorem
 203    (ι : Type) [Fintype ι] [DecidableEq ι] :
 204    MacroscopicLedgerTheorem ι where
 205  single_site_linear ψ φ a b := by
 206    rw [cyclicShiftLinear.map_add, cyclicShiftLinear.map_smul,
 207        cyclicShiftLinear.map_smul]
 208  tensor_action := MacroscopicShift_tprod
 209  additive := MacroscopicShift_map_add
 210  scalar_homogeneous := MacroscopicShift_map_smul
 211  finite_superposition := MacroscopicShift_finite_sum
 212
 213theorem macroscopicLedgerTheorem_inhabited
 214    (ι : Type) [Fintype ι] [DecidableEq ι] :
 215    Nonempty (MacroscopicLedgerTheorem ι) :=
 216  ⟨macroscopicLedgerTheorem ι⟩
 217
 218end
 219
 220end MacroscopicLedger
 221end Gravity
 222end IndisputableMonolith
 223