Documentation

Lean 4 Proof

theorem tsallis_uniqueness (J : ℕ) (q : ℝ) (hq : q > 0) :
    -- The Tsallis entropy is the unique entropy satisfying
    -- pseudo-additivity with parameter q, symmetry, continuity,
    -- and expansibility.
    -- For q → 1: recovers Shannon entropy (unique additive entropy).
    -- For q ≠ 1: the non-extensive deformation is unique.
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:69

Module Section

Theorem 2: Tsallis Uniqueness (Paper 2, Section 3.1)

In the same file