PulseExploreJournal ClubDebatesTrendingResearchersJournals
Instagram
HomeExploreJournal ClubTrending
Synapse
⌘+K
Synapse
April 7, 20260 citationsOpen Access

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

View Full Paper
NSNova Spivack

Key Points

  • The paper aims to present a sieve engine that structures theory spaces through constraints and residuals, enabling proof-carrying enumeration.
  • Defined a candidate space with equivalence and optional canonicalization.
  • Established constraints as predicates on candidates.
  • Developed a sieve as the conjunction of constraints and identified a residual as candidates meeting the sieve criteria.
  • Implemented the sieve engine in Lean 4, creating the Sieve library within nems-lean.
  • Proven that adding constraints reduces the residual (indicates monotonicity).
  • Demonstrated support for proof-carrying enumeration that integrates external generators for outputs.
  • Illustrated the functionality with small rewriting systems as a toy domain.

Abstract

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 .

Ask AI
Helpful
Bookmark
Share
View Full Paper

Cite This Study

Nova Spivack (2026) studied this question.

synapsesocial.com/papers/69d49f6bb33cc4c35a227e31https://doi.org/10.5281/zenodo.19429783
Ask AI
Helpful
Bookmark
Share
View Full Paper