31.3. Actions, transporters, blocks, and element access🔗

Finite actions retain their domain ordering. Images record the induced generator permutations; kernels are accepted only after checking the complete domain and every generator action. This is the kernel-checking boundary: a generator map alone does not prove an action law or a final kernel.

def opposite := polygon.blocks [(0, 2)]
#guard opposite.blockSize 0 = 2

def oppositeAction := polygon.blockAction opposite
  (polygon.blocks_invariant [(0, 2)]) 2
#guard oppositeAction.isOk

def source : Vector Bool 4 := #v[true, true, false, false]
def target : Vector Bool 4 := #v[false, true, true, false]
#guard (polygon.setTransporter? source target).isSome

def rankRoundTrip : Bool :=
  match polygon.unrank? 5 with
  | none => false
  | some p => (polygon.rank p).val == 5

#guard rankRoundTrip