ml_from_cost_diff

formal source

 109
 110This is because the optimal allocation minimizes total J-cost, and the
 111exponential weighting exp(-J) on paths gives Boltzmann-like statistics. -/
 112noncomputable def ml_from_cost_diff (Δδ : ℝ) : ℝ := Real.exp Δδ
 113
 114/-- When Δδ = n · J_bit = n · log(φ), we get M/L = φ^n -/
 115theorem ml_is_phi_power (n : ℤ) (Δδ : ℝ) (h : Δδ = n * J_bit) :
 116    ml_from_cost_diff Δδ = φ ^ n := by
 117  simp only [ml_from_cost_diff, J_bit] at *
 118  rw [h]
 119  -- exp(n * log(φ)) = φ^n by definition of zpow for positive reals
 120  have hφ : 0 < φ := Constants.phi_pos
 121  rw [← Real.rpow_intCast φ n]
 122  rw [Real.rpow_def_of_pos hφ]
 123  ring
 124
 125/-! ## Eight-Tick Determination of n -/
 126
 127/-- The eight-tick cycle partitions into mass and light phases.
 128
 129In one 8-tick cycle:
 130- Ticks 1-5: mass accumulation (matter recognition events)
 131- Ticks 6-8: light emission (photon recognition events)
 132
 133This 5:3 partition determines the base M/L scaling. -/
 134def mass_ticks : ℕ := 5
 135def light_ticks : ℕ := 3
 136def total_ticks : ℕ := 8
 137
 138theorem tick_partition : mass_ticks + light_ticks = total_ticks := rfl
 139
 140/-- The tick ratio determines the base scaling tier -/
 141noncomputable def tick_ratio : ℝ := mass_ticks / light_ticks
 142