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, the quotient ( dom T /. T ) is the standard carrier of T -blocks; see dfqs2 for the quotient-as-range viewpoint.
This is an untyped equilibrium predicate on pairs <. r , a >. . No hypothesis r e. Rels is built into the definition, because the fixpoint equation depends only on those ordered pairs <. x , y >. that belong to r and hence can witness an atomic instance x r y ; extra non-ordered-pair "junk" elements in r are ignored automatically by the relational membership predicate.
When later work needs r to be relation-typed (e.g. to intersect with ( Rels X. V ) -style typedness modules, or to apply Rels -based infrastructure uniformly), the additional typing constraint r e. Rels should be imposed locally as a separate conjunct (rather than being baked into this equilibrium module). (Contributed by Peter Mazsa, 25-Jan-2026) (Revised by Peter Mazsa, 20-Feb-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-blockliftfix | ⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 } |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cblockliftfix | ⊢ BlockLiftFix | |
| 1 | vr | ⊢ 𝑟 | |
| 2 | va | ⊢ 𝑎 | |
| 3 | 1 | cv | ⊢ 𝑟 |
| 4 | cep | ⊢ E | |
| 5 | 4 | ccnv | ⊢ ◡ E |
| 6 | 2 | cv | ⊢ 𝑎 |
| 7 | 5 6 | cres | ⊢ ( ◡ E ↾ 𝑎 ) |
| 8 | 3 7 | cxrn | ⊢ ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) |
| 9 | 8 | cdm | ⊢ dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) |
| 10 | 9 8 | cqs | ⊢ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) |
| 11 | 10 6 | wceq | ⊢ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 |
| 12 | 11 1 2 | copab | ⊢ { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 } |
| 13 | 0 12 | wceq | ⊢ BlockLiftFix = { ⟨ 𝑟 , 𝑎 ⟩ ∣ ( dom ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) / ( 𝑟 ⋉ ( ◡ E ↾ 𝑎 ) ) ) = 𝑎 } |