Sections / Section 13: Hierarchical Architecture / reform_substitutability

Reform Substitutability

theoremprovedHierarchy

Documentation

Lean 4 Proof

theorem reform_substitutability {sigma_prev delta beta_n : ℝ} (hb : beta_n ≠ 0) :
    welfareContribution (sigma_prev / 2) delta beta_n =
    welfareContribution sigma_prev delta (2 * beta_n) := by
  simp only [welfareContribution]
  field_simp

Dependency Graph

Location

thesis/CESProofs/Hierarchy/InstitutionalReform.lean:61

Module Section

Institutional Reform Equivalence, Adjustment Timescale, and Fragility Ordering

In the same file

reform_scaling_sigma reform_scaling_beta institutionalMargin 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