IndisputableMonolith.NumberTheory.ConcreteEulerLedger

declarations in this module (25)

• theorem sensor_realPart_pos L35
• def primeEulerEvent L41
• theorem primeEulerEvent_ratio L48
• theorem primeEulerEvent_target L51
• theorem primeEulerEvent_ratio_lt_one L55
• theorem primeEulerEvent_ratio_ne_one L60
• theorem reciprocal_primeEulerEvent_ratio L65
• theorem primeEulerEvent_cost_eq_J L70
• theorem primeEulerEvent_cost_pos L76
• def finiteEulerLedger L90
• theorem finiteEulerLedger_balanced L96
• theorem finiteEulerLedger_net_flow_zero L101
• theorem primeEulerEvent_mem_finiteEulerLedger L107
• theorem reciprocal_primeEulerEvent_mem_finiteEulerLedger L121
• theorem ledger_cost_foldl_with_offset L136
• theorem add_event_cost_formula L150
• theorem finiteEulerLedger_cost_formula L162
• theorem finiteEulerLedger_cost_formula_J L175
• def sensorEulerLedger L183
• theorem sensorEulerLedger_balanced L188
• theorem sensorEulerLedger_net_flow_zero L194
• theorem primeEulerEvent_mem_sensorEulerLedger L201
• theorem reciprocal_primeEulerEvent_mem_sensorEulerLedger L211
• theorem sensorEulerLedger_cost_formula L221
• theorem sensorEulerLedger_identification L242