dim

formal source

  67def W : ℕ := wallpaper_groups
  68
  69/-- Spatial dimension. -/
  70def dim : ℕ := D
  71
  72/-! ## The Coefficient Derivation -/
  73
  74/-- The Tau Step Coefficient derived from W and D.
  75    Formula: C_tau = W + D/2 -/
  76noncomputable def tauStepCoefficientDerived : ℝ :=
  77  (W : ℝ) + (dim : ℝ) / 2
  78
  79/-- Verify the derived coefficient equals 18.5 (37/2). -/
  80theorem tauStepCoefficientDerived_eq : tauStepCoefficientDerived = 18.5 := by
  81  unfold tauStepCoefficientDerived W dim D wallpaper_groups
  82  norm_num
  83
  84/-- Verify it matches the form (2W + 3)/2 used in the paper. -/
  85theorem tauStepCoefficientDerived_matches_paper :
  86    tauStepCoefficientDerived = (2 * (W : ℝ) + 3) / 2 := by
  87  unfold tauStepCoefficientDerived dim D
  88  ring
  89
  90/-! ## The Full Step Formula -/
  91
  92/-- The Tau Generation Step derived from F, W, D, and α. -/
  93noncomputable def stepMuTauDerived : ℝ :=
  94  (F : ℝ) - tauStepCoefficientDerived * Constants.alpha
  95
  96/-- Main Theorem: The derived step matches the definition in Defs.lean. -/
  97theorem stepMuTauDerived_matches_def (step_mu_tau_def : ℝ)
  98    (h_def : step_mu_tau_def = (F : ℝ) - (2 * (W : ℝ) + 3) / 2 * Constants.alpha) :
  99    stepMuTauDerived = step_mu_tau_def := by
 100  rw [h_def]