`W`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.MassTopology
domain: Physics
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.MassTopology on GitHub at line 48.

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

  45def E_passive : ℕ := passive_field_edges 3
  46
  47/-- Wallpaper groups (Face symmetries). -/
  48def W : ℕ := wallpaper_groups
  49
  50/-! ## The Ledger Fraction -/
  51
  52/-- The base topological fraction: (W + E) / 4E_p. -/
  53def ledger_fraction : ℚ := (W + E_total) / (4 * E_passive)
  54
  55/-- The base shift: 2W + Fraction. -/
  56noncomputable def base_shift : ℝ := 2 * W + ledger_fraction
  57
  58/-! ## Radiative Corrections -/
  59
  60/-- Primary radiative correction: α². -/
  61noncomputable def correction_order_2 : ℝ := alpha ^ 2
  62
  63/-- Secondary radiative correction: E · α³. -/
  64noncomputable def correction_order_3 : ℝ := E_total * (alpha ^ 3)
  65
  66/-- Total radiative correction. -/
  67noncomputable def radiative_correction : ℝ := correction_order_2 + correction_order_3
  68
  69/-! ## The Refined Shift -/
  70
  71/-- The complete predicted shift. -/
  72noncomputable def refined_shift : ℝ := base_shift + radiative_correction
  73
  74end MassTopology
  75end Physics
  76end IndisputableMonolith

papers checked against this theorem

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