It's because you're not using words in the way that people use them when talking about this stuff.

Rust (outside of the unsafe superset) has no undefined behavior. That is guaranteed, statically, at compile time: all execution paths have well-defined behaviors. That does not mean that there are no runtime consequences whatsoever. For example, the behavior of an invalid index is a panic, at runtime. Inserting a check for an invalid index at compile time is static enforcement of the behavior, even if the check itself happens at runtime.

If you had said "sometimes, Rust can't eliminate dynamic checks because it doesn't have a strong enough reasoning about some compile time properties" nobody would be arguing with you about this. Your example is one where a language with stronger reasoning would be able to detect it, for sure. Lean can do this, for example.