Maximal Safe Controllable Domain

Abstract

The semantic indefinitely safe domain is the greatest controlled-safe fixed point.

Theorem 1.1 (The indefinitely safe domain is the greatest fixed point).

$$\begin{gathered} \forall X\in Type,\forall system\in \mathrm{ControlSystem}\left(X\right),S\in \mathrm{Set}\left(X\right),\mathrm{let}F:\mathrm{OrderHom}\left(\mathrm{Set}\left(X\right),\mathrm{Set}\left(X\right)\right):=K\mapsto \mathrm{intersect}\left(S,\mathrm{CPre}\left(system,K\right)\right); \\ \mathrm{let}Kstar:\mathrm{Set}\left(X\right):=\{x\in X\mid \exists I\in \mathrm{Set}\left(X\right),x\in I\wedge \left(I\subseteq S\wedge \left(\forall y\in I,\exists u\in \mathrm{Action}\left(system,y\right),\mathrm{successor}\left(system,y,u\right)\subseteq I\right)\right)\}; \\ Kstar=\mathrm{gfp}\left(F\right)\wedge \left(\left(\forall x\in \mathrm{gfp}\left(F\right),\exists u\in \mathrm{Action}\left(system,x\right),\mathrm{successor}\left(system,x,u\right)\subseteq \mathrm{gfp}\left(F\right)\right)\wedge \left(\mathrm{gfp}\left(F\right)\subseteq Kstar\wedge Kstar\subseteq \mathrm{gfp}\left(F\right)\right)\right) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Control/MaximalSafeControllableDomain.maximal_safe_controllable_domain (✓ std3). ∎

Source. Repository-derived.

Commentary.

A control system supplies a state-dependent action type and a nonempty successor set for every available action. The controlled predecessor uses existential action choice and universal successor containment.

The indefinitely safe set is constructed semantically: a state must lie in some subset of the safe states that offers a confining action at each of its states. It is not defined as a fixed point.

Independently, the displayed monotone operator intersects the safe set with the canonical controlled predecessor. Knaster-Tarski identifies its greatest fixed point with the semantic indefinitely safe set.

The remaining public clauses expose the confining action, indefinite-safety inclusion, and converse maximality. Repository searches found no exact theorem; Mathlib’s greatest-fixed-point laws are applied directly.

References

• Truth anchor: D5/S3/ConceptDynamics/Control/MaximalSafeControllableDomain.maximal_safe_controllable_domain
• Dependency: D5/S3/ConceptDynamics/Control/FiniteHorizonReachability