GATE D32

Implicit realizability and the symbolic CEGAR kernel: PARTIAL

partialEvidence I2Verify: doublePublic claim: No2026-07-20

What changed

D32 tests the remaining unrefuted route, representing the global realizability problem implicitly and refining it with exact predicates rather than enumerating any product of local states. The scan defines an abstraction-refinement loop whose predicates, local admissibility, the top-coefficient square lift, positivity and Newton inequalities, and square splitting, are each proved to preserve every governed tuple, and on complete finite domains the loop agrees with brute-force enumeration, including a case where square splitting is the load-bearing refinement. Phase 1 implements a genuinely symbolic kernel with two independent exact backends, a canonical reduced decision diagram and an independent finite-domain engine. The local admissibility layer compresses genuinely: the diagram uses a number of nodes linear in the prime count while representing the full product, with zero Cartesian materialization. The coupling constraint does not compress in the implemented backends, because its construction materializes a bounded-square or product enumeration, so the cost moves to preprocessing. The local-separability result is a proved theorem; the coupled layer is a representation-specific obstruction, not a universal one. LRC(13) remains open.

Evidence

check 1Abstraction-refinement loop proved sound and exact on complete finite domains; each refinement preserves every governed tuple; the 34-state realizability pilot is established by a proved bijection, not by equal counts; a two-round empty case is certified on its domain

check 2Symbolic kernel: local admissibility compresses to a node count linear in the prime count while representing the full product with zero Cartesian materialization; the coupling constraint construction materializes a bounded enumeration, moving the cost to preprocessing

check 3D32-PARTIAL: a proved PASS-THEORY local-separability compression, with a representation-specific coupled-layer obstruction. V1 10/10, an independent second backend, corruption 560/560. No PASS-implicit-seeding, no campaign. No BASE-SURVIVOR, no GLOBAL-WITNESS. LRC(13) OPEN

Verification: double · I2 · 6 artifacts (reports, verifiers, corruption suites, manifest with SHA-256)

← All gates