Dinâmicas Locais, Semânticas Globais: Um Motor de Fechamento para o Papel de Não Localidade Semântica 45 da Suíte NEMS

Adotamos um forte axioma de localidade no nível Holds: fatoração—satisfação global de proposições observacionais é a conjunção sobre fragmentos de um predicado local aplicado ao mundo restrito. Isso é algébrico, não geométrico; nenhuma estrutura de espaço-tempo é assumida. Sob a fatoração, mesmas visões locais (mesma restrição em cada fragmento) implicam equivalência observacional; portanto, o tipo de mundo é determinado pelo mapa global de fragmentos para visões locais. Interpretação: dinâmicas locais sozinhas não garantem fechamento semântico local; a semântica é unida globalmente. Um modelo minimal (dois fragmentos, observáveis como reivindicações por fragmento) testemunha a fatoração e o teorema principal. O desenvolvimento é mecanizado em Lean 4 como a biblioteca SemanticNonlocality no nems-lean, com zero desculpas e sem axiomas personalizados. Limite de confiança. A fatoração é um axioma de nível algébrico, não uma afirmação de localidade no espaço-tempo; a linguagem interpretativa de "não localidade" diz respeito à colagem semântica, não a sinalização. A mecanização é nems-lean. Veja.