def CordialMiners.wt {P : Type u_1} (w : P → Weight) (A : Finset P) : Weight

The total weight of a finite participant set under a weight function. The PoR analogue of "how many signers", weighted by reputation.

Equations

• CordialMiners.wt w A = ∑ p ∈ A, w p

def CordialMiners.thresholdPassed (R W : Weight) (θ : Ratio) : Prop

A weighted set of total weight R crosses the threshold θ of committee weight W. Stated by cross-product so the check stays in ℕ: θ.num * W < R * θ.den reads as R / W > θ.num / θ.den.

Equations

• CordialMiners.thresholdPassed R W θ = (θ.num * W < R * θ.den)

def CordialMiners.thresholdPassedBool (R W : Weight) (θ : Ratio) : Bool

The decidable Boolean form of thresholdPassed, for executable reducers.

Equations

• CordialMiners.thresholdPassedBool R W θ = decide (θ.num * W < R * θ.den)

theorem CordialMiners.thresholdPassedBool_iff (R W : Weight) (θ : Ratio) : thresholdPassedBool R W θ = true ↔ thresholdPassed R W θ

Obligation D.3: the Boolean threshold check reflects the propositional one.

theorem CordialMiners.found_03_weight_mono {P : Type u_1} (w : P → Weight) {A B : Finset P} (h : A ⊆ B) : wt w A ≤ wt w B

FOUND-03: total weight is monotone in the set.

theorem CordialMiners.found_04_weight_inclusion_exclusion {P : Type u_1} [DecidableEq P] (w : P → Weight) (A B : Finset P) : wt w (A ∪ B) + wt w (A ∩ B) = wt w A + wt w B

FOUND-04: weighted inclusion-exclusion, stated additively so it stays in ℕ with no subtraction.

theorem CordialMiners.found_05_weighted_overlap {P : Type u_1} [DecidableEq P] (w : P → Weight) {C A B : Finset P} (θ : Ratio) (hAC : A ⊆ C) (hBC : B ⊆ C) (hA : thresholdPassed (wt w A) (wt w C) θ) (hB : thresholdPassed (wt w B) (wt w C) θ) : 2 * (θ.num * wt w C) < wt w (A ∩ B) * θ.den + wt w C * θ.den

FOUND-05: the weighted-overlap lemma, the heart of PoR threshold-finality safety. If two committee subsets A and B of C are each threshold-heavy for θ, their intersection carries more than (2θ - 1) of the committee weight. Stated Nat-safely as 2 (θ.num · W) < wt(A ∩ B) · θ.den + W · θ.den, which is exactly wt(A ∩ B) > (2θ - 1) W.