∴
Technical Spine

SCPI

Predicate Invention Under Sheaf Constraints

VerifiedCore results machine-checked in Lean 4 (Extension Torsor, circular-nerve vanishing, topological obstruction). Beth for Sites and SchemaDiscovery remain statement-only.
Key result

Extension Torsor Lemma: when global agreement is feasible, solutions form a principal homogeneous space over convention transformations

Falsification

A predicate invention problem that cannot be decomposed into the three gates, or a composition failure not captured by H¹

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.

Resources