The first-order instance of the initial trace estimate: the coordinate trace bound gives the gradient input of the initial-layer estimate. The trace bound itself is proved in TraceInstanceContract. No undifferentiated temperature norm enters the corrector bound.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_gradient_of_trace {g : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) {C r S : ℝ} (hr : 0 < r) (hS : 0 ≤ S) (hTraceOne : ∀ (i : Fin 2), √(l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad g x i) ≤ C * ↑(Nat.factorial 1) * (C / r) ^ 1 * S) : √(gradNormSq (spaceGrad g)) ≤ 2 * C ^ 2 * S / r

Coordinate n=1 trace implies the vector-gradient input of the initial-layer estimate.