StellarConfig

formal source

  78/-! ## Stellar Configuration -/
  79
  80/-- A stellar configuration specifies the scale ratios for emission and storage -/
  81structure StellarConfig where
  82  /-- Scale ratio for photon emission events -/
  83  r_emit : ℝ
  84  /-- Scale ratio for mass storage events -/
  85  r_store : ℝ
  86  /-- Both ratios must be positive -/
  87  emit_pos : 0 < r_emit
  88  store_pos : 0 < r_store
  89
  90namespace StellarConfig
  91
  92/-- Recognition cost for emission -/
  93noncomputable def δ_emit (cfg : StellarConfig) : ℝ := J cfg.r_emit
  94
  95/-- Recognition cost for storage -/
  96noncomputable def δ_store (cfg : StellarConfig) : ℝ := J cfg.r_store
  97
  98/-- Cost differential: Δδ = δ_emit - δ_store -/
  99noncomputable def Δδ (cfg : StellarConfig) : ℝ := cfg.δ_emit - cfg.δ_store
 100
 101end StellarConfig
 102
 103/-! ## Equilibrium M/L from Cost Minimization -/
 104
 105/-- The equilibrium mass-to-light ratio from J-minimization.
 106
 107When the cost differential is n · J_bit = n · log(φ), the equilibrium partition gives:
 108  M/L = exp(n · log(φ)) = φ^n
 109
 110This is because the optimal allocation minimizes total J-cost, and the
 111exponential weighting exp(-J) on paths gives Boltzmann-like statistics. -/