Function SolverSection 

pub fn SolverSection() -> Element

The “Our solver vs the field” section: per-family bar charts (ours vs Z3, Kissat, SaDiCaL) over the families where structure beats brute force, led by the pigeonhole wall. Bars are linear per row — the slowest fills the track, ours is its true fraction — so a microsecond refutation reads as the sliver it is. All numbers are measured by benchmarks/run-solver-vs-z3.sh; the framing is the honest one the data supports — SaDiCaL completes (we beat it), Z3 and Kissat hit the resolution wall.