phi_inv

formal source

  67/-! ## §1. The 1/φ active fraction -/
  68
  69/-- The predicted active-vocabulary fraction. -/
  70def phi_inv : ℝ := 1 / Constants.phi
  71
  72theorem phi_inv_pos : 0 < phi_inv :=
  73  div_pos one_pos Constants.phi_pos
  74
  75theorem phi_inv_lt_one : phi_inv < 1 := by
  76  unfold phi_inv
  77  rw [div_lt_one Constants.phi_pos]
  78  exact Constants.one_lt_phi
  79
  80theorem phi_inv_band : (0.6 : ℝ) < phi_inv ∧ phi_inv < 0.7 := by
  81  unfold phi_inv
  82  have h1 := Constants.phi_gt_onePointFive
  83  have h2 := Constants.phi_lt_onePointSixTwo
  84  have h_pos := Constants.phi_pos
  85  refine ⟨?_, ?_⟩
  86  · rw [lt_div_iff₀ h_pos]; linarith
  87  · rw [div_lt_iff₀ h_pos]; linarith
  88
  89/-! ## §2. The φ²=φ+1 identity and σ-conservation -/
  90
  91/-- The defining identity of φ: `φ² = φ + 1`. From `Constants.phi_sq_eq`. -/
  92theorem phi_sq : Constants.phi ^ 2 = Constants.phi + 1 :=
  93  Constants.phi_sq_eq
  94
  95/-- **THEOREM.** `1/φ` satisfies the Fibonacci fixed-point identity
  96`x + x² = 1`. This is the σ-conservation condition on the lexicon
  97steady state. -/
  98theorem phi_inv_fibonacci_fixed_point :
  99    phi_inv + phi_inv ^ 2 = 1 := by
 100  unfold phi_inv