The one-dimensional strict-oracle lower bounds transfer to every interior ℓp exponent.

theorem V7.Stage7StrictRandomizedExpected.lpNorm_fin_one {p : ℝ} (hp : 0 < p) (x : StrictPoint) : lpNorm p x = |x 0|

Direct derivation from the literal finite-sum definition: on Fin 1, every positive-exponent ell_p norm is absolute value.

theorem V7.oneDimensionalInteriorLpTransfer : OneDimensionalInteriorLpTransferStatement