`F`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
domain: Physics
line: 64 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  61/-! ## Ingredients -/
  62
  63/-- Face count (leading term). -/
  64def F : ℕ := cube_faces D
  65
  66/-- Wallpaper groups (2D symmetry count). -/
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.