structure
definition
def or abbrev
DirectedEulerLedgerSystem
show as:
view Lean formalization →
formal statement (Lean)
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
73 reciprocal. -/
74 stage_prime_pair :
75 ∀ {support : PrimeSupport} {p : Nat.Primes}, p ∈ support →
76 primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
77 (stage support).events ∧
78 LedgerForcing.reciprocal
79 (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
80 (stage support).events
81 /-- Coherence under support enlargement: any prime already present in a
82 smaller support remains present in every larger support. -/
83 stage_prime_pair_mono :
84 ∀ {S T : PrimeSupport} {p : Nat.Primes}, S ⊆ T → p ∈ S →
85 primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p ∈
86 (stage T).events ∧
87 LedgerForcing.reciprocal
88 (primeEulerEvent sensor.realPart (sensor_realPart_pos sensor) p) ∈
89 (stage T).events
90 /-- Directedness of the support index set. -/
91 directed_support :
92 ∀ S T : PrimeSupport, ∃ U : PrimeSupport, S ⊆ U ∧ T ⊆ U
93 /-- Explicit stage cost formula. -/
94 stage_cost_formula :
95 ∀ support : PrimeSupport,
96 LedgerForcing.ledger_cost (stage support) =
97 2 * (support.toList.map
98 (fun p : Nat.Primes => LedgerForcing.J ((p : ℝ) ^ (-sensor.realPart)))).sum
99
100/-- The canonical directed concrete Euler-ledger system attached to a sensor. -/