feat: expand Kleros sortition tree to 8-leaf 3-level model

[fricoben]

Summary

Expands the Kleros SortitionTrees benchmark from a 4-leaf 2-level binary tree to an 8-leaf 3-level binary tree, exercising multi-level parent propagation and deeper draw traversal. Adds a removeLeaf function, conditional overflow safety proofs (under no-wrap assumptions), removal correctness proofs, and a sequential setLeaf composition theorem proving the conservation invariant is inductive. All 12 theorems are proven and sorry-free; lake build passes cleanly.

Changes

• Contract.lean: 8-leaf tree (18 storage slots), 3-level setLeaf propagation, removeLeaf function, 3-level draw traversal
• Specs.lean: 12 specifications (up from 6) — split parent-sum into level-1/level-2, added overflow safety, removal, and composition specs
• Proofs.lean: 12 proven theorems including per-leaf helper lemmas for removal, conditional overflow proofs, and sequential conservation
• Task YAMLs + Generated stubs: 8 task files updated/created for the benchmark, all signatures match reference proofs
• Metadata: case.yaml, README, spec-review updated for eight_leaf_specialization + three_level_binary_tree

Test plan

• lake build Benchmark.Cases.Kleros.SortitionTrees.Compile passes
• rg "\bsorry\b" Benchmark/Cases/Kleros/ returns no matches
• Verify generated task stubs match theorem signatures in Proofs.lean

🤖 Generated with Claude Code