Proof of Theorem 10.1, p. 223 — the supervisor 𝒮⁰ = (S⁰, φ∘π) is complete

Proved

RamadgeWonham.Quotient.thm_10_1_complete

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

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

Under the hypotheses of Theorem 10.1 ( $\mathcal G$ trim over a finite $\Sigma$ ; $\mathcal S = (S, \phi)$ complete with $S$ accessible, $K_3$ -reduced and $K_3$ -trim, where $K_3 = L(\mathcal S/\mathcal G)$ ; $\hat S^0 = (X^0, \Sigma, \xi^0, x^0_0, X^0)$ a trim recognizer for $K_3$ ), let $\pi : X^0 \to X$ satisfy $\pi(\xi^0(s, x^0_0)) = \xi(s, x_0)$ for every $s \in K_3$ . Then the supervisor

\mathcal S^0 = (S^0, \phi \circ \pi), \qquad S^0 = (X^0, \Sigma, \xi^0, x^0_0, \pi^{-1}(X_m)),

is complete with respect to $\mathcal G$ .

Preamble

import Mathlib
import Definitions.Def_RamadgeWonham_Quotient_Projection
import Definitions.Def_RamadgeWonham_Quotient_Reduced
import Definitions.Def_RamadgeWonham_Quotient_Recognizer

Formal statement

namespace RamadgeWonham.Quotient

open Shared.Generator

/-- Proof of Theorem 10.1 (p. 223, last paragraph): for the map `π : X⁰ → X` with
`π(ξ⁰(s, x⁰₀)) = ξ(s, x₀)` on `K₃`, the supervisor `𝒮⁰ = (S⁰, φ ∘ π)` with
`S⁰ = (X⁰, Σ, ξ⁰, x⁰₀, π⁻¹(X_m))` is complete with respect to `𝒢`. -/
theorem thm_10_1_complete
    {α : Type} [Fintype α] {Ec : Set α} (𝒢 : Shared.Generator α) (h𝒢 : 𝒢.L = Shared.pre 𝒢.Lm)
    (𝒮 : Shared.Supervisor α Ec) (h𝒮acc : 𝒮.S.Accessible) (h𝒮 : Shared.Complete 𝒢 𝒮)
    (hred : KReduced 𝒮.S (Shared.Lsup 𝒢 𝒮)) (htrim : KTrim 𝒮.S (Shared.Lsup 𝒢 𝒮))
    (R : Shared.Generator α) (hRrec : IsRecognizer R (Shared.Lsup 𝒢 𝒮)) (hRtrim : R.IsTrim)
    (hRQm : R.Qm = Set.univ)
    (π : R.Q → 𝒮.S.Q)
    (hπ : ∀ s ∈ Shared.Lsup 𝒢 𝒮, ∀ x0 : R.Q, R.run s = some x0 → 𝒮.S.run s = some (π x0)) :
    Shared.Complete 𝒢 (ofRecognizer R (π ⁻¹' 𝒮.S.Qm) (fun x0 => 𝒮.φ (π x0))) := 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. 223, proof of Theorem 10.1, fifth paragraph

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