gap_correction

formal source

  32
  33/-- The recognition gap correction term: gap(Z) = log_φ(1 + Z/φ).
  34    This term corrects the rung position based on the charge-induced skew. -/
  35noncomputable def gap_correction (Z_val : ℤ) : ℝ :=
  36  Real.log (1 + (Z_val : ℝ) / phi) / Real.log phi
  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