def
definition
def or abbrev
labScaleRatio
show as:
view Lean formalization →
formal statement (Lean)
65def labScaleRatio : ℝ := typicalLabPeriod_seconds / tau0_seconds
proof body
Definition body.
66
67/-- The ILG exponent α = (1 - φ⁻¹)/2 ≈ 0.191.
68 Using the RS constant φ = (1 + √5)/2. -/