Documentation

Lean 4 Proof

theorem fully_specified_system
    (f_rho f_T : ℝ → ℝ → ℝ) :
    -- The pair (f_ρ, f_T) constitutes a complete 2D ODE system
    -- dρ/dt = f_ρ(ρ, T), dT/dt = f_T(ρ, T)
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/CoupledRhoT.lean:184

Module Section

Coupled (ρ, T) Jacobian Analysis

In the same file