Sections / Section 13: Hierarchical Architecture / trivial_fixed_point_at_rho_one

Trivial Fixed Point At Rho One

theoremprovedHierarchy

Documentation

Lean 4 Proof

theorem trivial_fixed_point_at_rho_one {J : ℕ} :
    curvatureK J 1 = 0 :=
  curvatureK_eq_zero_of_rho_one

Dependency Graph

Location

thesis/CESProofs/Hierarchy/RenormalizationGroup.lean:243

Module Section

Renormalization Group for CES:

In the same file

scalingDimension PerturbationType classifyMode rgBetaFunction anomalousDimension criticalExponentOrderParam criticalExponent_orderParam criticalExponent_susceptibility criticalExponentSusceptibility scalingDimension_zero_iff_ces scaling_dimension_zero_iff_ces scalingDimension_cubic scaling_dimension_cubic scalingDimension_monotone scaling_dimension_monotone no_relevant_perturbations modeRate_eq_rpow_neg_scaling modeAfterL_eq_rpow_scaling beta_function_vanishes anomalous_dimension_vanishes