Registry · Definition III.D28 established formalized

III.D28 — Lemniscate Operator H_L

The Laplacian H_L = −d²/dx² on L = S¹ ∨ S¹ with Kirchhoff boundary conditions at the crossing point. Standard self-adjoint operator on a metric graph. Compact resolvent, discrete spectrum.

Book III Part 4 Ch. 23

Dependency Graph

Depends on (2)

Depended on by (7)

Lean Formalization

Module: TauLib.BookIII.Doors.LemniscateOperator

Symbol: lemniscate_eigenvalue