We adopt a strong locality axiom at the Holds level: factorization—global satisfaction of observational propositions is the conjunction over fragments of a local predicate applied to the restricted world. This is algebraic, not geometric; no spacetime structure is assumed. Under factorization, same local views (same restriction at every fragment) imply observational equivalence; hence world-type is determined by the global map from fragments to local views. Interpretation: local dynamics alone do not guarantee local semantic closure; semantics is glued globally. A minimal toy (two fragments, observables as per-fragment claims) witnesses factorization and the main theorem. The development is mechanized in Lean 4 as the SemanticNonlocality library in nems-lean, with zero sorry and no custom axioms. Trust boundary. Factorization is an algebraic -level axiom, not a spacetime locality claim; interpretive "nonlocality" language is about semantic gluing, not signalling. Mechanization is nems-lean. See.
Nova Spivack (Sun,) studied this question.