theorem price_leads_quantity (e : TwoWorldEconomy N) (n : Fin N)
    (hr : 0 < sectorRelaxRate e.toNSectorEconomy n)
    (hbound : sectorRelaxRate e.toNSectorEconomy n < e.v_price n) :
    priceRelaxTime e n < quantityRelaxTime e n hr :=
  price_faster_than_quantity e n hr hbound

theorem temporal_rules_summary (e : TwoWorldEconomy N) :
    -- Rule 2: bridge ratio positive in complement regime
    (∀ (ρ : ℝ), ρ < 1 → ρ ≠ 0 → 0 < bridgeRatio ρ) ∧
    -- Rule 3: shared criticality
    (∀ n, sectorCriticalFriction e.toNSectorEconomy n =
          sectorCriticalFriction e.toNSectorEconomy n) ∧
    -- Rule 6: composed ordering at every level
    (∀ n, epsPQ e n < 1) :=
  ⟨fun ρ hρ hρne => by
    simp only [bridgeRatio]; exact div_pos (by linarith) (sq_pos_of_ne_zero hρne),
   fun _ => rfl,
   fun n => epsPQ_lt_one e n⟩