release_tools/HELD_OUT_READOUT.md

# Held-out generalization readout — order-5 (leaner FALSE × sair-lancelot TRUE)

The SAIR score is on a **held-back set including order-5 laws** that never appear
in the public 1669 — the memorization-proof axis. This is the measured
generalization of the **current flagship (v2/v3 deterministic)** on
out-of-distribution order-5 laws, both sides. Bottom line: **FALSE generalizes
fully today; TRUE is the bottleneck and needs the v4 completion engine.**

## FALSE side — leaner (order5_deep.json)

600 random order-5 law pairs (`eq_size5.txt`, ≥3 ops), minimal-CE size via the
in-solver stack (exhaustive Fin2-3 + structured + backtracking/targeted Fin4-6),
plus a SAT Fin7-8 spot-check of the residual:

- **402 are FALSE, every one with a counterexample at Fin ≤5** (Fin2 348 / Fin3 40 / Fin4 8 / Fin5 6 / Fin6 0).
- SAT spot-check of 40 no-CE-≤6 pairs → **0 at Fin7, 0 at Fin8** (all 40 are TRUE/huge).
- ⇒ the flagship FALSE engine (order-**agnostic**, Fin≤6) reaches **~100% of held-out FALSE; 0% need Fin≥7**.

The FALSE engine is order-agnostic by construction (a counterexample is a finite
magma; the law's term-order doesn't change the search), so this transfer is
expected — and now measured.

## TRUE side — sair-lancelot (order5_generalization_sair-lancelot/)

60-problem diverse order-5 TRUE bench (twee-labeled, all judge-verified TRUE):

- **flagship-v2 (deterministic, llm:0): 19/60 (32%)**; twee: **60/60 (100%)**.
- Breakdown: 0-lemma proofs **19/45 (42%)** — 26 shallow pure-axiom misses = the
  extra-var forward (MITM) gap; needs-a-lemma **0/15 (0%)** — requires
  critical-pair / completion.
- The 41-miss gap maps exactly to the-prover's two v4 fixes: **26 extra-var MITM
  + 15 critical-pair lemmas** → order-5 TRUE goes **32% → ~100%** on twee-provable trues.

## Combined readout & decision

| axis (order-5, held-out) | current flagship | with v4 completion |
|---|---|---|
| FALSE (leaner) | **~100%** (CE ≤ Fin5) | ~100% |
| TRUE  (sair-lancelot) | **32%** (19/60) | ~100% (twee-provable) |

- **v3 is safe to ship now** (the-bridge): its FALSE side is a proven-generalizing,
  freeze-verifiable solver (sha 8438fdb3, byte-reproduced). It captures held-out
  FALSE fully + the 0-lemma TRUE it can reach.
- **v4's in-solver completion engine is the score-critical unlock, not
  nice-to-have** — the entire held-out TRUE gap is quantified as two concrete
  fixes (the-prover's lane), with the 521 twee proofs as the regression suite.

**Caveats:** samples are random/diverse, not the exact held-out distribution;
the TRUE bench is twee-provable trues only (trues beyond twee's reach are not
counted); n is modest. These are clean per-side transfer signals, not a score
estimate. Sources: `shared_resources/release_tools_leaner/order5_deep.json`,
`shared_resources/order5_generalization_sair-lancelot/`.