structure CordialMiners.CommitteeSnapshot (P : Type u_2) : Type u_2

A committee snapshot: the finite committee, each member's PoR weight, the total committee weight, and the rational threshold. Reputation itself is a structured upstream object; the snapshot records only its projection to a weight, which is the parameter the consensus math depends on.

• committee : Finset P
• weight : P → Weight
• totalWeight : Weight
• threshold : Ratio

def CordialMiners.CommitteeSnapshot.WF {P : Type u_1} (S : CommitteeSnapshot P) : Prop

A snapshot is well formed when the recorded total weight is the sum of member weights and the threshold is strictly between 0 and 1 (so the overlap margin 2θ − 1 is meaningful).

Equations

• S.WF = (S.totalWeight = CordialMiners.wt S.weight S.committee ∧ 0 < S.threshold.num ∧ S.threshold.num < S.threshold.den)

def CordialMiners.CommitteeSnapshot.Heavy {P : Type u_1} (S : CommitteeSnapshot P) (A : Finset P) : Prop

A set of committee members is threshold-heavy: it is within the committee and its weight crosses the threshold of the total committee weight.

Equations

• S.Heavy A = (A ⊆ S.committee ∧ CordialMiners.thresholdPassed (CordialMiners.wt S.weight A) S.totalWeight S.threshold)

def CordialMiners.CommitteeSnapshot.ByzBound {P : Type u_1} [DecidableEq P] (S : CommitteeSnapshot P) (honest : Finset P) : Prop

The Byzantine-weight bound that makes threshold finality self-enforcing: the total weight of the non-honest committee members is at most (2θ − 1)·W. Stated Nat-safely as wt(C \ honest)·den + W·den ≤ 2·(num·W), i.e. wt(C \ honest) ≤ (2θ − 1)W.

Equations

• S.ByzBound honest = (CordialMiners.wt S.weight (S.committee \ honest) * S.threshold.den + S.totalWeight * S.threshold.den ≤ 2 * (S.threshold.num * S.totalWeight))