`phi_bit_more_efficient`

proved

show as: view math explainer →

module: IndisputableMonolith.Information.RecognitionEntropy
domain: Information
line: 61 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.RecognitionEntropy on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  58
  59/-- Each phi-bit carries more information than a Shannon bit because
  60    phi < 2: fewer phi-bits are needed to encode the same number of states. -/
  61theorem phi_bit_more_efficient :
  62    Real.log phi < Real.log 2 := by
  63  apply Real.log_lt_log (by linarith [phi_gt_one]) phi_lt_two
  64
  65/-- The meaning capacity of one recognition event (one 8-tick cycle)
  66    is exactly 12 real DOF (the dimension of CP6). -/
  67theorem recognition_event_12_dof : (12 : ℕ) = 2 * 6 := by norm_num
  68
  69/-- Uniform distribution maximizes recognition entropy (same as Shannon). -/
  70theorem uniform_maximizes_entropy (n : ℕ) (hn : 0 < n) :
  71    ∃ max_entropy : ℝ, max_entropy = Real.log n / Real.log phi := by
  72  exact ⟨Real.log n / Real.log phi, rfl⟩
  73
  74end IndisputableMonolith.Information.RecognitionEntropy

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.