fix(benchmarks): publish Farkas scalar replay contract (#1309)

* fix(benchmarks): publish Farkas scalar replay contract

* test: allow checker installation under parallel load

* test: allow inverse verification under parallel load

---------

Co-authored-by: morluto <76467478+morluto@users.noreply.github.com>

Author: yuelgrace1810-ops

benchmarks/datasets/mathematical-benchmarks-v1/exact-farkas-ldl-slice/README.md

@@ -17,7 +17,8 @@ calibration is pending. Either an exact LDL factorization or a Sylvester
 certificate is accepted. Floating-point eigenvalues, copied source status, or
 a single positive minor cannot pass.
 
-The verifier independently checks reduced fractions, scalar arithmetic and
-signs, and the selected positive-definiteness certificate. It intentionally
-does not check the remaining matrix entries, the other five blocks, the full
-Farkas implication, or Lean, and caps assurance at `COMPUTED`.
+The verifier independently checks reduced fractions, the published scalar
+replay `m00 = y0 + c00_y` with `m00 < 0` and `objective > 0`, and the selected
+positive-definiteness certificate. It intentionally does not check the
+remaining matrix entries, the other five blocks, the full Farkas implication,
+or Lean, and caps assurance at `COMPUTED`.

benchmarks/datasets/mathematical-benchmarks-v1/exact-farkas-ldl-slice/instruction.md

@@ -2,8 +2,9 @@
 
 The frozen input contains scalar values and a 4×4 principal submatrix extracted
 from the canonical exact rational Farkas certificate in the Bandeira 0.2a
-repository. Establish the two scalar sign checks and certify that this matrix
-is positive definite using either:
+repository. Replay the scalar identity `m00 = y0 + c00_y`, establish the two
+sign checks `m00 < 0` and `objective > 0`, and certify that this matrix is
+positive definite using either:
 
 - `LDL`: an exact unit-lower-triangular `L` and positive diagonal `D`
   satisfying `Q=L D L^T`; or

benchmarks/validation/mathematical_benchmarks_v1/test_exact_farkas_ldl_slice.py

@@ -10,6 +10,15 @@
 TASK = "exact-farkas-ldl-slice"
 
 
+def test_exact_farkas_slice_publishes_scored_scalar_identity() -> None:
+    task = support.TASKS / TASK
+    instruction = (task / "instruction.md").read_text()
+
+    assert "`m00 = y0 + c00_y`" in instruction
+    assert "`m00 < 0`" in instruction
+    assert "`objective > 0`" in instruction
+
+
 def _prepare_farkas_slice_case(tmp_path: Path):
     task, app, logs = support._prepare_case(
         tmp_path, "exact-farkas-ldl-slice", "computed"