ProgressionGateOnEdge.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

On a genuine increasing edge, the symmetric gate is precisely the original progression restriction for that edge's padding divisor.