Abstract real algebra for higher material velocity rates and scale sums.

theorem AVenhance.Infra.Section4.amnr_higher_material_spatial_scale {E β : ℝ} (hE : 0 < E) (k r : ℕ) : E ^ (β - 1) * (E ^ (β - 2)) ^ r * E⁻¹ ^ k = E ^ (β - 1 + (β - 2) * ↑r - ↑k)

The velocity scale is a single negative epsilon power at each level.

theorem AVenhance.Infra.Section4.amnr_higher_material_exponent_nonpos {β : ℝ} (hβ : β < 4 / 3) (k r : ℕ) (hkr : 1 ≤ k + r) : β - 1 + (β - 2) * ↑r - ↑k ≤ 0

Every nonzero derivative has a negative coarse-to-fine scale exponent.

theorem AVenhance.Infra.Section4.amnr_higher_material_exponent_le {β : ℝ} (hβ : β < 4 / 3) (k r : ℕ) (hr : 1 ≤ r) : β - 1 + (β - 2) * ↑r - ↑k ≤ -(1 / 7)

Positive material levels have the uniform negative exponent needed by the supergeometric scale summation.

theorem AVenhance.Infra.Section4.amnr_higher_velocity_scale_antitone {E F β : ℝ} (hE : 0 < E) (hF : 0 < F) (hEF : E ≤ F) (hβ : β < 4 / 3) (k r : ℕ) (hkr : 1 ≤ k + r) : F ^ (β - 1) * (F ^ (β - 2)) ^ r * F⁻¹ ^ k ≤ E ^ (β - 1) * (E ^ (β - 2)) ^ r * E⁻¹ ^ k

Nonempty coarse velocity jets are bounded by the same current-scale rates. The zero-order drift is deliberately absent from this statement.