Slashable bound
This file proves the quantitative half of accountable safety:
the weight of the slashable quorum intersection is lower-bounded by
a churn-adjusted expression involving the validator-set overlap and
the one-third residuals. Combined with the structural half
(Theories/AccountableSafety.lean), this yields the full
Gasper accountable-safety guarantee with dynamic validator sets.
The main theorem slashable_bound formalises Gasper's
Theorem 8.3 (dynamic-validator-set safety bound): given two
conflicting k-finalized blocks and a reference validator set
V_0, the weight of the slashable quorum intersection is at
least
\max\bigl(\operatorname{wt}(V_L) - a_L - e_R,\;\operatorname{wt}(V_R) - a_R - e_L\bigr) - f_{1/3}(\operatorname{wt}(V_L)) - f_{1/3}(\operatorname{wt}(V_R))
where a_L, a_R are activation weights and e_L, e_R are exit
weights relative to V_0. When V_L = V_R = V_0 (no churn),
the bound specialises to \operatorname{wt}(V) - 2\,f_{1/3}(\operatorname{wt}(V)),
recovering the static Casper FFG overlap.
Validator-set churn
Four functions capture validator churn between a reference set
V_0 and a branch set V:
-
activated = V \setminus V_0 (validators that entered)
-
exited = V_0 \setminus V (validators that left)
-
actwt, extwt — their weights
Derivation chain
The proof builds in two independent pipelines that merge in
slashable_bound:
-
Quorum overlap (purely weight-algebraic, no block tree):
wt_meet_bound_fUnion \to
wt_meet_subbound_fUnion \to
wt_quorum_union_bound_fUnion \to
quorum_intersection_weight_lower
-
Churn bound (Venn-diagram geometry on three sets):
wt_meet_tri_bound_fDiff \to
validator_intersection_lower_bound
The merger in slashable_bound invokes k_safety'
to obtain the structural witness, then chains the two pipelines
by truncated-subtraction monotonicity.
Non-goals of this file
This file does not prove that the displayed lower bound is
strictly positive — that depends on the concrete threshold instance
and the magnitude of churn (see the appendix of
Lemmas/AccountableSafety.lean).
variable {Validator : Type u}variable [DecidableEq Validator]
Activated validators
Validators present in s_2 but absent from s_1:
\operatorname{activated}(s_1, s_2) = \operatorname{fDiff}(s_2, s_1) = s_2 \setminus s_1.
The first argument s_1 is the reference set, the second s_2
the branch set; the result is the set that entered between them.
def activated (s1 s2 : Finset Validator) : Finset Validator :=
fDiff s2 s1
Exited validators
Validators present in s_1 but absent from s_2:
\operatorname{exited}(s_1, s_2) = \operatorname{fDiff}(s_1, s_2) = s_1 \setminus s_2.
The first argument s_1 is the reference set, the second s_2
the branch set; the result is the set that left between them.
def exited (s1 s2 : Finset Validator) : Finset Validator :=
fDiff s1 s2
Weight of the activated validators: \operatorname{wt}(\operatorname{activated}(s_1, s_2)).
def actwt (stake : Validator → Nat) (s1 s2 : Finset Validator) : Nat :=
wt stake (activated s1 s2)
Weight of the exited validators: \operatorname{wt}(\operatorname{exited}(s_1, s_2)).
def extwt (stake : Validator → Nat) (s1 s2 : Finset Validator) : Nat :=
wt stake (exited s1 s2)
Nested-intersection weight bound via inclusion–exclusion
\operatorname{wt}(s_1 \cap s_2) + \operatorname{wt}(s_1' \cap s_2') \;\ge\; \operatorname{wt}(s_1 \cap (s_1' \cap s_2')) + \operatorname{wt}(s_2 \cap (s_1' \cap s_2'))
Assumptions
s_1 \subseteq s_1' and s_2 \subseteq s_2' — quorum–set
inclusion hypotheses.
Interpretation
Each quorum's share of the validator-set intersection, when summed,
is bounded by the sum of the quorum–quorum intersection and the
validator–validator intersection. This is the first step in the
derivation chain toward the slashable bound.
Proof idea
Apply wt_add_inter_fUnion to the two crossed terms
s_1 \cap (s_1' \cap s_2') and s_2 \cap (s_1' \cap s_2'),
yielding their weight sum as a union weight plus an intersection
weight. Then:
-
Union bound: the union
\operatorname{fUnion}(s_1 \cap (s_1' \cap s_2'),\, s_2 \cap (s_1' \cap s_2'))
is a subset of s_1' \cap s_2' (each element comes from a
crossed term whose second factor is s_1' \cap s_2'), so
wt_inc_leq gives
\operatorname{wt}(\text{union}) \le \operatorname{wt}(s_1' \cap s_2').
-
Intersection simplification: the intersection of the two
crossed terms simplifies to s_1 \cap s_2 (hIeq, proved
by Finset.ext — the s_1' \cap s_2' factors cancel
because s_1 \subseteq s_1' and s_2 \subseteq s_2' make
them redundant when both are present). This replaces the
intersection weight with \operatorname{wt}(s_1 \cap s_2).
Combining and commuting gives the conclusion.
theorem wt_meet_bound_fUnion
(stake : Validator → Nat)
(s1 s2 s1' s2' : Finset Validator)
(hs1 : s1 ⊆ s1')
(hs2 : s2 ⊆ s2') :
wt stake (s1 ∩ s2) + wt stake (s1' ∩ s2')
≥
wt stake (s1 ∩ (s1' ∩ s2'))
+
wt stake (s2 ∩ (s1' ∩ s2')) :=
have hAdd : wt stake (s1 ∩ (s1' ∩ s2')) + wt stake (s2 ∩ (s1' ∩ s2')) =
wt stake (fUnion (s1 ∩ (s1' ∩ s2')) (s2 ∩ (s1' ∩ s2'))) +
wt stake ((s1 ∩ (s1' ∩ s2')) ∩ (s2 ∩ (s1' ∩ s2'))) :=
wt_add_inter_fUnion stake (s1 ∩ (s1' ∩ s2')) (s2 ∩ (s1' ∩ s2'))
have hUle : wt stake (fUnion (s1 ∩ (s1' ∩ s2')) (s2 ∩ (s1' ∩ s2')))
≤ wt stake (s1' ∩ s2') :=
wt_inc_leq stake (fun _ hx => (mem_fUnion.mp hx).elim
(fun hxA => match Finset.mem_inter.mp hxA with | ⟨_, h⟩ => h)
(fun hxB => match Finset.mem_inter.mp hxB with | ⟨_, h⟩ => h))
have hIeq : (s1 ∩ (s1' ∩ s2')) ∩ (s2 ∩ (s1' ∩ s2')) = s1 ∩ s2 :=
Finset.ext fun _ =>
⟨fun hx =>
match Finset.mem_inter.mp hx with
| ⟨hxA, hxB⟩ =>
Finset.mem_inter.mpr
⟨match Finset.mem_inter.mp hxA with | ⟨h, _⟩ => h,
match Finset.mem_inter.mp hxB with | ⟨h, _⟩ => h⟩,
fun hx =>
match Finset.mem_inter.mp hx with
| ⟨h1, h2⟩ =>
Finset.mem_inter.mpr
⟨Finset.mem_inter.mpr ⟨h1, Finset.mem_inter.mpr ⟨hs1 h1, hs2 h2⟩⟩,
Finset.mem_inter.mpr ⟨h2, Finset.mem_inter.mpr ⟨hs1 h1, hs2 h2⟩⟩⟩⟩
hAdd.le.trans
((Nat.add_le_add_right hUle _).trans
(Nat.le_of_eq
((congrArg (wt stake (s1' ∩ s2') + wt stake ·) hIeq).trans
(Nat.add_comm (wt stake (s1' ∩ s2')) (wt stake (s1 ∩ s2))))))
wt_meet_bound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s1 s2 s1' s2' : Finset Validator),
Subset s1 s1' →
Subset s2 s2' →
GE.ge (HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s1 ├ Finset Validator
4 │ │ s2 ├ Finset Validator
5 │ │ s1' ├ Finset Validator
6 │ │ s2' ├ Finset Validator
7 │ │ hs1 ├ Subset s1 s1'
8 │ │ hs2 ├ Subset s2 s2'
9 │ │ wt_add_inter_fUnion │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
11│ │ x✝ │ ┌ Validator
12│ │ hx │ ├ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
13│ │ mem_fUnion │ │ Iff
(Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(Or (Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝))
14│13,12 │ Iff.mp │ │ Or
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
15│ │ hxA │ │ ┌ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
16│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
17│16,15 │ Iff.mp │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
18│ │ left✝ │ │ │ ┌ Membership.mem s1 x✝
19│ │ h │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
20│18,19,19 │ ∀I │ │ │ Membership.mem s1 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem (Inter.inter s1' s2') x✝
21│17,20 │ wt_meet_bound_fUnion.match_1 │ │ │ Membership.mem (Inter.inter s1' s2') x✝
22│15,21 │ ∀I │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s1' s2') x✝
23│ │ hxB │ │ ┌ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
24│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s2 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
25│24,23 │ Iff.mp │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
26│ │ left✝ │ │ │ ┌ Membership.mem s2 x✝
27│ │ h │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
28│26,27,27 │ ∀I │ │ │ Membership.mem s2 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem (Inter.inter s1' s2') x✝
29│25,28 │ wt_meet_bound_fUnion.match_1 │ │ │ Membership.mem (Inter.inter s1' s2') x✝
30│23,29 │ ∀I │ │ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s1' s2') x✝
31│14,22,30 │ Or.elim │ │ Membership.mem (Inter.inter s1' s2') x✝
32│11,12,31 │ ∀I │ ∀ (x : Validator),
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x →
Membership.mem (Inter.inter s1' s2') x
33│32 │ wt_inc_leq │ LE.le
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter s1' s2'))
35│ │ x✝ │ ┌ Validator
36│ │ hx │ │ ┌ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
37│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(And (Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝))
38│37,36 │ Iff.mp │ │ │ And
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
39│ │ hxA │ │ │ ┌ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
40│ │ hxB │ │ │ ├ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
41│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1 s2) x✝) (And (Membership.mem s1 x✝) (Membership.mem s2 x✝))
42│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
43│42,39 │ Iff.mp │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
44│ │ h │ │ │ │ ┌ Membership.mem s1 x✝
45│ │ right✝ │ │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
46│44,45,44 │ ∀I │ │ │ │ Membership.mem s1 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem s1 x✝
47│43,46 │ wt_meet_bound_fUnion.match_1 │ │ │ │ Membership.mem s1 x✝
48│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s2 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
49│48,40 │ Iff.mp │ │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
50│ │ h │ │ │ │ ┌ Membership.mem s2 x✝
51│ │ right✝ │ │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
52│50,51,50 │ ∀I │ │ │ │ Membership.mem s2 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem s2 x✝
53│49,52 │ wt_meet_bound_fUnion.match_1 │ │ │ │ Membership.mem s2 x✝
54│47,53 │ And.intro │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem s2 x✝)
55│41,54 │ Iff.mpr │ │ │ │ Membership.mem (Inter.inter s1 s2)
x✝
56│39,40,55 │ ∀I │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝ → Membership.mem (Inter.inter s1 s2) x✝
57│38,56 │ wt_meet_bound_fUnion.match_2 │ │ │ Membership.mem (Inter.inter s1 s2) x✝
58│36,57 │ ∀I │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝ →
Membership.mem (Inter.inter s1 s2) x✝
59│ │ hx │ │ ┌ Membership.mem (Inter.inter s1 s2) x✝
60│41,59 │ Iff.mp │ │ │ And (Membership.mem s1 x✝)
(Membership.mem s2 x✝)
61│ │ h1 │ │ │ ┌ Membership.mem s1 x✝
62│ │ h2 │ │ │ ├ Membership.mem s2 x✝
63│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1' s2') x✝) (And (Membership.mem s1' x✝) (Membership.mem s2' x✝))
64│7,61 │ ∀E │ │ │ │ Membership.mem s1' x✝
65│8,62 │ ∀E │ │ │ │ Membership.mem s2' x✝
66│64,65 │ And.intro │ │ │ │ And (Membership.mem s1' x✝)
(Membership.mem s2' x✝)
67│63,66 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s1' s2') x✝
68│61,67 │ And.intro │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
69│42,68 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
70│62,67 │ And.intro │ │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
71│48,70 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
72│69,71 │ And.intro │ │ │ │ And
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
73│37,72 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
74│61,62,73 │ ∀I │ │ │ Membership.mem s1 x✝ →
Membership.mem s2 x✝ →
Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
75│60,74 │ wt_meet_bound_fUnion.match_3 │ │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
76│59,75 │ ∀I │ │ Membership.mem (Inter.inter s1 s2) x✝ →
Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
77│58,76 │ Iff.intro │ │ Iff
(Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(Membership.mem (Inter.inter s1 s2) x✝)
78│35,77 │ ∀I │ ∀ (x : Validator),
Iff (Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x)
(Membership.mem (Inter.inter s1 s2) x)
79│78 │ Finset.ext │ Eq
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) (Inter.inter s1 s2)
81│9 │ Eq.le │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
82│33 │ Nat.add_le_add_right │ LE.le
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
83│79 │ congrArg │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1' s2')) (wt stake (Inter.inter s1 s2)))
84│ │ Nat.add_comm │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2')) (wt stake (Inter.inter s1 s2)))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
85│83,84 │ Eq.trans │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
86│85 │ Nat.le_of_eq │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
87│82,86 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
88│81,87 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
89│0,1,2,3,4,5,6,7,8,88│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s1 s2 s1' s2' : Finset Validator),
Subset s1 s1' →
Subset s2 s2' →
LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
#detail_explode wt_meet_bound_fUnionwt_meet_bound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s1 s2 s1' s2' : Finset Validator),
Subset s1 s1' →
Subset s2 s2' →
GE.ge (HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s1 ├ Finset Validator
4 │ │ s2 ├ Finset Validator
5 │ │ s1' ├ Finset Validator
6 │ │ s2' ├ Finset Validator
7 │ │ hs1 ├ Subset s1 s1'
8 │ │ hs2 ├ Subset s2 s2'
9 │ │ wt_add_inter_fUnion │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
11│ │ x✝ │ ┌ Validator
12│ │ hx │ ├ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
13│ │ mem_fUnion │ │ Iff
(Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(Or (Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝))
14│13,12 │ Iff.mp │ │ Or
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
15│ │ hxA │ │ ┌ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
16│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
17│16,15 │ Iff.mp │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
18│ │ left✝ │ │ │ ┌ Membership.mem s1 x✝
19│ │ h │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
20│18,19,19 │ ∀I │ │ │ Membership.mem s1 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem (Inter.inter s1' s2') x✝
21│17,20 │ wt_meet_bound_fUnion.match_1 │ │ │ Membership.mem (Inter.inter s1' s2') x✝
22│15,21 │ ∀I │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s1' s2') x✝
23│ │ hxB │ │ ┌ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
24│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s2 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
25│24,23 │ Iff.mp │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
26│ │ left✝ │ │ │ ┌ Membership.mem s2 x✝
27│ │ h │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
28│26,27,27 │ ∀I │ │ │ Membership.mem s2 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem (Inter.inter s1' s2') x✝
29│25,28 │ wt_meet_bound_fUnion.match_1 │ │ │ Membership.mem (Inter.inter s1' s2') x✝
30│23,29 │ ∀I │ │ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s1' s2') x✝
31│14,22,30 │ Or.elim │ │ Membership.mem (Inter.inter s1' s2') x✝
32│11,12,31 │ ∀I │ ∀ (x : Validator),
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x →
Membership.mem (Inter.inter s1' s2') x
33│32 │ wt_inc_leq │ LE.le
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter s1' s2'))
35│ │ x✝ │ ┌ Validator
36│ │ hx │ │ ┌ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
37│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(And (Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝))
38│37,36 │ Iff.mp │ │ │ And
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
39│ │ hxA │ │ │ ┌ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
40│ │ hxB │ │ │ ├ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
41│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1 s2) x✝) (And (Membership.mem s1 x✝) (Membership.mem s2 x✝))
42│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
43│42,39 │ Iff.mp │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
44│ │ h │ │ │ │ ┌ Membership.mem s1 x✝
45│ │ right✝ │ │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
46│44,45,44 │ ∀I │ │ │ │ Membership.mem s1 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem s1 x✝
47│43,46 │ wt_meet_bound_fUnion.match_1 │ │ │ │ Membership.mem s1 x✝
48│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s2 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
49│48,40 │ Iff.mp │ │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
50│ │ h │ │ │ │ ┌ Membership.mem s2 x✝
51│ │ right✝ │ │ │ │ ├ Membership.mem
(Inter.inter s1' s2') x✝
52│50,51,50 │ ∀I │ │ │ │ Membership.mem s2 x✝ →
Membership.mem (Inter.inter s1' s2') x✝ → Membership.mem s2 x✝
53│49,52 │ wt_meet_bound_fUnion.match_1 │ │ │ │ Membership.mem s2 x✝
54│47,53 │ And.intro │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem s2 x✝)
55│41,54 │ Iff.mpr │ │ │ │ Membership.mem (Inter.inter s1 s2)
x✝
56│39,40,55 │ ∀I │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝ →
Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝ → Membership.mem (Inter.inter s1 s2) x✝
57│38,56 │ wt_meet_bound_fUnion.match_2 │ │ │ Membership.mem (Inter.inter s1 s2) x✝
58│36,57 │ ∀I │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝ →
Membership.mem (Inter.inter s1 s2) x✝
59│ │ hx │ │ ┌ Membership.mem (Inter.inter s1 s2) x✝
60│41,59 │ Iff.mp │ │ │ And (Membership.mem s1 x✝)
(Membership.mem s2 x✝)
61│ │ h1 │ │ │ ┌ Membership.mem s1 x✝
62│ │ h2 │ │ │ ├ Membership.mem s2 x✝
63│ │ Finset.mem_inter │ │ │ │ Iff
(Membership.mem (Inter.inter s1' s2') x✝) (And (Membership.mem s1' x✝) (Membership.mem s2' x✝))
64│7,61 │ ∀E │ │ │ │ Membership.mem s1' x✝
65│8,62 │ ∀E │ │ │ │ Membership.mem s2' x✝
66│64,65 │ And.intro │ │ │ │ And (Membership.mem s1' x✝)
(Membership.mem s2' x✝)
67│63,66 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s1' s2') x✝
68│61,67 │ And.intro │ │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
69│42,68 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
70│62,67 │ And.intro │ │ │ │ And (Membership.mem s2 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
71│48,70 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter s2 (Inter.inter s1' s2')) x✝
72│69,71 │ And.intro │ │ │ │ And
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝) (Membership.mem (Inter.inter s2 (Inter.inter s1' s2')) x✝)
73│37,72 │ Iff.mpr │ │ │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
74│61,62,73 │ ∀I │ │ │ Membership.mem s1 x✝ →
Membership.mem s2 x✝ →
Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
75│60,74 │ wt_meet_bound_fUnion.match_3 │ │ │ Membership.mem
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
76│59,75 │ ∀I │ │ Membership.mem (Inter.inter s1 s2) x✝ →
Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝
77│58,76 │ Iff.intro │ │ Iff
(Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x✝)
(Membership.mem (Inter.inter s1 s2) x✝)
78│35,77 │ ∀I │ ∀ (x : Validator),
Iff (Membership.mem (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) x)
(Membership.mem (Inter.inter s1 s2) x)
79│78 │ Finset.ext │ Eq
(Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))) (Inter.inter s1 s2)
81│9 │ Eq.le │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
82│33 │ Nat.add_le_add_right │ LE.le
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
83│79 │ congrArg │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1' s2')) (wt stake (Inter.inter s1 s2)))
84│ │ Nat.add_comm │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2')) (wt stake (Inter.inter s1 s2)))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
85│83,84 │ Eq.trans │ Eq
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
86│85 │ Nat.le_of_eq │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1' s2'))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
87│82,86 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2'))))
(wt stake (Inter.inter (Inter.inter s1 (Inter.inter s1' s2')) (Inter.inter s2 (Inter.inter s1' s2')))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
88│81,87 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
89│0,1,2,3,4,5,6,7,8,88│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s1 s2 s1' s2' : Finset Validator),
Subset s1 s1' →
Subset s2 s2' →
LE.le
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (Inter.inter s2 (Inter.inter s1' s2'))))
(HAdd.hAdd (wt stake (Inter.inter s1 s2)) (wt stake (Inter.inter s1' s2')))
A quorum's share of the validator-set intersection
Statement
\operatorname{wt}(s_1 \cap (s_1' \cap s_2')) + \operatorname{wt}(\operatorname{fDiff}(s_1', s_2')) \;\ge\; \operatorname{wt}(s_1)
Interpretation
Each quorum s_1 can be split, relative to the validator-set
intersection s_1' \cap s_2', into a part that lies inside the
intersection and a part that lies in the difference
s_1' \setminus s_2'. Their combined weight is at least
\operatorname{wt}(s_1), giving a lower bound on how much of
s_1's weight is accounted for by these two regions.
Proof idea
Every element of s_1 \subseteq s_1' either lies in
s_1' \cap s_2' (and hence in s_1 \cap (s_1' \cap s_2')) or
in s_1' \setminus s_2'. The two parts are disjoint
(disjointMF): an element of s_1 \cap (s_1' \cap s_2')
has its second factor in s_1' \cap s_2', whereas every
element of \operatorname{fDiff}(s_1', s_2') lies outside
s_2', so no element can belong to both. The subset inclusion
s_1 \;\subseteq\; \operatorname{fUnion}\bigl(s_1 \cap (s_1' \cap s_2'),\;\operatorname{fDiff}(s_1', s_2')\bigr)
then gives
\operatorname{wt}(s_1) \le \operatorname{wt}(\operatorname{fUnion}(\ldots))
by wt_inc_leq, and disjointness expands the right side
to the plain sum by wt_fUnion_of_disjointMF.
Role in the development
Supplies the per-quorum weight bound consumed by
wt_meet_bound_fUnion (which sums two such bounds) and
ultimately by quorum_intersection_weight_lower.
wt_meet_subbound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s1 s1' s2' : Finset Validator),
Subset s1 s1' →
GE.ge (HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2'))) (wt stake s1)
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s1 ├ Finset Validator
4 │ │ s1' ├ Finset Validator
5 │ │ s2' ├ Finset Validator
6 │ │ hs1 ├ Subset s1 s1'
7 │ │ x✝ │ ┌ Validator
8 │ │ hx │ ├ Membership.mem s1 x✝
9 │ │ hx2 │ │ ┌ Membership.mem s2' x✝
10│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
11│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1' s2') x✝) (And (Membership.mem s1' x✝) (Membership.mem s2' x✝))
12│6,8 │ ∀E │ │ │ Membership.mem s1' x✝
13│12,9 │ And.intro │ │ │ And (Membership.mem s1' x✝)
(Membership.mem s2' x✝)
14│11,13 │ Iff.mpr │ │ │ Membership.mem (Inter.inter s1' s2') x✝
15│8,14 │ And.intro │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
16│10,15 │ Iff.mpr │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
17│16 │ mem_fUnion_left │ │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
18│9,17 │ ∀I │ │ Membership.mem s2' x✝ →
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
19│ │ hx2 │ │ ┌ Not (Membership.mem s2' x✝)
20│12,19 │ mem_fDiff_of_mem_of_not_mem │ │ │ Membership.mem (fDiff s1' s2') x✝
21│20 │ mem_fUnion_right │ │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
22│19,21 │ ∀I │ │ Not (Membership.mem s2' x✝) →
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
23│18,22 │ dite │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
24│7,8,23 │ ∀I │ ∀ (x : Validator),
Membership.mem s1 x → Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x
26│ │ x │ ┌ Validator
27│ │ hxA │ ├ Membership.mem
(Finset.val (Inter.inter s1 (Inter.inter s1' s2'))) x
28│ │ hxB │ ├ Membership.mem (Finset.val (fDiff s1' s2'))
x
30│ │ Finset.mem_inter │ │ Iff (Membership.mem (Inter.inter s1' s2') x)
(And (Membership.mem s1' x) (Membership.mem s2' x))
31│ │ Finset.mem_inter │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x)
(And (Membership.mem s1 x) (Membership.mem (Inter.inter s1' s2') x))
33│31,27 │ Iff.mp │ │ And (Membership.mem s1 x)
(Membership.mem (Inter.inter s1' s2') x)
34│33 │ And.right │ │ Membership.mem (Inter.inter s1' s2') x
35│30,34 │ Iff.mp │ │ And (Membership.mem s1' x)
(Membership.mem s2' x)
36│35 │ And.right │ │ Membership.mem s2' x
37│28,36 │ not_mem_right_of_mem_fDiff │ │ False
38│26,27,28,37 │ ∀I │ ∀ (x : Validator),
Membership.mem (Finset.val (Inter.inter s1 (Inter.inter s1' s2'))) x →
Membership.mem (Finset.val (fDiff s1' s2')) x → False
40│24 │ wt_inc_leq │ LE.le (wt stake s1)
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
41│38 │ wt_fUnion_of_disjointMF │ Eq
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
42│41 │ Nat.le_of_eq │ LE.le
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
43│40,42 │ LE.le.trans │ LE.le (wt stake s1)
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
44│0,1,2,3,4,5,6,43│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s1 s1' s2' : Finset Validator),
Subset s1 s1' →
LE.le (wt stake s1) (HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
#detail_explode wt_meet_subbound_fUnionwt_meet_subbound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s1 s1' s2' : Finset Validator),
Subset s1 s1' →
GE.ge (HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2'))) (wt stake s1)
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s1 ├ Finset Validator
4 │ │ s1' ├ Finset Validator
5 │ │ s2' ├ Finset Validator
6 │ │ hs1 ├ Subset s1 s1'
7 │ │ x✝ │ ┌ Validator
8 │ │ hx │ ├ Membership.mem s1 x✝
9 │ │ hx2 │ │ ┌ Membership.mem s2' x✝
10│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x✝)
(And (Membership.mem s1 x✝) (Membership.mem (Inter.inter s1' s2') x✝))
11│ │ Finset.mem_inter │ │ │ Iff
(Membership.mem (Inter.inter s1' s2') x✝) (And (Membership.mem s1' x✝) (Membership.mem s2' x✝))
12│6,8 │ ∀E │ │ │ Membership.mem s1' x✝
13│12,9 │ And.intro │ │ │ And (Membership.mem s1' x✝)
(Membership.mem s2' x✝)
14│11,13 │ Iff.mpr │ │ │ Membership.mem (Inter.inter s1' s2') x✝
15│8,14 │ And.intro │ │ │ And (Membership.mem s1 x✝)
(Membership.mem (Inter.inter s1' s2') x✝)
16│10,15 │ Iff.mpr │ │ │ Membership.mem
(Inter.inter s1 (Inter.inter s1' s2')) x✝
17│16 │ mem_fUnion_left │ │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
18│9,17 │ ∀I │ │ Membership.mem s2' x✝ →
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
19│ │ hx2 │ │ ┌ Not (Membership.mem s2' x✝)
20│12,19 │ mem_fDiff_of_mem_of_not_mem │ │ │ Membership.mem (fDiff s1' s2') x✝
21│20 │ mem_fUnion_right │ │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
22│19,21 │ ∀I │ │ Not (Membership.mem s2' x✝) →
Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
23│18,22 │ dite │ │ Membership.mem
(fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x✝
24│7,8,23 │ ∀I │ ∀ (x : Validator),
Membership.mem s1 x → Membership.mem (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')) x
26│ │ x │ ┌ Validator
27│ │ hxA │ ├ Membership.mem
(Finset.val (Inter.inter s1 (Inter.inter s1' s2'))) x
28│ │ hxB │ ├ Membership.mem (Finset.val (fDiff s1' s2'))
x
30│ │ Finset.mem_inter │ │ Iff (Membership.mem (Inter.inter s1' s2') x)
(And (Membership.mem s1' x) (Membership.mem s2' x))
31│ │ Finset.mem_inter │ │ Iff
(Membership.mem (Inter.inter s1 (Inter.inter s1' s2')) x)
(And (Membership.mem s1 x) (Membership.mem (Inter.inter s1' s2') x))
33│31,27 │ Iff.mp │ │ And (Membership.mem s1 x)
(Membership.mem (Inter.inter s1' s2') x)
34│33 │ And.right │ │ Membership.mem (Inter.inter s1' s2') x
35│30,34 │ Iff.mp │ │ And (Membership.mem s1' x)
(Membership.mem s2' x)
36│35 │ And.right │ │ Membership.mem s2' x
37│28,36 │ not_mem_right_of_mem_fDiff │ │ False
38│26,27,28,37 │ ∀I │ ∀ (x : Validator),
Membership.mem (Finset.val (Inter.inter s1 (Inter.inter s1' s2'))) x →
Membership.mem (Finset.val (fDiff s1' s2')) x → False
40│24 │ wt_inc_leq │ LE.le (wt stake s1)
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
41│38 │ wt_fUnion_of_disjointMF │ Eq
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
42│41 │ Nat.le_of_eq │ LE.le
(wt stake (fUnion (Inter.inter s1 (Inter.inter s1' s2')) (fDiff s1' s2')))
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
43│40,42 │ LE.le.trans │ LE.le (wt stake s1)
(HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
44│0,1,2,3,4,5,6,43│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s1 s1' s2' : Finset Validator),
Subset s1 s1' →
LE.le (wt stake s1) (HAdd.hAdd (wt stake (Inter.inter s1 (Inter.inter s1' s2'))) (wt stake (fDiff s1' s2')))
Triangle bound on difference weights
\operatorname{wt}(\operatorname{fDiff}(s_1, s_2)) \;\le\; \operatorname{wt}(\operatorname{fDiff}(s_0, s_2)) + \operatorname{wt}(\operatorname{fDiff}(s_1, s_0))
The weight of s_1 \setminus s_2 is bounded by the sum of the
weights of s_0 \setminus s_2 and s_1 \setminus s_0.
Proof idea
fDiff_subset_triangle gives the set-level containment
s_1 \setminus s_2 \subseteq \operatorname{fUnion}(s_0 \setminus s_2,\, s_1 \setminus s_0).
Weighing via wt_inc_leq gives
\operatorname{wt}(s_1 \setminus s_2) \le \operatorname{wt}(\operatorname{fUnion}(\ldots)).
wt_fUnion expands the right side to
\operatorname{wt}(s_0 \setminus s_2) + \operatorname{wt}(\operatorname{fDiff}(\operatorname{fDiff}(s_1, s_0),\, \operatorname{fDiff}(s_0, s_2))),
and the inner fDiff is idempotent (an element of
s_1 \setminus s_0 cannot also lie in s_0 \setminus s_2,
since the latter requires \in s_0), so the auxiliary fact
hfdf simplifies the sum to
\operatorname{wt}(s_0 \setminus s_2) + \operatorname{wt}(s_1 \setminus s_0).
wt_meet_tri_bound_fDiff : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s0 s1 s2 : Finset Validator),
LE.le (wt stake (fDiff s1 s2)) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s0 ├ Finset Validator
4 │ │ s1 ├ Finset Validator
5 │ │ s2 ├ Finset Validator
6 │ │ x✝ │ ┌ Validator
7 │ │ hx │ │ ┌ Membership.mem
(fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
8 │7 │ mem_left_of_mem_fDiff │ │ │ Membership.mem (fDiff s1 s0) x✝
9 │7,8 │ ∀I │ │ Membership.mem
(fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝ →
Membership.mem (fDiff s1 s0) x✝
10│ │ hx │ │ ┌ Membership.mem (fDiff s1 s0) x✝
11│ │ hxfD │ │ │ ┌ Membership.mem (fDiff s0 s2) x✝
12│11 │ mem_left_of_mem_fDiff │ │ │ │ Membership.mem s0 x✝
13│10,12 │ not_mem_right_of_mem_fDiff │ │ │ │ False
14│11,13 │ ∀I │ │ │ Membership.mem (fDiff s0 s2) x✝ → False
15│10,14 │ mem_fDiff_of_mem_of_not_mem │ │ │ Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
16│10,15 │ ∀I │ │ Membership.mem (fDiff s1 s0) x✝ →
Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
17│9,16 │ Iff.intro │ │ Iff
(Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝) (Membership.mem (fDiff s1 s0) x✝)
18│6,17 │ ∀I │ ∀ (x : Validator),
Iff (Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x) (Membership.mem (fDiff s1 s0) x)
19│18 │ Finset.ext │ Eq (fDiff (fDiff s1 s0) (fDiff s0 s2))
(fDiff s1 s0)
21│ │ fDiff_subset_triangle │ Subset (fDiff s1 s2) (fUnion (fDiff s0 s2) (fDiff s1 s0))
22│21 │ wt_inc_leq │ LE.le (wt stake (fDiff s1 s2))
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0)))
23│ │ wt_fUnion │ Eq (wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0)))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff (fDiff s1 s0) (fDiff s0 s2))))
24│19 │ congrArg │ Eq
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff (fDiff s1 s0) (fDiff s0 s2))))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
25│23,24 │ Eq.trans │ Eq
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0))) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
26│25 │ Nat.le_of_eq │ LE.le
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0))) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
27│22,26 │ LE.le.trans │ LE.le (wt stake (fDiff s1 s2))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
28│0,1,2,3,4,5,27│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s0 s1 s2 : Finset Validator),
LE.le (wt stake (fDiff s1 s2)) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
#detail_explode wt_meet_tri_bound_fDiffwt_meet_tri_bound_fDiff : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(s0 s1 s2 : Finset Validator),
LE.le (wt stake (fDiff s1 s2)) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ s0 ├ Finset Validator
4 │ │ s1 ├ Finset Validator
5 │ │ s2 ├ Finset Validator
6 │ │ x✝ │ ┌ Validator
7 │ │ hx │ │ ┌ Membership.mem
(fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
8 │7 │ mem_left_of_mem_fDiff │ │ │ Membership.mem (fDiff s1 s0) x✝
9 │7,8 │ ∀I │ │ Membership.mem
(fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝ →
Membership.mem (fDiff s1 s0) x✝
10│ │ hx │ │ ┌ Membership.mem (fDiff s1 s0) x✝
11│ │ hxfD │ │ │ ┌ Membership.mem (fDiff s0 s2) x✝
12│11 │ mem_left_of_mem_fDiff │ │ │ │ Membership.mem s0 x✝
13│10,12 │ not_mem_right_of_mem_fDiff │ │ │ │ False
14│11,13 │ ∀I │ │ │ Membership.mem (fDiff s0 s2) x✝ → False
15│10,14 │ mem_fDiff_of_mem_of_not_mem │ │ │ Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
16│10,15 │ ∀I │ │ Membership.mem (fDiff s1 s0) x✝ →
Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝
17│9,16 │ Iff.intro │ │ Iff
(Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x✝) (Membership.mem (fDiff s1 s0) x✝)
18│6,17 │ ∀I │ ∀ (x : Validator),
Iff (Membership.mem (fDiff (fDiff s1 s0) (fDiff s0 s2)) x) (Membership.mem (fDiff s1 s0) x)
19│18 │ Finset.ext │ Eq (fDiff (fDiff s1 s0) (fDiff s0 s2))
(fDiff s1 s0)
21│ │ fDiff_subset_triangle │ Subset (fDiff s1 s2) (fUnion (fDiff s0 s2) (fDiff s1 s0))
22│21 │ wt_inc_leq │ LE.le (wt stake (fDiff s1 s2))
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0)))
23│ │ wt_fUnion │ Eq (wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0)))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff (fDiff s1 s0) (fDiff s0 s2))))
24│19 │ congrArg │ Eq
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff (fDiff s1 s0) (fDiff s0 s2))))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
25│23,24 │ Eq.trans │ Eq
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0))) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
26│25 │ Nat.le_of_eq │ LE.le
(wt stake (fUnion (fDiff s0 s2) (fDiff s1 s0))) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
27│22,26 │ LE.le.trans │ LE.le (wt stake (fDiff s1 s2))
(HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
28│0,1,2,3,4,5,27│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (s0 s1 s2 : Finset Validator),
LE.le (wt stake (fDiff s1 s2)) (HAdd.hAdd (wt stake (fDiff s0 s2)) (wt stake (fDiff s1 s0)))
Quorum sum bounded by overlap plus union
Statement
\operatorname{wt}(q_L) + \operatorname{wt}(q_R) \;\le\; \operatorname{wt}(q_L \cap q_R) + \operatorname{wt}(\operatorname{fUnion}(V_L, V_R))
Interpretation
The total weight of two quorums exceeds their intersection weight
by at most the weight of the union of the two validator sets. This
is the quorum-level restatement of inclusion–exclusion: the
"double-counted" part is \operatorname{wt}(q_L \cap q_R), and
the "universe" that bounds the remainder is
\operatorname{fUnion}(V_L, V_R).
Proof idea
Apply wt_add_inter_fUnion to the quorums themselves:
\operatorname{wt}(q_L) + \operatorname{wt}(q_R) = \operatorname{wt}(\operatorname{fUnion}(q_L, q_R)) + \operatorname{wt}(q_L \cap q_R)
Then bound \operatorname{wt}(\operatorname{fUnion}(q_L, q_R))
by \operatorname{wt}(\operatorname{fUnion}(V_L, V_R)) via
wt_inc_leq composed with fUnion_subset (using
q_L \subseteq V_L and q_R \subseteq V_R). Commuting the sum
gives the conclusion.
Role in the development
The quorum-level inclusion–exclusion step that feeds
quorum_intersection_weight_lower: it combines the two
quorum thresholds with the union weight to lower-bound the
quorum intersection.
theorem wt_quorum_union_bound_fUnion
(stake : Validator → Nat)
{qL qR vL vR : Finset Validator}
(hqLsub : qL ⊆ vL)
(hqRsub : qR ⊆ vR) :
wt stake qL + wt stake qR
≤
wt stake (qL ∩ qR) + wt stake (fUnion vL vR) :=
have hUle : wt stake (fUnion qL qR) ≤ wt stake (fUnion vL vR) :=
wt_inc_leq stake (fUnion_subset
(fun _ hx => mem_fUnion_left (hqLsub hx))
(fun _ hx => mem_fUnion_right (hqRsub hx)))
have hAdd : wt stake qL + wt stake qR =
wt stake (fUnion qL qR) + wt stake (qL ∩ qR) :=
wt_add_inter_fUnion stake qL qR
hAdd.le.trans
((Nat.le_of_eq (Nat.add_comm (wt stake (fUnion qL qR)) (wt stake (qL ∩ qR)))).trans
(Nat.add_le_add_left hUle _))
wt_quorum_union_bound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
{qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (HAdd.hAdd (wt stake qL) (wt stake qR)) (HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ qL ├ Finset Validator
4 │ │ qR ├ Finset Validator
5 │ │ vL ├ Finset Validator
6 │ │ vR ├ Finset Validator
7 │ │ hqLsub ├ Subset qL vL
8 │ │ hqRsub ├ Subset qR vR
9 │ │ x✝ │ ┌ Validator
10│ │ hx │ ├ Membership.mem qL x✝
11│7,10 │ ∀E │ │ Membership.mem vL x✝
12│11 │ mem_fUnion_left │ │ Membership.mem (fUnion vL vR) x✝
13│9,10,12 │ ∀I │ ∀ (x : Validator),
Membership.mem qL x → Membership.mem (fUnion vL vR) x
14│ │ x✝ │ ┌ Validator
15│ │ hx │ ├ Membership.mem qR x✝
16│8,15 │ ∀E │ │ Membership.mem vR x✝
17│16 │ mem_fUnion_right │ │ Membership.mem (fUnion vL vR) x✝
18│14,15,17 │ ∀I │ ∀ (x : Validator),
Membership.mem qR x → Membership.mem (fUnion vL vR) x
19│13,18 │ fUnion_subset │ Subset (fUnion qL qR) (fUnion vL vR)
20│19 │ wt_inc_leq │ LE.le (wt stake (fUnion qL qR)) (wt stake (fUnion vL vR))
22│ │ wt_add_inter_fUnion │ Eq (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
24│22 │ Eq.le │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
25│ │ Nat.add_comm │ Eq
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
26│25 │ Nat.le_of_eq │ LE.le
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
27│20 │ Nat.add_le_add_left │ LE.le
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
28│26,27 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
29│24,28 │ LE.le.trans │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
30│0,1,2,3,4,5,6,7,8,29│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (HAdd.hAdd (wt stake qL) (wt stake qR)) (HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
#detail_explode wt_quorum_union_bound_fUnionwt_quorum_union_bound_fUnion : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
{qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (HAdd.hAdd (wt stake qL) (wt stake qR)) (HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ qL ├ Finset Validator
4 │ │ qR ├ Finset Validator
5 │ │ vL ├ Finset Validator
6 │ │ vR ├ Finset Validator
7 │ │ hqLsub ├ Subset qL vL
8 │ │ hqRsub ├ Subset qR vR
9 │ │ x✝ │ ┌ Validator
10│ │ hx │ ├ Membership.mem qL x✝
11│7,10 │ ∀E │ │ Membership.mem vL x✝
12│11 │ mem_fUnion_left │ │ Membership.mem (fUnion vL vR) x✝
13│9,10,12 │ ∀I │ ∀ (x : Validator),
Membership.mem qL x → Membership.mem (fUnion vL vR) x
14│ │ x✝ │ ┌ Validator
15│ │ hx │ ├ Membership.mem qR x✝
16│8,15 │ ∀E │ │ Membership.mem vR x✝
17│16 │ mem_fUnion_right │ │ Membership.mem (fUnion vL vR) x✝
18│14,15,17 │ ∀I │ ∀ (x : Validator),
Membership.mem qR x → Membership.mem (fUnion vL vR) x
19│13,18 │ fUnion_subset │ Subset (fUnion qL qR) (fUnion vL vR)
20│19 │ wt_inc_leq │ LE.le (wt stake (fUnion qL qR)) (wt stake (fUnion vL vR))
22│ │ wt_add_inter_fUnion │ Eq (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
24│22 │ Eq.le │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
25│ │ Nat.add_comm │ Eq
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
26│25 │ Nat.le_of_eq │ LE.le
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
27│20 │ Nat.add_le_add_left │ LE.le
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
28│26,27 │ LE.le.trans │ LE.le
(HAdd.hAdd (wt stake (fUnion qL qR)) (wt stake (Inter.inter qL qR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
29│24,28 │ LE.le.trans │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
30│0,1,2,3,4,5,6,7,8,29│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (HAdd.hAdd (wt stake qL) (wt stake qR)) (HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
Quorum-intersection weight lower bound
Statement
\operatorname{wt}(V_L \cap V_R) - f_{1/3}(\operatorname{wt}(V_L)) - f_{1/3}(\operatorname{wt}(V_R)) \;\le\; \operatorname{wt}(q_L \cap q_R)
Interpretation
The weight of the quorum intersection q_L \cap q_R — the set
whose members are all slashed by the structural half — is at least
the validator-set overlap \operatorname{wt}(V_L \cap V_R) minus
the two one-third residuals. This is the quantitative core of the
pigeonhole argument: two \frac{2}{3}-quorums drawn from
overlapping validator sets must share a substantial portion. In
the static case V_L = V_R = V this reduces to
\operatorname{wt}(V) - 2\,f_{1/3}(\operatorname{wt}(V)) \le \operatorname{wt}(q_L \cap q_R),
the classic \frac{1}{3}-overlap bound.
Assumptions
-
q_L \subseteq V_L, q_R \subseteq V_R — quorum–set inclusion;
-
f_{2/3}(\operatorname{wt}(V_L)) \le \operatorname{wt}(q_L),
f_{2/3}(\operatorname{wt}(V_R)) \le \operatorname{wt}(q_R) — the
quorum weight conditions.
Proof idea
Instantiate the pure-arithmetic kernel
nat_quorum_intersection_arith with:
-
A + B = U + I ← wt_add_inter_fUnion on V_L, V_R;
-
A = O_L + T_L, B = O_R + T_R ←
threshold_decomposition on each set's weight;
-
T_L + T_R \le Q + U ←
wt_quorum_union_bound_fUnion composed with the quorum
weight hypotheses.
Non-assumptions
The two validator sets V_L, V_R need not be equal — this is the
dynamic-validator-set reading. When they coincide the bound
specialises to the static Casper FFG form.
quorum_intersection_weight_lower : ∀ {Validator : Type u} [inst : DecidableEq Validator] (τ : Threshold)
(stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (Threshold.two_third τ (wt stake vL)) (wt stake qL) →
LE.le (Threshold.two_third τ (wt stake vR)) (wt stake qR) →
LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ τ ├ Threshold
3 │ │ stake ├ Validator → Nat
4 │ │ qL ├ Finset Validator
5 │ │ qR ├ Finset Validator
6 │ │ vL ├ Finset Validator
7 │ │ vR ├ Finset Validator
8 │ │ hqLsub ├ Subset qL vL
9 │ │ hqRsub ├ Subset qR vR
10│ │ hqLwt ├ LE.le
(Threshold.two_third τ (wt stake vL)) (wt stake qL)
11│ │ hqRwt ├ LE.le
(Threshold.two_third τ (wt stake vR)) (wt stake qR)
12│ │ wt_add_inter_fUnion │ Eq (HAdd.hAdd (wt stake vL) (wt stake vR))
(HAdd.hAdd (wt stake (fUnion vL vR)) (wt stake (Inter.inter vL vR)))
13│ │ threshold_decomposition │ Eq (wt stake vL)
(HAdd.hAdd (Threshold.one_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vL)))
14│ │ threshold_decomposition │ Eq (wt stake vR)
(HAdd.hAdd (Threshold.one_third τ (wt stake vR)) (Threshold.two_third τ (wt stake vR)))
15│10,11 │ Nat.add_le_add │ LE.le
(HAdd.hAdd (Threshold.two_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vR)))
(HAdd.hAdd (wt stake qL) (wt stake qR))
16│8,9 │ wt_quorum_union_bound_fUnion │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
17│15,16 │ le_trans │ LE.le
(HAdd.hAdd (Threshold.two_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
18│12,13,14,17 │ nat_quorum_intersection_arith │ LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
19│0,1,2,3,4,5,6,7,8,9,10,11,18│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (τ : Threshold) (stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (Threshold.two_third τ (wt stake vL)) (wt stake qL) →
LE.le (Threshold.two_third τ (wt stake vR)) (wt stake qR) →
LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
#detail_explode quorum_intersection_weight_lowerquorum_intersection_weight_lower : ∀ {Validator : Type u} [inst : DecidableEq Validator] (τ : Threshold)
(stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (Threshold.two_third τ (wt stake vL)) (wt stake qL) →
LE.le (Threshold.two_third τ (wt stake vR)) (wt stake qR) →
LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ τ ├ Threshold
3 │ │ stake ├ Validator → Nat
4 │ │ qL ├ Finset Validator
5 │ │ qR ├ Finset Validator
6 │ │ vL ├ Finset Validator
7 │ │ vR ├ Finset Validator
8 │ │ hqLsub ├ Subset qL vL
9 │ │ hqRsub ├ Subset qR vR
10│ │ hqLwt ├ LE.le
(Threshold.two_third τ (wt stake vL)) (wt stake qL)
11│ │ hqRwt ├ LE.le
(Threshold.two_third τ (wt stake vR)) (wt stake qR)
12│ │ wt_add_inter_fUnion │ Eq (HAdd.hAdd (wt stake vL) (wt stake vR))
(HAdd.hAdd (wt stake (fUnion vL vR)) (wt stake (Inter.inter vL vR)))
13│ │ threshold_decomposition │ Eq (wt stake vL)
(HAdd.hAdd (Threshold.one_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vL)))
14│ │ threshold_decomposition │ Eq (wt stake vR)
(HAdd.hAdd (Threshold.one_third τ (wt stake vR)) (Threshold.two_third τ (wt stake vR)))
15│10,11 │ Nat.add_le_add │ LE.le
(HAdd.hAdd (Threshold.two_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vR)))
(HAdd.hAdd (wt stake qL) (wt stake qR))
16│8,9 │ wt_quorum_union_bound_fUnion │ LE.le (HAdd.hAdd (wt stake qL) (wt stake qR))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
17│15,16 │ le_trans │ LE.le
(HAdd.hAdd (Threshold.two_third τ (wt stake vL)) (Threshold.two_third τ (wt stake vR)))
(HAdd.hAdd (wt stake (Inter.inter qL qR)) (wt stake (fUnion vL vR)))
18│12,13,14,17 │ nat_quorum_intersection_arith │ LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
19│0,1,2,3,4,5,6,7,8,9,10,11,18│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (τ : Threshold) (stake : Validator → Nat) {qL qR vL vR : Finset Validator},
Subset qL vL →
Subset qR vR →
LE.le (Threshold.two_third τ (wt stake vL)) (wt stake qL) →
LE.le (Threshold.two_third τ (wt stake vR)) (wt stake qR) →
LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter vL vR)) (Threshold.one_third τ (wt stake vL)))
(Threshold.one_third τ (wt stake vR)))
(wt stake (Inter.inter qL qR))
Venn-diagram bound on validator-set overlap
Statement
\max\bigl(\operatorname{wt}(V_L) - a_L - e_R,\; \operatorname{wt}(V_R) - a_R - e_L\bigr) \;\le\; \operatorname{wt}(V_L \cap V_R)
where a_L = \operatorname{actwt}(V_0, V_L),
e_R = \operatorname{extwt}(V_0, V_R), etc.
Interpretation
The overlap V_L \cap V_R of two branch validator sets is
lower-bounded by the weight of each branch minus the churn relative
to a reference set V_0. The two branches of the \max give
two independent lower bounds — one from the V_L perspective
(subtracting V_L's activations and V_R's exits) and one
from V_R's — and the \max selects the tighter one. This
captures the Venn-diagram geometry of three overlapping sets
V_0, V_L, V_R: the part of V_L that survives in V_R is
at least V_L minus the validators that entered V_L after
V_0 (who were never in V_0 \cap V_R) and the validators
that left V_0 before reaching V_R.
Proof idea
Each branch of max_le follows the same pattern:
wt_fDiff rewrites
\operatorname{wt}(V_L) - \operatorname{wt}(V_L \cap V_R) as
\operatorname{wt}(\operatorname{fDiff}(V_L, V_R)), then
wt_meet_tri_bound_fDiff bounds that difference by
\operatorname{wt}(\operatorname{fDiff}(V_0, V_R)) + \operatorname{wt}(\operatorname{fDiff}(V_L, V_0)),
which unfold to e_R + a_L. The helper
nat_sub_sub_le_of_sub_le_add converts this additive bound
into the displayed truncated-subtraction form. The second branch
is symmetric, with inter_commF swapping V_L \cap V_R to
V_R \cap V_L.
Role in the development
The churn-pipeline terminus: feeds into slashable_bound as
the lower bound on
\operatorname{wt}(V_L \cap V_R), which is then chained with
quorum_intersection_weight_lower (the quorum-pipeline
terminus) via truncated-subtraction monotonicity.
validator_intersection_lower_bound : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(v0 vL vR : Finset Validator),
LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ v0 ├ Finset Validator
4 │ │ vL ├ Finset Validator
5 │ │ vR ├ Finset Validator
6 │ │ wt_fDiff │ Eq (wt stake (fDiff vL vR))
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR)))
7 │6 │ Eq.symm │ Eq
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vL vR))
8 │7 │ Nat.le_of_eq │ LE.le
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vL vR))
9 │ │ wt_meet_tri_bound_fDiff │ LE.le (wt stake (fDiff vL vR))
(HAdd.hAdd (wt stake (fDiff v0 vR)) (wt stake (fDiff vL v0)))
10│8,9 │ LE.le.trans │ LE.le
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (HAdd.hAdd (extwt stake v0 vR) (actwt stake v0 vL))
11│10 │ nat_sub_sub_le_of_sub_le_add │ LE.le
(HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR)) (wt stake (Inter.inter vL vR))
12│ │ inter_commF │ Eq (Inter.inter vR vL) (Inter.inter vL vR)
13│12 │ Eq.symm │ Eq (Inter.inter vL vR) (Inter.inter vR vL)
14│13 │ congrArg │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL)))
15│ │ wt_fDiff │ Eq (wt stake (fDiff vR vL))
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL)))
16│15 │ Eq.symm │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL))) (wt stake (fDiff vR vL))
17│14,16 │ Eq.trans │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vR vL))
18│17 │ Nat.le_of_eq │ LE.le
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vR vL))
19│ │ wt_meet_tri_bound_fDiff │ LE.le (wt stake (fDiff vR vL))
(HAdd.hAdd (wt stake (fDiff v0 vL)) (wt stake (fDiff vR v0)))
20│18,19 │ LE.le.trans │ LE.le
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (HAdd.hAdd (extwt stake v0 vL) (actwt stake v0 vR))
21│20 │ nat_sub_sub_le_of_sub_le_add │ LE.le
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)) (wt stake (Inter.inter vL vR))
22│11,21 │ max_le │ LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
23│0,1,2,3,4,5,22│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (v0 vL vR : Finset Validator),
LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
#detail_explode validator_intersection_lower_boundvalidator_intersection_lower_bound : ∀ {Validator : Type u} [inst : DecidableEq Validator] (stake : Validator → Nat)
(v0 vL vR : Finset Validator),
LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
0 │ │ Validator ├ Type u
1 │ │ inst✝ ├ DecidableEq Validator
2 │ │ stake ├ Validator → Nat
3 │ │ v0 ├ Finset Validator
4 │ │ vL ├ Finset Validator
5 │ │ vR ├ Finset Validator
6 │ │ wt_fDiff │ Eq (wt stake (fDiff vL vR))
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR)))
7 │6 │ Eq.symm │ Eq
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vL vR))
8 │7 │ Nat.le_of_eq │ LE.le
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vL vR))
9 │ │ wt_meet_tri_bound_fDiff │ LE.le (wt stake (fDiff vL vR))
(HAdd.hAdd (wt stake (fDiff v0 vR)) (wt stake (fDiff vL v0)))
10│8,9 │ LE.le.trans │ LE.le
(HSub.hSub (wt stake vL) (wt stake (Inter.inter vL vR))) (HAdd.hAdd (extwt stake v0 vR) (actwt stake v0 vL))
11│10 │ nat_sub_sub_le_of_sub_le_add │ LE.le
(HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR)) (wt stake (Inter.inter vL vR))
12│ │ inter_commF │ Eq (Inter.inter vR vL) (Inter.inter vL vR)
13│12 │ Eq.symm │ Eq (Inter.inter vL vR) (Inter.inter vR vL)
14│13 │ congrArg │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL)))
15│ │ wt_fDiff │ Eq (wt stake (fDiff vR vL))
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL)))
16│15 │ Eq.symm │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vR vL))) (wt stake (fDiff vR vL))
17│14,16 │ Eq.trans │ Eq
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vR vL))
18│17 │ Nat.le_of_eq │ LE.le
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (wt stake (fDiff vR vL))
19│ │ wt_meet_tri_bound_fDiff │ LE.le (wt stake (fDiff vR vL))
(HAdd.hAdd (wt stake (fDiff v0 vL)) (wt stake (fDiff vR v0)))
20│18,19 │ LE.le.trans │ LE.le
(HSub.hSub (wt stake vR) (wt stake (Inter.inter vL vR))) (HAdd.hAdd (extwt stake v0 vL) (actwt stake v0 vR))
21│20 │ nat_sub_sub_le_of_sub_le_add │ LE.le
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)) (wt stake (Inter.inter vL vR))
22│11,21 │ max_le │ LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
23│0,1,2,3,4,5,22│ ∀I │ ∀ {Validator : Type u}
[inst : DecidableEq Validator] (stake : Validator → Nat) (v0 vL vR : Finset Validator),
LE.le
(max (HSub.hSub (HSub.hSub (wt stake vL) (actwt stake v0 vL)) (extwt stake v0 vR))
(HSub.hSub (HSub.hSub (wt stake vR) (actwt stake v0 vR)) (extwt stake v0 vL)))
(wt stake (Inter.inter vL vR))
variable {Hash : Type v}variable [DecidableEq Hash]variable [Fintype Validator]
Slashable bound (main theorem)
A finalization fork produces a quorum pair whose intersection has
weight at least the churn-adjusted bound:
\max(\operatorname{wt}(V_L) - a_L - e_R,\; \operatorname{wt}(V_R) - a_R - e_L) - f_{1/3}(\operatorname{wt}(V_L)) - f_{1/3}(\operatorname{wt}(V_R)) \;\le\; \operatorname{wt}(q_L \cap q_R)
Proof idea
Apply k_safety' to the two k-finalized blocks and
their mutual non-ancestry hypotheses. This produces the
q_intersection_slashed witness — a 9-tuple
(b_L, b_R, q_L, q_R, \text{subset}_L, \text{subset}_R, \text{quorum}_L, \text{quorum}_R, \text{slashing}) — from
which the first eight components are retained and the ninth
(the universal slashing quantifier over the intersection) is
discarded (written _ in the match), since the quantitative
bound does not need the slashing itself.
With the two quorums in hand, compose two inequalities by
truncated-subtraction monotonicity (Nat.sub_le_sub_right):
-
validator_intersection_lower_bound — bounds
\operatorname{wt}(V_L \cap V_R) from below by the churn
expression \max(\operatorname{wt}(V_L) - a_L - e_R,\; \operatorname{wt}(V_R) - a_R - e_L);
-
quorum_intersection_weight_lower — bounds
\operatorname{wt}(q_L \cap q_R) from below by
\operatorname{wt}(V_L \cap V_R) - f_{1/3}(\operatorname{wt}(V_L)) - f_{1/3}(\operatorname{wt}(V_R)).
The transitivity of \le under iterated truncated subtraction
chains the two bounds into the displayed conclusion.
Assumptions
Two k-finalized blocks with mutual non-ancestry, plus a
reference block b_0 from which the churn is measured.
Non-assumptions
The theorem does not assert the intersection is nonempty; whether
the displayed lower bound is strictly positive depends on the
concrete threshold instance and the magnitude of churn (see the
appendix of Lemmas/AccountableSafety.lean).
theorem slashable_bound
(τ : Threshold)
(stake : Validator → Nat)
(vset : Hash → Finset Validator)
(parent : HashParent Hash)
(genesis : Hash)
(st : State Validator Hash)
(b0 b1 b2 : Hash)
(b1_h b2_h k1 k2 : Nat)
(hb1f : k_finalized τ stake vset parent genesis st b1 b1_h k1)
(hb2f : k_finalized τ stake vset parent genesis st b2 b2_h k2)
(hconf12 : ¬ hash_ancestor parent b1 b2)
(hconf21 : ¬ hash_ancestor parent b2 b1) :
∃ bL bR : Hash,
∃ qL qR : Finset Validator,
qL ⊆ vset bL ∧
qR ⊆ vset bR ∧
max
(wt stake (vset bL) - actwt stake (vset b0) (vset bL) - extwt stake (vset b0) (vset bR))
(wt stake (vset bR) - actwt stake (vset b0) (vset bR) - extwt stake (vset b0) (vset bL))
- τ.one_third (wt stake (vset bL))
- τ.one_third (wt stake (vset bR))
≤
wt stake (qL ∩ qR) :=
match k_safety' τ stake vset parent genesis st hb1f hb2f hconf21 hconf12 with
| ⟨bL, bR, qL, qR, hqLsub, hqRsub, hqLq2, hqRq2, _⟩ =>
⟨bL, bR, qL, qR, hqLsub, hqRsub,
le_trans
(Nat.sub_le_sub_right
(Nat.sub_le_sub_right
(validator_intersection_lower_bound stake (vset b0) (vset bL) (vset bR)) _) _)
(quorum_intersection_weight_lower τ stake hqLsub hqRsub hqLq2.2 hqRq2.2)⟩
slashable_bound : ∀ {Validator : Type u} [inst : DecidableEq Validator] {Hash : Type v} [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) (b0 b1 b2 : Hash) (b1_h b2_h k1 k2 : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b1 b2) →
Not (hash_ancestor parent b2 b1) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
0 │ │ Validator ├ Type
u
1 │ │ inst✝² ├ DecidableEq
Validator
2 │ │ Hash ├ Type
v
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b0 ├ Hash
12│ │ b1 ├ Hash
13│ │ b2 ├ Hash
14│ │ b1_h ├ Nat
15│ │ b2_h ├ Nat
16│ │ k1 ├ Nat
17│ │ k2 ├ Nat
18│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
19│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
20│ │ hconf12 ├ Not
(hash_ancestor parent b1 b2)
21│ │ hconf21 ├ Not
(hash_ancestor parent b2 b1)
22│18,19,21,20 │ k_safety' │ q_intersection_slashed
τ stake vset st
23│ │ bL │ ┌ Hash
24│ │ bR │ ├ Hash
25│ │ qL │ ├ Finset
Validator
26│ │ qR │ ├ Finset
Validator
27│ │ hqLsub │ ├ Subset
qL (vset bL)
28│ │ hqRsub │ ├ Subset
qR (vset bR)
29│ │ hqLq2 │ ├ quorum_2
τ stake vset qL bL
30│ │ hqRq2 │ ├ quorum_2
τ stake vset qR bR
31│ │ right✝ │ ├ ∀
(v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v
32│ │ validator_intersection_lower_bound │ │ LE.le
(max (HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR))) (extwt stake (vset b0) (vset bL))))
(wt stake (Inter.inter (vset bL) (vset bR)))
33│32 │ Nat.sub_le_sub_right │ │ LE.le
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR))) (extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
34│33 │ Nat.sub_le_sub_right │ │ LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(HSub.hSub (HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
35│29 │ And.right │ │ LE.le
(Threshold.two_third τ (wt stake (vset bL))) (wt stake qL)
36│30 │ And.right │ │ LE.le
(Threshold.two_third τ (wt stake (vset bR))) (wt stake qR)
37│27,28,35,36 │ quorum_intersection_weight_lower │ │ LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))
38│34,37 │ le_trans │ │ LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))
39│28,38 │ And.intro │ │ And
(Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR)))
40│27,39 │ And.intro │ │ And
(Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
41│40 │ Exists.intro │ │ Exists
fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
42│41 │ Exists.intro │ │ Exists
fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
43│42 │ Exists.intro │ │ Exists
fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
44│43 │ Exists.intro │ │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
45│23,24,25,26,27,28,29,30,31,44 │ ∀I │ ∀
(bL bR : Hash) (qL qR : Finset Validator),
Subset qL (vset bL) →
Subset qR (vset bR) →
quorum_2 τ stake vset qL bL →
quorum_2 τ stake vset qR bR →
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
46│22,45 │ slashable_bound.match_1 │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
47│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,46│ ∀I │ ∀
{Validator : Type u} [inst : DecidableEq Validator] {Hash : Type v} [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) (b0 b1 b2 : Hash) (b1_h b2_h k1 k2 : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b1 b2) →
Not (hash_ancestor parent b2 b1) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
#detail_explode slashable_boundslashable_bound : ∀ {Validator : Type u} [inst : DecidableEq Validator] {Hash : Type v} [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) (b0 b1 b2 : Hash) (b1_h b2_h k1 k2 : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b1 b2) →
Not (hash_ancestor parent b2 b1) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
0 │ │ Validator ├ Type
u
1 │ │ inst✝² ├ DecidableEq
Validator
2 │ │ Hash ├ Type
v
3 │ │ inst✝¹ ├ DecidableEq
Hash
4 │ │ inst✝ ├ Fintype
Validator
5 │ │ τ ├ Threshold
6 │ │ stake ├ Validator →
Nat
7 │ │ vset ├ Hash →
Finset Validator
8 │ │ parent ├ HashParent
Hash
9 │ │ genesis ├ Hash
10│ │ st ├ State
Validator Hash
11│ │ b0 ├ Hash
12│ │ b1 ├ Hash
13│ │ b2 ├ Hash
14│ │ b1_h ├ Nat
15│ │ b2_h ├ Nat
16│ │ k1 ├ Nat
17│ │ k2 ├ Nat
18│ │ hb1f ├ k_finalized
τ stake vset parent genesis st b1 b1_h k1
19│ │ hb2f ├ k_finalized
τ stake vset parent genesis st b2 b2_h k2
20│ │ hconf12 ├ Not
(hash_ancestor parent b1 b2)
21│ │ hconf21 ├ Not
(hash_ancestor parent b2 b1)
22│18,19,21,20 │ k_safety' │ q_intersection_slashed
τ stake vset st
23│ │ bL │ ┌ Hash
24│ │ bR │ ├ Hash
25│ │ qL │ ├ Finset
Validator
26│ │ qR │ ├ Finset
Validator
27│ │ hqLsub │ ├ Subset
qL (vset bL)
28│ │ hqRsub │ ├ Subset
qR (vset bR)
29│ │ hqLq2 │ ├ quorum_2
τ stake vset qL bL
30│ │ hqRq2 │ ├ quorum_2
τ stake vset qR bR
31│ │ right✝ │ ├ ∀
(v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v
32│ │ validator_intersection_lower_bound │ │ LE.le
(max (HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR))) (extwt stake (vset b0) (vset bL))))
(wt stake (Inter.inter (vset bL) (vset bR)))
33│32 │ Nat.sub_le_sub_right │ │ LE.le
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR))) (extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
34│33 │ Nat.sub_le_sub_right │ │ LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(HSub.hSub (HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
35│29 │ And.right │ │ LE.le
(Threshold.two_third τ (wt stake (vset bL))) (wt stake qL)
36│30 │ And.right │ │ LE.le
(Threshold.two_third τ (wt stake (vset bR))) (wt stake qR)
37│27,28,35,36 │ quorum_intersection_weight_lower │ │ LE.le
(HSub.hSub (HSub.hSub (wt stake (Inter.inter (vset bL) (vset bR))) (Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))
38│34,37 │ le_trans │ │ LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL))) (extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))
39│28,38 │ And.intro │ │ And
(Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR)))
40│27,39 │ And.intro │ │ And
(Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
41│40 │ Exists.intro │ │ Exists
fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
42│41 │ Exists.intro │ │ Exists
fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
43│42 │ Exists.intro │ │ Exists
fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
44│43 │ Exists.intro │ │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
45│23,24,25,26,27,28,29,30,31,44 │ ∀I │ ∀
(bL bR : Hash) (qL qR : Finset Validator),
Subset qL (vset bL) →
Subset qR (vset bR) →
quorum_2 τ stake vset qL bL →
quorum_2 τ stake vset qR bR →
(∀ (v : Validator), Membership.mem qL v → Membership.mem qR v → slashed st v) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
46│22,45 │ slashable_bound.match_1 │ Exists
fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))
47│0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,46│ ∀I │ ∀
{Validator : Type u} [inst : DecidableEq Validator] {Hash : Type v} [inst_1 : DecidableEq Hash]
[inst_2 : Fintype Validator] (τ : Threshold) (stake : Validator → Nat) (vset : Hash → Finset Validator)
(parent : HashParent Hash) (genesis : Hash) (st : State Validator Hash) (b0 b1 b2 : Hash) (b1_h b2_h k1 k2 : Nat),
k_finalized τ stake vset parent genesis st b1 b1_h k1 →
k_finalized τ stake vset parent genesis st b2 b2_h k2 →
Not (hash_ancestor parent b1 b2) →
Not (hash_ancestor parent b2 b1) →
Exists fun (bL : Hash) =>
Exists fun (bR : Hash) =>
Exists fun (qL : Finset Validator) =>
Exists fun (qR : Finset Validator) =>
And (Subset qL (vset bL))
(And (Subset qR (vset bR))
(LE.le
(HSub.hSub
(HSub.hSub
(max
(HSub.hSub (HSub.hSub (wt stake (vset bL)) (actwt stake (vset b0) (vset bL)))
(extwt stake (vset b0) (vset bR)))
(HSub.hSub (HSub.hSub (wt stake (vset bR)) (actwt stake (vset b0) (vset bR)))
(extwt stake (vset b0) (vset bL))))
(Threshold.one_third τ (wt stake (vset bL))))
(Threshold.one_third τ (wt stake (vset bR))))
(wt stake (Inter.inter qL qR))))