The formal proof for HS has been written (GitHub - bbchallenge/bbchallenge-proofs: Mathematical proofs of the bbchallenge project.) hence, the decider validates all the criteria of [Debate & Vote] Deciders’ validation process, hence the size-13 results were officially applied today!!!
Many thanks to @Iijil for proposing the method and being… extremely patient with the reviewing process. Many thanks to all those that also participated to the discussions and reviewing process, including @mateon1, @Nathan-Fenner, @TonyG and @UncombedCoconut !
Here is the main figure of the proof which gives the full Halting Segment graph (from the initial nodes) for a 3-state machine:
