> How is it logically coherent?

It's not. But Lean doesn't interrogate logical coherence, just internal consistency.