Proposition 8.1 (i), p. 219 — a projection from a complete supervisor is unique

Proved

RamadgeWonham.Quotient.prop_8_1_i

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 = (S, \phi)$ and $\hat{\mathcal S} = (\hat S, \hat \phi)$ be supervisors with accessible automata $S$ , $\hat S$ , and let $\mathcal S$ be complete with respect to $\mathcal G$ . If $\pi, \pi' : X \to \hat X$ are both projections $\mathcal S \to \hat{\mathcal S}$ , then

\pi = \pi'.

So the quotient relation between supervisors carries no choice: a projection, when it exists, is determined by the two supervisors.

Formalization Note The standing assumptions of the paper are hypotheses: $\Sigma$ finite (p. 207), $\mathcal G$ trim, i.e. $L(\mathcal G) = \bar L_m(\mathcal G)$ (pp. 212–213), and both supervisor automata accessible (p. 210, recalled on p. 219).

Preamble

import Mathlib
import Definitions.Def_RamadgeWonham_Quotient_Projection

Formal statement

namespace RamadgeWonham.Quotient

open Shared.Generator

/-- Proposition 8.1 (i) (p. 219): if `𝒮` is complete with respect to `𝒢` and `π : 𝒮 → 𝒮̂` is a
projection, then `π` is unique. -/
theorem prop_8_1_i
    {α : 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 π) (hπ' : IsProjection 𝒮 𝒮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 (i)

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