phi

formal source

  22namespace IndisputableMonolith.Information.RecognitionEntropy
  23
  24/-- The golden ratio (local definition for self-containment). -/
  25noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  26
  27/-- phi > 1 (needed for log base phi). -/
  28theorem phi_gt_one : phi > 1 := by
  29  unfold phi
  30  have h5 : Real.sqrt 5 > 1 := by
  31    rw [show (1 : ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
  32    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  33  linarith
  34
  35/-- A phi-bit: the amount of information in a binary choice
  36    with phi-weighted branches. -/
  37noncomputable def phiBit : ℝ := 1 / Real.log phi
  38
  39/-- Recognition entropy: H_R(p) = -sum p_i * log_phi(p_i).
  40    This is Shannon entropy but in base phi instead of base 2. -/
  41noncomputable def recognitionEntropy (probs : List ℝ) : ℝ :=
  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. -/
  47noncomputable def cp6CapacityPhiBits : ℝ := phi ^ 12
  48
  49/-- phi^12 > 2^12 = 4096... actually phi^12 ≈ 322, which is less than 4096.
  50    The correct comparison: log_phi of the capacity exceeds log_2 because
  51    phi < 2, so each phi-bit carries MORE discrimination. -/
  52theorem phi_lt_two : phi < 2 := by
  53  unfold phi
  54  have h5 : Real.sqrt 5 < 3 := by
  55    rw [show (3 : ℝ) = Real.sqrt 9 from by rw [show (9:ℝ) = 3^2 from by norm_num, Real.sqrt_sq (by norm_num : (3:ℝ) ≥ 0)]]