The positive-jet interface already used by relative_step supplies its initial n=1 trace. No sup norm of the undifferentiated temperature enters.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_trace_one_of_positive_jets {A r S : ℝ} {g : Homogenization.Vec 2 → ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (hT0 : T 0 = g) (hJets : PositiveTemperatureJets A r S T) (i : Fin 2) : √(l2NormSq fun (x : Homogenization.Vec 2) => spaceGrad g x i) ≤ A * ↑(Nat.factorial 1) * (A / r) ^ 1 * S

Initial n=1 trace from the actual positive temperature jet interface.