IndisputableMonolith.NumberTheory.DirectedEulerLedger

   1import IndisputableMonolith.NumberTheory.ConcreteEulerLedger
   2import IndisputableMonolith.Unification.UnifiedRH
   3
   4/-!
   5# Directed Euler Ledger Interface
   6
   7This module packages the finite concrete Euler ledgers from
   8`ConcreteEulerLedger.lean` into a directed system over finite prime supports,
   9and then connects that system to the existing ontology-side interfaces from
  10`UnifiedRH.lean`.
  11
  12## What is proved here
  13
  14For every `DefectSensor`, we construct:
  15
  16* a directed family of concrete finite arithmetic ledgers indexed by
  17  `Finset Nat.Primes`,
  18* coherence under support enlargement (every prime already present in a smaller
  19  support remains present in any larger support),
  20* the already-proved admissible Euler trace,
  21* the already-proved T1-bounded realizability proxy.
  22
  23## What is *not* yet proved here
  24
  25This still does not discharge `RSPhysicalThesis`. The remaining gap is the
  26global physical-identification step that would transport the concrete directed
  27Euler ledger into the `PhysicallyExists` predicate, which is defined using the
  28`eulerLedgerScalarState` rather than the bounded proxy `eulerScalarProxy`.
  29-/
  30
  31namespace IndisputableMonolith
  32namespace NumberTheory
  33
  34open IndisputableMonolith.Foundation
  35open IndisputableMonolith.Unification.UnifiedRH
  36
  37/-- Finite prime supports indexing concrete Euler-ledger stages. -/
  38abbrev PrimeSupport := Finset Nat.Primes
  39
  40/-- Finite prime supports form a directed set under inclusion, with upper bound
  41given by union. -/
  42theorem primeSupport_directed (S T : PrimeSupport) :
  43    ∃ U : PrimeSupport, S ⊆ U ∧ T ⊆ U := by
  44  exact ⟨S ∪ T, Finset.subset_union_left, Finset.subset_union_right⟩
  45
  46/-- Prime-event membership persists under support enlargement. -/
  47theorem primeEulerEvent_mem_sensorEulerLedger_of_subset
  48    (sensor : DefectSensor) {S T : PrimeSupport}
  49    (hST : S ⊆ T) {p : Nat.Primes} (hp : p ∈ S) :
  50    primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
  51      (sensorEulerLedger sensor T).events := by
  52  exact primeEulerEvent_mem_sensorEulerLedger sensor (hST hp)
  53
  54/-- Reciprocal prime-event membership also persists under support enlargement. -/
  55theorem reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset
  56    (sensor : DefectSensor) {S T : PrimeSupport}
  57    (hST : S ⊆ T) {p : Nat.Primes} (hp : p ∈ S) :
  58    LedgerForcing.reciprocal
  59        (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
  60      (sensorEulerLedger sensor T).events := by
  61  exact reciprocal_primeEulerEvent_mem_sensorEulerLedger sensor (hST hp)
  62
  63/-- A directed system of concrete Euler ledgers attached to a single sensor. -/
  64structure DirectedEulerLedgerSystem (sensor : DefectSensor) where
  65  /-- The finite-stage ledger at a given prime support. -/
  66  stage : PrimeSupport → LedgerForcing.Ledger
  67  /-- Every finite stage is balanced. -/
  68  stage_balanced : ∀ support, LedgerForcing.balanced (stage support)
  69  /-- Hence every finite stage has zero net flow. -/
  70  stage_net_flow_zero :
  71    ∀ support agent, LedgerForcing.net_flow (stage support) agent = 0
  72  /-- Every prime in the support contributes both the Euler event and its
  73  reciprocal. -/
  74  stage_prime_pair :
  75    ∀ {support : PrimeSupport} {p : Nat.Primes}, p ∈ support →
  76      primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
  77          (stage support).events ∧
  78        LedgerForcing.reciprocal
  79          (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
  80            (stage support).events
  81  /-- Coherence under support enlargement: any prime already present in a
  82  smaller support remains present in every larger support. -/
  83  stage_prime_pair_mono :
  84    ∀ {S T : PrimeSupport} {p : Nat.Primes}, S ⊆ T → p ∈ S →
  85      primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
  86          (stage T).events ∧
  87        LedgerForcing.reciprocal
  88          (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
  89            (stage T).events
  90  /-- Directedness of the support index set. -/
  91  directed_support :
  92    ∀ S T : PrimeSupport, ∃ U : PrimeSupport, S ⊆ U ∧ T ⊆ U
  93  /-- Explicit stage cost formula. -/
  94  stage_cost_formula :
  95    ∀ support : PrimeSupport,
  96      LedgerForcing.ledger_cost (stage support) =
  97        2 * (support.toList.map
  98          (fun p : Nat.Primes => LedgerForcing.J ((p : ℝ) ^ (-sensor.realPart)))).sum
  99
 100/-- The canonical directed concrete Euler-ledger system attached to a sensor. -/
 101noncomputable def concreteDirectedEulerLedgerSystem (sensor : DefectSensor) :
 102    DirectedEulerLedgerSystem sensor where
 103  stage := sensorEulerLedger sensor
 104  stage_balanced := sensorEulerLedger_balanced sensor
 105  stage_net_flow_zero := sensorEulerLedger_net_flow_zero sensor
 106  stage_prime_pair := by
 107    intro support p hp
 108    exact ⟨primeEulerEvent_mem_sensorEulerLedger sensor hp,
 109      reciprocal_primeEulerEvent_mem_sensorEulerLedger sensor hp⟩
 110  stage_prime_pair_mono := by
 111    intro S T p hST hp
 112    exact ⟨primeEulerEvent_mem_sensorEulerLedger_of_subset sensor hST hp,
 113      reciprocal_primeEulerEvent_mem_sensorEulerLedger_of_subset sensor hST hp⟩
 114  directed_support := primeSupport_directed
 115  stage_cost_formula := sensorEulerLedger_cost_formula sensor
 116
 117/-- A convenient union-stage corollary: the union support contains the prime
 118data from both constituent supports. -/
 119theorem concreteDirectedEulerLedgerSystem_union_contains
 120    (sensor : DefectSensor) {S T : PrimeSupport} {p : Nat.Primes}
 121    (hp : p ∈ S ∨ p ∈ T) :
 122    let sys := concreteDirectedEulerLedgerSystem sensor
 123    primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
 124        (sys.stage (S ∪ T)).events ∧
 125      LedgerForcing.reciprocal
 126        (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
 127          (sys.stage (S ∪ T)).events := by
 128  let sys := concreteDirectedEulerLedgerSystem sensor
 129  rcases hp with hp | hp
 130  · exact sys.stage_prime_pair_mono Finset.subset_union_left hp
 131  · exact sys.stage_prime_pair_mono Finset.subset_union_right hp
 132
 133/-- The finite-to-directed arithmetic package, connected to the ontology-side
 134admissibility and realizability interfaces. -/
 135structure EulerLedgerOntologyInterface (sensor : DefectSensor) where
 136  /-- Concrete finite stages over prime supports. -/
 137  directedLedger : DirectedEulerLedgerSystem sensor
 138  /-- Analytic admissibility of the associated Euler trace. -/
 139  admissibleTrace : EulerTraceAdmissible sensor
 140  /-- T1-bounded realizability proxy coming from the Euler carrier. -/
 141  realizableProxy : PhysicallyRealizableLedger sensor
 142
 143/-- Every sensor has the combined directed-ledger / admissibility /
 144realizability package. -/
 145noncomputable def concreteEulerLedgerOntologyInterface (sensor : DefectSensor) :
 146    EulerLedgerOntologyInterface sensor where
 147  directedLedger := concreteDirectedEulerLedgerSystem sensor
 148  admissibleTrace := euler_trace_admissible sensor
 149  realizableProxy := euler_physically_realizable sensor
 150
 151/-- The ontology package carries a compatible regular Euler carrier. -/
 152theorem EulerLedgerOntologyInterface.has_regular_carrier
 153    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) :
 154    ∃ carrier : RegularCarrier,
 155      carrier.radius = sensor.realPart - 1 / 2 ∧ 0 < carrier.radius :=
 156  pkg.admissibleTrace.carrier_compatible
 157
 158/-- The realizability proxy in the ontology package is positive at every depth. -/
 159theorem EulerLedgerOntologyInterface.scalarState_pos
 160    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) (N : ℕ) :
 161    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 162    0 < PhysicallyRealizableLedger.scalarState (sensor := sensor) N := by
 163  letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 164  simpa using PhysicallyRealizableLedger.scalarStatePos (sensor := sensor) N
 165
 166/-- The realizability proxy in the ontology package has uniformly bounded T1
 167defect. -/
 168theorem EulerLedgerOntologyInterface.scalarDefectBounded
 169    {sensor : DefectSensor} (pkg : EulerLedgerOntologyInterface sensor) :
 170    letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 171    ∃ K : ℝ, ∀ N : ℕ,
 172      IndisputableMonolith.Foundation.LawOfExistence.defect
 173        (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) ≤ K := by
 174  letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 175  simpa using PhysicallyRealizableLedger.scalarDefectBounded (sensor := sensor)
 176
 177/-- Concrete theorem form: every sensor has a directed arithmetic Euler ledger,
 178an admissible Euler trace, and a T1-bounded realizability proxy. This is the
 179current strongest proved bridge from arithmetic Euler data into the ontology
 180layer. -/
 181theorem concreteEulerLedgerOntologyInterface_exists (sensor : DefectSensor) :
 182    ∃ pkg : EulerLedgerOntologyInterface sensor,
 183      (∀ support : PrimeSupport,
 184        LedgerForcing.balanced (pkg.directedLedger.stage support)) ∧
 185      (∀ support : PrimeSupport, ∀ agent : ℕ,
 186        LedgerForcing.net_flow (pkg.directedLedger.stage support) agent = 0) ∧
 187      (∃ carrier : RegularCarrier,
 188        carrier.radius = sensor.realPart - 1 / 2 ∧ 0 < carrier.radius) ∧
 189      (letI : PhysicallyRealizableLedger sensor := pkg.realizableProxy
 190       ∃ K : ℝ, ∀ N : ℕ,
 191        IndisputableMonolith.Foundation.LawOfExistence.defect
 192          (PhysicallyRealizableLedger.scalarState (sensor := sensor) N) ≤ K) := by
 193  refine ⟨concreteEulerLedgerOntologyInterface sensor, ?_, ?_, ?_, ?_⟩
 194  · intro support
 195    exact (concreteEulerLedgerOntologyInterface sensor).directedLedger.stage_balanced support
 196  · intro support agent
 197    exact (concreteEulerLedgerOntologyInterface sensor).directedLedger.stage_net_flow_zero support agent
 198  · exact (concreteEulerLedgerOntologyInterface sensor).has_regular_carrier
 199  · exact (concreteEulerLedgerOntologyInterface sensor).scalarDefectBounded
 200
 201end NumberTheory
 202end IndisputableMonolith
 203