Registry · Proposition IV.P30 tau-effective formalized

IV.P30 — Entropy-Mode-Count Bound

S[ψ] ≤ ln|A| where A ⊂ Λ_CR is the support of ψ. Equality when all modes contribute equally.

Book IV Part 3 Ch. 22

Dependency Graph

Depends on (1)

IV.D80

Lean Formalization

Module: TauLib.BookIV.QuantumMechanics.EnergyEntropy

Symbol: Tau.BookIV.QuantumMechanics.EntropymodecountBound