Pinned Loading

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

   NRS and NRS³: exact Robertson–Schrödinger inequality for the path-graph pair (T_d, P_d) and its lift to the product of three path graphs — Lean 4 (Mathlib + physlib), with a declared physical bridge

   Lean 12 2

2. nrs3-poincare nrs3-poincare Public

   NRS³ · Poincaré: Planck's law forces discrete energy levels (1912) — Lean 4 + Mathlib

   Lean

3. 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

4. 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

5. nrs3-penrose nrs3-penrose Public

   NRS³ · Penrose: the collapse time ħ/ΔE is a bound, not a lifetime — Lean 4 + Mathlib

   Lean

6. nrs3-defect-curvature nrs3-defect-curvature Public

   NRS³ · Defect and curvature: each non-local link of transport closes a cycle with one quantum δ∞; 2g links fix the curvature of Σ_g; the entropy of a cut counts its quanta and its horizon hides the…

   Lean