concreteDirectedEulerLedgerSystem

formal source

  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