pith. machine review for the scientific record. sign in
def definition def or abbrev

ilg_alpha

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  69def ilg_alpha : ℝ := (1 - 1/phi) / 2

proof body

Definition body.

  70
  71/-- Lab-scale weight deviation: for α ≈ 0.191 and ratio ≈ 10¹³,
  72    the term (T_dyn/τ₀)^α ≈ (10¹³)^0.191 ≈ 10^2.5 ≈ 316.
  73
  74    However, C_lag is typically 10⁻³ to 10⁻⁵ for consistency with
  75    solar system tests. So the deviation is:
  76      w - 1 = C_lag * 315 ≈ 0.3 (at C_lag = 10⁻³)
  77
  78    This is a TESTABLE prediction if C_lag is not too small.
  79-/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.