NGM Characteristic Polynomial, N=2

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem ngm_char_poly_two_level (k10 k21 : ℝ) (hk10 : 0 < k10) (hk21 : 0 < k21) :
    -- The product of the two NGM entries gives the cycle product
    -- The spectral radius squared equals the cycle product
    Real.sqrt (k10 * k21) ^ 2 = k10 * k21 := by
  rw [sq_sqrt (mul_nonneg (le_of_lt hk10) (le_of_lt hk21))]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:33

Module Section

Theorems 5-6, Proposition 3: Next-Generation Matrix and Activation Threshold

In the same file

activation_two_level ngm_char_poly_general activation_threshold_iff_product reduced_dynamics cross_level_amplification weakest_link_bottleneck sensitivity_ratio_bottleneck activation_threshold_with_weights concentration_bottleneck irs_modified_activation cross_level_amplification_with_weights weakest_link_with_weights