One thing that initially stood out to me on the fundamental theorem was: where did the N→M arrow come from? It ‘gets introduced’ in the first bookkeeping step (we draw N→M and then reorder the (N,M,X¯i) subgraph at each i.
This seemed suspicious to me at first! It seemed like kind of a choice, so what if we just didn’t add that arrow? Could we land at a conclusion of N AND M→X? That’s way too strong! But I played with it a bit, and there’s no obvious way to do the second frankenstitch which brings everything together unless you draw in that extra arrow and rearrange. You just can’t get a globally consistent topological ordering without N somehow becoming ancesterable to X¯i. (Otherwise the glommed X¯i variables interfere with each other when you try to find N’s ancestors in the stitch.)
Still, this move seems quite salient—in particular that arrow-addition feels something like the ‘lossiest’ step in the proof (except for the final bookkeeping which gloms all the Xi together, implicitly drawing a load of arrows between them all)?
One thing that initially stood out to me on the fundamental theorem was: where did the N→M arrow come from? It ‘gets introduced’ in the first bookkeeping step (we draw N→M and then reorder the (N,M,X¯i) subgraph at each i.
This seemed suspicious to me at first! It seemed like kind of a choice, so what if we just didn’t add that arrow? Could we land at a conclusion of N AND M→X? That’s way too strong! But I played with it a bit, and there’s no obvious way to do the second frankenstitch which brings everything together unless you draw in that extra arrow and rearrange. You just can’t get a globally consistent topological ordering without N somehow becoming ancesterable to X¯i. (Otherwise the glommed X¯i variables interfere with each other when you try to find N’s ancestors in the stitch.)
Still, this move seems quite salient—in particular that arrow-addition feels something like the ‘lossiest’ step in the proof (except for the final bookkeeping which gloms all the Xi together, implicitly drawing a load of arrows between them all)?