Documentation

Lean 4 Proof

theorem closure_integrability :
    -- Euler identity constrains rho trajectories to a submanifold
    -- of the full (rho, T) plane
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Closure.lean:153

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file