Lean scope and the inspected target files

The scope note lean/docs/119.md names 119-01 and describes soft contraction, the Boolean refinement, and the selected production inequality Lean119Scope. The inspected Comparator challenge files CourtadeKumar.lean and SoftChannel204.lean specify these targets. Their respective principal theorem bodies, courtadeKumarAndAttainment and fullMain, contain sorry Lean119CK,Lean119Soft.

Thus the inspected target files are not completed proofs of those theorem bodies. This is a statement about the inspected files, not an exhaustive inspection of every possible solution artifact. The Hellinger inequality of 119-02 is not separately specified by these targets. No Lean execution or independent formal verification is asserted here.