predict_mass

formal source

  37
  38/-- **THE MASTER MASS LAW**
  39    Predicts the mass of a species in a given sector. -/
  40noncomputable def predict_mass (sector : Sector) (rung : ℤ) (Z_val : ℤ) : ℝ :=
  41  yardstick sector * (phi ^ ((rung : ℝ) - 8 + gap_correction Z_val))
  42
  43/-- Mass is positive for any valid configuration. -/
  44theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
  45    predict_mass s r Z_val > 0 := by
  46  unfold predict_mass
  47  apply mul_pos
  48  · -- yardstick is positive
  49    unfold yardstick Anchor.E_coh
  50    apply mul_pos
  51    · apply mul_pos
  52      · exact zpow_pos (by norm_num) (B_pow s)
  53      · exact zpow_pos phi_pos (-5 : ℤ)
  54    · exact zpow_pos phi_pos (r0 s)
  55  · -- phi^... is positive
  56    exact Real.rpow_pos_of_pos phi_pos _
  57
  58/-! ## Derived Properties -/
  59
  60/-- The mass law exhibits φ-scaling: increasing rung by 1 scales mass by φ. -/
  61theorem mass_rung_scaling (s : Sector) (r : ℤ) (Z_val : ℤ) :
  62    predict_mass s (r + 1) Z_val = phi * predict_mass s r Z_val := by
  63  unfold predict_mass
  64  -- φ^(r+1-8+gap) = φ^1 * φ^(r-8+gap)
  65  set gap := gap_correction Z_val
  66  have h_add : (((r + 1 : ℤ) : ℝ) - 8 + gap) = 1 + (((r : ℤ) : ℝ) - 8 + gap) := by
  67    push_cast
  68    ring
  69  rw [h_add, Real.rpow_add phi_pos]
  70  rw [Real.rpow_one]