def
definition
def or abbrev
recognitionEntropy
show as:
view Lean formalization →
formal statement (Lean)
41noncomputable def recognitionEntropy (probs : List ℝ) : ℝ :=
proof body
Definition body.
42 -(probs.map fun p => if p > 0 then p * (Real.log p / Real.log phi) else 0).sum
43
44/-- The CP6 meaning manifold has 12 real dimensions.
45 In phi-bits, the capacity at resolution epsilon is
46 phi^12 * log_phi(1/epsilon) ≈ phi^12 ≈ 321.997. -/