recognitionEntropy
plain-language theorem explainer
Recognition entropy supplies the base-phi information measure H_R(p) = -sum p_i log_phi(p_i) for a probability list. Information theorists comparing recognition channels to Shannon theory would cite it when quantifying CP6 capacity. The definition is a direct one-line expression that maps the list, applies the scaled logarithm only to positive entries, and sums the result.
Claim. For a list of real numbers interpreted as probabilities, the recognition entropy is $H_R(p) = -sum_{p_i>0} p_i log_φ(p_i)$, where $log_φ$ denotes the logarithm with base φ.
background
The module treats information in phi-bits as more fundamental than base-2 bits, with the CP6 recognition channel capacity scaling as φ^12. Recognition entropy is defined using the golden-ratio constant φ imported via Constants and the Real.log operation from Mathlib. Upstream definitions such as the measurement map in RSNative.Core and the phi-related structures in JcostCore supply the numerical base and list-handling primitives.
proof idea
The declaration is a direct definition. It applies list.map to replace each positive entry p with p times (Real.log p divided by Real.log phi), replaces non-positive entries with zero, then negates the sum of the resulting list.
why it matters
This definition anchors the phi-based information theory section of the Recognition framework and supports the claim that recognition capacity exceeds Shannon capacity for the same manifold. It aligns with the T6 fixed-point status of phi and the eight-tick octave structure. No downstream theorems yet reference it, leaving open its insertion into explicit capacity bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.