Core Lean 4 proof that the Bohmian guidance identity clears to Im(dψ conj ψ) = dS |ψ|². Not a Schrödinger solver. Not a winding proof.
TeX Updated 1 day ago 1 commits
sigma-ai|Mirror: BenFrohman/bohm-identities (⭐0)
1 day agoAbout
Core Lean 4 proof that the Bohmian guidance identity clears to Im(dψ conj ψ) = dS |ψ|². Not a Schrödinger solver. Not a winding proof.
Readme