Proposition 8.1 (iii), p. 219 — the quotient of a complete supervisor is complete

Proved

RamadgeWonham.Quotient.prop_8_1_iii

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-event-systemsp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1supervisory-control

Let $\mathcal G$ be a trim generator over a finite alphabet $\Sigma$ with controllable events $\Sigma_c$ . Let $\mathcal S$ and $\hat{\mathcal S}$ be supervisors with accessible automata, let $\mathcal S$ be complete with respect to $\mathcal G$ , and let $\pi : \mathcal S \to \hat{\mathcal S}$ be a projection. Then

\hat{\mathcal S} \text{ is complete with respect to } \mathcal G.

Formalization Note Standing assumptions as hypotheses: $\Sigma$ finite, $\mathcal G$ trim, both supervisor automata accessible.

Preamble

import Mathlib
import Definitions.Def_RamadgeWonham_Quotient_Projection

Formal statement

namespace RamadgeWonham.Quotient

open Shared.Generator

/-- Proposition 8.1 (iii) (p. 219): if `𝒮` is complete with respect to `𝒢` and `π : 𝒮 → 𝒮̂` is a
projection, then `𝒮̂` is complete with respect to `𝒢`. -/
theorem prop_8_1_iii
    {α : Type} [Fintype α] {Ec : Set α} (𝒢 : Shared.Generator α) (h𝒢 : 𝒢.L = Shared.pre 𝒢.Lm)
    (𝒮 𝒮h : Shared.Supervisor α Ec) (h𝒮acc : 𝒮.S.Accessible) (h𝒮hacc : 𝒮h.S.Accessible)
    (h𝒮 : Shared.Complete 𝒢 𝒮)
    (π : 𝒮.S.Q → 𝒮h.S.Q) (hπ : IsProjection 𝒮 𝒮h π) :
    Shared.Complete 𝒢 𝒮h := by sorry

end RamadgeWonham.Quotient

Source

Ramadge and Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25(1), 1987, p. 219, Proposition 8.1 (iii)

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph