Axiom audit for the low individual degree test

The soundness theorem, proved through the MIPStarRE development (a Lake dependency), must not depend on anything beyond the three standard axioms; this file fails to build otherwise.

The seeded-CL adapter of MIPRE/Background/LIDT/Adapter/ is this project's own mathematics rather than vendored, but it lives under MIPRE/Background/ and its guards are cheapest here, where the imports are already paid for. scripts/lean-coverage.py reads all three guard files and checks that the names guarded are exactly the names the blueprint marks with a proof-level \leanok, so which file a name sits in does not change what is claimed.

The seeded-CL adapter

Blueprint lem:lidt-cl-adapter-maps, lem:lidt-cl-adapter-weights, lem:lidt-cl-adapter-params and thm:lidt-cl-soundness-one. The headline theorem is the one worth printing in full: it says the seeded CL theorem at ldc = 1 rests on the vendored canonical-line theorem and nothing else.