Relational Reach Stage Expansion

Abstract

A relation-generated reachability operator expands from the empty and initial stages through every finite successor stage.

Theorem 1.1 (Relational reachability expands through all finite stages).

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

Proof. Machine-checked in Lean as D5/S1/FixedPoints/Reachability/RelationalReachStageExpansion.finite_step_expansion_with_initial_stages (✓ std3). ∎

Source. Repository-derived.

Commentary.

The transition relation R and initial set I0 construct the canonical operator Phi(S) = I0 union image_R(S). No reachability object is defined by the conclusion it is meant to satisfy.

The frozen finite-step theorem supplies arbitrary-union preservation and identifies the least fixed point with the union of all finite iterates from the empty set.

The restored public clauses expose the zeroth and first iterates and the successor recurrence. Thus every later stage keeps I0 and adds one further direct relational image.

Repository body-shape search found the canonical reachStep primitive and no existing public theorem carrying all restored stage clauses. Pinned Mathlib’s iterate identities discharge those clauses.

References

• Truth anchor: D5/S1/FixedPoints/Reachability/RelationalReachStageExpansion.finite_step_expansion_with_initial_stages
• Dependency: D5/S1/FixedPoints/RelationalReachExpansion