theorem proved term proof

`deterministic_has_zero_entropy`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 158theorem deterministic_has_zero_entropy {n : ℕ} (d : ShannonEntropy.ProbDist n) (i : Fin n)
 159    (hdet : d.probs i = 1) (hother : ∀ j ≠ i, d.probs j = 0) :
 160    ShannonEntropy.shannonEntropy d = 0 :=

proof body

Term-mode proof.

 161  ShannonEntropy.zero_entropy_deterministic d i hdet hother
 162
 163/-- **THEOREM IC-001.12**: Maximum entropy occurs for the uniform distribution.
 164    Uniform = maximum uncertainty = maximum information cost. -/

depends on (11)

Lean names referenced from this declaration's body.

entropy in IndisputableMonolith.Foundation.InitialCondition decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
ProbDist in IndisputableMonolith.Information.ShannonEntropy decl_use
shannonEntropy in IndisputableMonolith.Information.ShannonEntropy decl_use
uniform in IndisputableMonolith.Information.ShannonEntropy decl_use
zero_entropy_deterministic in IndisputableMonolith.Information.ShannonEntropy decl_use
ProbDist in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use
entropy in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
entropy in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use