type: definition
verification: machine_ready
dependencies: ["D1-1-formal.md", "D1-2-formal.md"]
verification_points:
- entropy_non_negativity
- entropy_monotonicity
- entropy_additivity
- information_equivalence
SystemEntropy(S : SelfReferentialComplete) : Prop ≡
∃H : Function[SystemState → Real⁺] .
NonNegative(H) ∧
StrictlyMonotonic(H) ∧
Additive(H) ∧
InformationMeasure(H)
H(S_t) : Real⁺ ≡
log |{d ∈ L | ∃s ∈ S_t . d = Desc_t(s)}|
where
S_t : SystemState at time t
L : FormalLanguage (set of finite symbol strings)
Desc_t : S_t → L (description function at time t)
log : natural logarithm
H_desc(S_t) : Real⁺ ≡
log |D_t|
where
D_t := {Desc_t(s) | s ∈ S_t}
H_info(S_t) : Real⁺ ≡
max_P Σ(s ∈ S_t) P(s) · log(1/P(s))
where
P : Probability distribution over S_t
H_encode(S_t) : Real⁺ ≡
lower_bound {avg_length(Encode) | Encode is valid encoding}
NonNegative(H) : Prop ≡
∀S_t . H(S_t) ≥ 0 ∧
(H(S_t) = 0 ⟺ |S_t| = 1)
StrictlyMonotonic(H) : Prop ≡
∀t ∈ ℕ . H(S_{t+1}) > H(S_t)
Additive(H) : Prop ≡
∀S₁, S₂ . S₁ ∩ S₂ = ∅ →
H(S₁ ∪ S₂) = H(S₁) + H(S₂)
InformationMeasure(H) : Prop ≡
∀S . H(S) = log |EquivalenceClasses(S, InfoEquiv)|
InfoEquiv(s₁, s₂ : Element) : Prop ≡
Desc(s₁) = Desc(s₂)
EquivalenceClasses(S, ~) : Set[Set[Element]] ≡
{[s] | s ∈ S}
where
[s] := {s' ∈ S | s ~ s'}
ΔH_desc(S_t) : Real⁺ ≡
H(S_t ∪ {Desc^(t+1)(S_t)}) - H(S_t)
ΔH_recursive(S, k) : Real⁺ ≡
log(|Desc^(k+1)(S)| / |Desc^(k)(S)|)
ΔH_measurement(S, result) : Real⁺ ≡
H(S ∪ {result}) - H(S)
LowerBound(H, S_t) : Prop ≡
H(S_t) ≥ log(t)
GrowthRateBound(H) : Prop ≡
∀t . dH/dt ≤ log(φ)
where φ = (1 + √5)/2
Type Real⁺ := {r ∈ ℝ | r ≥ 0}
Type FormalLanguage := Set[String]
Type Description := Element → String
Type ProbabilityDist := Element → [0,1]
def verify_entropy_non_negativity(system):
return entropy(system) >= 0 and (entropy(system) == 0 iff len(system) == 1)
def verify_entropy_monotonicity(system_sequence):
return all(entropy(s[i+1]) > entropy(s[i]) for i in range(len(s)-1))
def verify_entropy_additivity(subsystem1, subsystem2):
if disjoint(subsystem1, subsystem2):
return entropy(union(subsystem1, subsystem2)) == entropy(subsystem1) + entropy(subsystem2)
def verify_information_equivalence(system):
equiv_classes = compute_equivalence_classes(system)
return entropy(system) == log(len(equiv_classes))