feat: concrete Bernoulli lottery model proving lemma1's good-event bound

[adust09]

Summary

Shrinks the trusted base around the three probabilistic axioms (lemma1, lemma4, proposition1): the already-proved Chernoff/measure-theoretic layer (Probabilistic/CountBound.lean, Basic.lean, LeaderWindow.lean) is now connected to a concrete product-Bernoulli lottery model, so that the good event assumed by axiom lemma1 is proved as a real theorem with explicit constants. What remains between this theorem and discharging the axiom is stated precisely in the capstone docstring — the gap is now a documented model-instantiation gap, not an unproved concentration argument.

New file Goldfish/Probabilistic/Lottery.lean (539 lines), wired into the Goldfish.Probabilistic umbrella, plus a Barrier-1 status note in README.md.

Model

• eligLot V thr hthr : Measure ((Slot × V) → Bool) — Measure.infinitePi product-Bernoulli over per-(slot, validator) eligibility coordinates; counts are defined at every slot, horizons enter only through the good event.
• advEligibleCount / honEligibleCount — random counts over the adversarial split A / Aᶜ.
• leaderLot p hp : Measure (Slot → Bool) — per-slot Bernoulli honest-leader lottery.

Theorems and explicit constants

• diff_count_subG — Hoeffding instantiation: each signed indicator lies in a length-1 interval ⇒ sub-Gaussian parameter c = 1/4 per validator (hasSubgaussianMGF_of_mem_Icc), independence via iIndepFun_infinitePi, parameters add via HasSubgaussianMGF.sum_of_iIndepFun. Packaged as eligCountLottery : CountLottery, feeding the already-proved exceeds_bound_union.
• honest_majority_horizon_bound — consumes the actual Compliant (1/2) ε n₀ fields; concludes μ.real {∃ t ∈ H, hon ≤ adv} ≤ |H| · exp(−g²/(2c)) with g = ε·thr·n₀, c = |V|/4.
• no_honest_leader_window_bound — ≤ |H| · (1 − p₀)^κ for any p₀ ≤ p, reusing the proved no_leader_window_union_bound (the iIndepSet hypothesis proved from the product structure).
• lemma1_good_event_bound — capstone on the product measure: failure of the horizon reading of HonestMajorityPerSlot ∧ HonestLeaderEveryWindow is ≤ |H|·exp(−(ε·thr·n₀)²/(2·|V|/4)) + |H|·(1−p₀)^κ.

Verification

• lake build passes with zero warnings (2905 jobs).
• #print axioms on all four theorems: [propext, Classical.choice, Quot.sound] only — no Goldfish axioms, no sorry, no new axioms.

Documented residual gap (capstone docstring)

1. VRF pseudorandomness ⇒ iid Bernoulli (cryptographic idealization).
2. Identifying abstract Execution fields (honEligible/advEligible/leader) with the sampled ω (Barrier-1 idealization).
3. HonestMajorityPerSlot's unbounded ∀ t : Slot — under any iid model an infinite horizon fails a.s., so the axiom must be read over the poly(κ) horizon (the theorem covers every finite horizon).
4. Static awake split (constant |A|/|Aᶜ| in Compliant).
5. Cross-lottery independence of eligibility and leadership (same VRF, distinct inputs — part of the pseudorandomness idealization).