Registry · Proposition IV.P19 tau-effective formalized

IV.P19 — Central Theorem Implies Boundary Determination

Book II Central Theorem O(τ³) = A_spec(L) induces H_τ ≅ L²(L̂, dν_spec). The Hilbert space is determined by boundary spectral data.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (2)

IV.D62 IV.T18

Depended on by (1)

IV.T19

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.CentralTheoremImpliesBoundaryDetermination