Function check_scaling 

pub fn check_scaling(
    model: &Model,
    scaling: &Scaling,
    before: &[Cell],
    after: &[Cell],
    flights_before: &[Algebraic],
    flights_after: &[Algebraic],
) -> Result<(), String>

The certificate a tail rests on, checked on its own: the slots are closed under what feeds them, the field, the guards and the cycle’s statements setting them are homogeneous for the weights, after is the scaling’s image of before, and each flight of the round after is s^q times the same flight of the round before. A run whose state the scaling maps to its state a round later is then, round after round, the scaled copy of the round before. A scaling by one is the identity, which every model is homogeneous for: its certificate is that the state repeats.