IndisputableMonolith.NumberTheory.ConcreteEulerLedger

   1import Mathlib
   2import IndisputableMonolith.Foundation.LedgerForcing
   3import IndisputableMonolith.Foundation.RecognitionForcing
   4import IndisputableMonolith.NumberTheory.EulerInstantiation
   5
   6/-!
   7# Concrete Euler Ledger
   8
   9This module formalizes the first arithmetic-to-ledger identification step.
  10
  11For any positive real exponent `σ` and any finite prime support, we build an
  12actual `LedgerForcing.Ledger` whose recognition-event ratios are the Euler
  13terms `p^{-σ}` together with their reciprocals. For a `DefectSensor`, taking
  14`σ = sensor.realPart` produces a finite, balanced arithmetic ledger indexed by
  15the same strip coordinate that appears in the sensor machinery.
  16
  17This does **not** yet prove `RSPhysicalThesis`. What it does provide is the
  18first fully concrete bridge object:
  19
  20* a real arithmetic ledger built from prime Euler data,
  21* double-entry balance by construction,
  22* zero net flow by the generic ledger conservation theorem,
  23* positive nontrivial recognition cost for each prime event,
  24* an explicit total ledger-cost formula in terms of `J (p^{-σ})`.
  25-/
  26
  27namespace IndisputableMonolith
  28namespace NumberTheory
  29
  30open IndisputableMonolith.Foundation
  31
  32/-! ## Prime Euler events -/
  33
  34/-- The strip real part of a defect sensor is positive. -/
  35theorem sensor_realPart_pos (sensor : DefectSensor) : 0 < sensor.realPart := by
  36  linarith [sensor.in_strip.1]
  37
  38/-- The basic arithmetic recognition event contributed by a prime Euler factor.
  39
  40Its ratio is the positive real quantity `p^{-σ}`. -/
  41noncomputable def primeEulerEvent (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  42    LedgerForcing.RecognitionEvent where
  43  source := 0
  44  target := p
  45  ratio := (p : ℝ) ^ (-σ)
  46  ratio_pos := eigenvalue_pos hσ p
  47
  48@[simp] theorem primeEulerEvent_ratio (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  49    (primeEulerEvent σ hσ p).ratio = (p : ℝ) ^ (-σ) := rfl
  50
  51@[simp] theorem primeEulerEvent_target (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  52    (primeEulerEvent σ hσ p).target = p := rfl
  53
  54/-- The prime Euler event is genuinely nontrivial: its ratio is strictly below `1`. -/
  55theorem primeEulerEvent_ratio_lt_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  56    (primeEulerEvent σ hσ p).ratio < 1 := by
  57  simpa [primeEulerEvent] using eigenvalue_lt_one hσ p
  58
  59/-- Hence the prime Euler event does not have ratio `1`. -/
  60theorem primeEulerEvent_ratio_ne_one {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  61    (primeEulerEvent σ hσ p).ratio ≠ 1 := by
  62  exact (primeEulerEvent_ratio_lt_one hσ p).ne
  63
  64/-- The reciprocal Euler event has ratio `p^σ`. -/
  65theorem reciprocal_primeEulerEvent_ratio {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  66    (LedgerForcing.reciprocal (primeEulerEvent σ hσ p)).ratio = (p : ℝ) ^ σ := by
  67  simp [LedgerForcing.reciprocal, primeEulerEvent, Real.rpow_neg, inv_inv]
  68
  69/-- The cost of the prime Euler event is exactly `J(p^{-σ})`. -/
  70@[simp] theorem primeEulerEvent_cost_eq_J (σ : ℝ) (hσ : 0 < σ) (p : Nat.Primes) :
  71    LedgerForcing.event_cost (primeEulerEvent σ hσ p) =
  72      LedgerForcing.J ((p : ℝ) ^ (-σ)) := by
  73  rfl
  74
  75/-- Each prime Euler event has strictly positive recognition cost. -/
  76theorem primeEulerEvent_cost_pos {σ : ℝ} (hσ : 0 < σ) (p : Nat.Primes) :
  77    0 < LedgerForcing.event_cost (primeEulerEvent σ hσ p) := by
  78  have hrecognition :
  79      0 < RecognitionForcing.recognition_cost (primeEulerEvent σ hσ p) := by
  80    exact RecognitionForcing.nontrivial_recognition_positive_cost
  81      (primeEulerEvent σ hσ p) (primeEulerEvent_ratio_ne_one hσ p)
  82  simpa [RecognitionForcing.recognition_cost, LedgerForcing.event_cost] using hrecognition
  83
  84/-! ## Finite Euler ledgers -/
  85
  86/-- Build a concrete finite Euler ledger from a finite list of primes.
  87
  88Each prime contributes one event with ratio `p^{-σ}` and one reciprocal event,
  89so balance is preserved at every step. -/
  90noncomputable def finiteEulerLedger (σ : ℝ) (hσ : 0 < σ) :
  91    List Nat.Primes → LedgerForcing.Ledger
  92  | [] => LedgerForcing.empty_ledger
  93  | p :: ps => LedgerForcing.add_event (finiteEulerLedger σ hσ ps) (primeEulerEvent σ hσ p)
  94
  95/-- Every finite Euler ledger is balanced. -/
  96theorem finiteEulerLedger_balanced (σ : ℝ) (hσ : 0 < σ) (support : List Nat.Primes) :
  97    LedgerForcing.balanced (finiteEulerLedger σ hσ support) :=
  98  LedgerForcing.ledger_balanced _
  99
 100/-- Every finite Euler ledger has zero net flow at every agent. -/
 101theorem finiteEulerLedger_net_flow_zero (σ : ℝ) (hσ : 0 < σ)
 102    (support : List Nat.Primes) (agent : ℕ) :
 103    LedgerForcing.net_flow (finiteEulerLedger σ hσ support) agent = 0 := by
 104  exact LedgerForcing.conservation_from_balance _ (finiteEulerLedger_balanced σ hσ support) agent
 105
 106/-- If a prime belongs to the support list, its Euler event appears in the ledger. -/
 107theorem primeEulerEvent_mem_finiteEulerLedger {σ : ℝ} {hσ : 0 < σ} :
 108    ∀ {support : List Nat.Primes} {p : Nat.Primes},
 109      p ∈ support →
 110      primeEulerEvent σ hσ p ∈ (finiteEulerLedger σ hσ support).events
 111  | [], _, hp => by cases hp
 112  | q :: qs, p, hp => by
 113      simp only [List.mem_cons] at hp
 114      rcases hp with hp | hp
 115      · subst p
 116        simp [finiteEulerLedger, LedgerForcing.add_event]
 117      · simp [finiteEulerLedger, LedgerForcing.add_event,
 118          primeEulerEvent_mem_finiteEulerLedger (support := qs) hp]
 119
 120/-- If a prime belongs to the support list, its reciprocal Euler event also appears. -/
 121theorem reciprocal_primeEulerEvent_mem_finiteEulerLedger {σ : ℝ} {hσ : 0 < σ} :
 122    ∀ {support : List Nat.Primes} {p : Nat.Primes},
 123      p ∈ support →
 124      LedgerForcing.reciprocal (primeEulerEvent σ hσ p) ∈
 125        (finiteEulerLedger σ hσ support).events
 126  | [], _, hp => by cases hp
 127  | q :: qs, p, hp => by
 128      simp only [List.mem_cons] at hp
 129      rcases hp with hp | hp
 130      · subst p
 131        simp [finiteEulerLedger, LedgerForcing.add_event]
 132      · simp [finiteEulerLedger, LedgerForcing.add_event,
 133          reciprocal_primeEulerEvent_mem_finiteEulerLedger (support := qs) hp]
 134
 135/-- Adding one paired event contributes exactly twice its single-event cost. -/
 136private theorem ledger_cost_foldl_with_offset
 137    (events : List LedgerForcing.RecognitionEvent) (acc : ℝ) :
 138    events.foldl (fun acc e => acc + LedgerForcing.event_cost e) acc =
 139      acc + events.foldl (fun acc e => acc + LedgerForcing.event_cost e) 0 := by
 140  induction events generalizing acc with
 141  | nil =>
 142      simp
 143  | cons e es ih =>
 144      simp only [List.foldl_cons]
 145      rw [ih (acc + LedgerForcing.event_cost e),
 146        ih (0 + LedgerForcing.event_cost e)]
 147      ring
 148
 149/-- Adding one paired event contributes exactly twice its single-event cost. -/
 150private theorem add_event_cost_formula (L : LedgerForcing.Ledger)
 151    (e : LedgerForcing.RecognitionEvent) :
 152    LedgerForcing.ledger_cost (LedgerForcing.add_event L e) =
 153      2 * LedgerForcing.event_cost e + LedgerForcing.ledger_cost L := by
 154  unfold LedgerForcing.ledger_cost LedgerForcing.add_event
 155  simp only [List.foldl_cons]
 156  rw [LedgerForcing.reciprocity]
 157  rw [ledger_cost_foldl_with_offset]
 158  ring
 159
 160/-- Explicit total-cost formula for a finite Euler ledger in terms of the
 161single-event costs. -/
 162theorem finiteEulerLedger_cost_formula (σ : ℝ) (hσ : 0 < σ) :
 163    ∀ support : List Nat.Primes,
 164      LedgerForcing.ledger_cost (finiteEulerLedger σ hσ support) =
 165        2 * (support.map (fun p => LedgerForcing.event_cost (primeEulerEvent σ hσ p))).sum
 166  | [] => by
 167      simp [finiteEulerLedger, LedgerForcing.empty_ledger_cost]
 168  | p :: ps => by
 169      rw [finiteEulerLedger, add_event_cost_formula,
 170        finiteEulerLedger_cost_formula σ hσ ps]
 171      simp
 172      ring
 173
 174/-- The same total-cost formula, rewritten directly in terms of `J (p^{-σ})`. -/
 175theorem finiteEulerLedger_cost_formula_J (σ : ℝ) (hσ : 0 < σ) (support : List Nat.Primes) :
 176    LedgerForcing.ledger_cost (finiteEulerLedger σ hσ support) =
 177      2 * (support.map (fun p : Nat.Primes => LedgerForcing.J ((p : ℝ) ^ (-σ)))).sum := by
 178  simpa [primeEulerEvent_cost_eq_J] using finiteEulerLedger_cost_formula σ hσ support
 179
 180/-! ## Sensor-indexed concrete Euler ledgers -/
 181
 182/-- The concrete finite Euler ledger attached to a defect sensor. -/
 183noncomputable def sensorEulerLedger (sensor : DefectSensor) (support : Finset Nat.Primes) :
 184    LedgerForcing.Ledger :=
 185  finiteEulerLedger sensor.realPart (sensor_realPart_pos sensor) support.toList
 186
 187/-- The sensor-indexed concrete Euler ledger is balanced. -/
 188theorem sensorEulerLedger_balanced (sensor : DefectSensor) (support : Finset Nat.Primes) :
 189    LedgerForcing.balanced (sensorEulerLedger sensor support) := by
 190  unfold sensorEulerLedger
 191  exact finiteEulerLedger_balanced sensor.realPart (sensor_realPart_pos sensor) support.toList
 192
 193/-- The sensor-indexed concrete Euler ledger has zero net flow. -/
 194theorem sensorEulerLedger_net_flow_zero (sensor : DefectSensor)
 195    (support : Finset Nat.Primes) (agent : ℕ) :
 196    LedgerForcing.net_flow (sensorEulerLedger sensor support) agent = 0 := by
 197  unfold sensorEulerLedger
 198  exact finiteEulerLedger_net_flow_zero sensor.realPart (sensor_realPart_pos sensor) support.toList agent
 199
 200/-- Every supported prime contributes its Euler event to the sensor-indexed ledger. -/
 201theorem primeEulerEvent_mem_sensorEulerLedger
 202    (sensor : DefectSensor) {support : Finset Nat.Primes} {p : Nat.Primes}
 203    (hp : p ∈ support) :
 204    primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
 205      (sensorEulerLedger sensor support).events := by
 206  unfold sensorEulerLedger
 207  exact primeEulerEvent_mem_finiteEulerLedger
 208    (support := support.toList) (p := p) (by simpa using hp)
 209
 210/-- Every supported prime also contributes the reciprocal Euler event. -/
 211theorem reciprocal_primeEulerEvent_mem_sensorEulerLedger
 212    (sensor : DefectSensor) {support : Finset Nat.Primes} {p : Nat.Primes}
 213    (hp : p ∈ support) :
 214    LedgerForcing.reciprocal (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
 215      (sensorEulerLedger sensor support).events := by
 216  unfold sensorEulerLedger
 217  exact reciprocal_primeEulerEvent_mem_finiteEulerLedger
 218    (support := support.toList) (p := p) (by simpa using hp)
 219
 220/-- Explicit total J-cost formula for the sensor-indexed concrete Euler ledger. -/
 221theorem sensorEulerLedger_cost_formula (sensor : DefectSensor)
 222    (support : Finset Nat.Primes) :
 223    LedgerForcing.ledger_cost (sensorEulerLedger sensor support) =
 224      2 * (support.toList.map
 225        (fun p : Nat.Primes => LedgerForcing.J ((p : ℝ) ^ (-sensor.realPart)))).sum := by
 226  unfold sensorEulerLedger
 227  simpa using finiteEulerLedger_cost_formula_J
 228    sensor.realPart (sensor_realPart_pos sensor) support.toList
 229
 230/-- First concrete arithmetic identification theorem.
 231
 232Finite Euler-product data at the real part of a `DefectSensor` determines an
 233actual double-entry ledger with:
 234
 235* balance,
 236* zero net flow,
 237* explicit prime-event membership,
 238* explicit total J-cost.
 239
 240This is the first fully concrete bridge object from arithmetic Euler data into
 241the ledger language used by the RS sensor framework. -/
 242theorem sensorEulerLedger_identification (sensor : DefectSensor)
 243    (support : Finset Nat.Primes) :
 244    let L := sensorEulerLedger sensor support
 245    LedgerForcing.balanced L ∧
 246    (∀ agent : ℕ, LedgerForcing.net_flow L agent = 0) ∧
 247    (∀ p : Nat.Primes, p ∈ support →
 248      primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈ L.events ∧
 249      LedgerForcing.reciprocal
 250        (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈ L.events) ∧
 251    LedgerForcing.ledger_cost L =
 252      2 * (support.toList.map
 253        (fun p : Nat.Primes => LedgerForcing.J ((p : ℝ) ^ (-sensor.realPart)))).sum := by
 254  refine ⟨sensorEulerLedger_balanced sensor support, ?_, ?_,
 255    sensorEulerLedger_cost_formula sensor support⟩
 256  · intro agent
 257    exact sensorEulerLedger_net_flow_zero sensor support agent
 258  · intro p hp
 259    exact ⟨primeEulerEvent_mem_sensorEulerLedger sensor hp,
 260      reciprocal_primeEulerEvent_mem_sensorEulerLedger sensor hp⟩
 261
 262end NumberTheory
 263end IndisputableMonolith
 264