Description: Define shift-stability, a general "procedure" pattern for "the one-step backward shift/transport of F along S ", and then i^i F enforces "and it already holds here".
Let F be a relation encoding a property that depends on a "level" coordinate (for example, a feasibility condition indexed by a carrier, a grade, or a stage in a construction). Let S be a shift relation between levels (for example, the successor map SucMap , or any other grading step).
The composed relation ( S o. F ) transports F one step along the shift: r ( S o. F ) n means there exists a predecessor level m such that r F m and m S n (e.g., m SucMap n ). We do not introduce a separate notation for "Shift" because it is simply the standard relational composition df-co .
The intersection ( ( S o. F ) i^i F ) is the locally shift-stable fragment of F : it consists exactly of those points where the property holds at some immediate predecessor that shifts to n and also holds at level n . In other words, it isolates the part of F that is already compatible with one-step tower coherence.
This definition packages a common construction pattern used throughout the development: "constrain by one-step stability under a chosen shift, then additionally constrain by F ". Iterating the operator ( X |-> ( ( S o. X ) i^i X ) corresponds to multi-step/tower coherence; the one-step definition here is the economical kernel from which such "tower" readings can be developed when needed. (Contributed by Peter Mazsa, 25-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-shiftstable | ⊢ ( 𝑆 ShiftStable 𝐹 ) = ( ( 𝑆 ∘ 𝐹 ) ∩ 𝐹 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cS | ⊢ 𝑆 | |
| 1 | cF | ⊢ 𝐹 | |
| 2 | 0 1 | cshiftstable | ⊢ ( 𝑆 ShiftStable 𝐹 ) |
| 3 | 0 1 | ccom | ⊢ ( 𝑆 ∘ 𝐹 ) |
| 4 | 3 1 | cin | ⊢ ( ( 𝑆 ∘ 𝐹 ) ∩ 𝐹 ) |
| 5 | 2 4 | wceq | ⊢ ( 𝑆 ShiftStable 𝐹 ) = ( ( 𝑆 ∘ 𝐹 ) ∩ 𝐹 ) |