I understand the different domains quite well. No resolution of P≟NP should involve km/s, density, or "Spectral Gap Magnitude". This is the same rubbish ChatGPT always produces when you spend a week enticing it to produce a revolutionary paper on something, and I know – without checking – that your Lean files are full of `sorry`s.