Documentation

Lean 4 Proof

theorem eigenstructure_bridge (e : NSectorEconomy N) (n : Fin N) :
    -- For the block-diagonal (sector-decoupled) case, the eigenvalue of
    -- the dynamics matrix M = W · ∇²V at sector n equals the sector
    -- relaxation rate: μ_n = ℓ_n · |λ_⊥(n)| · (1 - T_n/T*_n)⁺.
    -- This is exactly sectorRelaxRate, proving that the eigenstructure
    -- bridge is definitionally built into the relaxation spectrum.
    sectorRelaxRate e n =
    e.ℓ n * |logCesEigenvaluePerp (e.J n) (e.ρ n) (e.c n)| *
      max 0 (1 - e.T n / sectorCriticalFriction e n) := rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/Relaxation.lean:154

Module Section

Results 1-7: Relaxation on the CES Potential Landscape

In the same file