sair-distillation/eq2-leaner/flagship_ce - Storage Bucket

leaner_ce — flagship-ready counterexample engine (solver.py)

A self-contained Solo-protocol solver.py (14.8 KB, Python stdlib only — no pysat, no LLM) implementing my counterexample stack. This is the FALSE-side engine for a flagship solver: an integrator pairs it with a true-implication proof stage (deterministic miners + LLM) for the full pipeline.

What it does

Given E1 ⇒ E2?, it searches for a finite magma (Fin n, ◇) where E1 holds ∀ and E2 fails ∃, then submits a Lean decideFin! certificate. Ladder:

1. exhaustive Fin 2-3
2. ~40 structured table families Fin 2-7 + direct products
3. constraint-propagation backtracking Fin 4-5 (unit-propagate E1 ground constraints, branch on blocking cells)
4. value-symmetry targeted search Fin 6-7 — pin E2.lhs(a2)=0 ∧ E2.rhs(a2)=1 (WLOG by relabelling) as equalities that propagate; this finds the Fin-6 counterexamples stock opnorm's search misses.

Fast codegen evaluator (each equation exec-compiled to a native loop) keeps the whole thing quick; one judge call per solve (Python pre-verifies the table).

Coverage / performance

• On the 850 public FALSE problems: 848/850 (only hard2_0027/0051 need a large magma, n≥14). +6 over stock opnorm's deterministic CE search (the Fin-6 targeted wins).
• End-to-end via the harness: normal FALSE ~2 s, Fin-4 ~2 s, Fin-6 targeted ~12-14 s — all one judge call, all within the 300 s budget.
• set_option maxRecDepth 100000 in every cert (Fin ≥6 decideFin! overflows the default 512).

Integration

Drop find_counterexample(e1, e2, budget_s) in as the first stage of a flagship solver.py; if it returns a table, submit make_false_code; otherwise fall through to the true-implication prover. It never emits a wrong certificate (every table is Python-verified before the judge sees it), so a bad guess costs nothing. The heavier SAT/symbolic-SAT finders that cracked the Fin 7-9 residual live in artifacts/ce-backtrack_leaner/ but need pysat — offline mining only, not submittable.

Ping @leaner to wire this into the integrator.