feat: Add Auxiliary script test

[jstoobysmith]

Made with the help of Claude Opus 5.5.

AI Summary

Adds lake exe auxillary_script_test, which runs and checks the scripts that generate the website data. It runs in CI, and CI now treats warnings and info messages as errors. The PR also fixes everything the stricter CI exposed: five "Try this" info messages and the declaration name clashes between PhyslibAlpha and Physlib/QuantumInfo.

1. Auxiliary script test and CI

• scripts/auxillary-script-test.lean (new, lean_exe auxillary_script_test in lakefile.toml) runs make_tag, TODO_to_yml mkFile, stats mkHTML and informal mkFile mkDot mkHTML, and checks their output files.
• Each script runs in a temporary working directory with the source folders symlinked in, so it leaves no files behind.
• .github/workflows/build.yml absorbs alphaBuild.yml, which is deleted. Both builds use --iofail (fail on warnings and info messages), and the new test runs once both builds pass.
• Docs: AGENTS.md, scripts/README.md, scripts/PhyslibAlpha/README.md, and the bump template .github/ISSUE_TEMPLATE/Bump.yml, whose four script checkboxes and manual rm step become one item.

2. --iofail fixes

• ring → ring_nf in AnalyticVector/Local.lean, Existence/GaussianKernelGrowth.lean and JordanOrderUnit/Examples/SpinFactor.lean (×2).
• abel → abel_nf in JordanOrderUnit/Operator.lean.

3. Harmonic oscillator dedup

• Physlib/QuantumMechanics/HarmonicOscillator/Basic.lean:
  • potentialFunction_continuous (new): the potential function is continuous.
  • potentialFunction_aestronglyMeasurable, potentialOperator_isSelfAdjoint: previously informal_lemmas, now proved (the proofs come from PhyslibAlpha).
• PhyslibAlpha/QuantumMechanics/HarmonicOscillator/LadderSystem.lean (new):
  • toLadderSystem: the lowering and raising operators as a LadderSystem.
  • toLadderSystem_N_toLinearMap: its number operators are numberCLM.
• Removed PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Basic.lean and LadderOperators.lean, which duplicated Physlib: annihilationCLM/creationCLM are Physlib's loweringCLM/raisingCLM, and numberCLM and the commutation relations exist in Physlib.
• PhyslibAlpha/QuantumMechanics/HarmonicOscillator/Vacuum.lean: annihilationCLM_vacuumGaussian → loweringCLM_vacuumGaussian, and annihilationCLM_stdGaussian_of_xi_eq_one → loweringCLM_stdGaussian_of_xi_eq_one.

4. ProbabilisticTheory namespace

• Every declaration in PhyslibAlpha/ProbabilisticTheory and Physlib/ProbabilisticTheory moves into namespace ProbabilisticTheory. This fixes the clash between PhyslibAlpha's POVM and QuantumInfo's.
• Exception: API on types defined outside these folders (e.g. selfAdjoint, LinearPMap, PositiveLinearMap, unitary, StarAlgEquiv, BoundedMeasurable) stays in those types' namespaces so dot notation keeps working. Where needed it uses _root_.X.foo.
• One downstream fix: open ProbabilisticTheory in PhyslibAlpha/CondensedMatter/TightBindingChain/Uncertainty.lean.

Reviewer map

Look at each commit separately don't look at overall files changed.

Checks run locally

• lake build -KCI --iofail and lake build -KCI --iofail PhyslibAlpha
• lake exe auxillary_script_test (all four scripts pass)
• runPhyslibAlphaLinters, alphaFileImports, alphaPythonLinters.sh, check_file_imports
• python scripts/api_map_linter.py --repo .

🤖 Generated with Claude Code

[github-actions]

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

1. Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).

2. A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

3. The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages.

If you have any problems or questions, please reach out to the community on the Zulip.

[nateabr]

Changes look good to me, one point for clarification -- if auxillary_script_test fails in CI, will GitHub block the PR from being merged? Is the Style linters check required for merging to master?

awaiting-author

[jstoobysmith]

Changes look good to me, one point for clarification -- if auxillary_script_test fails in CI, will GitHub block the PR from being merged? Is the Style linters check required for merging to master?

auxillary_script_test yes it will block it. But I think this is what we want. The only time this would ever really break is when bumping Physlib.

[jstoobysmith]

--awaiting-author

[nateabr]

Okay sounds good, I think this can be merged :)