primeSupport_directed

formal source

  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