def
definition
isLock
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RRF.Hypotheses.EightTick on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44def balance_end : Phase := 7
45
46/-- Is this phase in the LOCK region? -/
47def isLock (p : Phase) : Bool := p.val ≤ 3
48
49/-- Is this phase in the BALANCE region? -/
50def isBalance (p : Phase) : Bool := p.val ≥ 4
51
52/-- LOCK and BALANCE partition the phases. -/
53theorem lock_balance_partition (p : Phase) : p.isLock ∨ p.isBalance := by
54 simp [isLock, isBalance]
55 omega
56
57/-- LOCK and BALANCE are disjoint. -/
58theorem lock_balance_disjoint (p : Phase) : ¬(p.isLock ∧ p.isBalance) := by
59 simp [isLock, isBalance]
60 omega
61
62/-- Successor phase (cyclic). -/
63def next (p : Phase) : Phase := p + 1
64
65/-- Predecessor phase (cyclic). -/
66def prev (p : Phase) : Phase := p - 1
67
68theorem next_prev (p : Phase) : (p.next).prev = p := by
69 simp [next, prev]
70
71theorem prev_next (p : Phase) : (p.prev).next = p := by
72 simp [next, prev]
73
74end Phase
75
76/-! ## The 8-Tick Hypothesis Class -/
77