Shannon.Entropy.Final

Final theorem layer.

Combines the rational characterization and continuity extension to prove:

• natural-log uniqueness (entropyNat_unique);
• base-parametric uniqueness (entropyBase_unique).

Final Characterization Theorems

Theorem Index

• entropyNat_unique
• entropyBase_unique

theorem LeanPool.Shannon1948Formalization.entropyNat_unique (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {α : Type} [Fintype α] (p : ProbDist α) : H p = (-K fun {α : Type} [Fintype α] => H) * ∑ a : α, ↑p a * Real.log (↑p a)

Uniqueness in natural-log units: every H satisfying the condition bundle agrees with Shannon entropy up to the positive multiplicative scale factor K H.

theorem LeanPool.Shannon1948Formalization.entropyBase_unique (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (b : ℝ) (hb : 1 < b) : ∃ (Kb : ℝ), 0 < Kb ∧ ∀ {α : Type} [inst : Fintype α] (p : ProbDist α), H p = -Kb * ∑ a : α, ↑p a * Real.logb b (↑p a)

Base-parametric uniqueness: for each base b > 1, there is a positive scale factor Kb with H p = -Kb * ∑ p_i log_b p_i.