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).
Certificado de janela de Bell
Cole as probabilidades P(a,b|x,y) do seu experimento (cenário 2×2×2). O certificador checa no-signaling, computa o valor CHSH em aritmética exata e classifica na janela verificada — local (≤2), quântica (≤2√2) ou pós-quântica (≤4) — emitindo um certificado Lean que prova o valor por `norm_num`.
Aceita decimais ("0.426775") ou frações ("3/8"). Cada contexto deve somar 1.
Certificado GHZ (3 partes)
Informe os 4 correladores ⟨XXX⟩, ⟨XYY⟩, ⟨YXY⟩, ⟨YYX⟩ do seu experimento de 3 partes. O certificador computa o valor de Mermin M = ⟨XXX⟩−⟨XYY⟩−⟨YXY⟩−⟨YYX⟩ e classifica: local (|M| ≤ 2), super-clássico (até 4), ou — no caso exato (+1,−1,−1,−1) — o paradoxo GHZ determinístico: modelo local impossível com probabilidade 1, não improvável.
Decimais ("0.9", "-1") ou frações ("-9/10"); valores em [−1, 1].
Certificado do quadrado mágico (Mermin–Peres)
Informe vitórias e rodadas do jogo do quadrado mágico. A taxa exata é comparada com os DOIS tetos com teorema: o valor clássico é exatamente 8/9 (e justo — atingido), e existe estratégia quântica que vence 9/9 (dois pares de Bell).
Um circuito quântico, verificado
O circuito que prepara o estado de Bell, passo a passo — cada passo ancorado num teorema Lean do corpus ZX. Igualdade exata de morfismos, não simulação numérica.
Corpus ZX auditado no export: 17 arquivos Lean · 104 teoremas/lemas · 0 com `sorry`.
Ponto de partida: dois qubits no estado |00⟩. Em FinHilb, o estado é um morfismo 𝟙 ⟶ Q⊗Q — preparar um estado já é uma seta na categoria.
Estado: |00⟩
sumno é um assistente de pesquisa acadêmica.
Busca em milhões de papers, resumo de abstracts em português e referências pela ABNT.