Experimental refactoring of LCM.lean

Stream: PrimeNumberTheorem+

[Terence Tao]

The integrated explicit analytic number theory network has two components. The "public" side of the network is the formalization project that so many of you are kindly contributing to; thank you very much for all the proofs and other work! But there is also an "internal" side in which I am working with a small group at UCLA to try to extract a more systematic network of "pipelines" from one type of bound to another from this formalization, with the eventual aim being to create some sort of living "spreadsheet" of analytic number theory estimates.

This will likely take several months to complete, but one of the students I am supervising, Xinjie He, has created a PR branch PNT#731 in which the LCM file has been experimentally refactored into components that will make this pipelining easier to work with, with a "static" layer of Lean proofs that do not involve any specific hardcoded constants, and a "dynamic layer" in which constants which were previously hardcoded in LCM.lean, such as 89683, are replaced with mutable parameters obeying some explicit numerical (or at least Lean-verifiable) constraints. This structure will then be combined with some non-Lean tools (some of which will involve AI) to create a robust pipeline from input bounds to output bounds. The LCM file is being used as a test case, but we plan to also similarly refactor the other files in the network as well.

We do not plan to merge this branch into the main branch for a while, and now that all the lemmas in LCM.lean are proved, this file should be fairly stable. But I thought you might be interested at getting a glimpse of what we are doing "behind the scenes".