{"id":"linear-inconsistency-certificate-check","version":"1.0.0","description":"Check a witness y that A x = b has no solution (yA = 0, yb != 0) or no x >= 0 solution (Farkas: yA >= 0, yb < 0).","supported_operations":["verify a certificate that a linear system has no solution","check a Farkas witness for A x = b with x >= 0","prove inconsistent simultaneous equations with multipliers","does this combination of equations give 0 = 1","validate an infeasibility proof for equality constraints","theorem of alternatives witness check","בדיקת הוכחה שאין פתרון למערכת משוואות"],"unsupported_operations":["finding a witness or solving the system (it only checks a supplied witness)","inequality rows or implied bounds (see linear-inequality-certificate-check)","integer infeasibility (no integer solution) proofs","floating-point witnesses given as JSON numbers"],"semantics":["Exact rationals are strings: an integer, a fraction p/q with q >= 1 or a finite decimal; JSON numbers, exponents, NaN and Infinity are rejected; outputs are canonical (reduced p/q, or an integer).","matrix is m x n (1-64 each) with equal row lengths; rhs and witness have m entries; dimensions are checked before any dot product. Column j of yA is sum_i y_i a_ij and yb = sum_i y_i b_i, exact.","variant free (x unrestricted, theorem of alternatives): valid when every column of yA is 0 and yb != 0. variant nonnegative (x >= 0, Farkas lemma): valid when every column of yA is >= 0 and yb < 0. There is no default variant.","Check order: columns j = 0..n-1 (combination_not_zero for free, sign_condition_violated for nonnegative; check column, index j, computed (yA)_j, required_relation = or >=, required_value 0), then the right-hand side (rhs_combination_zero with !=, or rhs_not_negative with <; check rhs, index null).","A valid free witness proves free-variable inconsistency; either it or its negation passes the nonnegative variant. The converse does not hold. Every output carries reference_version."],"limits":{"max_rows":64,"max_columns":64,"max_number_chars":64},"pricing":{"status":"unpriced","charge_usd":null},"input_schema":{"type":"object","additionalProperties":false,"required":["matrix","rhs","variant","witness"],"properties":{"matrix":{"type":"array","minItems":1,"maxItems":64,"items":{"type":"array","minItems":1,"maxItems":64,"items":{"type":"string","minLength":1,"maxLength":64,"pattern":"^-?(0|[1-9][0-9]*)(/[1-9][0-9]*|\\.[0-9]+)?$"}}},"rhs":{"type":"array","minItems":1,"maxItems":64,"items":{"type":"string","minLength":1,"maxLength":64,"pattern":"^-?(0|[1-9][0-9]*)(/[1-9][0-9]*|\\.[0-9]+)?$"}},"variant":{"type":"string","enum":["free","nonnegative"]},"witness":{"type":"array","minItems":1,"maxItems":64,"items":{"type":"string","minLength":1,"maxLength":64,"pattern":"^-?(0|[1-9][0-9]*)(/[1-9][0-9]*|\\.[0-9]+)?$"}}}},"output_schema":{"type":"object","additionalProperties":false,"required":["valid","reason","first_discrepancy","reference_version"],"properties":{"valid":{"type":"boolean"},"reason":{"type":["string","null"],"enum":["combination_not_zero","sign_condition_violated","rhs_combination_zero","rhs_not_negative",null]},"first_discrepancy":{"type":["object","null"],"additionalProperties":false,"required":["check","index","computed","required_relation","required_value"],"properties":{"check":{"type":"string","enum":["column","rhs"]},"index":{"type":["integer","null"],"minimum":0},"computed":{"type":"string","pattern":"^-?(0|[1-9][0-9]*)(/[1-9][0-9]*)?$"},"required_relation":{"type":"string","enum":["=",">=","!=","<"]},"required_value":{"type":"string","pattern":"^-?(0|[1-9][0-9]*)(/[1-9][0-9]*)?$"}}},"reference_version":{"type":"string","const":"r49-linear-inconsistency-1.0.0 (theorem of alternatives for Ax = b and Farkas lemma for Ax = b, x >= 0, Schrijver 1986 sections 3.1 and 7.3; exact rational arithmetic)"}}},"examples":[{"input":{"matrix":[["1","1"],["1","1"]],"rhs":["1","2"],"variant":"free","witness":["1","-1"]},"output":{"valid":true,"reason":null,"first_discrepancy":null,"reference_version":"r49-linear-inconsistency-1.0.0 (theorem of alternatives for Ax = b and Farkas lemma for Ax = b, x >= 0, Schrijver 1986 sections 3.1 and 7.3; exact rational arithmetic)"}},{"input":{"matrix":[["1","1"],["1","-1"]],"rhs":["1","3"],"variant":"nonnegative","witness":["1","-1"]},"output":{"valid":true,"reason":null,"first_discrepancy":null,"reference_version":"r49-linear-inconsistency-1.0.0 (theorem of alternatives for Ax = b and Farkas lemma for Ax = b, x >= 0, Schrijver 1986 sections 3.1 and 7.3; exact rational arithmetic)"}},{"input":{"matrix":[["1","-1"]],"rhs":["-1"],"variant":"nonnegative","witness":["1"]},"output":{"valid":false,"reason":"sign_condition_violated","first_discrepancy":{"check":"column","index":1,"computed":"-1","required_relation":">=","required_value":"0"},"reference_version":"r49-linear-inconsistency-1.0.0 (theorem of alternatives for Ax = b and Farkas lemma for Ax = b, x >= 0, Schrijver 1986 sections 3.1 and 7.3; exact rational arithmetic)"}}],"execute_url":"/v1/tools/linear-inconsistency-certificate-check/versions/1.0.0/execute"}