Memory infrastructure for the AMNR tensors.

theorem AVenhance.Infra.Section4.amnrOp_timeOnly {b : AmnrSpace → Homogenization.Vec 2} {f : ℝ → ℝ} {z : AmnrSpace} (hf : DifferentiableAt ℝ f z.1) (d : Option (Fin 2)) : amnrOp b d (fun (y : AmnrSpace) => f y.1) z = match d with | none => deriv f z.1 | some val => 0

A time-only scalar has no spatial derivative; its material derivative is its ordinary time derivative, regardless of the velocity.

theorem AVenhance.Infra.Section4.amnrWord_timeOnly_material {b : AmnrSpace → Homogenization.Vec 2} {f : ℝ → ℝ} {N : ℕ} (hf : ContDiff ℝ (↑N) f) (ℓ : ℕ) (hℓ : ℓ ≤ N) : (amnrWord b (List.replicate ℓ none) fun (z : AmnrSpace) => f z.1) = fun (z : AmnrSpace) => iteratedDeriv ℓ f z.1

Pure material words on the actual memory coefficient reduce to ordinary time derivatives, retaining its finite approved regularity order.

theorem AVenhance.Infra.Section4.amnrWord_timeOnly_mixed {b : AmnrSpace → Homogenization.Vec 2} {f : ℝ → ℝ} {N : ℕ} (hf : ContDiff ℝ (↑N) f) (α : List (Fin 2)) (ℓ : ℕ) (h : α.length + ℓ ≤ N) : (amnrWord b (amnrMixedWord α ℓ) fun (z : AmnrSpace) => f z.1) = if α = [] then fun (z : AmnrSpace) => iteratedDeriv ℓ f z.1 else 0

Spatial letters outside a time-only material word annihilate it.

theorem AVenhance.Infra.Section4.LMN_mixed_word_abs_le {β C₀ : ℝ} (I : Ingredients β) (hcutoff : I.Chat ≤ C₀) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {n : ℕ} (hn : n ≤ Nstar β) {b : AmnrSpace → Homogenization.Vec 2} {S : ℝ} (hS : 0 ≤ S) (α : List (Fin 2)) (ℓ : ℕ) (hbudget : α.length + 2 * ℓ ≤ Nstar β) (z : AmnrSpace) : |amnrWord b (amnrMixedWord α ℓ) (fun (y : AmnrSpace) => I.LMN κ m n y.1) z| ≤ amnrMemoryConstant β C₀ * (epsilon β I.Λ m ^ 2 / κ) * S ^ α.length * (tauP β I.Λ m)⁻¹ ^ ℓ

All admissible mixed memory derivatives use the proved §3 bound and the large cutoff rate. Spatial derivatives vanish. The invalid fine-rate comparison is neither assumed nor used.