Ciência verificada
Fatos quânticos, com a prova do lado.
Resultados conhecidos de mecânica quântica, verificados passo a passo por um assistente de prova. Clique em qualquer fato para ver o teorema em Lean.
O que isto é — e o que não é
Estas ferramentas mostram verificações formais machine-checked (Lean 4 + mathlib, zero `sorry`) de resultados conhecidos de mecânica quântica. Não é física nova: é prova auditável de teoremas estabelecidos. Cada fato traz a fonte e uma nota de honestidade.
Fatos verificados
Cada cartão é um resultado conhecido com prova machine-checked. A prova é o teorema Lean exato — sem hand-waving.
Corpus auditado no export: 82 arquivos Lean · 313 teoremas/lemas · 0 com `sorry`.
Paradoxo GHZ: com 3 partículas, a previsão quântica contradiz qualquer modelo local de variáveis ocultas com certeza (determinístico, não estatístico).
nonlocalityall-vs-nothingdeterministicTeto de Tsirelson: correlações quânticas violam a desigualdade de CHSH, mas nunca acima do teto exato 2√2 ≈ 2,828.
nonlocalitychshboundContextualidade (Kochen–Specker via quadrado de Mermin): é impossível atribuir valores definidos a todas as medições de uma vez de forma consistente.
contextualityTeorema da não-clonagem: não existe operação que copie um estado quântico arbitrário desconhecido.
no-goPara um sistema único, números reais bastam: a MQ complexa é simulada por duplicação de dimensão (i ↦ J, com J² = −1), e ℂ se embute fielmente nas matrizes reais 2×2.
real-vs-complexsingle-systemA tomografia local seleciona o complexo: contando parâmetros de estado (real d(d+1)/2, complexo d², quaterniônico 2d²−d), só a MQ complexa é localmente tomográfica.
real-vs-complextomographyQuantas observáveis ±1 anticomutam aos pares: o complexo admite três (σx, σy, σz), o real no máximo duas. A 'dimensão imaginária' (σy) é o que falta no real — a raiz algébrica da separação em rede.
real-vs-complexanticommutation
Certificador de ordem causal
Descreva quem sinaliza para quem entre as partes. O certificador decide se a ordem causal é definida (acíclica, com função-tempo) ou indefinida (laço causal) e emite um certificado Lean que você pode verificar com `lake`.
Uma por linha ou separadas por vírgula, no formato i->j (ex.: 0->1, 1->2).
sumno é um assistente de pesquisa acadêmica.
Busca em milhões de papers, resumo de abstracts em português e referências pela ABNT.