pith. sign in
module module high

IndisputableMonolith.Information.RecognitionEntropy

show as:
view Lean formalization →

This module supplies self-contained definitions for the golden ratio phi and phi-bit entropy measures in the Information domain of Recognition Science. It supports calculations involving recognitionEntropy, phiBit, and capacity bounds without external dependencies. Researchers analyzing information content in RS events or phi-ladder structures would cite these definitions. The module is purely definitional with supporting inequalities and no proofs.

claim$\phi = \frac{1 + \sqrt{5}}{2}$, recognitionEntropy, phiBit, cp6CapacityPhiBits, recognition_event_12_dof, uniform_maximizes_entropy

background

The module resides in the Information domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants together with J-cost definitions from JcostCore. It supplies a local definition of the golden ratio for self-containment, along with basic properties (phi > 1, phi < 2) and derived objects such as phiBit (information unit) and recognitionEntropy (entropy measure in phi bits). The sibling definitions include cp6CapacityPhiBits and uniform_maximizes_entropy, which operate in the same phi-native information setting.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module grounds the information-theoretic layer of Recognition Science by providing phi-based entropy and capacity primitives. It feeds downstream results on recognition events and entropy maximization within the phi-ladder framework (T5 J-uniqueness and T6 self-similar fixed point). The local phi definition ensures the module remains independent while supporting RCL-compatible calculations.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)