Documentation

Lean 4 Proof

theorem closure_no_free_params :
    -- All dynamics determined by (J, rho, T, ell, c, d_sq)
    -- No free fitting parameters beyond structural CES quantities
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/Closure.lean:130

Module Section

Results 80-85: Rho-Diversity Selection and Closure

In the same file