Machine-Checked Formalization of the HHL and QSVT Quantum Algorithms in Lean 4

When an LLM-assisted Lean 4 project controls theorem statements as well as proofs, kernel acceptance certifies derivations but not the scientific claims as- sembled across files. We audit one frozen release of such a repository, covering quantum signal processing (QSP, a single-qubit phase-sequence primitive), its matrix generalisation quantum singular value transformation (QSVT), and the HHL linear-systems algorithm. We ask which layer of evidence is first sufficient to deter- mine the supported scope of its advertised headline results. From an earlier draft of this paper we enumerate 142 candidate claim occurrences and retain 116 after linking repeats; this is the broad universe, and the principal analysis is not a draw from it. It follows three purposively selected headline promotion paths, yielding 13 semantic and cross-layer diagnostics, supplemented by one archive-replay diagnos- tic and two engineering controls. In this artifact, under this fixed A–F order and these post-hoc audit diagnostics, build and trust checks confirm their two controls and are first-decisive for none of the 14; statement inspection is first-decisive for two, consumer and prose tracing for three, and Lean 4-checked boundary tests for eight. These counts describe one artifact under one ordering; they are not a defect rate, a method ranking, or evidence that any layer is universally decisive. A sixth layer, clean replay of the exact distributed archive, has not been completed and is not included among the established results. The supported core is a scalar real-part QSP characterisation, a restricted Hermitian-unitary flag-block eigenbasis lifting, and an exact positive-spectrum HHL algebraic capstone beginning from a supplied postselected and renormalised state. The artifact does not establish general operator-level QSVT, end-to-end HHL, or application complexity. We contribute a release-level claim-promotion protocol, a fixed-order descriptive analysis of this artifact, and Lean 4-checked boundary witnesses. Appendix A summarises the protocol as a standalone checklist