C-D22-IMPLICIT-STATE

D22 implicit CEGAR architecture PROVED-SOUND: keeping the bounded global object symbolic (coefficient master E_j and root master X_i), projecting to each prime, asking the narrowed local subproblem (MATCH-WITNESS / EMPTY-CERTIFIED / OPEN-INCOMPLETE) and generating proof-carrying cuts is sound by the one-way theorem: a bounded counterexample survives every certified cut (its base cover matches at every prime, so an empty-certified cut can never contain it; applicability and square-splitting cuts also exclude it). No certified cut ever removes a counterexample

In plain language

The symbolic-and-cut architecture is proved safe: no proof-carrying cut can ever throw away a real counterexample.

Exact statement

D22 implicit CEGAR architecture PROVED-SOUND: keeping the bounded global object symbolic (coefficient master E_j and root master X_i), projecting to each prime, asking the narrowed local subproblem (MATCH-WITNESS / EMPTY-CERTIFIED / OPEN-INCOMPLETE) and generating proof-carrying cuts is sound by the one-way theorem: a bounded counterexample survives every certified cut (its base cover matches at every prime, so an empty-certified cut can never contain it; applicability and square-splitting cuts also exclude it). No certified cut ever removes a counterexample