SCPI
Predicate Invention Under Sheaf Constraints
How does predicate invention decompose into topological, model-theoretic, and definability gates?
Extension Torsor Lemma: when global agreement is feasible, solutions form a principal homogeneous space over convention transformations
The torsor, counterexample, and conservativity core is machine-checked; Beth.lean is proposition-level scaffolding and the site-level Beth assembly remains unmechanized.
Abstract
Reduces predicate invention to a descent problem with three independent gates: topological, model-theoretic, and definability. The separation enables targeted diagnostics for composition failures.
Beth.lean compiles but abstracts implicit and explicit definability to bare propositions; it is not evidence for semantic Beth definability, constructivity, or interpolation extraction.
The geometric and general Beth-for-sites arguments are prose-derived, nonconstructive, unmechanized, and under review.
A counterexample to the retained formal core under its exact abstractions, or any public surface using Beth.lean as semantic theorem or extractor evidence.
not requested
- is formalized by Interpolant Envelope