Does calling non-const mem. fun. on const object via non-const ref obtained via const_cast invoke UB only if the fun actually modifies the object?

In short, I'm asking whether the following code invokes UB only if /* body */ does indeed change the value of i, or also if it doesn't, by virtue of calling the non-const maybeChange member function on a const object.

// header.hpp
struct Foo {
  int i;
  void maybeChange();
};

void work(Foo const& foo);

// foo.cpp
#include "header.hpp"
void Foo::maybeChange() {
  /* body */
}

// work.cpp
#include "header.hpp"
void work(Foo const& foo) {
  const_cast<Foo&>(foo).maybeChange();
}

// main.cpp
#include "header.hpp"
Foo const foo{6};

int main() {
  work(foo);
}

I do see that the problem exists in case the modification really takes place, because that violates a legit assumption the compiler can make, i.e. that the foo global object doesn't change.

But on the other hand, http://eel.is/c++draft/dcl.type.cv#4 shows no example of calling non-const member function on const object to which const was const_casted away, but that doesn't actually modify it, like in my example above. It shows trivial examples like

const int* ciq = new const int (3);     // initialized as required
int* iq = const_cast<int*>(ciq);        // cast required
*iq = 4;                                // undefined behavior: modifies a const object

where the last line does truly modify the object *ciq.

Calling the function itself is not UB. There is only UB if you try to modify the value of one of the members or the object itself.

And if foo wasn't declared const, then there wouldn't even be UB if the function modified the object or its members.

It is exactly the same as for explicit function parameters. You can view the operand on the left-hand side of . as an implicit argument to an implicit parameter of type Foo&. It mostly behaves the same way as other arguments with that interpretation.

As referenced in your question, [dcl.type.cv]/4 is the only rule that results in UB due to constness and nothing in your example violates it. That there doesn't happen to be a suitable example for this in the standard doesn't change anything. If you think that it may help understanding, you could suggest adding such an example via editorial issue here, although I don't know the policies regarding examples or such suggestions.