phiSpacedInterval

formal source

  37open Constants Cost
  38
  39/-- φ-spaced pulse intervals. -/
  40noncomputable def phiSpacedInterval (τ₀ : ℝ) (k : ℕ) : ℝ := τ₀ * phi ^ k
  41
  42/-- Ratio of adjacent φ-spaced intervals = φ. -/
  43theorem phiSpaced_ratio (τ₀ : ℝ) (hτ₀ : 0 < τ₀) (k : ℕ) :
  44    phiSpacedInterval τ₀ (k + 1) / phiSpacedInterval τ₀ k = phi := by
  45  unfold phiSpacedInterval
  46  have hpos := mul_pos hτ₀ (pow_pos phi_pos k)
  47  rw [pow_succ, div_eq_iff hpos.ne']
  48  ring
  49
  50/-- J-cost of the φ-spacing ratio: J(φ) > 0. -/
  51theorem phiSpacing_jcost_pos : 0 < Jcost phi :=
  52  Jcost_pos_of_ne_one phi phi_pos phi_ne_one
  53
  54/-- φ minimises J among ratios > 1 of "comparable" scale (proved: J(φ) < J(2)). -/
  55theorem phi_beats_2 : Jcost phi < Jcost 2 := by
  56  rw [Jcost_eq_sq phi_ne_zero, Jcost_eq_sq (by norm_num : (2 : ℝ) ≠ 0)]
  57  rw [div_lt_div_iff₀ (by exact mul_pos (by norm_num) phi_pos) (by norm_num)]
  58  nlinarith [phi_gt_onePointSixOne, phi_lt_onePointSixTwo, phi_sq_eq]
  59
  60/-- Uniform spacing has zero step-cost (ratio = 1). -/
  61theorem uniform_step_cost : Jcost 1 = 0 := Jcost_unit0
  62
  63/-- The RS Experiment A prediction (MODEL level):
  64    φ-spaced pulses have lower global J-cost than sub-optimal alternatives. -/
  65def ExperimentAPrediction : Prop :=
  66  ∀ τ₀ : ℝ, 0 < τ₀ →
  67  ∀ k : ℕ, 0 < Jcost (phiSpacedInterval τ₀ (k + 1) / phiSpacedInterval τ₀ k)
  68
  69/-- Under RS, the φ-spacing ratio has positive J-cost per step (off-equilibrium drive). -/
  70theorem experiment_a_prediction_holds :