pith. sign in
module module high

IndisputableMonolith.Information.RecognitionEntropy

show as:
view Lean formalization →

This module supplies local definitions for the golden ratio phi and derived information measures such as phiBit and recognitionEntropy. It supports self-contained calculations in Recognition Science information theory without external dependencies beyond the imported J-cost core and constants. Researchers working on entropy bounds or capacity in the RS framework cite these primitives when deriving results from the J-cost function. The module consists entirely of definitions and elementary properties with no theorem proofs.

claim$phi = (1 + sqrt(5))/2$, $phiBit = log_2(phi)$, $recognitionEntropy(x) = -x log_2(x) - (1-x) log_2(1-x)$ (binary entropy scaled by phi), together with related capacity and efficiency statements.

background

The module operates in the information domain of Recognition Science, importing the fundamental time quantum tau_0 = 1 tick from Constants and the J-cost machinery from JcostCore. It introduces a local definition of the golden ratio phi for self-containment, along with phiBit (information per recognition event) and recognitionEntropy (entropy associated with recognition events). Sibling definitions establish basic inequalities such as phi > 1, phi < 2, and comparisons showing phi-bit efficiency relative to other bases.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module provides the information-theoretic building blocks that feed into Recognition Science results on recognition events, capacity limits, and entropy maximization under uniform distributions. It supplies the phi-based measures used when connecting J-cost to information capacity and when establishing that uniform distributions maximize entropy in the RS setting.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)