Relational Reachability Expansion

Abstract

A transition relation’s direct image preserves arbitrary unions, and its reachability least fixed point is the union of all finite stages.

Theorem 1.1 (Relational reachability expands through finite stages).

$$\begin{gathered} \forall X,J:\mathrm{Type}, \\ R:\mathrm{Set}(X\times X),I:\mathrm{Set}(X),A:J\to \mathrm{Set}(X), \\ {\mathrm{image}}_R({\mathrm{union}}_{i\in J}A(i))={\mathrm{union}}_{i\in J}{\mathrm{image}}_R(A(i))\wedge \\ \mathrm{lfp}((S\mapsto I\mathrm{union}{\mathrm{image}}_R(S)))={\mathrm{union}}_{n\in \mathbb{N}}(S\mapsto I\mathrm{union}{\mathrm{image}}_R(S){)}^{[n]}(\varnothing ). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S1/FixedPoints/RelationalReachExpansion.finite_step_expansion (✓ std3). ∎

Source. Repository-derived.

Commentary.

The transition relation is supplied as a set of state pairs. Its direct image sends a set of current states to all one-step successors. The first public conjunct states preservation of an arbitrary indexed union, including an empty family.

The reachability operator is constructed from the source primitives as Phi(A) = I0 union image_R(A). Reachability is its independently defined least fixed point, rather than a name assigned to the target stage union.

Mathlib’s exact SetRel.image_iUnion theorem proves the first conjunct and makes the constructed operator omega-Scott-continuous. The frozen Kleene-stage theorem is then applied directly to obtain the second conjunct.

References

• Truth anchor: D5/S1/FixedPoints/RelationalReachExpansion.finite_step_expansion
• Dependency: D5/S1/FixedPoints/KleeneStageLimit