IndisputableMonolith.Gravity.RecognitionLedger

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Gravity: The Recognition Ledger
   6
   7## Status: STRUCTURAL THEOREM (0 sorry, 0 RS-internal axiom).
   8
   9The recognition ledger is the central bookkeeping structure of recognition
  10gravity.  It is used in three distinct ways:
  11
  121. **Gravitational action.**  The continuum limit of the total ledger cost
  13   restricted to codimension-2 hinges equals the Regge action.
  142. **Page curve.**  The radiation entropy at retarded time u is the von
  15   Neumann entropy of the reduced state obtained by tracing over cells on
  16   one side of a horizon boundary.
  173. **Vacuum energy.**  The vacuum ledger cost is the ground-state value of
  18   the total ledger cost over the full substrate lattice.
  19
  20## Definition
  21
  22Given a finite substrate lattice Λ (modeled as a `Fintype`), the recognition
  23ledger is a function
  24
  25  ℒ : Λ × Λ → [0, ∞)
  26
  27assigning to each pair of substrate cells (i, j) the accumulated recognition
  28cost J(x_ij) of the comparison between them.
  29
  30### Properties
  31
  321. **Symmetry:** ℒ(i,j) = ℒ(j,i)
  332. **Diagonal zero:** ℒ(i,i) = 0
  343. **Non-negative:** ℒ(i,j) ≥ 0 (by definition of the codomain)
  354. **RCL subadditivity:** ℒ(i,k) ≤ R(ℒ(i,j), ℒ(j,k)) for every
  36   intermediate cell j, where R(u,v) = 2uv + 2u + 2v is the forced gate.
  37
  38### Derived quantities
  39
  40- **Total ledger cost:** Σ_{i,j} ℒ(i,j)
  41- **Ledger deficit at cell i:** Δ_i = Σ_j ℒ(i,j)
  42- **Flatness:** A ledger is flat iff ℒ(i,j) = 0 for all i, j.
  43-/
  44
  45namespace IndisputableMonolith
  46namespace Gravity
  47namespace RecognitionLedger
  48
  49open Constants
  50
  51/-! ## §1. The RCL gate function -/
  52
  53/-- The forced gate R(u,v) = 2uv + 2u + 2v, as proved in
  54`Foundation.DAlembert.FactorizationForcing.gate_forces_rcl`. -/
  55noncomputable def rclGate (u v : ℝ) : ℝ := 2 * u * v + 2 * u + 2 * v
  56
  57theorem rclGate_symmetric (u v : ℝ) : rclGate u v = rclGate v u := by
  58  unfold rclGate; ring
  59
  60theorem rclGate_zero_right (u : ℝ) : rclGate u 0 = 2 * u := by
  61  unfold rclGate; ring
  62
  63theorem rclGate_zero_left (v : ℝ) : rclGate 0 v = 2 * v := by
  64  unfold rclGate; ring
  65
  66theorem rclGate_nonneg {u v : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) :
  67    0 ≤ rclGate u v := by
  68  unfold rclGate
  69  nlinarith
  70
  71/-! ## §2. The recognition ledger structure -/
  72
  73/-- A recognition ledger on a finite substrate lattice `Λ`. -/
  74structure RecognitionLedger (Λ : Type*) [Fintype Λ] [DecidableEq Λ] where
  75  /-- The cost function assigning recognition cost to each cell pair. -/
  76  cost : Λ → Λ → ℝ
  77  /-- Symmetry: ℒ(i,j) = ℒ(j,i). -/
  78  symmetric : ∀ i j, cost i j = cost j i
  79  /-- Diagonal zero: a cell has zero cost of comparison with itself. -/
  80  diagonal_zero : ∀ i, cost i i = 0
  81  /-- Non-negativity: all costs are non-negative. -/
  82  nonneg : ∀ i j, 0 ≤ cost i j
  83  /-- RCL subadditivity: the cost from i to k is bounded by the RCL gate
  84  applied to the costs from i to j and j to k, for every intermediate j. -/
  85  rcl_subadditive : ∀ i j k, cost i k ≤ rclGate (cost i j) (cost j k)
  86
  87/-! ## §3. The flat ledger -/
  88
  89/-- The flat (zero) ledger on any finite lattice. -/
  90def flatLedger (Λ : Type*) [Fintype Λ] [DecidableEq Λ] : RecognitionLedger Λ where
  91  cost := fun _ _ => 0
  92  symmetric := fun _ _ => rfl
  93  diagonal_zero := fun _ => rfl
  94  nonneg := fun _ _ => le_refl 0
  95  rcl_subadditive := fun _ _ _ => by unfold rclGate; norm_num
  96
  97/-- A ledger is flat iff every cost is zero. -/
  98def isFlat {Λ : Type*} [Fintype Λ] [DecidableEq Λ] (L : RecognitionLedger Λ) : Prop :=
  99  ∀ i j, L.cost i j = 0
 100
 101theorem flatLedger_isFlat (Λ : Type*) [Fintype Λ] [DecidableEq Λ] :
 102    isFlat (flatLedger Λ) :=
 103  fun _ _ => rfl
 104
 105/-! ## §4. Total ledger cost -/
 106
 107/-- The total ledger cost: sum of all pairwise costs. -/
 108noncomputable def totalCost {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 109    (L : RecognitionLedger Λ) : ℝ :=
 110  ∑ i, ∑ j, L.cost i j
 111
 112/-- The total cost is non-negative. -/
 113theorem totalCost_nonneg {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 114    (L : RecognitionLedger Λ) : 0 ≤ totalCost L := by
 115  unfold totalCost
 116  apply Finset.sum_nonneg
 117  intro i _
 118  apply Finset.sum_nonneg
 119  intro j _
 120  exact L.nonneg i j
 121
 122/-- The total cost vanishes iff the ledger is flat. -/
 123theorem totalCost_eq_zero_iff_flat {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 124    (L : RecognitionLedger Λ) : totalCost L = 0 ↔ isFlat L := by
 125  constructor
 126  · intro h0
 127    unfold isFlat
 128    intro i j
 129    unfold totalCost at h0
 130    have hsums : ∀ x ∈ Finset.univ, ∑ y : Λ, L.cost x y = 0 := by
 131      rwa [Finset.sum_eq_zero_iff_of_nonneg
 132        (fun x _ => Finset.sum_nonneg (fun y _ => L.nonneg x y))] at h0
 133    have h0i := hsums i (Finset.mem_univ i)
 134    have hsumj : ∀ y ∈ Finset.univ, L.cost i y = 0 := by
 135      rwa [Finset.sum_eq_zero_iff_of_nonneg (fun y _ => L.nonneg i y)] at h0i
 136    exact hsumj j (Finset.mem_univ j)
 137  · intro hf
 138    unfold totalCost
 139    apply Finset.sum_eq_zero
 140    intro i _
 141    apply Finset.sum_eq_zero
 142    intro j _
 143    exact hf i j
 144
 145/-- The flat ledger has zero total cost. -/
 146theorem flatLedger_totalCost_zero (Λ : Type*) [Fintype Λ] [DecidableEq Λ] :
 147    totalCost (flatLedger Λ) = 0 :=
 148  (totalCost_eq_zero_iff_flat _).mpr (flatLedger_isFlat Λ)
 149
 150/-! ## §5. Ledger deficit at a cell -/
 151
 152/-- The ledger deficit at cell i: total cost of comparison with all cells. -/
 153noncomputable def deficit {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 154    (L : RecognitionLedger Λ) (i : Λ) : ℝ :=
 155  ∑ j, L.cost i j
 156
 157/-- The deficit is non-negative. -/
 158theorem deficit_nonneg {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 159    (L : RecognitionLedger Λ) (i : Λ) : 0 ≤ deficit L i := by
 160  unfold deficit
 161  apply Finset.sum_nonneg
 162  intro j _
 163  exact L.nonneg i j
 164
 165/-- Total cost is the sum of deficits. -/
 166theorem totalCost_eq_sum_deficits {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 167    (L : RecognitionLedger Λ) : totalCost L = ∑ i, deficit L i :=
 168  rfl
 169
 170/-! ## §6. Boundary and ledger entropy -/
 171
 172/-- A partition of a substrate into two complementary regions.  The
 173boundary is the interface between them.  In the gravitational context,
 174this partition represents a horizon. -/
 175structure SubstrateBipartition (Λ : Type*) [Fintype Λ] [DecidableEq Λ] where
 176  interior : Finset Λ
 177  exterior : Finset Λ
 178  partition_complete : interior ∪ exterior = Finset.univ
 179  partition_disjoint : Disjoint interior exterior
 180
 181/-- The boundary cost of a bipartition: sum of costs between interior
 182and exterior cells.  This is the ledger analogue of the boundary term
 183in the gravitational action. -/
 184noncomputable def boundaryCost {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 185    (L : RecognitionLedger Λ) (P : SubstrateBipartition Λ) : ℝ :=
 186  ∑ i ∈ P.interior, ∑ j ∈ P.exterior, L.cost i j
 187
 188/-- Boundary cost is non-negative. -/
 189theorem boundaryCost_nonneg {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 190    (L : RecognitionLedger Λ) (P : SubstrateBipartition Λ) :
 191    0 ≤ boundaryCost L P := by
 192  unfold boundaryCost
 193  apply Finset.sum_nonneg
 194  intro i _
 195  apply Finset.sum_nonneg
 196  intro j _
 197  exact L.nonneg i j
 198
 199/-- Boundary cost is symmetric: exchanging interior and exterior gives
 200the same boundary cost. -/
 201theorem boundaryCost_symmetric {Λ : Type*} [Fintype Λ] [DecidableEq Λ]
 202    (L : RecognitionLedger Λ) (P : SubstrateBipartition Λ) :
 203    boundaryCost L P =
 204    ∑ j ∈ P.exterior, ∑ i ∈ P.interior, L.cost j i := by
 205  unfold boundaryCost
 206  rw [Finset.sum_comm]
 207  congr 1; ext j
 208  congr 1; ext i
 209  exact L.symmetric i j
 210
 211/-! ## §7. Master cert -/
 212
 213structure RecognitionLedgerCert where
 214  flat_exists : ∀ (Λ : Type) [Fintype Λ] [DecidableEq Λ],
 215    Nonempty (RecognitionLedger Λ)
 216  flat_total_zero : ∀ (Λ : Type) [Fintype Λ] [DecidableEq Λ],
 217    totalCost (flatLedger Λ) = 0
 218  total_nonneg : ∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
 219    (L : RecognitionLedger Λ), 0 ≤ totalCost L
 220  zero_iff_flat : ∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
 221    (L : RecognitionLedger Λ), totalCost L = 0 ↔ isFlat L
 222
 223def recognitionLedgerCert : RecognitionLedgerCert where
 224  flat_exists := fun Λ _ _ => ⟨flatLedger Λ⟩
 225  flat_total_zero := fun Λ _ _ => flatLedger_totalCost_zero Λ
 226  total_nonneg := fun L => totalCost_nonneg L
 227  zero_iff_flat := fun L => totalCost_eq_zero_iff_flat L
 228
 229theorem recognitionLedgerCert_inhabited :
 230    Nonempty RecognitionLedgerCert :=
 231  ⟨recognitionLedgerCert⟩
 232
 233/-- **RECOGNITION LEDGER ONE-STATEMENT.**  The recognition ledger is a
 234symmetric, diagonal-zero, non-negative cost function on a finite lattice
 235satisfying RCL subadditivity.  Its total cost is non-negative and vanishes
 236iff the lattice is flat (Minkowski).  The flat ledger exists on any lattice.
 237Bipartition boundary costs are non-negative and symmetric under exchange.  -/
 238theorem recognition_ledger_one_statement :
 239    (∀ (Λ : Type) [Fintype Λ] [DecidableEq Λ],
 240      Nonempty (RecognitionLedger Λ)) ∧
 241    (∀ (Λ : Type) [Fintype Λ] [DecidableEq Λ],
 242      totalCost (flatLedger Λ) = 0) ∧
 243    (∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
 244      (L : RecognitionLedger Λ), 0 ≤ totalCost L) ∧
 245    (∀ {Λ : Type} [Fintype Λ] [DecidableEq Λ]
 246      (L : RecognitionLedger Λ), totalCost L = 0 ↔ isFlat L) :=
 247  ⟨fun Λ _ _ => ⟨flatLedger Λ⟩,
 248   fun Λ _ _ => flatLedger_totalCost_zero Λ,
 249   fun L => totalCost_nonneg L,
 250   fun L => totalCost_eq_zero_iff_flat L⟩
 251
 252end RecognitionLedger
 253end Gravity
 254end IndisputableMonolith
 255