def
definition
SimpleLedger
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Recognition.ModelingExamples on GitHub at line 16.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
13}
14
15/-- A balanced ledger on the simple structure. -/
16def SimpleLedger : Ledger SimpleStructure := {
17 debit := fun _ => 1,
18 credit := fun _ => 0
19}
20
21/-- The simple structure satisfies conservation on closed chains. -/
22instance : Conserves SimpleLedger := {
23 conserve := by
24 intro ch hclosed
25 simp [chainFlux, phi]
26 -- For any closed chain, head = last, so flux = 0
27 rw [hclosed]
28 ring
29}
30
31/-- A simple tick schedule alternating between the two vertices. -/
32def SimpleTicks : Nat → Bool → Prop := fun t v => v = (t % 2 == 1)
33
34instance : AtomicTick SimpleStructure := {
35 postedAt := SimpleTicks,
36 unique_post := by
37 intro t
38 use (t % 2 == 1)
39 constructor
40 · rfl
41 · intro u hu
42 simp [SimpleTicks] at hu
43 exact hu
44}
45
46/-- Example of BoundedStep on Bool with degree 1. -/