pith. machine review for the scientific record. sign in
theorem proved term proof

nu_leading_lt_one

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)

 122theorem nu_leading_lt_one : nu_leading < 1 := by

proof body

Term-mode proof.

 123  rw [nu_leading, div_lt_one thermal_eigenvalue_pos]
 124  exact thermal_eigenvalue_relevant
 125
 126/-! ## 5. Anomalous-Dimension Correction -/
 127
 128/-- The anomalous correction to ν on a D-dimensional lattice.
 129
 130    When the anomalous dimension η ≠ 0, the thermal direction couples to
 131    the D field modes at the Q₃ spectral gap (multiplicity D).
 132    The correction η/(D + η) is the unique simplest (Padé [0/1]) rational
 133    function satisfying:
 134    * f(0) = 0 (vanishes at leading order),
 135    * f'(0) = 1/D (rate set by the spectral-gap multiplicity).
 136
 137    On Q₃ with D = `Q3_degree` = 3, the spectral-gap multiplicity equals D,
 138    matching the denominator. -/

depends on (16)

Lean names referenced from this declaration's body.