`sensorEulerLedger_balanced`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.ConcreteEulerLedger
domain: NumberTheory
line: 188 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.ConcreteEulerLedger on GitHub at line 188.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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)

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.