Counterterm Running and Fixed-Mass Ambiguity

Exact root statement

∀ {Scale : Type u_1} {Momentum : Type u_2} (data : PionCoefficientData Scale Momentum) (momentum : Momentum),
  data.CalibratedAt momentum →
    (∃ left right, data.scaleValue left ≠ data.scaleValue right) →
      have observe := PionAmplitudeJet.retainedScatteringReadout data.mass (data.momentumValue momentum);
      (∀ (scale : Scale),
          Complex.normSq (observe (data.withMassInsertion scale momentum)).1 = 1 ∧
            Complex.normSq (observe (data.withoutMassInsertion scale momentum)).1 = 1 ∧
              (observe (data.withMassInsertion scale momentum)).2.im = 0 ∧
                (observe (data.withoutMassInsertion scale momentum)).2.im = 0) ∧
        (∀ (left right : Scale),
            observe (data.withMassInsertion left momentum) = observe (data.withMassInsertion right momentum)) ∧
          (∀ (left right : Scale),
              (observe (data.withoutMassInsertion left momentum)).1 =
                (observe (data.withoutMassInsertion right momentum)).1) ∧
            ∃ left right,
              (observe (data.withoutMassInsertion left momentum)).2 ≠
                (observe (data.withoutMassInsertion right momentum)).2