SCPI
Predicate Invention Under Sheaf Constraints
Lean checks finite Z/2 examples and finite-indexed set-valued gluing. General conservativity and Beth statements remain unsupported by their scaffolding.
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.
Evidence and record
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
conservativity_descent returns a conclusion already provided for arbitrary model classes by h_local; this does not establish general model-theoretic descent.
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