Documentation

Lean 4 Proof

theorem effectiveCurvature_taylor (J : ℕ) (ρ T c : ℝ) (hρ : ρ < 1)
    (hT : 0 < T) (hc : 0 < c) (hJ : 2 ≤ J) :
    -- The effective Hessian eigenvalue on 1⊥ is:
    -- λ_eff = logCesEigenvaluePerp + T · (Tsallis contribution)
    -- = -(1-ρ)/(Jc²) + T·ρ·J^{2-ρ}/c²
    -- = -(1-ρ)/(Jc²) · (1 - T/T*)
    -- where T* = (1-ρ)/(ρ·J^{2-ρ})
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/EffectiveCurvature.lean:50

Module Section

Theorem 4 and Propositions 5-7, Corollary 1:

In the same file