I like that option a lot. It’s simple and well-defined, and won’t run into trouble specifying some exact algorithm which may not match Python’s str.lower.
So we would change
Arbitrary equality comparisons are simple string equality operations which do not take into account any of the semantic information such as zero padding or local versions.
to, perhaps?
Arbitrary equality comparisons are simple string equality operations which do not take into account any of the semantic information such as zero padding or local versions. The comparison is case-insensitive for ASCII letters and undefined for any non-ASCII text.
Notably, I think we have to call it out as explicitly undefined in order for str.lower() to still be allowed as an implementation. Without that, and ascii text understood as case insensitive, I would assume that a correct implementation carefully does not upper, lower, or casefold arbitrary unicode text.