PrimeSupport

formal source

  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)