A Sieve Engine for Theory Spaces: Proof-Carrying Classification and Residual Certification Paper 34 of the NEMS Suite

Papers 26–33 completed the abstract-core spine of the NEMS Suite: self-reference (26), closure audits (27), reflection as a resource (28), selector-strength barriers (29), self-trust incompleteness (30), epistemic agency and social verification (31), self-improvement under diagonal constraints (32), and self-awareness as a resource (33). The present paper adds a meta-methodology kernel: a generic sieve engine for theory spaces. We define a candidate space with equivalence and optional canonicalization, constraints as predicates on candidates, a sieve as the conjunction of constraints, and a residual as the subtype of candidates satisfying the sieve. We prove that adding constraints shrinks the residual (monotonicity) and that the framework supports proof-carrying enumeration: an external generator can output candidates plus certificates that Lean verifies. The development is mechanized in Lean 4 as the Sieve library in nems-lean, with zero sorry and no custom axioms. A toy domain (small rewriting systems) illustrates the engine. Trust boundary. The sieve engine is reusable methodology: constraints and residuals are user-supplied predicates; toy domains illustrate the API, not physical uniqueness claims. Mechanization is nems-lean . See .