Definition df-shiftstable 38505

Description: Define shift-stability, a general "procedure" pattern for "the one-step backward shift/transport of 𝐹 along 𝑆", and then ∩ 𝐹 enforces "and it already holds here".

Let 𝐹 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 𝑆 be a shift relation between levels (for example, the successor map SucMap, or any other grading step).

The composed relation (𝑆 ∘ 𝐹) transports 𝐹 one step along the shift: 𝑟(𝑆 ∘ 𝐹)𝑛 means there exists a predecessor level 𝑚 such that 𝑟𝐹𝑚 and 𝑚𝑆𝑛 (e.g., 𝑚 SucMap 𝑛). We do not introduce a separate notation for "Shift" because it is simply the standard relational composition df-co 5623.

The intersection ((𝑆 ∘ 𝐹) ∩ 𝐹) is the locally shift-stable fragment of 𝐹: it consists exactly of those points where the property holds at some immediate predecessor that shifts to 𝑛 and also holds at level 𝑛. In other words, it isolates the part of 𝐹 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 𝐹". Iterating the operator (𝑋 ↦ ((𝑆 ∘ 𝑋) ∩ 𝑋) 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.)

Assertion

Ref	Expression
df-shiftstable	⊢ (𝑆 ShiftStable 𝐹) = ((𝑆 ∘ 𝐹) ∩ 𝐹)

Detailed syntax breakdown of Definition df-shiftstable

Step	Hyp	Ref	Expression
1		cS	. . 3 class 𝑆
2		cF	. . 3 class 𝐹
3	1, 2	cshiftstable 38231	. 2 class (𝑆 ShiftStable 𝐹)
4	1, 2	ccom 5618	. . 3 class (𝑆 ∘ 𝐹)
5	4, 2	cin 3896	. 2 class ((𝑆 ∘ 𝐹) ∩ 𝐹)
6	3, 5	wceq 1541	1 wff (𝑆 ShiftStable 𝐹) = ((𝑆 ∘ 𝐹) ∩ 𝐹)

This definition is referenced by: (None)