Stage 4 checked EPR reconstruction

[dollspace-gay]

What changed

• defines the production canonical S2Recon bridge from source clauses, with typed sorts, literals, binder scopes, signatures, source addresses, and deterministic serialization
• replaces model-relative relation/array atoms with typed Lean semantics for equality, ordering, relations, unary functions, sequence reads, and lengths
• adds kernel-checked normalization, substitution, Skolemization, finite grounding, structural instantiation, and ground-theory reconstruction
• recomputes Tseitin CNF in Lean, parses and checks LRAT, and proves the actual req → clause theorem
• returns Lean-checked finite countermodels for false admitted clauses
• records full content-addressed reconstruction evidence and validates every verdict-determining hash on cache replay
• enables EPR reconstruction in normal automatic routing, including BV-aware routes, while preserving vacuity, mutation, slag, body-safety, and lowered-assurance gates
• pins CaDiCaL and drat-trim to exact upstream revisions; missing or wrong-version tools fail rather than skip
• adds the full G4 gate, tamper/refusal/negative-pin coverage, and current documentation/correspondence pins

Why

Stage 3 left admitted S2.0 relation and array atoms at a model-relative solver boundary. Stage 4 closes that residual: admitted clauses now migrate to L4 only after Lean reconstructs the finite problem and kernel-checks the exact implication, while false clauses produce checked concrete models.

CI runner fix

The first complete matrix exposed that the ordinary test and lean-spine-forge runners had Lean but did not install the new pinned CaDiCaL/drat-trim pair. Automatic EPR tests therefore returned EprSolverUnavailable, which appeared as expected-L4 results falling to L0. Both matrices now restore/build the pinned tools and export their absolute paths before tests run. Missing tooling remains a hard failure.

Validation

• cargo test --workspace --no-fail-fast -- --test-threads=1 — full workspace and doctests green
• lake build — 1,153 jobs green, warning-free, with no sorry/admit
• strict workspace Clippy green
• make audit — 17/17 admitted corpus programs, 3,460 live-Z3 obligations, zero divergences; all 40 falsification cases green; correspondence drift, third-party Verus replay, and G2 green
• documentation drift tripwire green
• requirement registry green: 472 requirements / 119 views
• Gate G4 green, including exact replay, countermodels, tamper failures, dependency/version failures, placeholder scan, and allowed-axiom probe
• GitHub Actions run 30523760927 — all 12 jobs green, including all four ordinary test shards and all four Lean-spine shards

All heavy local validation ran serially under a 6 GiB address-space limit.