Registry · Proposition IV.P22 tau-effective formalized

IV.P22 — Superposition from Linearity

If f, g ∈ H_τ then αf + βg ∈ H_τ. Superposition is a theorem about linearity of ∂̄_b, not a postulate.

Book IV Part 3 Ch. 18

Dependency Graph

Depends on (2)

IV.D62 IV.D60

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.HilbertSpace

Symbol: Tau.BookIV.QuantumMechanics.SuperpositionFromLinearity