Coherence of Composition and Effects

A declared inverse-like composition relation needs the second operator to be able to change what the first must change. Footprints are upper bounds that contain every required dimension, so such a pair cannot have disjoint effects.

This is a consistency result about the declared composition entries. It does not derive the composition vocabulary and does not show that any pair restores anything.

theorem SE.Transformation.declared_inverseLike_effectsOverlap (a b : OperatorCode) (h : composition? a b = some CompositionRelation.inverseLike) : EffectsOverlap a b

Every declared inverse-like pair has overlapping effects, so no declared inverse-like pair is effect-disjoint.