Ramadge–Wonham as the math home for the vibe-linter

Parent: vibe-linter · Reference: ramadge-wonham-supervisory-control

RW is the precise math home for vibe-linter (better than Petri nets). "The supervisor can only disable controllable events, never force the plant" is the mathematical definition of a gatekeeper-not-driver.

The mapping:

• Test results are Σ_u — you allow running tests, you can't control red/green. So "tests must pass" is not a controllable spec; the controllable version is "commit is disabled until green is observed." RW elevates the gate-not-command intuition to a theorem.
• supC(K) = synthesis: you declare the property, the linter computes the minimal lock set — the least-restrictive set of commits/actions to disable.
• Partial observation = the observation surface: the supervisor sees only the projection (tool calls, not internal reasoning); any spec depending on "what the agent thought" is unexecutable. Lever: Σ_o can be bought larger — forcing all actions through tool calls (syscall-ization) enlarges the observation surface.