The canonical L2 envelope needs only the source finite regularity order.

theorem AVenhance.Infra.Section4.amnrCanonicalEnvelope_finite_L2_le {U : Set AmnrSpace} (hU : IsOpen U) {μ : MeasureTheory.Measure AmnrSpace} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict U)) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {N cut : ℕ} (hb : ContDiffOn ℝ (↑N) b U) (hf : ContDiffOn ℝ (↑N) f U) {S H G : ℝ} (hS : 0 < S) (hH : 0 < H) (hbound : ∀ (α : List (Fin 2)) (r : ℕ), α.length + 2 * r ≤ N → r ≤ cut → MeasureTheory.eLpNorm (amnrWord b (amnrMixedWord α r) f) 2 μ ≤ ENNReal.ofReal (G * amnrWeight S H (amnrMixedWord α r))) : MeasureTheory.eLpNorm (amnrCanonicalEnvelope N cut S H b f) 2 μ ≤ ENNReal.ofReal (↑(amnrCanonicalSamples N cut).card * G)

Summing only admissible canonical jets gives a finite L2 majorant with a constant depending on the finite budget and cutoff, never on the source scale.