Documentation

Lean 4 Proof

inductive PerturbationType where
  | relevant    -- Δ < 0: grows under aggregation (none for CES)
  | marginal    -- Δ = 0: preserved exactly (modes m ≤ 2, including ρ)
  | irrelevant  -- Δ > 0: decays under aggregation (modes m ≥ 3)

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:55

Module Section

Renormalization Group for CES:

In the same file