{ "status": "PASS", "coverage_configurations": 34, "certified_path_optima": 68, "kernel_feasibility_crosschecks": 68, "all_zero_case_is_not_a_probability_distribution": true, "cases": [ { "weights": [ "0", "0", "0", "0", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": false }, { "weights": [ "0", "0", "0", "0", "1" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "0", "1", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "0", "1/2", "1/2" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "1/64", "error": [ "-3/8", "0", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/8" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "1", "0", "0" ], "root": { "cost": "0", "error": [ "-2", "-13/8", "0", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "1/2", "0", "1/2" ], "root": { "cost": "0", "error": [ "-2", "-13/8", "0", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "1/2", "1/2", "0" ], "root": { "cost": "0", "error": [ "-2", "-13/8", "0", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "0", "1/3", "1/3", "1/3" ], "root": { "cost": "0", "error": [ "-2", "-13/8", "0", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "1/96", "error": [ "-3/8", "0", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/12" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1", "0", "0", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/2", "0", "0", "1/2" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/2", "0", "1/2", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/3", "0", "1/3", "1/3" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "1/96", "error": [ "-3/8", "0", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/12" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/2", "1/2", "0", "0" ], "root": { "cost": "169/256", "error": [ "-19/16", "-13/16", "13/16", "0", "0" ], "multipliers": [ "0", "13/16" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/3", "1/3", "0", "1/3" ], "root": { "cost": "169/384", "error": [ "-19/16", "-13/16", "13/16", "0", "0" ], "multipliers": [ "0", "13/24" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/3", "1/3", "1/3", "0" ], "root": { "cost": "169/384", "error": [ "-19/16", "-13/16", "13/16", "0", "0" ], "multipliers": [ "0", "13/24" ] }, "enter": { "cost": "0", "error": [ "-3/8", "0", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "0", "1/4", "1/4", "1/4", "1/4" ], "root": { "cost": "169/512", "error": [ "-19/16", "-13/16", "13/16", "0", "0" ], "multipliers": [ "0", "13/32" ] }, "enter": { "cost": "1/128", "error": [ "-3/8", "0", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/16" ] }, "threshold": "1/128", "normalized_mse": true }, { "weights": [ "1", "0", "0", "0", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/2", "0", "0", "0", "1/2" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/2", "0", "0", "1/2", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "0", "0", "1/3", "1/3" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "1/96", "error": [ "0", "3/8", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/12" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/2", "0", "1/2", "0", "0" ], "root": { "cost": "1", "error": [ "-1", "-5/8", "1", "0", "0" ], "multipliers": [ "1", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "0", "1/3", "0", "1/3" ], "root": { "cost": "2/3", "error": [ "-1", "-5/8", "1", "0", "0" ], "multipliers": [ "2/3", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "-1/4", "0" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "0", "1/3", "1/3", "0" ], "root": { "cost": "2/3", "error": [ "-1", "-5/8", "1", "0", "0" ], "multipliers": [ "2/3", "0" ] }, "enter": { "cost": "0", "error": [ "0", "3/8", "0", "0", "1/4" ], "multipliers": [ "0", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/4", "0", "1/4", "1/4", "1/4" ], "root": { "cost": "1/2", "error": [ "-1", "-5/8", "1", "0", "0" ], "multipliers": [ "1/2", "0" ] }, "enter": { "cost": "1/128", "error": [ "0", "3/8", "0", "-1/8", "1/8" ], "multipliers": [ "0", "0", "1/16" ] }, "threshold": "1/128", "normalized_mse": true }, { "weights": [ "1/2", "1/2", "0", "0", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "9/256", "error": [ "-3/16", "3/16", "0", "-1/4", "0" ], "multipliers": [ "3/16", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "1/3", "0", "0", "1/3" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "3/128", "error": [ "-3/16", "3/16", "0", "-1/4", "0" ], "multipliers": [ "1/8", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "1/3", "0", "1/3", "0" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "3/128", "error": [ "-3/16", "3/16", "0", "0", "1/4" ], "multipliers": [ "1/8", "0", "0" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/4", "1/4", "0", "1/4", "1/4" ], "root": { "cost": "0", "error": [ "0", "0", "2", "0", "0" ], "multipliers": [ "0", "0" ] }, "enter": { "cost": "13/512", "error": [ "-3/16", "3/16", "0", "-1/8", "1/8" ], "multipliers": [ "3/32", "0", "1/16" ] }, "threshold": "0", "normalized_mse": true }, { "weights": [ "1/3", "1/3", "1/3", "0", "0" ], "root": { "cost": "217/288", "error": [ "-19/24", "-5/12", "29/24", "0", "0" ], "multipliers": [ "19/36", "5/18" ] }, "enter": { "cost": "3/128", "error": [ "-3/16", "3/16", "0", "-1/4", "0" ], "multipliers": [ "1/8", "0", "0" ] }, "threshold": "3/128", "normalized_mse": true }, { "weights": [ "1/4", "1/4", "1/4", "0", "1/4" ], "root": { "cost": "217/384", "error": [ "-19/24", "-5/12", "29/24", "0", "0" ], "multipliers": [ "19/48", "5/24" ] }, "enter": { "cost": "9/512", "error": [ "-3/16", "3/16", "0", "-1/4", "0" ], "multipliers": [ "3/32", "0", "0" ] }, "threshold": "9/512", "normalized_mse": true }, { "weights": [ "1/4", "1/4", "1/4", "1/4", "0" ], "root": { "cost": "217/384", "error": [ "-19/24", "-5/12", "29/24", "0", "0" ], "multipliers": [ "19/48", "5/24" ] }, "enter": { "cost": "9/512", "error": [ "-3/16", "3/16", "0", "0", "1/4" ], "multipliers": [ "3/32", "0", "0" ] }, "threshold": "9/512", "normalized_mse": true }, { "weights": [ "1/5", "1/5", "1/5", "1/5", "1/5" ], "root": { "cost": "217/480", "error": [ "-19/24", "-5/12", "29/24", "0", "0" ], "multipliers": [ "19/60", "1/6" ] }, "enter": { "cost": "13/640", "error": [ "-3/16", "3/16", "0", "-1/8", "1/8" ], "multipliers": [ "3/40", "0", "1/20" ] }, "threshold": "13/640", "normalized_mse": true }, { "weights": [ "9/10", "1/100", "1/100", "1/25", "1/25" ], "root": { "cost": "18/455", "error": [ "-2/91", "0", "180/91", "0", "0" ], "multipliers": [ "18/455", "0" ] }, "enter": { "cost": "769/291200", "error": [ "-3/728", "135/364", "0", "-1/8", "1/8" ], "multipliers": [ "27/3640", "0", "1/100" ] }, "threshold": "769/291200", "normalized_mse": true }, { "weights": [ "1/100", "9/10", "1/100", "1/25", "1/25" ], "root": { "cost": "4069/147200", "error": [ "-143/368", "-5/368", "593/368", "0", "0" ], "multipliers": [ "143/18400", "9/368" ] }, "enter": { "cost": "769/291200", "error": [ "-135/364", "3/728", "0", "-1/8", "1/8" ], "multipliers": [ "27/3640", "0", "1/100" ] }, "threshold": "769/291200", "normalized_mse": true } ], "common_error_line": [ { "A": [ [ "1", "0", "-1", "0", "0" ], [ "0", "1", "-1", "0", "0" ], [ "-1", "1", "0", "0", "0" ], [ "1", "-1", "0", "0", "0" ], [ "-1", "0", "1", "0", "0" ], [ "1", "0", "-1", "0", "0" ], [ "-1", "0", "0", "1", "0" ], [ "1", "0", "0", "-1", "0" ], [ "-1", "0", "0", "0", "1" ], [ "1", "0", "0", "0", "-1" ] ], "b": [ "-2", "-13/8", "0", "0", "0", "0", "0", "0", "0", "0" ], "farkas": [ "1", "0", "0", "0", "1", "0", "0", "0", "0", "0" ] }, { "A": [ [ "1", "-1", "0", "0", "0" ], [ "0", "-1", "1", "0", "0" ], [ "0", "0", "0", "1", "-1" ], [ "-1", "1", "0", "0", "0" ], [ "1", "-1", "0", "0", "0" ], [ "-1", "0", "1", "0", "0" ], [ "1", "0", "-1", "0", "0" ], [ "-1", "0", "0", "1", "0" ], [ "1", "0", "0", "-1", "0" ], [ "-1", "0", "0", "0", "1" ], [ "1", "0", "0", "0", "-1" ] ], "b": [ "-3/8", "13/8", "-1/4", "0", "0", "0", "0", "0", "0", "0", "0" ], "farkas": [ "0", "0", "1", "0", "0", "0", "0", "0", "1", "1", "0" ] } ], "nonlinear_sequence": [ { "n": 1, "error": [ "1", "-4", "2" ], "mse": "1" }, { "n": 2, "error": [ "1/2", "-9/2", "3/2" ], "mse": "1/4" }, { "n": 3, "error": [ "1/3", "-16/3", "4/3" ], "mse": "1/9" }, { "n": 5, "error": [ "1/5", "-36/5", "6/5" ], "mse": "1/25" }, { "n": 10, "error": [ "1/10", "-121/10", "11/10" ], "mse": "1/100" }, { "n": 100, "error": [ "1/100", "-10201/100", "101/100" ], "mse": "1/10000" }, { "n": 1000, "error": [ "1/1000", "-1002001/1000", "1001/1000" ], "mse": "1/1000000" } ], "falsification_controls": { "replace_strict_threshold_by_non_strict": true, "any_zero_weight_implies_zero_threshold": true, "local_zero_threshold_is_reachable_zero_threshold": true, "structural_links_can_be_dropped": true, "closed_convex_set_always_attains_psd_minimum": true }, "limits": "Exact finite fixtures and certificates; universal claims use RESULT.md proof.", "environment": { "python": "3.12.14", "platform": "Linux-6.8.0-137-generic-x86_64-with-glibc2.39", "executable": "/srv/venv/bin/python3", "checker_sha256": "46b13bc0869e77dfcf8dfb5579db71f7738541deae53b4cb73684f5f73677bf9" } }