Images of flexible and non-flexible things

[zeramorphic]

There are a number of places where we seem to need the fact that the image of a flexible litter (or a near-litter to a flexible litter) is mapped to (something near) a flexible litter under an allowable partial permutation. The condition on non-flexible litters does not give everything that we need, however. It reads (currently):

Whenever $σ$ contains some condition $⟨⟨f{γ,δ}^A(g), N⟩, [-1,δ,A]⟩$, then every $A$-allowable permutation $ρ$ extending $σ$ has $N \sim f{γ,δ}^A(ρ • g)$.

We are often in a position where we either do not know if such a ρ even exists, or we have a permutation that is of too low a level, and therefore we can't use this condition. (Just noticed that in the code, this talks about $\gamma$-allowable permutations not $A$-allowable ones, this may be one of the problems?)

Non-flexible case

Flexible allowability condition

In this case, we add the condition $⟨f{γ,δ}^A(t), \pi(f{γ,δ}^A(t))⟩$ to a specification, where $\pi$ is $\delta$-allowable and $t \in \tau\gamma$. We need to show that $\pi(f{γ,δ}^A(t))$ is a non-flexible litter. However, because $\pi$ is $\delta$-allowable, we can't use the unpacked coherence condition on it.

Range is support-closed

We need to show that $\sigma$ along with the new constraint is support-closed under the action of $\gamma$-allowable permutations. These permutations are too low to use the unpacked coherence condition.

Carefully extends: all flexible litters lie in the range

Here we also need that the newly added near-litter is non-flexible.

There may be other cases where we need this, I've looked quite thoroughly at the code but I don't understand all of the partially-completed proofs.

[zeramorphic]

Just fixed the $A$ vs. $\gamma$ distinction - that doesn't solve any of the above problems I don't think but it did solve some others!