Description: Define the equilibrium / fixed-point condition for "block carriers".
Start with a candidate block-family a (a set whose elements you intend to treat as blocks). Combine it with a relation r by forming the block-lift span T = ( r |X. (`'E |`a ) ) . For a block u e. a , the fiber [ u ] T is the set of all outputs produced from "external targets" of r together with "internal members" of u ; in other words, T is the mechanism that generates new blocks from old ones.
Now apply the standard quotient construction ( dom T /. T ) . This produces the family of all T-blocks (the cosets [ x ] T of witnesses x in the domain of T ). In general, this operation can change your carrier: starting from a , it may generate a different block-family ( dom T /. T ) .
The equation ( dom ( r |X. (`' E |`a ) ) /. ( r |X. (`'E |`a ) ) ) = a says exactly: if you generate blocks from a using the lift determined by r (cf. df-blockliftmap ), you get back the same a . So a is stable under the block-generation operator induced by r . This is why it is a genuine fixpoint/equilibrium condition: one application of the "make-the-blocks" operator causes no carrier drift, i.e. no hidden refinement/coarsening of what counts as a block.
Here, we generate this from the df-blockliftmap , taking the range of the two sides, resulting in ( dom ( r |X. (`' E |`a ) ) /. ( r |X. (`' _E |`a ) ) ) (via dfqs2 ), which you can define as "( R BlockLift A )" . In that case, you can define BlockLiftFix as "{ <. r , a >. | ( r BlockLift a ) = a }", or typed as "{ <. r , a >. | ( r e. Rels /\ ( r BlockLift a ) = a ) }".
This is a relation-typed equilibrium predicate. Restricting it to r e. Rels (see the explicit restriction in the alternate definition dfblockliftfix2 ) prevents representation junk (which may contain non-ordered-pair r that would not affect the predicate x r y , because that predicate only looks at ordered pairs) and makes the module composable with later Rels -based infrastructure; sethood of the quotient does not require it in itself. (Contributed by Peter Mazsa, 25-Jan-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-blockliftfix | |- BlockLiftFix = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cblockliftfix | |- BlockLiftFix |
|
| 1 | vr | |- r |
|
| 2 | va | |- a |
|
| 3 | 1 | cv | |- r |
| 4 | crels | |- Rels |
|
| 5 | 3 4 | wcel | |- r e. Rels |
| 6 | cep | |- _E |
|
| 7 | 6 | ccnv | |- `' _E |
| 8 | 2 | cv | |- a |
| 9 | 7 8 | cres | |- ( `' _E |` a ) |
| 10 | 3 9 | cxrn | |- ( r |X. ( `' _E |` a ) ) |
| 11 | 10 | cdm | |- dom ( r |X. ( `' _E |` a ) ) |
| 12 | 11 10 | cqs | |- ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) |
| 13 | 12 8 | wceq | |- ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a |
| 14 | 5 13 | wa | |- ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) |
| 15 | 14 1 2 | copab | |- { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) } |
| 16 | 0 15 | wceq | |- BlockLiftFix = { <. r , a >. | ( r e. Rels /\ ( dom ( r |X. ( `' _E |` a ) ) /. ( r |X. ( `' _E |` a ) ) ) = a ) } |