Pinned Loading

1. nava-robertson-schrodinger nava-robertson-schrodinger Public

   NRS, NRS³ & det|NRS³: exact Robertson–Schrödinger inequality for the transport–position pair (T_d, P_d), the finite counterpart of H(X,P), its lift to x, y, z, and Robertson 1934 for the six observ…

   Lean 12 2

2. nrs3-mandelstam-tamm-cramer-rao nrs3-mandelstam-tamm-cramer-rao Public

   NRS³ · Mandelstam–Tamm and Cramér–Rao: no state is orthogonal to itself before πħ/(2ΔE), sharp; F_X ≤ 4 Var H, on NRS³ the efficiency is 1/C_Nava(d)² — Lean 4 + Mathlib

   Lean

3. nrs3-uncertainty-cone nrs3-uncertainty-cone Public

   NRS³ · The uncertainty cone — the Gram matrix of a conjugate pair is a Minkowski four-vector; Robertson–Schrödinger is the light cone, the NRS³ quantum keeps it strictly inside. Lean 4.

   Lean

4. nrs3-pauli-dirac nrs3-pauli-dirac Public

   NRS³ · Pauli–Dirac: exclusion, shells 2n², three spin matrices and no fourth in 2×2; no 2×2 gamma matrices, the least dimension is 4 — Lean 4 + Mathlib

   Lean

5. leanprover-community/physlib leanprover-community/physlib Public

   A project to digitalise results from physics into Lean.

   Lean 793 209

6. nrs3-de-sitter nrs3-de-sitter Public

   NRS³ · de Sitter: the horizon entropy fixes the cosmological constant, Λ = 3π/(ℓ_P² S); it solves both Friedmann equations with H² = πc²/(ℓ_P² S) — Lean 4 + Physlib

   Lean