Formalization-status correction

The note lean/docs/279.md describes the intended endpoint as a uniform polynomial-resource family with probability-one complete factorization LeanScope279. That is a scope statement.

In the inspected lean/ComparatorChallenges/ExactQuantumFactoring.lean, the endpoint is

theorem exact_quantum_factoring : MainTheorem := by sorry

LeanTarget279. Consequently, that file's endpoint is not a completed proof of its theorem body. This observation does not classify uninspected files or assert that no other proof artifact can exist. No Lean execution or completed formalization is claimed here.