NGM Characteristic Polynomial, general N

theorem trivial Hierarchy

Documentation

Lean 4 Proof

theorem ngm_char_poly_general (N : ℕ) (hN : 2 ≤ N) (k : Fin N → ℝ)
    (hk : ∀ n, 0 < k n) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Activation.lean:67

Module Section

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

In the same file

ngm_char_poly_two_level activation_two_level 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