Sections / Section 13: Hierarchical Architecture / institutionalMargin

Institutional Margin

defprovedHierarchy

Documentation

Lean 4 Proof

def institutionalMargin (T Tstar : ℝ) : ℝ := max 0 (1 - T / Tstar)

Dependency Graph

Used by

margin_monotone_in_Tstar institutionalMargin_nonneg margin_strict_in_Tstar institutionalMargin_at_critical fragility_at_critical institutionalMargin_at_zero

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:76

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file

reform_scaling_sigma reform_scaling_beta reform_substitutability institutionalMargin_nonneg institutionalMargin_at_zero institutionalMargin_at_critical institutionalAdjustmentTime adjustmentTimescale_connection adjustment_timescale_connection institutionalAdjustmentTime_pos inst_adjustment_decreasing_margin effectiveWelfareContribution eff_welfare_at_full_margin eff_welfare_decreasing_margin eff_welfare_nonneg fragility_at_critical margin_monotone_in_Tstar margin_strict_in_Tstar