Comparison with the continuous-loop Vervaat map

On a continuous loop, the first minimizing time agrees with the existing continuous-path choice, and the endpoint correction vanishes.

theorem BGW.Skorokhod.vervaatTime_ofContinuous (g : C(↑unitInterval, ℝ)) : vervaatTime (ofContinuous g) = ContinuumTrees.Vervaat.firstMinimum g

On continuous paths, the first minimizing time agrees with the continuous-path choice.

theorem BGW.Skorokhod.vervaatD_ofContinuous (g : C(↑unitInterval, ℝ)) (hloop : g 0 = g 1) : vervaatD (ofContinuous g) = ofContinuous (ContinuumTrees.Vervaat.vervaat ⟨g, hloop⟩)

On continuous loops, the càdlàg Vervaat map agrees with the existing continuous-loop transform (C33, comparison with ContinuumTrees.Vervaat.vervaat).