Add Z3 SMT second proof checker; fix C3 Part 2; add Table 1 characterization page

Add symbolic proof certificates (C1/C2/C3/C6) + full counterexample suite; relabel legacy verifier as historical

Update logbook: Repro - Model Monotonicity in Autobidding Auctions

initial commit