From 7fdae743973bebb77daf4508d05655dc1e8915c7 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Mon, 2 Nov 2026 15:59:11 -0800 Subject: [PATCH] Certify the minimum 237-row P112 demand subfamily --- research/p112-farkas-kernel/NOTICE | 17 + research/p112-farkas-kernel/ORACLE.json | 1 + research/p112-farkas-kernel/PROOF.md | 105 ++ research/p112-farkas-kernel/README.md | 99 ++ research/p112-farkas-kernel/RESULT.json | 1 + research/p112-farkas-kernel/SOURCE-PINS.json | 20 + research/p112-farkas-kernel/SOURCES.json | 19 + research/p112-farkas-kernel/TASK.json | 101 ++ research/p112-farkas-kernel/VALIDATION.md | 56 + research/p112-farkas-kernel/VERIFY.json | 33 + research/p112-farkas-kernel/oracle.py | 281 ++++ .../p112-farkas-kernel/sources/README-6425.md | 123 ++ .../sources/RESULT-6425.json | 1493 +++++++++++++++++ research/p112-farkas-kernel/verify.py | 275 +++ 14 files changed, 2624 insertions(+) create mode 100644 research/p112-farkas-kernel/NOTICE create mode 100644 research/p112-farkas-kernel/ORACLE.json create mode 100644 research/p112-farkas-kernel/PROOF.md create mode 100644 research/p112-farkas-kernel/README.md create mode 100644 research/p112-farkas-kernel/RESULT.json create mode 100644 research/p112-farkas-kernel/SOURCE-PINS.json create mode 100644 research/p112-farkas-kernel/SOURCES.json create mode 100644 research/p112-farkas-kernel/TASK.json create mode 100644 research/p112-farkas-kernel/VALIDATION.md create mode 100644 research/p112-farkas-kernel/VERIFY.json create mode 100644 research/p112-farkas-kernel/oracle.py create mode 100644 research/p112-farkas-kernel/sources/README-6425.md create mode 100644 research/p112-farkas-kernel/sources/RESULT-6425.json create mode 100644 research/p112-farkas-kernel/verify.py diff --git a/research/p112-farkas-kernel/NOTICE b/research/p112-farkas-kernel/NOTICE new file mode 100644 index 0000000000..83e68e0313 --- /dev/null +++ b/research/p112-farkas-kernel/NOTICE @@ -0,0 +1,17 @@ +New finite-kernel generator, certificate checker, proof and package metadata: +ToikY, with substantial OpenAI Codex assistance. Apache-2.0. + +The two source files are retained verbatim from Nick Petalas's PR6425, exact +head092dcbd13d1263e691ad29f34fbf286fea1fac2c. Their original headings and credit +remain. SOURCE-PINS.json records exact Git blob identities, byte lengths and +SHA256 digests; no predecessor executable is imported or replayed. + +Retain predecessor credit to Jeremy Diviney/PR1422 for the complete-clique guard, +geometry/caps and smaller-family question; Cinna Davis/PR1347/1323 for the support +model and geometry; Navinor, David Arias, Hanson Sun, DreamingOfClouds, +themilkman216 and the retained E8/label/decoder lineage. + +PR5767 is related exact-certificate tooling, not the source of an optimization +solver here. Its shared limits and code are unchanged. Linear programming, +nonnegative implication/Farkas certificates, simplex and Bland's rule are +classical methods; no literature priority is claimed. diff --git a/research/p112-farkas-kernel/ORACLE.json b/research/p112-farkas-kernel/ORACLE.json new file mode 100644 index 0000000000..ab09c25452 --- /dev/null +++ b/research/p112-farkas-kernel/ORACLE.json @@ -0,0 +1 @@ +{"checked":{"deletions":[{"coefficients":["0","1","0","1","1","0","1","1","1","1","1","1","0","0"],"demand":5,"premises":3,"right_hand_side":"5","target":"0xfda"},{"coefficients":["1","1","0","1","1","0","1","0","1","0","1","0","1","0"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x155b"},{"coefficients":["0","1","1","1","1","0","1","0","1","0","1","0","1","0"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x155e"},{"coefficients":["0","1","0","1","1","0","0","0","1/2","0","1","1","1","0"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x1d1a"},{"coefficients":["0","1","0","1","0","0","1","0","1","0","1","1","1","0"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x1d4a"},{"coefficients":["0","0","0","1","1","0","1","0","1/2","0","1","1","1","0"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x1d58"},{"coefficients":["0","1","0","1","0","0","1","1","0","1","1","1","1","0"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x1eca"},{"coefficients":["0","1","0","1","1","0","0","1","1/2","1","1","1","1","0"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x1f9a"},{"coefficients":["0","1","0","1","0","0","1","1","1","1","1","1","1","0"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x1fca"},{"coefficients":["0","1","0","0","1","0","1","1","1","1","1","1","1","0"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x1fd2"},{"coefficients":["0","0","0","1","1","0","1","1","1/2","1","1","1","1","0"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x1fd8"},{"coefficients":["1","1","0","1","1","0","1","1","1","1","1","1","1","0"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x1fdb"},{"coefficients":["0","1","1","1","1","0","1","1","1","1","1","1","1","0"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x1fde"},{"coefficients":["0","1","0","1","1","0","1","0","1","0","1","0","0","1"],"demand":5,"premises":3,"right_hand_side":"5","target":"0x255a"},{"coefficients":["1","1","0","1","1","0","1","0","1","0","1","0","0","1"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x255b"},{"coefficients":["1","1","0","1","1","0","1","1","1","1","1","1","0","1"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x2fdb"},{"coefficients":["0","1","0","1","1","0","1","0","1","0","0","0","1","1"],"demand":5,"premises":3,"right_hand_side":"5","target":"0x315a"},{"coefficients":["0","1","0","1","1","1/2","0","0","0","0","1","0","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x343a"},{"coefficients":["0","0","0","1","1","1/2","1","0","0","0","1","0","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x3478"},{"coefficients":["0","1","0","1","1","0","0","0","1","0","1","0","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x351a"},{"coefficients":["0","1","0","1","0","0","1","0","1","0","1","0","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x354a"},{"coefficients":["0","1","0","0","1","0","1","0","1","0","1","0","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x3552"},{"coefficients":["0","0","0","1","1","0","1","0","1","0","1","0","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x3558"},{"coefficients":["1","1","1","1","1","0","1","0","1","0","1","0","1","1"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x355f"},{"coefficients":["1","1","0","1","1","1","1","0","1","0","1","0","1","1"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x357b"},{"coefficients":["0","1","1","1","1","1","1","0","1","0","1","0","1","1"],"demand":7,"premises":5,"right_hand_side":"7","target":"0x357e"},{"coefficients":["0","1","0","1","1","0","0","0","1","0","0","1","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x399e"},{"coefficients":["0","1","0","1","1","0","0","0","1","0","0","1","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x3b1e"},{"coefficients":["0","1","0","1","1","0","0","0","1","0","0","1","1","1"],"demand":4,"premises":3,"right_hand_side":"4","target":"0x3b9a"},{"coefficients":["0","1","1/2","1","1","0","0","1/2","1","1/2","0","1","1","1"],"demand":5,"premises":3,"right_hand_side":"5","target":"0x3b9e"},{"coefficients":["0","0","1","1","1","1","1","1","1","1","0","1","1","1"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x3bfc"},{"coefficients":["1","0","0","0","1","1","1","0","0","0","1","1","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x3c75"},{"coefficients":["1","1","0","1","0","0","1","0","1","0","1","0","1","1"],"demand":5,"premises":4,"right_hand_side":"5","target":"0x3dcb"},{"coefficients":["1/2","1","0","1","0","1","0","1/2","0","1/2","1","1","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x3eab"},{"coefficients":["0","1","1/2","1","0","1","0","1/2","0","1/2","1","1","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x3eae"},{"coefficients":["1","0","0","0","1","1","1","0","0","0","1","1","1","1"],"demand":3,"premises":3,"right_hand_side":"3","target":"0x3ef1"},{"coefficients":["1","1","1","1","1","1","1","1","0","1","1","1","1","1"],"demand":8,"premises":2,"right_hand_side":"8","target":"0x3eff"},{"coefficients":["1","1","0","1","0","0","1","0","1","0","1","0","1","1"],"demand":5,"premises":4,"right_hand_side":"5","target":"0x3f4b"},{"coefficients":["1","1","1","1","0","1","0","1","1","1","1","1","1","1"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x3faf"},{"coefficients":["1","1","1","1","1","0","1","1","1","1","1","1","1","1"],"demand":8,"premises":2,"right_hand_side":"8","target":"0x3fdf"},{"coefficients":["1","0","1","0","1","1","1","1","1","1","1","1","1","1"],"demand":6,"premises":3,"right_hand_side":"6","target":"0x3ff5"},{"coefficients":["1","1","0","1","1","1","1","1","1","1","1","1","1","1"],"demand":8,"premises":4,"right_hand_side":"8","target":"0x3ffb"},{"coefficients":["0","1","1","1","1","1","1","1","1","1","1","1","1","1"],"demand":8,"premises":4,"right_hand_side":"8","target":"0x3ffe"}],"retained":["0x5a","0xc0a","0xc50","0xc51","0xd0a","0xd50","0xe8a","0xedb","0xf8a","0xf8b","0xfd0","0xfd1","0x1412","0x1448","0x145f","0x1513","0x1516","0x1549","0x154c","0x1818","0x1842","0x1942","0x1a98","0x1a9c","0x1ac2","0x1ada","0x1ade","0x1bc2","0x1bc6","0x1c52","0x1c59","0x1c5c","0x1c9b","0x1c9e","0x1e1b","0x1e1e","0x1e9b","0x1edf","0x1f9b","0x1f9e","0x1fcb","0x1fce","0x1fd3","0x1fd6","0x1fd9","0x1fdc","0x2418","0x2442","0x2462","0x2463","0x247a","0x247b","0x2518","0x2519","0x2542","0x2543","0x2812","0x2848","0x2912","0x2932","0x295a","0x297a","0x2ada","0x2afa","0x2bc8","0x2be8","0x2c1b","0x2c3a","0x2c4a","0x2c52","0x2c58","0x2d1a","0x2d3a","0x2d3b","0x2d52","0x2d72","0x2d73","0x2d7b","0x2dca","0x2dd8","0x2eca","0x2ed3","0x2eea","0x2eeb","0x2ef3","0x2efb","0x2f4a","0x2f58","0x2f9b","0x2fca","0x2fcb","0x2fd2","0x2fd3","0x2fd8","0x2fd9","0x2fda","0x300a","0x302a","0x3050","0x3070","0x307e","0x310a","0x312e","0x3150","0x3174","0x341b","0x341e","0x344a","0x344b","0x344e","0x3452","0x3453","0x3456","0x3459","0x345b","0x345c","0x345e","0x346f","0x3477","0x347f","0x351f","0x353b","0x353e","0x354f","0x3557","0x355d","0x356b","0x356e","0x3573","0x3576","0x3579","0x357c","0x383a","0x3852","0x3858","0x386a","0x393a","0x393e","0x3952","0x395a","0x3976","0x397e","0x39ce","0x39d8","0x39ea","0x3aca","0x3ada","0x3af8","0x3afe","0x3b4e","0x3b58","0x3b6a","0x3bca","0x3bd8","0x3bee","0x3c01","0x3c04","0x3c0b","0x3c0e","0x3c13","0x3c16","0x3c1f","0x3c21","0x3c24","0x3c33","0x3c36","0x3c49","0x3c4c","0x3c54","0x3c69","0x3c6c","0x3c99","0x3c9c","0x3caf","0x3cc3","0x3cc6","0x3d1b","0x3d1e","0x3d37","0x3d3f","0x3d48","0x3d68","0x3d77","0x3d7f","0x3d8f","0x3dab","0x3dbc","0x3dc6","0x3dce","0x3dea","0x3df1","0x3df8","0x3e19","0x3e1c","0x3e2f","0x3e43","0x3e46","0x3e85","0x3ea5","0x3ec7","0x3ecb","0x3ece","0x3ed3","0x3ed6","0x3ee6","0x3ee7","0x3eef","0x3ef4","0x3ef7","0x3f0f","0x3f2b","0x3f3c","0x3f46","0x3f4e","0x3f6a","0x3f71","0x3f78","0x3f8e","0x3f9d","0x3f9f","0x3fb3","0x3fb6","0x3fbb","0x3fbe","0x3fc7","0x3fcf","0x3fd4","0x3fd7","0x3fdd","0x3fe9","0x3feb","0x3fec","0x3fee","0x3ff3","0x3ff6","0x3ff9","0x3ffc"],"separators":[{"integral_witness":true,"minimum_other_slack":"14","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"4","target":"0x5a","target_demand":4,"target_lhs":"0","x":["8","0","8","0","0","8","0","8","8","8","8","8","8","8"]},{"integral_witness":true,"minimum_other_slack":"6","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1","target":"0xc0a","target_demand":1,"target_lhs":"0","x":["8","0","8","0","8","8","8","8","8","8","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"6","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1","target":"0xc50","target_demand":1,"target_lhs":"0","x":["8","8","8","8","0","8","0","8","8","8","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1","target":"0xc51","target_demand":2,"target_lhs":"1","x":["0","8","8","8","1","8","0","8","8","8","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1","target":"0xd0a","target_demand":2,"target_lhs":"1","x":["8","1","8","0","8","8","8","8","0","8","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1","target":"0xd50","target_demand":2,"target_lhs":"1","x":["8","8","8","8","1","8","0","8","0","8","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1","target":"0xe8a","target_demand":2,"target_lhs":"1","x":["8","1","8","0","8","8","8","0","8","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0xedb","target_demand":6,"target_lhs":"4","x":["0","2","8","0","2","8","0","0","8","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1","target":"0xf8a","target_demand":3,"target_lhs":"2","x":["8","2","8","0","8","8","8","0","0","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xf8a","other_original_rows_checked":279,"strict_violation":"1","target":"0xf8b","target_demand":4,"target_lhs":"3","x":["0","3","8","0","8","8","8","0","0","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xd50","other_original_rows_checked":279,"strict_violation":"1","target":"0xfd0","target_demand":3,"target_lhs":"2","x":["8","8","8","8","2","8","0","0","0","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"1","target":"0xfd1","target_demand":4,"target_lhs":"3","x":["0","8","8","8","3","8","0","0","0","0","0","0","8","8"]},{"integral_witness":true,"minimum_other_slack":"12","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x1412","target_demand":2,"target_lhs":"0","x":["8","0","8","8","0","8","8","8","8","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"12","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x1448","target_demand":2,"target_lhs":"0","x":["8","8","8","0","8","8","0","8","8","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x145f","target_demand":6,"target_lhs":"4","x":["0","2","0","2","0","8","0","8","8","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"2","target":"0x1513","target_demand":4,"target_lhs":"2","x":["0","2","8","8","0","8","8","8","0","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"2","target":"0x1516","target_demand":4,"target_lhs":"2","x":["8","2","0","8","0","8","8","8","0","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"2","target":"0x1549","target_demand":4,"target_lhs":"2","x":["0","8","8","2","8","8","0","8","0","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"2","target":"0x154c","target_demand":4,"target_lhs":"2","x":["8","8","0","2","8","8","0","8","0","8","0","8","0","8"]},{"integral_witness":true,"minimum_other_slack":"12","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x1818","target_demand":2,"target_lhs":"0","x":["8","8","8","0","0","8","8","8","8","8","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"6","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1","target":"0x1842","target_demand":1,"target_lhs":"0","x":["8","0","8","8","8","8","0","8","8","8","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x1942","target_demand":2,"target_lhs":"1","x":["8","1","8","8","8","8","0","8","0","8","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1","target":"0x1a98","target_demand":3,"target_lhs":"2","x":["8","8","8","2","0","8","8","0","8","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1a98","other_original_rows_checked":279,"strict_violation":"1","target":"0x1a9c","target_demand":4,"target_lhs":"3","x":["8","8","0","3","0","8","8","0","8","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x1ac2","target_demand":2,"target_lhs":"1","x":["8","1","8","8","8","8","0","0","8","0","8","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1ada","target_demand":5,"target_lhs":"9/2","x":["8","3/2","8","5/2","0","8","0","1/2","8","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x1ade","target_demand":6,"target_lhs":"5","x":["8","1","0","3","0","8","0","1","8","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1","target":"0x1bc2","target_demand":3,"target_lhs":"2","x":["8","2","8","8","8","8","0","0","0","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1bc2","other_original_rows_checked":279,"strict_violation":"1","target":"0x1bc6","target_demand":4,"target_lhs":"3","x":["8","3","0","8","8","8","0","0","0","0","8","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1","target":"0x1c52","target_demand":3,"target_lhs":"2","x":["8","1","8","8","1","8","0","8","8","8","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1","target":"0x1c59","target_demand":4,"target_lhs":"3","x":["0","8","8","1","1","8","1","8","8","8","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"3/2","target":"0x1c5c","target_demand":4,"target_lhs":"5/2","x":["8","8","0","3/2","1/2","8","1/2","8","8","8","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1c9b","target_demand":3,"target_lhs":"5/2","x":["0","1/2","8","1/2","3/2","8","8","0","8","8","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1c9e","target_demand":3,"target_lhs":"5/2","x":["8","1/2","0","1/2","3/2","8","8","0","8","8","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1e1b","target_demand":3,"target_lhs":"5/2","x":["0","1/2","8","1/2","3/2","8","8","8","8","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1e1e","target_demand":3,"target_lhs":"5/2","x":["8","1/2","0","1/2","3/2","8","8","8","8","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1e9b","target_demand":4,"target_lhs":"7/2","x":["0","1/2","8","3/2","3/2","8","8","0","8","0","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x1edf","target_demand":7,"target_lhs":"6","x":["0","0","0","2","2","8","2","0","8","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1f9b","target_demand":6,"target_lhs":"11/2","x":["0","5/2","8","3/2","3/2","8","8","0","0","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1f9e","target_demand":6,"target_lhs":"11/2","x":["8","3/2","0","3/2","5/2","8","8","0","0","0","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x1fcb","target_demand":6,"target_lhs":"5","x":["0","1","8","1","8","8","1","0","2","0","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x1fce","target_demand":6,"target_lhs":"5","x":["8","1","0","1","8","8","2","0","1","0","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"1","target":"0x1fd3","target_demand":6,"target_lhs":"5","x":["0","1","8","8","2","8","1","0","1","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"4/3","target":"0x1fd6","target_demand":6,"target_lhs":"14/3","x":["8","5/3","0","8","2/3","8","2/3","0","5/3","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1fd9","target_demand":6,"target_lhs":"11/2","x":["0","8","8","3/2","3/2","8","5/2","0","0","0","0","0","0","8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x1fdc","target_demand":6,"target_lhs":"11/2","x":["8","8","0","5/2","3/2","8","3/2","0","0","0","0","0","0","8"]},{"integral_witness":true,"minimum_other_slack":"5","minimum_slack_row":"0x2518","other_original_rows_checked":279,"strict_violation":"2","target":"0x2418","target_demand":2,"target_lhs":"0","x":["8","8","8","0","0","8","8","8","8","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"5","minimum_slack_row":"0x2462","other_original_rows_checked":279,"strict_violation":"2","target":"0x2442","target_demand":2,"target_lhs":"0","x":["8","0","8","8","8","8","0","8","8","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x2462","target_demand":3,"target_lhs":"2","x":["8","2","8","8","8","0","0","8","8","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2462","other_original_rows_checked":279,"strict_violation":"1","target":"0x2463","target_demand":4,"target_lhs":"3","x":["0","3","8","8","8","0","0","8","8","8","0","8","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x247a","target_demand":5,"target_lhs":"9/2","x":["8","5/2","8","3/2","0","0","0","8","8","8","1/2","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x247b","target_demand":6,"target_lhs":"5","x":["0","3","8","1","0","0","0","8","8","8","1","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2418","other_original_rows_checked":279,"strict_violation":"1","target":"0x2518","target_demand":3,"target_lhs":"2","x":["8","8","8","2","0","8","8","8","0","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2518","other_original_rows_checked":279,"strict_violation":"1","target":"0x2519","target_demand":4,"target_lhs":"3","x":["0","8","8","3","0","8","8","8","0","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x2542","target_demand":3,"target_lhs":"2","x":["8","2","8","8","8","8","0","8","0","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2542","other_original_rows_checked":279,"strict_violation":"1","target":"0x2543","target_demand":4,"target_lhs":"3","x":["0","3","8","8","8","8","0","8","0","8","0","8","8","0"]},{"integral_witness":true,"minimum_other_slack":"5","minimum_slack_row":"0x2912","other_original_rows_checked":279,"strict_violation":"2","target":"0x2812","target_demand":2,"target_lhs":"0","x":["8","0","8","8","0","8","8","8","8","8","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"12","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x2848","target_demand":2,"target_lhs":"0","x":["8","8","8","0","8","8","0","8","8","8","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2812","other_original_rows_checked":279,"strict_violation":"1","target":"0x2912","target_demand":3,"target_lhs":"2","x":["8","2","8","8","0","8","8","8","0","8","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2912","other_original_rows_checked":279,"strict_violation":"1","target":"0x2932","target_demand":4,"target_lhs":"3","x":["8","3","8","8","0","0","8","8","0","8","8","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x295a","target_demand":5,"target_lhs":"9/2","x":["8","5/2","8","3/2","0","8","0","8","0","8","8","1/2","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x297a","target_demand":6,"target_lhs":"5","x":["8","3","8","1","0","0","0","8","0","8","8","1","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2ada","target_demand":5,"target_lhs":"4","x":["8","2","8","2","0","8","0","0","8","0","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2848","other_original_rows_checked":279,"strict_violation":"1","target":"0x2afa","target_demand":6,"target_lhs":"5","x":["8","3","8","2","0","0","0","0","8","0","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2848","other_original_rows_checked":279,"strict_violation":"1","target":"0x2bc8","target_demand":3,"target_lhs":"2","x":["8","8","8","2","8","8","0","0","0","0","8","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2bc8","other_original_rows_checked":279,"strict_violation":"1","target":"0x2be8","target_demand":4,"target_lhs":"3","x":["8","8","8","3","8","0","0","0","0","0","8","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2c1b","target_demand":3,"target_lhs":"5/2","x":["0","1/2","8","1/2","3/2","8","8","8","8","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2c3a","target_demand":3,"target_lhs":"5/2","x":["8","1/2","8","1/2","3/2","0","8","8","8","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2c4a","target_demand":3,"target_lhs":"5/2","x":["8","1/2","8","1/2","8","8","3/2","8","8","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2c52","target_demand":3,"target_lhs":"5/2","x":["8","3/2","8","8","1/2","8","1/2","8","8","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2c58","target_demand":3,"target_lhs":"5/2","x":["8","8","8","3/2","1/2","8","1/2","8","8","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2d1a","target_demand":4,"target_lhs":"7/2","x":["8","1/2","8","1/2","3/2","8","8","8","1","8","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2d3a","target_demand":5,"target_lhs":"4","x":["8","1","8","0","2","0","8","8","1","8","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2d3b","target_demand":6,"target_lhs":"5","x":["0","1","8","1","3","0","8","8","0","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd50","other_original_rows_checked":279,"strict_violation":"1/3","target":"0x2d52","target_demand":4,"target_lhs":"11/3","x":["8","5/3","8","8","2/3","8","2/3","8","2/3","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2d72","target_demand":5,"target_lhs":"9/2","x":["8","5/2","8","8","3/2","0","1/2","8","0","8","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1","target":"0x2d73","target_demand":6,"target_lhs":"5","x":["0","3","8","8","1","0","1","8","0","8","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2d7b","target_demand":7,"target_lhs":"6","x":["0","2","8","0","2","0","0","8","0","8","0","0","8","2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2dca","target_demand":4,"target_lhs":"7/2","x":["8","3/2","8","1/2","8","8","3/2","0","0","8","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2dd8","target_demand":4,"target_lhs":"7/2","x":["8","8","8","3/2","3/2","8","1/2","0","0","8","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2eca","target_demand":4,"target_lhs":"3","x":["8","1","8","1","8","8","1","0","8","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1","target":"0x2ed3","target_demand":4,"target_lhs":"3","x":["0","1","8","8","1","8","1","0","8","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2eea","target_demand":5,"target_lhs":"4","x":["8","1","8","1","8","0","2","0","8","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2eeb","target_demand":6,"target_lhs":"5","x":["0","1","8","1","8","0","3","0","8","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"2","target":"0x2ef3","target_demand":6,"target_lhs":"4","x":["0","2","8","8","0","0","2","0","8","0","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2efb","target_demand":7,"target_lhs":"13/2","x":["0","7/2","8","1/2","1/2","0","1","0","8","0","1/2","0","8","1/2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2f4a","target_demand":4,"target_lhs":"7/2","x":["8","3/2","8","1/2","8","8","3/2","8","0","0","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x2f58","target_demand":4,"target_lhs":"7/2","x":["8","8","8","3/2","3/2","8","1/2","8","0","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x2f9b","target_demand":6,"target_lhs":"5","x":["0","1","8","1","1","8","8","0","2","0","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8a","other_original_rows_checked":279,"strict_violation":"2/3","target":"0x2fca","target_demand":5,"target_lhs":"13/3","x":["8","4/3","8","4/3","8","8","4/3","0","1/3","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"1","target":"0x2fcb","target_demand":6,"target_lhs":"5","x":["0","2","8","1","8","8","1","0","1","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"1","target":"0x2fd2","target_demand":5,"target_lhs":"4","x":["8","1","8","8","1","8","1","0","1","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"1","target":"0x2fd3","target_demand":6,"target_lhs":"5","x":["0","1","8","8","1","8","2","0","1","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"1","target":"0x2fd8","target_demand":5,"target_lhs":"4","x":["8","8","8","1","1","8","1","0","1","0","0","0","8","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"1","target":"0x2fd9","target_demand":6,"target_lhs":"5","x":["0","8","8","1","2","8","1","0","1","0","0","0","8","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/6","target":"0x2fda","target_demand":6,"target_lhs":"35/6","x":["8","5/6","8","5/6","5/6","8","3/2","1/3","5/6","0","0","1/6","8","1/2"]},{"integral_witness":true,"minimum_other_slack":"5","minimum_slack_row":"0x310a","other_original_rows_checked":279,"strict_violation":"1","target":"0x300a","target_demand":1,"target_lhs":"0","x":["8","0","8","0","8","8","8","8","8","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x300a","other_original_rows_checked":279,"strict_violation":"1","target":"0x302a","target_demand":2,"target_lhs":"1","x":["8","1","8","0","8","0","8","8","8","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"5","minimum_slack_row":"0x3150","other_original_rows_checked":279,"strict_violation":"1","target":"0x3050","target_demand":1,"target_lhs":"0","x":["8","8","8","8","0","8","0","8","8","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3050","other_original_rows_checked":279,"strict_violation":"1","target":"0x3070","target_demand":2,"target_lhs":"1","x":["8","8","8","8","1","0","0","8","8","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"2","target":"0x307e","target_demand":6,"target_lhs":"4","x":["8","2","0","0","2","0","0","8","8","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x300a","other_original_rows_checked":279,"strict_violation":"2","target":"0x310a","target_demand":3,"target_lhs":"1","x":["8","1","8","0","8","8","8","8","0","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x310a","other_original_rows_checked":279,"strict_violation":"1","target":"0x312e","target_demand":4,"target_lhs":"3","x":["8","3","0","0","8","0","8","8","0","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3050","other_original_rows_checked":279,"strict_violation":"2","target":"0x3150","target_demand":3,"target_lhs":"1","x":["8","8","8","8","1","8","0","8","0","8","8","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3150","other_original_rows_checked":279,"strict_violation":"1","target":"0x3174","target_demand":4,"target_lhs":"3","x":["8","8","0","8","3","0","0","8","0","8","8","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x341b","target_demand":3,"target_lhs":"5/2","x":["0","1/2","8","1/2","3/2","8","8","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x341e","target_demand":3,"target_lhs":"5/2","x":["8","1/2","0","1/2","3/2","8","8","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x344a","target_demand":3,"target_lhs":"5/2","x":["8","1/2","8","1/2","8","8","3/2","8","8","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x344b","target_demand":4,"target_lhs":"3","x":["0","0","8","1","8","8","2","8","8","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x344e","target_demand":4,"target_lhs":"3","x":["8","0","0","1","8","8","2","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3452","target_demand":3,"target_lhs":"5/2","x":["8","3/2","8","8","1/2","8","1/2","8","8","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x3453","target_demand":4,"target_lhs":"3","x":["0","2","8","8","1","8","0","8","8","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2442","other_original_rows_checked":279,"strict_violation":"1","target":"0x3456","target_demand":4,"target_lhs":"3","x":["8","2","0","8","1","8","0","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3459","target_demand":3,"target_lhs":"5/2","x":["0","8","8","3/2","1/2","8","1/2","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/3","target":"0x345b","target_demand":5,"target_lhs":"14/3","x":["0","5/3","8","2/3","2/3","8","1","8","8","8","2/3","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x345c","target_demand":3,"target_lhs":"5/2","x":["8","8","0","3/2","1/2","8","1/2","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1/3","target":"0x345e","target_demand":5,"target_lhs":"14/3","x":["8","5/3","0","2/3","2/3","8","1","8","8","8","2/3","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"2","target":"0x346f","target_demand":6,"target_lhs":"4","x":["0","2","0","0","8","0","2","8","8","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"2","target":"0x3477","target_demand":6,"target_lhs":"4","x":["0","2","0","8","0","0","2","8","8","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x347f","target_demand":7,"target_lhs":"13/2","x":["0","7/2","0","1/2","1/2","0","1","8","8","8","1/2","8","0","1/2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"4/3","target":"0x351f","target_demand":6,"target_lhs":"14/3","x":["0","2/3","0","2/3","5/3","8","8","8","5/3","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"1","target":"0x353b","target_demand":6,"target_lhs":"5","x":["0","1","8","1","2","0","8","8","1","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1516","other_original_rows_checked":279,"strict_violation":"1","target":"0x353e","target_demand":6,"target_lhs":"5","x":["8","2","0","1","1","0","8","8","1","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1549","other_original_rows_checked":279,"strict_violation":"1","target":"0x354f","target_demand":6,"target_lhs":"5","x":["0","1","0","1","8","8","2","8","1","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"1","target":"0x3557","target_demand":6,"target_lhs":"5","x":["0","2","0","8","1","8","1","8","1","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1549","other_original_rows_checked":279,"strict_violation":"4/3","target":"0x355d","target_demand":6,"target_lhs":"14/3","x":["0","8","0","5/3","2/3","8","2/3","8","5/3","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1549","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x356b","target_demand":6,"target_lhs":"11/2","x":["0","3/2","8","3/2","8","0","5/2","8","0","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x154c","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x356e","target_demand":6,"target_lhs":"11/2","x":["8","3/2","0","5/2","8","0","3/2","8","0","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3573","target_demand":6,"target_lhs":"11/2","x":["0","5/2","8","8","3/2","0","3/2","8","0","8","0","8","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1516","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3576","target_demand":6,"target_lhs":"11/2","x":["8","3/2","0","8","5/2","0","3/2","8","0","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1549","other_original_rows_checked":279,"strict_violation":"1","target":"0x3579","target_demand":6,"target_lhs":"5","x":["0","8","8","2","1","0","1","8","1","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x154c","other_original_rows_checked":279,"strict_violation":"1","target":"0x357c","target_demand":6,"target_lhs":"5","x":["8","8","0","1","1","0","2","8","1","8","0","8","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1","target":"0x383a","target_demand":4,"target_lhs":"3","x":["8","1","8","1","1","0","8","8","8","8","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x3852","target_demand":3,"target_lhs":"2","x":["8","1","8","8","1","8","0","8","8","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3858","target_demand":3,"target_lhs":"5/2","x":["8","8","8","3/2","1/2","8","1/2","8","8","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x386a","target_demand":3,"target_lhs":"5/2","x":["8","1/2","8","3/2","8","0","1/2","8","8","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x393a","target_demand":5,"target_lhs":"9/2","x":["8","5/2","8","1/2","3/2","0","8","8","0","8","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1","target":"0x393e","target_demand":6,"target_lhs":"5","x":["8","3","0","1","1","0","8","8","0","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"4/3","target":"0x3952","target_demand":5,"target_lhs":"11/3","x":["8","2/3","8","8","5/3","8","2/3","8","2/3","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x395a","target_demand":6,"target_lhs":"21/4","x":["8","7/4","8","1/4","5/4","8","3/4","8","0","8","8","1/4","1/4","3/4"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x2812","other_original_rows_checked":279,"strict_violation":"1","target":"0x3976","target_demand":6,"target_lhs":"5","x":["8","1","0","8","1","0","1","8","2","8","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x5a","other_original_rows_checked":279,"strict_violation":"1","target":"0x397e","target_demand":7,"target_lhs":"6","x":["8","2","0","0","2","0","0","8","0","8","8","0","0","2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x39ce","target_demand":4,"target_lhs":"7/2","x":["8","3/2","0","3/2","8","8","1/2","0","0","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x39d8","target_demand":4,"target_lhs":"7/2","x":["8","8","8","1/2","3/2","8","3/2","0","0","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x39ea","target_demand":4,"target_lhs":"7/2","x":["8","3/2","8","3/2","8","0","1/2","0","0","8","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3aca","target_demand":3,"target_lhs":"5/2","x":["8","1/2","8","1/2","8","8","3/2","0","8","0","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1a98","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ada","target_demand":6,"target_lhs":"5","x":["8","2","8","2","1","8","0","0","8","0","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1a98","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3af8","target_demand":4,"target_lhs":"7/2","x":["8","8","8","3/2","3/2","0","1/2","0","8","0","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1a9c","other_original_rows_checked":279,"strict_violation":"1","target":"0x3afe","target_demand":7,"target_lhs":"6","x":["8","1","0","1","3","0","1","0","8","0","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3b4e","target_demand":4,"target_lhs":"7/2","x":["8","3/2","0","3/2","8","8","1/2","8","0","0","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3b58","target_demand":4,"target_lhs":"7/2","x":["8","8","8","1/2","3/2","8","3/2","8","0","0","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3b6a","target_demand":4,"target_lhs":"7/2","x":["8","3/2","8","3/2","8","0","1/2","8","0","0","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1","target":"0x3bca","target_demand":5,"target_lhs":"4","x":["8","1","8","1","8","8","1","0","1","0","8","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1a98","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3bd8","target_demand":5,"target_lhs":"9/2","x":["8","8","8","3/2","3/2","8","3/2","0","0","0","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1","target":"0x3bee","target_demand":6,"target_lhs":"5","x":["8","1","0","1","8","0","1","0","2","0","8","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"6","minimum_slack_row":"0x3c21","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c01","target_demand":1,"target_lhs":"0","x":["0","8","8","8","8","8","8","8","8","8","0","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"6","minimum_slack_row":"0x3c24","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c04","target_demand":1,"target_lhs":"0","x":["8","8","0","8","8","8","8","8","8","8","0","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c0b","target_demand":2,"target_lhs":"3/2","x":["0","1/2","8","0","8","8","8","8","8","8","1/2","0","1/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c0e","target_demand":2,"target_lhs":"3/2","x":["8","1/2","0","0","8","8","8","8","8","8","1/2","0","1/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c13","target_demand":3,"target_lhs":"5/2","x":["0","3/2","8","8","0","8","8","8","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c16","target_demand":3,"target_lhs":"5/2","x":["8","3/2","0","8","0","8","8","8","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x3c1f","target_demand":4,"target_lhs":"13/4","x":["0","3/4","0","1/4","5/4","8","8","8","8","8","1/2","1/4","1/4","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3c01","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c21","target_demand":2,"target_lhs":"1","x":["1","8","8","8","8","0","8","8","8","8","0","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3c04","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c24","target_demand":2,"target_lhs":"1","x":["8","8","1","8","8","0","8","8","8","8","0","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c33","target_demand":4,"target_lhs":"3","x":["0","1","8","8","0","0","8","8","8","8","1","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c36","target_demand":4,"target_lhs":"3","x":["8","1","0","8","0","0","8","8","8","8","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c49","target_demand":3,"target_lhs":"5/2","x":["0","8","8","3/2","8","8","0","8","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c4c","target_demand":3,"target_lhs":"5/2","x":["8","8","0","3/2","8","8","0","8","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c54","target_demand":2,"target_lhs":"3/2","x":["8","8","0","8","1/2","8","0","8","8","8","1/2","0","1/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c69","target_demand":4,"target_lhs":"3","x":["0","8","8","1","8","0","0","8","8","8","1","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1","target":"0x3c6c","target_demand":4,"target_lhs":"3","x":["8","8","0","1","8","0","0","8","8","8","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c99","target_demand":3,"target_lhs":"5/2","x":["0","8","8","3/2","0","8","8","0","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3c9c","target_demand":3,"target_lhs":"5/2","x":["8","8","0","3/2","0","8","8","0","8","8","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3caf","target_demand":3,"target_lhs":"5/2","x":["0","1/2","0","0","8","0","8","0","8","8","1/2","0","3/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x3cc3","target_demand":3,"target_lhs":"2","x":["0","1","8","8","8","8","0","0","8","8","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x3cc6","target_demand":3,"target_lhs":"2","x":["8","1","0","8","8","8","0","0","8","8","1","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"2/9","target":"0x3d1b","target_demand":5,"target_lhs":"43/9","x":["0","4/9","8","1/3","4/3","8","8","8","13/9","8","4/9","0","1/3","4/9"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1516","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3d1e","target_demand":5,"target_lhs":"9/2","x":["8","1","0","1/2","1","8","8","8","1","8","1/2","0","1/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d37","target_demand":6,"target_lhs":"5","x":["0","3","0","8","0","0","8","8","0","8","1","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d3f","target_demand":7,"target_lhs":"6","x":["0","1","0","0","2","0","8","8","1","8","0","0","0","2"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d48","target_demand":3,"target_lhs":"2","x":["8","8","8","2","8","8","0","8","0","8","0","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3d48","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d68","target_demand":4,"target_lhs":"3","x":["8","8","8","3","8","0","0","8","0","8","0","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d77","target_demand":7,"target_lhs":"6","x":["0","2","0","8","2","0","0","8","0","8","0","0","0","2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x145f","other_original_rows_checked":279,"strict_violation":"1/5","target":"0x3d7f","target_demand":8,"target_lhs":"39/5","x":["0","9/5","0","4/5","1","0","4/5","8","4/5","8","4/5","0","4/5","1"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1","target":"0x3d8f","target_demand":4,"target_lhs":"3","x":["0","2","0","0","8","8","8","0","0","8","0","0","1","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3dab","target_demand":4,"target_lhs":"7/2","x":["0","3/2","8","0","8","0","8","0","0","8","1/2","0","3/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3dbc","target_demand":4,"target_lhs":"7/2","x":["8","8","0","3/2","0","0","8","0","0","8","3/2","1/2","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1","target":"0x3dc6","target_demand":4,"target_lhs":"3","x":["8","2","0","8","8","8","0","0","0","8","1","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x154c","other_original_rows_checked":279,"strict_violation":"1/4","target":"0x3dce","target_demand":5,"target_lhs":"19/4","x":["8","3/4","0","3/4","8","8","3/2","0","3/4","8","1/4","0","3/4","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"2/3","target":"0x3dea","target_demand":5,"target_lhs":"13/3","x":["8","1/3","8","2/3","8","0","1","0","2/3","8","1/3","0","0","4/3"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3df1","target_demand":4,"target_lhs":"7/2","x":["0","8","8","8","3/2","0","0","0","0","8","1/2","0","3/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"2/3","target":"0x3df8","target_demand":5,"target_lhs":"13/3","x":["8","8","8","4/3","1/3","0","1","0","1","8","0","0","1/3","1/3"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3e19","target_demand":3,"target_lhs":"5/2","x":["0","8","8","3/2","0","8","8","8","8","0","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3e1c","target_demand":3,"target_lhs":"5/2","x":["8","8","0","3/2","0","8","8","8","8","0","1/2","1/2","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3e2f","target_demand":3,"target_lhs":"5/2","x":["0","1/2","0","0","8","0","8","8","8","0","1/2","0","3/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x3e43","target_demand":3,"target_lhs":"2","x":["0","1","8","8","8","8","0","8","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1842","other_original_rows_checked":279,"strict_violation":"1","target":"0x3e46","target_demand":3,"target_lhs":"2","x":["8","1","0","8","8","8","0","8","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3c01","other_original_rows_checked":279,"strict_violation":"1","target":"0x3e85","target_demand":2,"target_lhs":"1","x":["0","8","0","8","8","8","8","0","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x3c21","other_original_rows_checked":279,"strict_violation":"2","target":"0x3ea5","target_demand":4,"target_lhs":"2","x":["0","8","0","8","8","0","8","0","8","0","2","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ec7","target_demand":4,"target_lhs":"3","x":["0","1","0","8","8","8","0","0","8","0","1","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ecb","target_demand":5,"target_lhs":"4","x":["0","0","8","1","8","8","2","0","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ece","target_demand":5,"target_lhs":"4","x":["8","0","0","1","8","8","2","0","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ed3","target_demand":5,"target_lhs":"4","x":["0","1","8","8","1","8","1","0","8","0","1","0","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ed6","target_demand":5,"target_lhs":"4","x":["8","1","0","8","0","8","0","0","8","0","1","0","1","1"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3ee6","target_demand":4,"target_lhs":"7/2","x":["8","3/2","0","8","8","0","0","0","8","0","3/2","1/2","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1ac2","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ee7","target_demand":6,"target_lhs":"5","x":["0","1","0","8","8","0","0","0","8","0","3","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1448","other_original_rows_checked":279,"strict_violation":"1","target":"0x3eef","target_demand":7,"target_lhs":"6","x":["0","2","0","0","8","0","0","0","8","0","2","0","0","2"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc50","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3ef4","target_demand":3,"target_lhs":"5/2","x":["8","8","0","8","1/2","0","0","0","8","0","1/2","0","3/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1412","other_original_rows_checked":279,"strict_violation":"1","target":"0x3ef7","target_demand":7,"target_lhs":"6","x":["0","0","0","8","0","0","2","0","8","0","2","0","0","2"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1","target":"0x3f0f","target_demand":4,"target_lhs":"3","x":["0","2","0","0","8","8","8","8","0","0","0","0","1","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3f2b","target_demand":4,"target_lhs":"7/2","x":["0","3/2","8","0","8","0","8","8","0","0","1/2","0","3/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3f3c","target_demand":4,"target_lhs":"7/2","x":["8","8","0","3/2","0","0","8","8","0","0","3/2","1/2","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1942","other_original_rows_checked":279,"strict_violation":"1","target":"0x3f46","target_demand":4,"target_lhs":"3","x":["8","2","0","8","8","8","0","8","0","0","1","0","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x154c","other_original_rows_checked":279,"strict_violation":"1/4","target":"0x3f4e","target_demand":5,"target_lhs":"19/4","x":["8","3/4","0","3/4","8","8","3/2","8","3/4","0","1/4","0","3/4","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xd0a","other_original_rows_checked":279,"strict_violation":"2/3","target":"0x3f6a","target_demand":5,"target_lhs":"13/3","x":["8","1/3","8","2/3","8","0","1","8","2/3","0","1/3","0","0","4/3"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xc51","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3f71","target_demand":4,"target_lhs":"7/2","x":["0","8","8","8","3/2","0","0","8","0","0","1/2","0","3/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0x1818","other_original_rows_checked":279,"strict_violation":"2/3","target":"0x3f78","target_demand":5,"target_lhs":"13/3","x":["8","8","8","4/3","1/3","0","1","8","1","0","0","0","1/3","1/3"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8a","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3f8e","target_demand":4,"target_lhs":"7/2","x":["8","5/2","0","0","8","8","8","0","0","0","1/2","0","1/2","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1a9c","other_original_rows_checked":279,"strict_violation":"1","target":"0x3f9d","target_demand":6,"target_lhs":"5","x":["0","8","0","3","0","8","8","0","0","0","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x3f9f","target_demand":7,"target_lhs":"25/4","x":["0","1/4","0","7/4","7/4","8","8","0","1/2","0","5/4","1/4","1/4","1/4"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1513","other_original_rows_checked":279,"strict_violation":"1","target":"0x3fb3","target_demand":6,"target_lhs":"5","x":["1","3","8","8","0","0","8","0","0","0","0","1","0","0"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1516","other_original_rows_checked":279,"strict_violation":"1","target":"0x3fb6","target_demand":6,"target_lhs":"5","x":["8","3","1","8","0","0","8","0","0","0","0","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"5/8","target":"0x3fbb","target_demand":7,"target_lhs":"51/8","x":["0","13/8","8","3/8","15/8","0","8","0","1/2","0","9/8","3/8","3/8","1/8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xe8a","other_original_rows_checked":279,"strict_violation":"5/8","target":"0x3fbe","target_demand":7,"target_lhs":"51/8","x":["8","9/8","0","3/8","15/8","0","8","0","1","0","1/8","3/8","11/8","1/8"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1bc6","other_original_rows_checked":279,"strict_violation":"1","target":"0x3fc7","target_demand":6,"target_lhs":"5","x":["0","3","0","8","8","8","0","0","0","0","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x3fcf","target_demand":7,"target_lhs":"25/4","x":["0","1","0","1/4","8","8","7/4","0","5/4","0","5/4","1/4","1/4","1/4"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"1/2","target":"0x3fd4","target_demand":4,"target_lhs":"7/2","x":["8","8","0","8","5/2","8","0","0","0","0","1/2","0","1/2","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x3fd7","target_demand":7,"target_lhs":"25/4","x":["0","7/4","0","8","1/4","8","1","0","5/4","0","5/4","1/4","1/4","1/4"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"3/4","target":"0x3fdd","target_demand":7,"target_lhs":"25/4","x":["0","8","0","7/4","7/4","8","1/4","0","1/2","0","5/4","1/4","1/4","1/4"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x1549","other_original_rows_checked":279,"strict_violation":"1","target":"0x3fe9","target_demand":6,"target_lhs":"5","x":["0","8","8","3","8","0","0","0","0","0","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8b","other_original_rows_checked":279,"strict_violation":"7/12","target":"0x3feb","target_demand":7,"target_lhs":"77/12","x":["0","5/12","8","7/4","8","0","23/12","0","1/3","0","5/4","1/4","1/12","5/12"]},{"integral_witness":true,"minimum_other_slack":"0","minimum_slack_row":"0x154c","other_original_rows_checked":279,"strict_violation":"1","target":"0x3fec","target_demand":6,"target_lhs":"5","x":["8","8","0","3","8","0","0","0","0","0","1","1","0","0"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xf8a","other_original_rows_checked":279,"strict_violation":"7/12","target":"0x3fee","target_demand":7,"target_lhs":"77/12","x":["8","5/12","0","7/4","8","0","23/12","0","1/3","0","1/4","1/4","13/12","5/12"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"7/12","target":"0x3ff3","target_demand":7,"target_lhs":"77/12","x":["0","23/12","8","8","7/4","0","5/12","0","1/3","0","5/4","1/4","1/12","5/12"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"5/8","target":"0x3ff6","target_demand":7,"target_lhs":"51/8","x":["8","15/8","0","8","3/4","0","3/8","0","11/8","0","3/8","1/8","9/8","3/8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd1","other_original_rows_checked":279,"strict_violation":"5/8","target":"0x3ff9","target_demand":7,"target_lhs":"51/8","x":["0","8","8","15/8","3/8","0","13/8","0","1/2","0","9/8","3/8","3/8","1/8"]},{"integral_witness":false,"minimum_other_slack":"0","minimum_slack_row":"0xfd0","other_original_rows_checked":279,"strict_violation":"5/8","target":"0x3ffc","target_demand":7,"target_lhs":"51/8","x":["8","8","0","15/8","3/8","0","13/8","0","1/2","0","1/8","3/8","11/8","1/8"]}]},"dimension":14,"limits":["Fixed 14-rectangle nonnegative-real demand system from exact source6425 RESULT only.","Each deletion uses retained source rows only; every retained separator satisfies all other279 original rows.","Fractional separators prove real nonimplication; integral_witness labels an inspected stronger witness, not physical decoder admission.","Source clique census/witness validity and geometry-to-demand equivalence remain credited predecessor results, not rerun here.","No claim of fewest arbitrary inequalities, coefficient synthesis, COPY floor, native realization, kappa or frontier change."],"method":"Independent direct exact-rational checking of sealed primary certificate data; no solver, primary import, clique census or predecessor execution","negative_controls":{"coefficient_overrun":"coefficient exceeds target","duplicate_key":"duplicate JSON key","exponent_rational":"rational integer/quotient grammar","missing_witness":"separator count","negative_coordinate":"nonnegative separator coordinates","negative_multiplier":"nonnegative multiplier","noncanonical_rational":"canonical rational string","nonfinite_json":"nonfinite JSON value: NaN","nonviolating_witness":"separator must strictly violate target","other_row_violation":"separator violates another original inequality","overflowing_json_number":"nonfinite JSON number","self_premise":"retained unique donor; no self or cyclic premise","source_byte_mutation":"source SHA256: RESULT-6425.json","zero_rhs":"right-hand side below target demand"},"primary_certificate_sha256":"b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704","removed_rows":43,"retained_rows":237,"schema_version":1,"source_manifest_sha256":"d9d9e3785d6496adf112ccafbe25689057e9a1f28384ca28a536660c9f55f6e9","source_result_sha256":"f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89","source_rows":280,"status":"PASS_INDEPENDENT_EXACT_FARKAS_CERTIFICATE_CHECK"} diff --git a/research/p112-farkas-kernel/PROOF.md b/research/p112-farkas-kernel/PROOF.md new file mode 100644 index 0000000000..b649f002d8 --- /dev/null +++ b/research/p112-farkas-kernel/PROOF.md @@ -0,0 +1,105 @@ +# Exact implications in the fixed P112 demand system + +This is a finite, source-bound inequality result, quantified over all nonnegative +real multiplicity vectors. No predecessor executable or clique census is replayed. +The source matrix is the literal 280-row kernel in Nick Petalas's PR6425 at +`092dcbd13d1263e691ad29f34fbf286fea1fac2c`, authenticated by `SOURCE-PINS.json`. +Its 14 ordered cap rectangles, source clique witnesses and earlier completeness +claims retain their original meaning and attribution. + +## Matrix and domain + +For each saved pair `(H_i,d_i)`, let `a_i` be the 14-dimensional 0/1 indicator of +hit mask `H_i`. The row is `a_i x >= d_i`, with the common baseline `x >= 0`. +The source rows have distinct nonempty 14-bit masks and positive integer demands +at most 8. These conditions are checked, not inferred from a row count. + +PR6425's [proof](https://github.com/petalas/integer-mult-bounds/blob/092dcbd13d1263e691ad29f34fbf286fea1fac2c/research/p112-demand-kernel/PROOF.md) +defines the hit predicate and proves equivalence of this kernel to its full +262,928-clique demand screen. That earlier theorem is a credited premise when +composing the present result with the full geometry. The present standalone +certificate establishes equivalence of the literal 280-row matrix and its new +retained subfamily; it does not independently certify the source clique census, +the witnesses' geometric validity, decoder coefficients or physical admission. + +## Checkable deletion implication + +For each omitted row `t`, the certificate supplies nonnegative rational weights +`lambda_j`, with every donor `j` in the **final retained family** `R`. The exact +checks are + + sum_j lambda_j a_j <= a_t (coordinatewise), + sum_j lambda_j d_j >= d_t. + +For any nonnegative `x` satisfying the retained rows, + + a_t x >= (sum_j lambda_j a_j) x + >= sum_j lambda_j d_j >= d_t. + +Thus the retained system implies every omitted row. Conversely a solution of +all original rows satisfies their retained subfamily. This proves equivalence +for all nonnegative real vectors, including unbounded integer vectors. No LP +solver status or floating tolerance enters this acceptance argument. + +## Generation and simultaneous deletion + +A positive donor weight cannot use a row having a 1 outside `H_t`, because the +target coefficient there is zero and all donor coefficients/weights are +nonnegative. Restrict candidate donors to strict subsets of `H_t`. Process +targets by increasing support size, retaining a row whenever it is not certified +implied by the already retained strict subsets. Retained rows are never deleted +later. Consequently every deletion refers directly to rows in final `R`; +simultaneous deletion is justified without circular premises. + +The bounded generator uses exact rational packing simplex: maximize +`sum_j d_j lambda_j`, subject to coefficient capacities at most 1 on `H_t` and +`lambda >= 0`. Zero weights plus slacks form an initial feasible basis. Bland +entering/leaving rules include nonbasic slack columns. A feasible packing reaching +`d_t` already certifies deletion; full optimality is unnecessary for that case. +Explicit bounds reject exhausted work instead of truncating coverage. + +The generator is a discovery mechanism. The elementary coefficient checks above +and the explicit points below independently establish the result even if the +simplex implementation is not trusted. + +## Separating points and the restricted minimum claim + +For every retained row `t`, the certificate supplies a full 14-dimensional +rational vector `x^(t) >= 0` which satisfies **all 279 other original rows** and +strictly violates row `t`. This is checked literally against the original matrix, +not just against `R`, a restricted LP, or an objective value. + +A packing dual optimum below `d_t` can suggest the coordinates on `H_t`. +Setting each coordinate outside `H_t` to 8 covers any source row touching an +outside bit, since every demand is at most 8. Original rows wholly inside `H_t` +are covered by retained rows and their certified implications. This explains a +construction of the points; their literal checks are the acceptance evidence. + +Given the full-original checks, any subfamily `S` of the original 280 rows +equivalent to the full system must contain every `t` in `R`: otherwise `x^(t)` +would satisfy `S` but fail the full system. Since `R` is itself equivalent, it is +the unique minimum-cardinality and unique inclusion-minimal **subfamily of these +original rows**, with the baseline `x >= 0` fixed. This claim is conditional on +every retained point passing the stated full-original checks. + +No minimum over arbitrary new inequalities or alternative representations is +claimed. Fractional separating points do not establish integer-only +indispensability. Changing caps, adding rectangles or trimming actual supports +changes the matrix and requires new certificates. + +## Credit and limits + +Credit Nick Petalas/PR6425 for the fixed matrix, pairwise kernel and explicit +combined-implication handoff; Jeremy Diviney/PR1422 for the complete-clique guard, +source geometry, caps and smaller-family question; Cinna Davis/PR1347/1323 and +the retained E8/label/decoder lineage. Exact LP certificate semantics also have +repository precedent in PR5767; no shared solver or 128-variable cap is changed. +Nonnegative implication, packing/covering duality, simplex and Bland's rule are +classical. No general mathematical priority is asserted for them. + +New work uses substantial OpenAI Codex assistance. A separately implemented +certificate checker is independent code verification of a frozen certificate, +not blind rediscovery or independent human/formal proof-kernel acceptance. +No coefficient synthesis, complete COPY floor, native/physical supplier, +restoration/access/precision/stock/compiler closure, signed invoice, outer +integration, κ improvement or selected-frontier change follows. diff --git a/research/p112-farkas-kernel/README.md b/research/p112-farkas-kernel/README.md new file mode 100644 index 0000000000..27aea79adb --- /dev/null +++ b/research/p112-farkas-kernel/README.md @@ -0,0 +1,99 @@ +# A 237-row exact P112 demand system + +For the fixed 14-variable, 280-row cap-demand matrix of Nick Petalas's +[PR6425](https://github.com/CrocSwap/integer-mult-bounds/pull/6425), exact +nonnegative rational combinations remove 43 rows. The retained 237 rows are +equivalent for every nonnegative real multiplicity vector. Each retained row has +a rational point satisfying all 279 other original rows and strictly violating +that row. Together these certificates establish the **unique minimum subfamily +of the original 280 rows**, with `x >= 0` fixed. + +This answers PR6425's first Open next question. Its pairwise reduction, source +clique census and geometry-to-demand equivalence remain credited predecessor +results; no predecessor executable or census is replayed. The present result is +an exact reduction of the literal source matrix. It supplies no coefficients, +decoder, physical supplier, COPY floor or κ improvement. + +## Concrete implication + +The first deleted mask is `0x1d1a`, demand 3. One half of each of the retained +rows `0x1412`, `0x1818` and `0xd0a`, each demand 2, gives RHS 3. The resulting +coefficient is 1 on target coordinates 1, 3, 4, 10, 11 and 12, and one half on +coordinate 8 (zero-based); all are at most the target's coefficients. The +missing half of coordinate 8 is supplied by `x_8 >= 0`. No single retained row +dominates this target: the source family was already pairwise nondominated. +`RESULT.json` retains all 43 exact combinations and all 237 full separating +points; `PROOF.md` gives the universal implication and restricted minimum proof. + +## Replay + +CPython 3.12 and the standard library suffice. No Git executable, network, solver +package or predecessor executable is needed for the package's two replays. + +```sh +python3.12 -I -W error -B research/p112-farkas-kernel/verify.py +python3.12 -I -W error -B research/p112-farkas-kernel/oracle.py +``` + +Also run with `-O`. Default commands require strict complete retained JSON; +`--emit` prints regenerated output without overwriting files. The primary +regenerates the certificate with bounded exact `Fraction` packing simplex and +checks every implication and separator literally. The separate checker treats +the sealed primary result as untrusted certificate data and computes all +coefficient/RHS budgets and full-original-row separations independently. It does +not import the generator, solve an LP or claim blind rediscovery. + +The generator uses 2,272 pivots, at most 49 per target, on this exact instance. +Explicit time/pivot/coefficient bounds fail closed. These are generation counts, +not a general runtime improvement. `VERIFY.json` registers the two bounded checks. +`SOURCE-PINS.json` authenticates both inert source files before parsing them. +`SOURCES.json` pins the originating current-main card/selected record as +provenance; all runtime bytes are package-local. + +## Scope, evidence and limitations + +The equivalence covers nonnegative real vectors and therefore preserves all +nonnegative integer tests too. Fractional separating points do **not** establish +integer-only indispensability or the smallest integer-only screen. The minimum +claim is over subfamilies of these original inequalities; it does not minimize +arbitrary newly introduced normals or alternative descriptions. + +The independent checker exercises actual coefficient, demand, premise and +separator corruptions, along with source/schema controls. `VALIDATION.md` +records the actual run evidence, corrections and remaining obligations. Passing +this finite necessary-condition screen does not construct coefficient vectors +or pay for access, dirty restoration, precision, tape, stock, compiler or outer +integration. No native, Lean, Docker, selected cold supplier or complete +multiplication replay was run. + +Orientation was frozen at canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, +selected PR6030, selected-record SHA256 +`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`. +The broader `complex-rank-shape-decoder` card is explicitly changed to this fixed +support-screen implication. Main/overlap are rechecked before submission; +sparse/history/hidden/unpublished coverage limits are not novelty evidence. + +## Open next questions + +1. Can integer multiplicity implications remove further rows? Specify the + integer domain and produce integer implication/separation certificates; + fractional witnesses alone do not answer that question. +2. For changed support caps, what is the new exact demand screen? Rebuild the + complete changed quotient before applying or attempting new combinations. +3. Can a passing vector admit actual coefficients and a fully charged decoder? + Specify one vector and its full interface before synthesis and pricing. + +## Credit + +Credit Nick Petalas/PR6425 for the fixed matrix, pairwise reduction and explicit +combined-implication question; Jeremy Diviney/PR1422 for the complete-clique +guard, pinned geometry/caps and smaller-family question; Cinna Davis/PR1347/1323 +and Navinor, David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the +retained E8/label/decoder lineage. PR5767 is related exact-certificate tooling; +its code and 128-variable cap are unchanged. Nonnegative implication, +packing/covering duality, simplex and Bland's rule are classical. + +New work is ToikY with substantial OpenAI Codex assistance. Separate AI +certificate checking is not independent human review or formal proof-kernel +acceptance. `NOTICE` preserves attribution; the two source files remain verbatim. diff --git a/research/p112-farkas-kernel/RESULT.json b/research/p112-farkas-kernel/RESULT.json new file mode 100644 index 0000000000..1ee2f62695 --- /dev/null +++ b/research/p112-farkas-kernel/RESULT.json @@ -0,0 +1 @@ +{"controls":{"actual_combination_coefficient_overflow":{"observed_error":"Farkas coefficient overflow","target":"0x1d1a"},"actual_combination_half_demand":{"mutant_rhs":"3/2","observed_error":"Farkas demand shortfall","target":"0x1d1a"},"actual_separator_made_target_feasible":{"coordinate":1,"observed_error":"separator must strictly violate target","target":"0x5a"},"outside_extension_required":{"restricted_zero_point_error":"separator violates another original row"},"two_row_combination":{"multipliers":[["0x1","1"],["0x2","1"]],"target":"0x3"}},"counts":{"deleted":43,"retained":237,"strict_separators":237},"declared_caps":{"coefficient_bits":4096,"per_target_pivots":2000,"seconds":120,"total_pivots":100000},"deletions":[{"multipliers":[["0x1412","1/2"],["0x1818","1/2"],["0xd0a","1/2"]],"target":"0x1d1a"},{"multipliers":[["0x1448","1/2"],["0xd0a","1/2"],["0x1942","1/2"]],"target":"0x1d4a"},{"multipliers":[["0x1448","1/2"],["0x1818","1/2"],["0xd50","1/2"]],"target":"0x1d58"},{"multipliers":[["0x5a","1/2"],["0x2518","1/2"],["0x2542","1/2"]],"target":"0x255a"},{"multipliers":[["0x5a","1/2"],["0x310a","1/2"],["0x3150","1/2"]],"target":"0x315a"},{"multipliers":[["0x1412","1/2"],["0x2418","1/2"],["0x302a","1/2"]],"target":"0x343a"},{"multipliers":[["0x1448","1/2"],["0x2418","1/2"],["0x3070","1/2"]],"target":"0x3478"},{"multipliers":[["0x1412","1/2"],["0x2518","1/2"],["0x310a","1/2"]],"target":"0x351a"},{"multipliers":[["0x1448","1/2"],["0x2542","1/2"],["0x310a","1/2"]],"target":"0x354a"},{"multipliers":[["0x1412","1/2"],["0x2542","1/2"],["0x3150","1/2"]],"target":"0x3552"},{"multipliers":[["0x1448","1/2"],["0x2518","1/2"],["0x3150","1/2"]],"target":"0x3558"},{"multipliers":[["0x5a","1/2"],["0x1513","1/2"],["0x1549","1/2"]],"target":"0x155b"},{"multipliers":[["0x5a","1/2"],["0x1516","1/2"],["0x154c","1/2"]],"target":"0x155e"},{"multipliers":[["0x1448","1/2"],["0xe8a","1/2"],["0x1ac2","1/2"]],"target":"0x1eca"},{"multipliers":[["0x5a","1/2"],["0x2519","1/2"],["0x2543","1/2"]],"target":"0x255b"},{"multipliers":[["0x5a","1/2"],["0xf8a","1/2"],["0xfd0","1/2"]],"target":"0xfda"},{"multipliers":[["0x1412","1/2"],["0x1a98","1/2"],["0xf8a","1/2"]],"target":"0x1f9a"},{"multipliers":[["0x1448","1/2"],["0xf8a","1/2"],["0x1bc2","1/2"]],"target":"0x1fca"},{"multipliers":[["0x1412","1/2"],["0xfd0","1/2"],["0x1bc2","1/2"]],"target":"0x1fd2"},{"multipliers":[["0x1448","1/2"],["0x1a98","1/2"],["0xfd0","1/2"]],"target":"0x1fd8"},{"multipliers":[["0x1818","1/2"],["0x2912","1/2"],["0x310a","1/2"]],"target":"0x399e"},{"multipliers":[["0x1818","1/2"],["0x2912","1/2"],["0x310a","1/2"]],"target":"0x3b1e"},{"multipliers":[["0x1818","1/2"],["0x2912","1/2"],["0x310a","1/2"]],"target":"0x3b9a"},{"multipliers":[["0xc51","1/2"],["0x3070","1/2"],["0x3c21","1/2"]],"target":"0x3c75"},{"multipliers":[["0x5a","1/4"],["0x351f","1/4"],["0x354f","1/4"],["0x3557","1/4"],["0x355d","1/4"]],"target":"0x355f"},{"multipliers":[["0x5a","1/4"],["0x353b","1/4"],["0x356b","1/4"],["0x3573","1/4"],["0x3579","1/4"]],"target":"0x357b"},{"multipliers":[["0x5a","1/4"],["0x353e","1/4"],["0x356e","1/4"],["0x3576","1/4"],["0x357c","1/4"]],"target":"0x357e"},{"multipliers":[["0x2912","1/2"],["0x310a","1/2"],["0x1a9c","1/2"]],"target":"0x3b9e"},{"multipliers":[["0x310a","1/3"],["0x1549","1/3"],["0x2543","1/3"],["0x344b","1/3"]],"target":"0x3dcb"},{"multipliers":[["0x302a","1/2"],["0xe8a","1/2"],["0x3c21","1/2"]],"target":"0x3eab"},{"multipliers":[["0x302a","1/2"],["0xe8a","1/2"],["0x3c24","1/2"]],"target":"0x3eae"},{"multipliers":[["0xc51","1/2"],["0x3070","1/2"],["0x3c21","1/2"]],"target":"0x3ef1"},{"multipliers":[["0x310a","1/3"],["0x1549","1/3"],["0x2543","1/3"],["0x344b","1/3"]],"target":"0x3f4b"},{"multipliers":[["0x5a","1/4"],["0x1f9b","1/4"],["0x1fcb","1/4"],["0x1fd3","1/4"],["0x1fd9","1/4"]],"target":"0x1fdb"},{"multipliers":[["0x5a","1/4"],["0x1f9e","1/4"],["0x1fce","1/4"],["0x1fd6","1/4"],["0x1fdc","1/4"]],"target":"0x1fde"},{"multipliers":[["0x5a","1/4"],["0x2f9b","1/4"],["0x2fcb","1/4"],["0x2fd3","1/4"],["0x2fd9","1/4"]],"target":"0x2fdb"},{"multipliers":[["0x1a9c","1/2"],["0x3174","1/2"],["0x2be8","1/2"]],"target":"0x3bfc"},{"multipliers":[["0x312e","1/2"],["0xf8b","1/2"],["0x3ea5","1/2"]],"target":"0x3faf"},{"multipliers":[["0x3174","1/2"],["0xfd1","1/2"],["0x3ea5","1/2"]],"target":"0x3ff5"},{"multipliers":[["0x2463","1"],["0x1a9c","1"]],"target":"0x3eff"},{"multipliers":[["0x2543","1"],["0x1a9c","1"]],"target":"0x3fdf"},{"multipliers":[["0x2afa","1/3"],["0x3579","1/3"],["0x1fcb","1/3"],["0x3fb3","1/3"]],"target":"0x3ffb"},{"multipliers":[["0x2afa","1/3"],["0x357c","1/3"],["0x1fce","1/3"],["0x3fb6","1/3"]],"target":"0x3ffe"}],"dimension":14,"limits":["Equivalence and irredundancy of this frozen real nonnegative-variable system only; retained separators may be fractional, so integer irredundancy is not claimed.","Original clique census, support geometry and source280-row equivalence remain credited PR6425 premises, not independently replayed here.","No globally smallest arbitrary inequality description, new cap alphabet, coefficients/decoder, physical COPY bound, kappa, native/outer admission or frontier change."],"method":"Exact Fraction packing simplex; feasible slack basis and Bland entering/leaving rules, including nonbasic slacks. Early feasible deletion certificates need no optimality claim.","pivot_statistics":{"maximum_per_target":49,"per_target":[["0x5a",0],["0xc0a",0],["0xc50",0],["0x1412",0],["0x1448",0],["0x1818",0],["0x1842",0],["0x2418",0],["0x2442",0],["0x2812",0],["0x2848",0],["0x300a",0],["0x3050",0],["0xc51",1],["0xd0a",1],["0xd50",1],["0x1942",1],["0x2462",1],["0x2518",1],["0x2542",1],["0x2912",1],["0x302a",1],["0x3070",1],["0x310a",1],["0x3150",1],["0x3c01",0],["0x3c04",0],["0xe8a",1],["0x1513",1],["0x1516",1],["0x1549",1],["0x154c",1],["0x1a98",1],["0x1ac2",1],["0x1c52",3],["0x2463",2],["0x2519",2],["0x2543",2],["0x2932",2],["0x2c4a",4],["0x2c52",3],["0x2c58",4],["0x344a",3],["0x3452",3],["0x3852",3],["0x3858",3],["0x3c21",1],["0x3c24",1],["0xf8a",2],["0xfd0",2],["0x1a9c",2],["0x1bc2",2],["0x1c59",4],["0x1c5c",3],["0x1d1a",5],["0x1d4a",5],["0x1d58",4],["0x247a",3],["0x255a",5],["0x295a",3],["0x2bc8",1],["0x2c1b",3],["0x2c3a",3],["0x2d1a",6],["0x2d52",7],["0x312e",3],["0x315a",4],["0x3174",3],["0x341b",3],["0x341e",3],["0x343a",4],["0x344b",4],["0x344e",4],["0x3453",4],["0x3456",4],["0x3459",3],["0x345c",3],["0x3478",4],["0x351a",5],["0x354a",5],["0x3552",5],["0x3558",5],["0x383a",4],["0x386a",4],["0x3952",8],["0x3c0b",3],["0x3c0e",3],["0x3c13",3],["0x3c16",3],["0x3c49",3],["0x3c4c",3],["0x3c54",3],["0x3d48",1],["0xf8b",3],["0xfd1",3],["0x145f",2],["0x155b",4],["0x155e",4],["0x1ada",4],["0x1bc6",3],["0x1c9b",4],["0x1c9e",4],["0x1e1b",4],["0x1e1e",4],["0x1eca",5],["0x247b",4],["0x255b",7],["0x297a",4],["0x2ada",2],["0x2be8",2],["0x2d3a",8],["0x2d72",7],["0x2dca",6],["0x2dd8",6],["0x2eca",5],["0x2f4a",6],["0x2f58",6],["0x307e",3],["0x345b",11],["0x345e",11],["0x393a",7],["0x395a",13],["0x39d8",4],["0x3aca",4],["0x3b58",4],["0x3c33",4],["0x3c36",4],["0x3c69",4],["0x3c6c",4],["0x3c99",3],["0x3c9c",3],["0x3cc3",3],["0x3cc6",3],["0x3d68",2],["0x3e19",3],["0x3e1c",3],["0x3e43",3],["0x3e46",3],["0x3e85",2],["0xedb",3],["0xfda",5],["0x1ade",5],["0x1e9b",6],["0x1f9a",7],["0x1fca",7],["0x1fd2",7],["0x1fd8",6],["0x2afa",3],["0x2d3b",10],["0x2d73",8],["0x2ed3",4],["0x2eea",7],["0x2fca",9],["0x2fd2",8],["0x2fd8",8],["0x346f",6],["0x3477",6],["0x351f",9],["0x353b",10],["0x353e",9],["0x354f",10],["0x3557",10],["0x355d",9],["0x356b",8],["0x356e",8],["0x3573",8],["0x3576",8],["0x3579",10],["0x357c",9],["0x393e",8],["0x3976",12],["0x399e",5],["0x39ce",5],["0x39ea",6],["0x3ada",8],["0x3af8",5],["0x3b1e",5],["0x3b4e",5],["0x3b6a",6],["0x3b9a",5],["0x3bca",7],["0x3bd8",6],["0x3c1f",13],["0x3c75",6],["0x3d1b",21],["0x3d1e",15],["0x3dc6",4],["0x3ea5",4],["0x3f46",4],["0x1f9b",9],["0x1f9e",9],["0x1fcb",11],["0x1fce",11],["0x1fd3",10],["0x1fd6",12],["0x1fd9",8],["0x1fdc",8],["0x2d7b",16],["0x2eeb",8],["0x2ef3",6],["0x2f9b",11],["0x2fcb",10],["0x2fd3",10],["0x2fd9",10],["0x2fda",32],["0x347f",12],["0x355f",18],["0x357b",22],["0x357e",28],["0x397e",19],["0x3b9e",7],["0x3caf",5],["0x3d37",8],["0x3d8f",4],["0x3dab",6],["0x3dbc",5],["0x3dcb",21],["0x3dce",23],["0x3dea",17],["0x3df1",7],["0x3df8",18],["0x3e2f",5],["0x3eab",5],["0x3eae",5],["0x3ec7",6],["0x3ecb",12],["0x3ece",12],["0x3ed3",18],["0x3ed6",17],["0x3ee6",6],["0x3ef1",5],["0x3ef4",5],["0x3f0f",4],["0x3f2b",6],["0x3f3c",5],["0x3f4b",21],["0x3f4e",23],["0x3f6a",17],["0x3f71",7],["0x3f78",18],["0x3f8e",5],["0x3fd4",5],["0x1edf",17],["0x1fdb",22],["0x1fde",29],["0x2efb",17],["0x2fdb",29],["0x3afe",24],["0x3bee",11],["0x3bfc",10],["0x3d3f",32],["0x3d77",20],["0x3ee7",9],["0x3f9d",7],["0x3fb3",6],["0x3fb6",6],["0x3fc7",7],["0x3fe9",7],["0x3fec",7],["0x3d7f",49],["0x3eef",21],["0x3ef7",19],["0x3f9f",30],["0x3faf",10],["0x3fbb",31],["0x3fbe",27],["0x3fcf",37],["0x3fd7",39],["0x3fdd",26],["0x3feb",28],["0x3fee",33],["0x3ff3",32],["0x3ff5",12],["0x3ff6",32],["0x3ff9",28],["0x3ffc",27],["0x3eff",14],["0x3fdf",22],["0x3ffb",43],["0x3ffe",44]],"total":2272},"retained":["0x5a","0xc0a","0xc50","0x1412","0x1448","0x1818","0x1842","0x2418","0x2442","0x2812","0x2848","0x300a","0x3050","0xc51","0xd0a","0xd50","0x1942","0x2462","0x2518","0x2542","0x2912","0x302a","0x3070","0x310a","0x3150","0x3c01","0x3c04","0xe8a","0x1513","0x1516","0x1549","0x154c","0x1a98","0x1ac2","0x1c52","0x2463","0x2519","0x2543","0x2932","0x2c4a","0x2c52","0x2c58","0x344a","0x3452","0x3852","0x3858","0x3c21","0x3c24","0xf8a","0xfd0","0x1a9c","0x1bc2","0x1c59","0x1c5c","0x247a","0x295a","0x2bc8","0x2c1b","0x2c3a","0x2d1a","0x2d52","0x312e","0x3174","0x341b","0x341e","0x344b","0x344e","0x3453","0x3456","0x3459","0x345c","0x383a","0x386a","0x3952","0x3c0b","0x3c0e","0x3c13","0x3c16","0x3c49","0x3c4c","0x3c54","0x3d48","0xf8b","0xfd1","0x145f","0x1ada","0x1bc6","0x1c9b","0x1c9e","0x1e1b","0x1e1e","0x247b","0x297a","0x2ada","0x2be8","0x2d3a","0x2d72","0x2dca","0x2dd8","0x2eca","0x2f4a","0x2f58","0x307e","0x345b","0x345e","0x393a","0x395a","0x39d8","0x3aca","0x3b58","0x3c33","0x3c36","0x3c69","0x3c6c","0x3c99","0x3c9c","0x3cc3","0x3cc6","0x3d68","0x3e19","0x3e1c","0x3e43","0x3e46","0x3e85","0xedb","0x1ade","0x1e9b","0x2afa","0x2d3b","0x2d73","0x2ed3","0x2eea","0x2fca","0x2fd2","0x2fd8","0x346f","0x3477","0x351f","0x353b","0x353e","0x354f","0x3557","0x355d","0x356b","0x356e","0x3573","0x3576","0x3579","0x357c","0x393e","0x3976","0x39ce","0x39ea","0x3ada","0x3af8","0x3b4e","0x3b6a","0x3bca","0x3bd8","0x3c1f","0x3d1b","0x3d1e","0x3dc6","0x3ea5","0x3f46","0x1f9b","0x1f9e","0x1fcb","0x1fce","0x1fd3","0x1fd6","0x1fd9","0x1fdc","0x2d7b","0x2eeb","0x2ef3","0x2f9b","0x2fcb","0x2fd3","0x2fd9","0x2fda","0x347f","0x397e","0x3caf","0x3d37","0x3d8f","0x3dab","0x3dbc","0x3dce","0x3dea","0x3df1","0x3df8","0x3e2f","0x3ec7","0x3ecb","0x3ece","0x3ed3","0x3ed6","0x3ee6","0x3ef4","0x3f0f","0x3f2b","0x3f3c","0x3f4e","0x3f6a","0x3f71","0x3f78","0x3f8e","0x3fd4","0x1edf","0x2efb","0x3afe","0x3bee","0x3d3f","0x3d77","0x3ee7","0x3f9d","0x3fb3","0x3fb6","0x3fc7","0x3fe9","0x3fec","0x3d7f","0x3eef","0x3ef7","0x3f9f","0x3fbb","0x3fbe","0x3fcf","0x3fd7","0x3fdd","0x3feb","0x3fee","0x3ff3","0x3ff6","0x3ff9","0x3ffc"],"schema_version":1,"separators":[{"target":"0x5a","x":["8","0","8","0","0","8","0","8","8","8","8","8","8","8"]},{"target":"0xc0a","x":["8","0","8","0","8","8","8","8","8","8","0","0","8","8"]},{"target":"0xc50","x":["8","8","8","8","0","8","0","8","8","8","0","0","8","8"]},{"target":"0x1412","x":["8","0","8","8","0","8","8","8","8","8","0","8","0","8"]},{"target":"0x1448","x":["8","8","8","0","8","8","0","8","8","8","0","8","0","8"]},{"target":"0x1818","x":["8","8","8","0","0","8","8","8","8","8","8","0","0","8"]},{"target":"0x1842","x":["8","0","8","8","8","8","0","8","8","8","8","0","0","8"]},{"target":"0x2418","x":["8","8","8","0","0","8","8","8","8","8","0","8","8","0"]},{"target":"0x2442","x":["8","0","8","8","8","8","0","8","8","8","0","8","8","0"]},{"target":"0x2812","x":["8","0","8","8","0","8","8","8","8","8","8","0","8","0"]},{"target":"0x2848","x":["8","8","8","0","8","8","0","8","8","8","8","0","8","0"]},{"target":"0x300a","x":["8","0","8","0","8","8","8","8","8","8","8","8","0","0"]},{"target":"0x3050","x":["8","8","8","8","0","8","0","8","8","8","8","8","0","0"]},{"target":"0xc51","x":["0","8","8","8","1","8","0","8","8","8","0","0","8","8"]},{"target":"0xd0a","x":["8","1","8","0","8","8","8","8","0","8","0","0","8","8"]},{"target":"0xd50","x":["8","8","8","8","1","8","0","8","0","8","0","0","8","8"]},{"target":"0x1942","x":["8","1","8","8","8","8","0","8","0","8","8","0","0","8"]},{"target":"0x2462","x":["8","2","8","8","8","0","0","8","8","8","0","8","8","0"]},{"target":"0x2518","x":["8","8","8","2","0","8","8","8","0","8","0","8","8","0"]},{"target":"0x2542","x":["8","2","8","8","8","8","0","8","0","8","0","8","8","0"]},{"target":"0x2912","x":["8","2","8","8","0","8","8","8","0","8","8","0","8","0"]},{"target":"0x302a","x":["8","1","8","0","8","0","8","8","8","8","8","8","0","0"]},{"target":"0x3070","x":["8","8","8","8","1","0","0","8","8","8","8","8","0","0"]},{"target":"0x310a","x":["8","1","8","0","8","8","8","8","0","8","8","8","0","0"]},{"target":"0x3150","x":["8","8","8","8","1","8","0","8","0","8","8","8","0","0"]},{"target":"0x3c01","x":["0","8","8","8","8","8","8","8","8","8","0","0","0","0"]},{"target":"0x3c04","x":["8","8","0","8","8","8","8","8","8","8","0","0","0","0"]},{"target":"0xe8a","x":["8","1","8","0","8","8","8","0","8","0","0","0","8","8"]},{"target":"0x1513","x":["0","2","8","8","0","8","8","8","0","8","0","8","0","8"]},{"target":"0x1516","x":["8","2","0","8","0","8","8","8","0","8","0","8","0","8"]},{"target":"0x1549","x":["0","8","8","2","8","8","0","8","0","8","0","8","0","8"]},{"target":"0x154c","x":["8","8","0","2","8","8","0","8","0","8","0","8","0","8"]},{"target":"0x1a98","x":["8","8","8","2","0","8","8","0","8","0","8","0","0","8"]},{"target":"0x1ac2","x":["8","1","8","8","8","8","0","0","8","0","8","0","0","8"]},{"target":"0x1c52","x":["8","1","8","8","1","8","0","8","8","8","0","0","0","8"]},{"target":"0x2463","x":["0","3","8","8","8","0","0","8","8","8","0","8","8","0"]},{"target":"0x2519","x":["0","8","8","3","0","8","8","8","0","8","0","8","8","0"]},{"target":"0x2543","x":["0","3","8","8","8","8","0","8","0","8","0","8","8","0"]},{"target":"0x2932","x":["8","3","8","8","0","0","8","8","0","8","8","0","8","0"]},{"target":"0x2c4a","x":["8","1/2","8","1/2","8","8","3/2","8","8","8","0","0","8","0"]},{"target":"0x2c52","x":["8","3/2","8","8","1/2","8","1/2","8","8","8","0","0","8","0"]},{"target":"0x2c58","x":["8","8","8","3/2","1/2","8","1/2","8","8","8","0","0","8","0"]},{"target":"0x344a","x":["8","1/2","8","1/2","8","8","3/2","8","8","8","0","8","0","0"]},{"target":"0x3452","x":["8","3/2","8","8","1/2","8","1/2","8","8","8","0","8","0","0"]},{"target":"0x3852","x":["8","1","8","8","1","8","0","8","8","8","8","0","0","0"]},{"target":"0x3858","x":["8","8","8","3/2","1/2","8","1/2","8","8","8","8","0","0","0"]},{"target":"0x3c21","x":["1","8","8","8","8","0","8","8","8","8","0","0","0","0"]},{"target":"0x3c24","x":["8","8","1","8","8","0","8","8","8","8","0","0","0","0"]},{"target":"0xf8a","x":["8","2","8","0","8","8","8","0","0","0","0","0","8","8"]},{"target":"0xfd0","x":["8","8","8","8","2","8","0","0","0","0","0","0","8","8"]},{"target":"0x1a9c","x":["8","8","0","3","0","8","8","0","8","0","8","0","0","8"]},{"target":"0x1bc2","x":["8","2","8","8","8","8","0","0","0","0","8","0","0","8"]},{"target":"0x1c59","x":["0","8","8","1","1","8","1","8","8","8","0","0","0","8"]},{"target":"0x1c5c","x":["8","8","0","3/2","1/2","8","1/2","8","8","8","0","0","0","8"]},{"target":"0x247a","x":["8","5/2","8","3/2","0","0","0","8","8","8","1/2","8","8","0"]},{"target":"0x295a","x":["8","5/2","8","3/2","0","8","0","8","0","8","8","1/2","8","0"]},{"target":"0x2bc8","x":["8","8","8","2","8","8","0","0","0","0","8","0","8","0"]},{"target":"0x2c1b","x":["0","1/2","8","1/2","3/2","8","8","8","8","8","0","0","8","0"]},{"target":"0x2c3a","x":["8","1/2","8","1/2","3/2","0","8","8","8","8","0","0","8","0"]},{"target":"0x2d1a","x":["8","1/2","8","1/2","3/2","8","8","8","1","8","0","0","8","0"]},{"target":"0x2d52","x":["8","5/3","8","8","2/3","8","2/3","8","2/3","8","0","0","8","0"]},{"target":"0x312e","x":["8","3","0","0","8","0","8","8","0","8","8","8","0","0"]},{"target":"0x3174","x":["8","8","0","8","3","0","0","8","0","8","8","8","0","0"]},{"target":"0x341b","x":["0","1/2","8","1/2","3/2","8","8","8","8","8","0","8","0","0"]},{"target":"0x341e","x":["8","1/2","0","1/2","3/2","8","8","8","8","8","0","8","0","0"]},{"target":"0x344b","x":["0","0","8","1","8","8","2","8","8","8","0","8","0","0"]},{"target":"0x344e","x":["8","0","0","1","8","8","2","8","8","8","0","8","0","0"]},{"target":"0x3453","x":["0","2","8","8","1","8","0","8","8","8","0","8","0","0"]},{"target":"0x3456","x":["8","2","0","8","1","8","0","8","8","8","0","8","0","0"]},{"target":"0x3459","x":["0","8","8","3/2","1/2","8","1/2","8","8","8","0","8","0","0"]},{"target":"0x345c","x":["8","8","0","3/2","1/2","8","1/2","8","8","8","0","8","0","0"]},{"target":"0x383a","x":["8","1","8","1","1","0","8","8","8","8","8","0","0","0"]},{"target":"0x386a","x":["8","1/2","8","3/2","8","0","1/2","8","8","8","8","0","0","0"]},{"target":"0x3952","x":["8","2/3","8","8","5/3","8","2/3","8","2/3","8","8","0","0","0"]},{"target":"0x3c0b","x":["0","1/2","8","0","8","8","8","8","8","8","1/2","0","1/2","0"]},{"target":"0x3c0e","x":["8","1/2","0","0","8","8","8","8","8","8","1/2","0","1/2","0"]},{"target":"0x3c13","x":["0","3/2","8","8","0","8","8","8","8","8","1/2","1/2","0","0"]},{"target":"0x3c16","x":["8","3/2","0","8","0","8","8","8","8","8","1/2","1/2","0","0"]},{"target":"0x3c49","x":["0","8","8","3/2","8","8","0","8","8","8","1/2","1/2","0","0"]},{"target":"0x3c4c","x":["8","8","0","3/2","8","8","0","8","8","8","1/2","1/2","0","0"]},{"target":"0x3c54","x":["8","8","0","8","1/2","8","0","8","8","8","1/2","0","1/2","0"]},{"target":"0x3d48","x":["8","8","8","2","8","8","0","8","0","8","0","0","0","0"]},{"target":"0xf8b","x":["0","3","8","0","8","8","8","0","0","0","0","0","8","8"]},{"target":"0xfd1","x":["0","8","8","8","3","8","0","0","0","0","0","0","8","8"]},{"target":"0x145f","x":["0","2","0","2","0","8","0","8","8","8","0","8","0","8"]},{"target":"0x1ada","x":["8","3/2","8","5/2","0","8","0","1/2","8","0","8","0","0","8"]},{"target":"0x1bc6","x":["8","3","0","8","8","8","0","0","0","0","8","0","0","8"]},{"target":"0x1c9b","x":["0","1/2","8","1/2","3/2","8","8","0","8","8","0","0","0","8"]},{"target":"0x1c9e","x":["8","1/2","0","1/2","3/2","8","8","0","8","8","0","0","0","8"]},{"target":"0x1e1b","x":["0","1/2","8","1/2","3/2","8","8","8","8","0","0","0","0","8"]},{"target":"0x1e1e","x":["8","1/2","0","1/2","3/2","8","8","8","8","0","0","0","0","8"]},{"target":"0x247b","x":["0","3","8","1","0","0","0","8","8","8","1","8","8","0"]},{"target":"0x297a","x":["8","3","8","1","0","0","0","8","0","8","8","1","8","0"]},{"target":"0x2ada","x":["8","2","8","2","0","8","0","0","8","0","8","0","8","0"]},{"target":"0x2be8","x":["8","8","8","3","8","0","0","0","0","0","8","0","8","0"]},{"target":"0x2d3a","x":["8","1","8","0","2","0","8","8","1","8","0","0","8","0"]},{"target":"0x2d72","x":["8","5/2","8","8","3/2","0","1/2","8","0","8","0","0","8","0"]},{"target":"0x2dca","x":["8","3/2","8","1/2","8","8","3/2","0","0","8","0","0","8","0"]},{"target":"0x2dd8","x":["8","8","8","3/2","3/2","8","1/2","0","0","8","0","0","8","0"]},{"target":"0x2eca","x":["8","1","8","1","8","8","1","0","8","0","0","0","8","0"]},{"target":"0x2f4a","x":["8","3/2","8","1/2","8","8","3/2","8","0","0","0","0","8","0"]},{"target":"0x2f58","x":["8","8","8","3/2","3/2","8","1/2","8","0","0","0","0","8","0"]},{"target":"0x307e","x":["8","2","0","0","2","0","0","8","8","8","8","8","0","0"]},{"target":"0x345b","x":["0","5/3","8","2/3","2/3","8","1","8","8","8","2/3","8","0","0"]},{"target":"0x345e","x":["8","5/3","0","2/3","2/3","8","1","8","8","8","2/3","8","0","0"]},{"target":"0x393a","x":["8","5/2","8","1/2","3/2","0","8","8","0","8","8","0","0","0"]},{"target":"0x395a","x":["8","7/4","8","1/4","5/4","8","3/4","8","0","8","8","1/4","1/4","3/4"]},{"target":"0x39d8","x":["8","8","8","1/2","3/2","8","3/2","0","0","8","8","0","0","0"]},{"target":"0x3aca","x":["8","1/2","8","1/2","8","8","3/2","0","8","0","8","0","0","0"]},{"target":"0x3b58","x":["8","8","8","1/2","3/2","8","3/2","8","0","0","8","0","0","0"]},{"target":"0x3c33","x":["0","1","8","8","0","0","8","8","8","8","1","1","0","0"]},{"target":"0x3c36","x":["8","1","0","8","0","0","8","8","8","8","1","1","0","0"]},{"target":"0x3c69","x":["0","8","8","1","8","0","0","8","8","8","1","1","0","0"]},{"target":"0x3c6c","x":["8","8","0","1","8","0","0","8","8","8","1","1","0","0"]},{"target":"0x3c99","x":["0","8","8","3/2","0","8","8","0","8","8","1/2","1/2","0","0"]},{"target":"0x3c9c","x":["8","8","0","3/2","0","8","8","0","8","8","1/2","1/2","0","0"]},{"target":"0x3cc3","x":["0","1","8","8","8","8","0","0","8","8","1","0","0","0"]},{"target":"0x3cc6","x":["8","1","0","8","8","8","0","0","8","8","1","0","0","0"]},{"target":"0x3d68","x":["8","8","8","3","8","0","0","8","0","8","0","0","0","0"]},{"target":"0x3e19","x":["0","8","8","3/2","0","8","8","8","8","0","1/2","1/2","0","0"]},{"target":"0x3e1c","x":["8","8","0","3/2","0","8","8","8","8","0","1/2","1/2","0","0"]},{"target":"0x3e43","x":["0","1","8","8","8","8","0","8","8","0","1","0","0","0"]},{"target":"0x3e46","x":["8","1","0","8","8","8","0","8","8","0","1","0","0","0"]},{"target":"0x3e85","x":["0","8","0","8","8","8","8","0","8","0","1","0","0","0"]},{"target":"0xedb","x":["0","2","8","0","2","8","0","0","8","0","0","0","8","8"]},{"target":"0x1ade","x":["8","1","0","3","0","8","0","1","8","0","8","0","0","8"]},{"target":"0x1e9b","x":["0","1/2","8","3/2","3/2","8","8","0","8","0","0","0","0","8"]},{"target":"0x2afa","x":["8","3","8","2","0","0","0","0","8","0","8","0","8","0"]},{"target":"0x2d3b","x":["0","1","8","1","3","0","8","8","0","8","0","0","8","0"]},{"target":"0x2d73","x":["0","3","8","8","1","0","1","8","0","8","0","0","8","0"]},{"target":"0x2ed3","x":["0","1","8","8","1","8","1","0","8","0","0","0","8","0"]},{"target":"0x2eea","x":["8","1","8","1","8","0","2","0","8","0","0","0","8","0"]},{"target":"0x2fca","x":["8","4/3","8","4/3","8","8","4/3","0","1/3","0","0","0","8","0"]},{"target":"0x2fd2","x":["8","1","8","8","1","8","1","0","1","0","0","0","8","0"]},{"target":"0x2fd8","x":["8","8","8","1","1","8","1","0","1","0","0","0","8","0"]},{"target":"0x346f","x":["0","2","0","0","8","0","2","8","8","8","0","8","0","0"]},{"target":"0x3477","x":["0","2","0","8","0","0","2","8","8","8","0","8","0","0"]},{"target":"0x351f","x":["0","2/3","0","2/3","5/3","8","8","8","5/3","8","0","8","0","0"]},{"target":"0x353b","x":["0","1","8","1","2","0","8","8","1","8","0","8","0","0"]},{"target":"0x353e","x":["8","2","0","1","1","0","8","8","1","8","0","8","0","0"]},{"target":"0x354f","x":["0","1","0","1","8","8","2","8","1","8","0","8","0","0"]},{"target":"0x3557","x":["0","2","0","8","1","8","1","8","1","8","0","8","0","0"]},{"target":"0x355d","x":["0","8","0","5/3","2/3","8","2/3","8","5/3","8","0","8","0","0"]},{"target":"0x356b","x":["0","3/2","8","3/2","8","0","5/2","8","0","8","0","8","0","0"]},{"target":"0x356e","x":["8","3/2","0","5/2","8","0","3/2","8","0","8","0","8","0","0"]},{"target":"0x3573","x":["0","5/2","8","8","3/2","0","3/2","8","0","8","0","8","0","0"]},{"target":"0x3576","x":["8","3/2","0","8","5/2","0","3/2","8","0","8","0","8","0","0"]},{"target":"0x3579","x":["0","8","8","2","1","0","1","8","1","8","0","8","0","0"]},{"target":"0x357c","x":["8","8","0","1","1","0","2","8","1","8","0","8","0","0"]},{"target":"0x393e","x":["8","3","0","1","1","0","8","8","0","8","8","0","0","0"]},{"target":"0x3976","x":["8","1","0","8","1","0","1","8","2","8","8","0","0","0"]},{"target":"0x39ce","x":["8","3/2","0","3/2","8","8","1/2","0","0","8","8","0","0","0"]},{"target":"0x39ea","x":["8","3/2","8","3/2","8","0","1/2","0","0","8","8","0","0","0"]},{"target":"0x3ada","x":["8","2","8","2","1","8","0","0","8","0","8","0","0","0"]},{"target":"0x3af8","x":["8","8","8","3/2","3/2","0","1/2","0","8","0","8","0","0","0"]},{"target":"0x3b4e","x":["8","3/2","0","3/2","8","8","1/2","8","0","0","8","0","0","0"]},{"target":"0x3b6a","x":["8","3/2","8","3/2","8","0","1/2","8","0","0","8","0","0","0"]},{"target":"0x3bca","x":["8","1","8","1","8","8","1","0","1","0","8","0","0","0"]},{"target":"0x3bd8","x":["8","8","8","3/2","3/2","8","3/2","0","0","0","8","0","0","0"]},{"target":"0x3c1f","x":["0","3/4","0","1/4","5/4","8","8","8","8","8","1/2","1/4","1/4","0"]},{"target":"0x3d1b","x":["0","4/9","8","1/3","4/3","8","8","8","13/9","8","4/9","0","1/3","4/9"]},{"target":"0x3d1e","x":["8","1","0","1/2","1","8","8","8","1","8","1/2","0","1/2","0"]},{"target":"0x3dc6","x":["8","2","0","8","8","8","0","0","0","8","1","0","0","0"]},{"target":"0x3ea5","x":["0","8","0","8","8","0","8","0","8","0","2","0","0","0"]},{"target":"0x3f46","x":["8","2","0","8","8","8","0","8","0","0","1","0","0","0"]},{"target":"0x1f9b","x":["0","5/2","8","3/2","3/2","8","8","0","0","0","0","0","0","8"]},{"target":"0x1f9e","x":["8","3/2","0","3/2","5/2","8","8","0","0","0","0","0","0","8"]},{"target":"0x1fcb","x":["0","1","8","1","8","8","1","0","2","0","0","0","0","8"]},{"target":"0x1fce","x":["8","1","0","1","8","8","2","0","1","0","0","0","0","8"]},{"target":"0x1fd3","x":["0","1","8","8","2","8","1","0","1","0","0","0","0","8"]},{"target":"0x1fd6","x":["8","5/3","0","8","2/3","8","2/3","0","5/3","0","0","0","0","8"]},{"target":"0x1fd9","x":["0","8","8","3/2","3/2","8","5/2","0","0","0","0","0","0","8"]},{"target":"0x1fdc","x":["8","8","0","5/2","3/2","8","3/2","0","0","0","0","0","0","8"]},{"target":"0x2d7b","x":["0","2","8","0","2","0","0","8","0","8","0","0","8","2"]},{"target":"0x2eeb","x":["0","1","8","1","8","0","3","0","8","0","0","0","8","0"]},{"target":"0x2ef3","x":["0","2","8","8","0","0","2","0","8","0","0","0","8","0"]},{"target":"0x2f9b","x":["0","1","8","1","1","8","8","0","2","0","0","0","8","0"]},{"target":"0x2fcb","x":["0","2","8","1","8","8","1","0","1","0","0","0","8","0"]},{"target":"0x2fd3","x":["0","1","8","8","1","8","2","0","1","0","0","0","8","0"]},{"target":"0x2fd9","x":["0","8","8","1","2","8","1","0","1","0","0","0","8","0"]},{"target":"0x2fda","x":["8","5/6","8","5/6","5/6","8","3/2","1/3","5/6","0","0","1/6","8","1/2"]},{"target":"0x347f","x":["0","7/2","0","1/2","1/2","0","1","8","8","8","1/2","8","0","1/2"]},{"target":"0x397e","x":["8","2","0","0","2","0","0","8","0","8","8","0","0","2"]},{"target":"0x3caf","x":["0","1/2","0","0","8","0","8","0","8","8","1/2","0","3/2","0"]},{"target":"0x3d37","x":["0","3","0","8","0","0","8","8","0","8","1","1","0","0"]},{"target":"0x3d8f","x":["0","2","0","0","8","8","8","0","0","8","0","0","1","0"]},{"target":"0x3dab","x":["0","3/2","8","0","8","0","8","0","0","8","1/2","0","3/2","0"]},{"target":"0x3dbc","x":["8","8","0","3/2","0","0","8","0","0","8","3/2","1/2","0","0"]},{"target":"0x3dce","x":["8","3/4","0","3/4","8","8","3/2","0","3/4","8","1/4","0","3/4","0"]},{"target":"0x3dea","x":["8","1/3","8","2/3","8","0","1","0","2/3","8","1/3","0","0","4/3"]},{"target":"0x3df1","x":["0","8","8","8","3/2","0","0","0","0","8","1/2","0","3/2","0"]},{"target":"0x3df8","x":["8","8","8","4/3","1/3","0","1","0","1","8","0","0","1/3","1/3"]},{"target":"0x3e2f","x":["0","1/2","0","0","8","0","8","8","8","0","1/2","0","3/2","0"]},{"target":"0x3ec7","x":["0","1","0","8","8","8","0","0","8","0","1","1","0","0"]},{"target":"0x3ecb","x":["0","0","8","1","8","8","2","0","8","0","1","0","0","0"]},{"target":"0x3ece","x":["8","0","0","1","8","8","2","0","8","0","1","0","0","0"]},{"target":"0x3ed3","x":["0","1","8","8","1","8","1","0","8","0","1","0","0","0"]},{"target":"0x3ed6","x":["8","1","0","8","0","8","0","0","8","0","1","0","1","1"]},{"target":"0x3ee6","x":["8","3/2","0","8","8","0","0","0","8","0","3/2","1/2","0","0"]},{"target":"0x3ef4","x":["8","8","0","8","1/2","0","0","0","8","0","1/2","0","3/2","0"]},{"target":"0x3f0f","x":["0","2","0","0","8","8","8","8","0","0","0","0","1","0"]},{"target":"0x3f2b","x":["0","3/2","8","0","8","0","8","8","0","0","1/2","0","3/2","0"]},{"target":"0x3f3c","x":["8","8","0","3/2","0","0","8","8","0","0","3/2","1/2","0","0"]},{"target":"0x3f4e","x":["8","3/4","0","3/4","8","8","3/2","8","3/4","0","1/4","0","3/4","0"]},{"target":"0x3f6a","x":["8","1/3","8","2/3","8","0","1","8","2/3","0","1/3","0","0","4/3"]},{"target":"0x3f71","x":["0","8","8","8","3/2","0","0","8","0","0","1/2","0","3/2","0"]},{"target":"0x3f78","x":["8","8","8","4/3","1/3","0","1","8","1","0","0","0","1/3","1/3"]},{"target":"0x3f8e","x":["8","5/2","0","0","8","8","8","0","0","0","1/2","0","1/2","0"]},{"target":"0x3fd4","x":["8","8","0","8","5/2","8","0","0","0","0","1/2","0","1/2","0"]},{"target":"0x1edf","x":["0","0","0","2","2","8","2","0","8","0","0","0","0","8"]},{"target":"0x2efb","x":["0","7/2","8","1/2","1/2","0","1","0","8","0","1/2","0","8","1/2"]},{"target":"0x3afe","x":["8","1","0","1","3","0","1","0","8","0","8","0","0","0"]},{"target":"0x3bee","x":["8","1","0","1","8","0","1","0","2","0","8","0","0","0"]},{"target":"0x3d3f","x":["0","1","0","0","2","0","8","8","1","8","0","0","0","2"]},{"target":"0x3d77","x":["0","2","0","8","2","0","0","8","0","8","0","0","0","2"]},{"target":"0x3ee7","x":["0","1","0","8","8","0","0","0","8","0","3","1","0","0"]},{"target":"0x3f9d","x":["0","8","0","3","0","8","8","0","0","0","1","1","0","0"]},{"target":"0x3fb3","x":["1","3","8","8","0","0","8","0","0","0","0","1","0","0"]},{"target":"0x3fb6","x":["8","3","1","8","0","0","8","0","0","0","0","1","0","0"]},{"target":"0x3fc7","x":["0","3","0","8","8","8","0","0","0","0","1","1","0","0"]},{"target":"0x3fe9","x":["0","8","8","3","8","0","0","0","0","0","1","1","0","0"]},{"target":"0x3fec","x":["8","8","0","3","8","0","0","0","0","0","1","1","0","0"]},{"target":"0x3d7f","x":["0","9/5","0","4/5","1","0","4/5","8","4/5","8","4/5","0","4/5","1"]},{"target":"0x3eef","x":["0","2","0","0","8","0","0","0","8","0","2","0","0","2"]},{"target":"0x3ef7","x":["0","0","0","8","0","0","2","0","8","0","2","0","0","2"]},{"target":"0x3f9f","x":["0","1/4","0","7/4","7/4","8","8","0","1/2","0","5/4","1/4","1/4","1/4"]},{"target":"0x3fbb","x":["0","13/8","8","3/8","15/8","0","8","0","1/2","0","9/8","3/8","3/8","1/8"]},{"target":"0x3fbe","x":["8","9/8","0","3/8","15/8","0","8","0","1","0","1/8","3/8","11/8","1/8"]},{"target":"0x3fcf","x":["0","1","0","1/4","8","8","7/4","0","5/4","0","5/4","1/4","1/4","1/4"]},{"target":"0x3fd7","x":["0","7/4","0","8","1/4","8","1","0","5/4","0","5/4","1/4","1/4","1/4"]},{"target":"0x3fdd","x":["0","8","0","7/4","7/4","8","1/4","0","1/2","0","5/4","1/4","1/4","1/4"]},{"target":"0x3feb","x":["0","5/12","8","7/4","8","0","23/12","0","1/3","0","5/4","1/4","1/12","5/12"]},{"target":"0x3fee","x":["8","5/12","0","7/4","8","0","23/12","0","1/3","0","1/4","1/4","13/12","5/12"]},{"target":"0x3ff3","x":["0","23/12","8","8","7/4","0","5/12","0","1/3","0","5/4","1/4","1/12","5/12"]},{"target":"0x3ff6","x":["8","15/8","0","8","3/4","0","3/8","0","11/8","0","3/8","1/8","9/8","3/8"]},{"target":"0x3ff9","x":["0","8","8","15/8","3/8","0","13/8","0","1/2","0","9/8","3/8","3/8","1/8"]},{"target":"0x3ffc","x":["8","8","0","15/8","3/8","0","13/8","0","1/2","0","1/8","3/8","11/8","1/8"]}],"source_manifest_sha256":"d9d9e3785d6496adf112ccafbe25689057e9a1f28384ca28a536660c9f55f6e9","source_rows":280} diff --git a/research/p112-farkas-kernel/SOURCE-PINS.json b/research/p112-farkas-kernel/SOURCE-PINS.json new file mode 100644 index 0000000000..ac788b8940 --- /dev/null +++ b/research/p112-farkas-kernel/SOURCE-PINS.json @@ -0,0 +1,20 @@ +{ + "files": { + "README-6425.md": { + "git_blob": "d9ce3b644cff65dadd88663189638a4bfd52bac3", + "sha256": "f35f0a30796e94ced74686bc3614b4478f5460bac0adb7c8d80827991f70ed0c", + "bytes": 7410, + "repository": "petalas/integer-mult-bounds", + "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c", + "path": "research/p112-demand-kernel/README.md" + }, + "RESULT-6425.json": { + "git_blob": "e18f92e001b8ce9d44287760516bf6ea002bcbcd", + "sha256": "f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89", + "bytes": 22234, + "repository": "petalas/integer-mult-bounds", + "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c", + "path": "research/p112-demand-kernel/RESULT.json" + } + } +} diff --git a/research/p112-farkas-kernel/SOURCES.json b/research/p112-farkas-kernel/SOURCES.json new file mode 100644 index 0000000000..b04149366d --- /dev/null +++ b/research/p112-farkas-kernel/SOURCES.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ], + "note": "Canonical catalogue/selected are provenance only. Runtime inputs are the package-local source pair and result certificate. SOURCE-PINS.json authenticates the external source data; no predecessor executable is imported or replayed." +} diff --git a/research/p112-farkas-kernel/TASK.json b/research/p112-farkas-kernel/TASK.json new file mode 100644 index 0000000000..fc06a87fc7 --- /dev/null +++ b/research/p112-farkas-kernel/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "scope_change_reason": "Take PR6425 first Open next question: combine retained rank-demand inequalities, rather than synthesize a new full supplier/rank-shape decoder. The result is a finite exact reduction of one fixed necessary-condition screen; it does not claim physical realization, coefficients or a paid multiplication bound.", + "actual_scope": "Exact nonnegative-combination certificates and real-multiplicity separation witnesses for the fixed 280-row,14-variable P112 cap-demand system from PR6425.", + "bottleneck_link": "A smaller equivalent demand screen removes provably redundant constraints from support search while preserving all fixed-source real and integer multiplicity tests; it is a search-side implication, not a supplier.", + "budget_minutes": 60, + "stop_rule": "One fixed-system classification or precise capped/failed search. Freeze scientific work by2026-11-03T00:26:08Z, reserving at least15minutes for verification/handoff; do not change caps, synthesize coefficients or rerun predecessor clique censuses.", + "outcome": "completed", + "evidence": "Exact rational RESULT.json certificates checked by regenerated primary and separately implemented oracle; source pins, PROOF.md and VALIDATION.md delimit the source-bound claim.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance in exact generator, proof, packaging and separate certificate checker/static review. Independent AI certificate checking is not blind rediscovery, human review or formal proof-kernel acceptance.", + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362724", + "source_head": "092dcbd13d1263e691ad29f34fbf286fea1fac2c", + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "overlap": { + "checked_open_prs": 405, + "nearest_work": [ + "PR6425 exact280-row kernel and explicit combined-redundancy question", + "PR1422 original complete-clique guard/cap geometry", + "PR5767 supplied exactLPcertificate checking, no optimizer; shared cap128 unchanged", + "PR6430 compatibility replay uses another P112 screen", + "PR6424 B2 quotient-direction counterexample uses another model" + ], + "limits": "Sparse local notes, non-atomic PR body pages, bounded all-state queries and visible Discussion claims do not cover arbitrary historical code, hidden replies or unpublished work." + }, + "open_questions": [ + { + "question": "Do the removed inequalities remain redundant after adding or changing support caps?", + "why_it_matters": "The certificates bind exactly14source rectangles and cannot be transferred to another alphabet by count alone.", + "first_step": "Rebuild the complete changed cap-demand quotient, then certify new explicit coefficient implications.", + "blocked_by": "No changed alphabet/quotient is part of this session." + }, + { + "question": "What is the smallest screen equivalent only on nonnegative integer multiplicities?", + "why_it_matters": "Fractional separating points prove real-system necessity but need not exclude integer-only redundancy.", + "first_step": "Retain the source row system and search for exact integer implication/separation certificates under a separately stated domain.", + "blocked_by": "This contribution deliberately concerns the nonnegative real polyhedron." + }, + { + "question": "Can a passing fixed-cap multiplicity vector admit actual coefficients and a fully charged decoder?", + "why_it_matters": "Necessary rank demands do not provide coefficient vectors or pay native/restoration/access/precision/stock/compiler costs.", + "first_step": "Specify one passing vector and synthesize coefficients under the full original interface before pricing a physical construction.", + "blocked_by": "No coefficient synthesis or physical supplier claim is supplied here." + } + ] +} diff --git a/research/p112-farkas-kernel/VALIDATION.md b/research/p112-farkas-kernel/VALIDATION.md new file mode 100644 index 0000000000..324045c39b --- /dev/null +++ b/research/p112-farkas-kernel/VALIDATION.md @@ -0,0 +1,56 @@ +# Validation and source boundary + +The two inert source files were pinned before scientific execution: + +- PR6425 head `092dcbd13d1263e691ad29f34fbf286fea1fac2c`. +- `RESULT.json`: Git blob `e18f92e001b8ce9d44287760516bf6ea002bcbcd`, + 22,234 bytes, SHA256 + `f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89`. +- `README.md`: Git blob `d9ce3b644cff65dadd88663189638a4bfd52bac3`, + 7,410 bytes, SHA256 + `f35f0a30796e94ced74686bc3614b4478f5460bac0adb7c8d80827991f70ed0c`. +- Two-source manifest SHA256 + `d9d9e3785d6496adf112ccafbe25689057e9a1f28384ca28a536660c9f55f6e9`. + +The primary's first scientific run passed. Normal and optimized emissions and +strict defaults passed with identical complete JSON, empty stderr and no source +execution failure. Primary certificate: 31,660 bytes, SHA256 +`b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704`. +It contains 237 retained rows, 43 deleted rows and 237 strict rational separating +points; 2,272 pivots total, at most 49 per target. No floating LP or optional +dependency was used. + +The primary and separate checker have distinct code ownership. The latter was +written before reading the new primary code or result, then consumes the sealed +result as untrusted certificate data. This is independently implemented +certificate checking, not blind rediscovery or a second simplex. It authenticates +both source objects independently, verifies every implication using only final +retained premises and checks every separator against all 279 other original +rows. Its corruption controls test actual certificate data and rejection reasons. + +The generator's simplex is not trusted for the mathematical conclusion: literal +rational coefficient inequalities establish deletions; explicit rational points +establish nonimplications. Shared `verify_rational_lp.py` from PR5767 is related +certificate tooling, not an optimizer. Its shared 128-variable limit is not +widened and it is not represented as a full-instance replay here. + +The independent checker passed on its first run. Normal/optimized emissions were +byte-identical and both strict-default runs passed with empty stderr. Its 71,360 +byte receipt SHA256 is +`02c89eed3237e401b4b16563529de77cba8925439f2e67c86021a27846fccc81`. +It checks 43 deletion certificates, 237 full-original-row separators and 14 +corruption/schema controls. Of the displayed separators, 134 are integral; +that observation does not establish the smallest integer-only screen. + +The original 262,928-clique census and geometric witness validity are predecessor +coverage, not rerun or independently accepted in this session. Composing the +new 280-to-237 equivalence with that larger screen uses PR6425's proof as a +credited premise. Passing either screen does not produce a decoder or a physical +supplier. Fractional separators concern the real polyhedron; they do not prove +integer-only indispensability or minimum over arbitrary replacement inequalities. + +Package/runtime, source/commit modes/history, normal/optimized strict replay, +read-only cold export, corruption controls, static review and exact-head hosted +CI are separate obligations recorded in the session receipts and public handoff. +No κ, selected-frontier, compiler/precision/stock/access/restoration/native/outer +admission claim is made. All five selected framework assumptions remain. diff --git a/research/p112-farkas-kernel/VERIFY.json b/research/p112-farkas-kernel/VERIFY.json new file mode 100644 index 0000000000..630990d944 --- /dev/null +++ b/research/p112-farkas-kernel/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Authenticate the fixed source matrix, regenerate the exact bounded rational packing certificate, verify every omitted row using final-retained premises and every retained separator against all other original279rows, then strictly compare the complete typed receipt. No predecessor executable/census." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 180, + "checks": "Independently implemented exact rational certificate checking without importing the generator or solving an LP. Authenticate sources, verify every coefficient/RHS implication and full-original-row separator, semantic corruption controls, and strict typed ORACLE.json comparison." + } + ] +} diff --git a/research/p112-farkas-kernel/oracle.py b/research/p112-farkas-kernel/oracle.py new file mode 100644 index 0000000000..10b1e93a76 --- /dev/null +++ b/research/p112-farkas-kernel/oracle.py @@ -0,0 +1,281 @@ +#!/usr/bin/env python3 +"""Independent exact certificate checking; no solver or predecessor execution. + +This consumes the primary's sealed RESULT as untrusted certificate data. It is +independent verification of a discovered certificate, not blind rediscovery. +Credit Nick Petalas/6425, Jeremy Diviney/1422 and the retained geometry lineage. +New material: ToikY with OpenAI Codex assistance, Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction +import hashlib +import json +import math +from pathlib import Path +import re +import sys + +ROOT = Path(__file__).resolve().parent +MANIFEST_SHA = 'd9d9e3785d6496adf112ccafbe25689057e9a1f28384ca28a536660c9f55f6e9' +PINS = { + 'README-6425.md': (7410, 'f35f0a30796e94ced74686bc3614b4478f5460bac0adb7c8d80827991f70ed0c', + 'd9ce3b644cff65dadd88663189638a4bfd52bac3'), + 'RESULT-6425.json': (22234, 'f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89', + 'e18f92e001b8ce9d44287760516bf6ea002bcbcd'), +} +DIMENSION = 14 +ROWS = 280 +MAX_BYTES = 1024 * 1024 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def decode(raw): + def unique(items): + result = {} + for key, value in items: + require(key not in result, 'duplicate JSON key') + result[key] = value + return result + def nonfinite(value): + raise ValueError('nonfinite JSON value: ' + value) + def floating(value): + number = float(value) + require(math.isfinite(number), 'nonfinite JSON number') + return number + return json.loads(raw, object_pairs_hook=unique, parse_constant=nonfinite, parse_float=floating) + + +def bounded_read(path): + with path.open('rb') as handle: + value = handle.read(MAX_BYTES + 1) + require(len(value) <= MAX_BYTES, 'input size bound') + return value + + +def authenticate_sources(values, manifest): + require(hashlib.sha256(manifest).hexdigest() == MANIFEST_SHA, 'source manifest SHA256') + require(set(values) == set(PINS), 'exact two-source closure') + for name, (length, digest, blob) in PINS.items(): + raw = values[name] + require(len(raw) == length, 'source byte length: ' + name) + require(hashlib.sha256(raw).hexdigest() == digest, 'source SHA256: ' + name) + framed = b'blob ' + str(len(raw)).encode('ascii') + b'\0' + raw + require(hashlib.sha1(framed).hexdigest() == blob, 'source Git blob: ' + name) + + +def mask(value): + require(type(value) is str and 1 <= len(value) <= 6, 'hex mask string') + try: + number = int(value, 16) + except ValueError: + raise ValueError('invalid hex mask') from None + require(value == hex(number) and 0 < number < 1 << DIMENSION, 'canonical 14-bit nonempty mask') + return number + + +def rational(value): + require(type(value) is str and 1 <= len(value) <= 512, 'bounded rational string') + require(re.fullmatch(r'-?(?:0|[1-9][0-9]*)(?:/[1-9][0-9]*)?', value) is not None, + 'rational integer/quotient grammar') + try: + number = Fraction(value) + except (ValueError, ZeroDivisionError): + raise ValueError('invalid rational') from None + require(abs(number.numerator).bit_length() <= 256 and number.denominator.bit_length() <= 256, + 'rational 256-bit capacity') + require(str(number) == value, 'canonical rational string') + return number + + +def source_rows(raw): + source = decode(raw) + require(type(source) is dict and source.get('kernel_rows') == ROWS, 'source row count') + require(type(source.get('alphabet')) is list and len(source['alphabet']) == DIMENSION, 'source dimension') + require(type(source.get('kernel')) is list and len(source['kernel']) == ROWS, 'source kernel list') + rows = {} + for record in source['kernel']: + require(type(record) is list and len(record) == 3, 'source row shape') + hit, demand, witness = record + number = mask(hit) + require(number not in rows, 'unique source masks') + require(type(demand) is int and 1 <= demand <= 8, 'source demand integer') + require(type(witness) is str and witness.startswith('0x'), 'source witness provenance') + rows[number] = demand + return rows + + +def certificate_sets(certificate, rows): + require(type(certificate) is dict, 'certificate object') + for name, expected in [('schema_version', 1), ('dimension', DIMENSION), ('source_rows', ROWS)]: + require(type(certificate.get(name)) is int and certificate[name] == expected, 'typed ' + name) + require(certificate.get('source_manifest_sha256') == MANIFEST_SHA, 'certificate source binding') + retained = certificate.get('retained') + require(type(retained) is list and 1 <= len(retained) < ROWS, 'strict retained-row reduction') + numbers = [mask(value) for value in retained] + require(len(set(numbers)) == len(numbers) and set(numbers) <= rows.keys(), 'distinct original retained rows') + require(type(certificate.get('deletions')) is list and len(certificate['deletions']) == ROWS-len(numbers), 'deletion count') + require(type(certificate.get('separators')) is list and len(certificate['separators']) == len(numbers), 'separator count') + return set(numbers) + + +def deletion_check(record, retained, rows): + require(type(record) is dict, 'deletion record') + target = mask(record.get('target')) + require(target in rows and target not in retained, 'deleted original row') + terms = record.get('multipliers') + require(type(terms) is list and 1 <= len(terms) <= ROWS, 'bounded multiplier list') + coefficients, rhs, used = [Fraction(0) for _ in range(DIMENSION)], Fraction(0), set() + for term in terms: + require(type(term) is list and len(term) == 2, 'multiplier pair') + donor, weight = mask(term[0]), rational(term[1]) + require(donor in retained and donor not in used, 'retained unique donor; no self or cyclic premise') + require(weight >= 0, 'nonnegative multiplier') + used.add(donor) + rhs += weight * rows[donor] + for column in range(DIMENSION): + if donor >> column & 1: + coefficients[column] += weight + require(all(value <= (target >> k & 1) for k, value in enumerate(coefficients)), 'coefficient exceeds target') + require(rhs >= rows[target], 'right-hand side below target demand') + return {'target': hex(target), 'premises': len(terms), 'right_hand_side': str(rhs), + 'demand': rows[target], 'coefficients': [str(value) for value in coefficients]} + + +def dot(row, vector): + total = Fraction(0) + for column, value in enumerate(vector): + if row >> column & 1: + total += value + return total + + +def separator_check(record, retained, rows): + require(type(record) is dict, 'separator record') + target = mask(record.get('target')) + require(target in retained, 'retained separator target') + encoded = record.get('x') + require(type(encoded) is list and len(encoded) == DIMENSION, '14-coordinate separator') + vector = [rational(value) for value in encoded] + require(all(value >= 0 for value in vector), 'nonnegative separator coordinates') + value = dot(target, vector) + require(value < rows[target], 'separator must strictly violate target') + slacks = [(dot(other, vector)-demand, other) for other, demand in rows.items() if other != target] + require(len(slacks) == ROWS-1 and all(slack >= 0 for slack, _other in slacks), 'separator violates another original inequality') + minimum, tight = min(slacks) + return {'target': hex(target), 'x': [str(value) for value in vector], 'target_lhs': str(value), + 'target_demand': rows[target], 'strict_violation': str(rows[target]-value), + 'other_original_rows_checked': len(slacks), 'minimum_other_slack': str(minimum), + 'minimum_slack_row': hex(tight), 'integral_witness': all(value.denominator == 1 for value in vector)} + + +def verify_certificate(certificate, rows): + retained = certificate_sets(certificate, rows) + deletions = [deletion_check(record, retained, rows) for record in certificate['deletions']] + targets = [mask(record['target']) for record in deletions] + require(len(set(targets)) == len(targets) and set(targets) == rows.keys()-retained, 'complete disjoint deletion coverage') + separators = [separator_check(record, retained, rows) for record in certificate['separators']] + witnessed = [mask(record['target']) for record in separators] + require(len(set(witnessed)) == len(witnessed) and set(witnessed) == retained, 'complete distinct separator coverage') + return {'retained': [hex(value) for value in sorted(retained)], + 'deletions': sorted(deletions, key=lambda item: mask(item['target'])), + 'separators': sorted(separators, key=lambda item: mask(item['target']))} + + +def rejected(callback, expected): + try: + callback() + except ValueError as error: + require(expected in str(error), 'mutation rejected for unexpected reason: ' + str(error)) + return str(error) + raise ValueError('mutated certificate unexpectedly accepted: ' + expected) + + +def negative_controls(certificate, rows, sources, manifest): + controls = {} + bad = deepcopy(certificate) + bad['deletions'][0]['multipliers'][0][1] = '-1' + controls['negative_multiplier'] = rejected(lambda: verify_certificate(bad, rows), 'nonnegative multiplier') + bad = deepcopy(certificate) + term = bad['deletions'][0]['multipliers'][0] + term[1] = str(rational(term[1])+2) + controls['coefficient_overrun'] = rejected(lambda: verify_certificate(bad, rows), 'coefficient exceeds target') + bad = deepcopy(certificate) + for term in bad['deletions'][0]['multipliers']: + term[1] = '0' + controls['zero_rhs'] = rejected(lambda: verify_certificate(bad, rows), 'right-hand side below target demand') + bad = deepcopy(certificate) + bad['deletions'][0]['multipliers'][0][0] = bad['deletions'][0]['target'] + controls['self_premise'] = rejected(lambda: verify_certificate(bad, rows), 'no self or cyclic premise') + bad = deepcopy(certificate) + bad['separators'][0]['x'][0] = '-1' + controls['negative_coordinate'] = rejected(lambda: verify_certificate(bad, rows), 'nonnegative separator coordinates') + bad = deepcopy(certificate) + bad['separators'][0]['x'] = ['8'] * DIMENSION + controls['nonviolating_witness'] = rejected(lambda: verify_certificate(bad, rows), 'strictly violate target') + bad = deepcopy(certificate) + bad['separators'][0]['x'] = ['0'] * DIMENSION + controls['other_row_violation'] = rejected(lambda: verify_certificate(bad, rows), 'another original inequality') + bad = deepcopy(certificate) + bad['separators'].pop() + controls['missing_witness'] = rejected(lambda: verify_certificate(bad, rows), 'separator count') + altered = dict(sources) + altered['RESULT-6425.json'] = b'X'+sources['RESULT-6425.json'][1:] + controls['source_byte_mutation'] = rejected(lambda: authenticate_sources(altered, manifest), 'source SHA256') + controls['duplicate_key'] = rejected(lambda: decode('{"a":1,"a":2}'), 'duplicate JSON key') + controls['nonfinite_json'] = rejected(lambda: decode('{"a":NaN}'), 'nonfinite JSON') + controls['overflowing_json_number'] = rejected(lambda: decode('{"a":1e999}'), 'nonfinite JSON') + controls['noncanonical_rational'] = rejected(lambda: rational('2/4'), 'canonical rational') + controls['exponent_rational'] = rejected(lambda: rational('1e999999999'), 'quotient grammar') + return controls + + +def compute(): + manifest = bounded_read(ROOT / 'SOURCE-PINS.json') + sources = {name: bounded_read(ROOT / 'sources' / name) for name in PINS} + authenticate_sources(sources, manifest) + rows = source_rows(sources['RESULT-6425.json']) + certificate_bytes = bounded_read(ROOT / 'RESULT.json') + certificate = decode(certificate_bytes) + checked = verify_certificate(certificate, rows) + controls = negative_controls(certificate, rows, sources, manifest) + return {'schema_version': 1, 'status': 'PASS_INDEPENDENT_EXACT_FARKAS_CERTIFICATE_CHECK', + 'source_manifest_sha256': MANIFEST_SHA, 'source_result_sha256': PINS['RESULT-6425.json'][1], + 'primary_certificate_sha256': hashlib.sha256(certificate_bytes).hexdigest(), + 'method': 'Independent direct exact-rational checking of sealed primary certificate data; no solver, primary import, clique census or predecessor execution', + 'dimension': DIMENSION, 'source_rows': len(rows), 'retained_rows': len(checked['retained']), + 'removed_rows': len(checked['deletions']), 'checked': checked, 'negative_controls': controls, + 'limits': ['Fixed 14-rectangle nonnegative-real demand system from exact source6425 RESULT only.', + 'Each deletion uses retained source rows only; every retained separator satisfies all other279 original rows.', + 'Fractional separators prove real nonimplication; integral_witness labels an inspected stronger witness, not physical decoder admission.', + 'Source clique census/witness validity and geometry-to-demand equivalence remain credited predecessor results, not rerun here.', + 'No claim of fewest arbitrary inequalities, coefficient synthesis, COPY floor, native realization, kappa or frontier change.']} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = compute() + if args.emit: + print(canonical(result)) + else: + retained = decode(bounded_read(ROOT / 'ORACLE.json')) + require(canonical(retained) == canonical(result), 'strict complete retained oracle receipt mismatch') + print('PASS_INDEPENDENT_EXACT_FARKAS_CERTIFICATE_CHECK') + + +if __name__ == '__main__': + try: + main() + except (ValueError, KeyError, TypeError, OSError) as error: + print('FAIL: ' + str(error), file=sys.stderr) + sys.exit(1) diff --git a/research/p112-farkas-kernel/sources/README-6425.md b/research/p112-farkas-kernel/sources/README-6425.md new file mode 100644 index 0000000000..d9ce3b644c --- /dev/null +++ b/research/p112-farkas-kernel/sources/README-6425.md @@ -0,0 +1,123 @@ +# An exact 280-row P112 demand kernel + +This contribution was produced by Nick Petalas. Claim type: finite certificate +and scoped equivalence proof. No new kappa. + +For the fixed alphabet formed by the union of Jeremy Diviney's PR1422 support +layouts and the eight coordinate rectangles, all 262,928 orthogonal-clique +rank demands are equivalent to 280 saved demands. Exact duplicates leave +14 rectangles in this alphabet. Multiplicities can be any nonnegative real +numbers, in particular any unbounded nonnegative integer counts of terms. + +Equal hit signatures give 1,141 inequalities. Keeping their maximum demands +and deleting rows dominated by a smaller hit set with at least as large a +demand leaves 280. Every retained inequality has a literal orthogonal-clique +witness. Every omitted original inequality has an explicit retained dominator. +[PROOF.md](PROOF.md) gives the equivalence argument; [RESULT.json](RESULT.json) +contains the generated kernel, exact alphabet and deterministic stream hashes. + +This answers Open next question 2 of +[PR1422](https://github.com/CrocSwap/integer-mult-bounds/pull/1422) for a concrete +alphabet. It is a new smaller equivalent necessary-condition system. The source +census, counterexamples, costs and decoder claims are not audit deliverables. +The first strict reduction is the stopping point; no further optimization was +attempted. The broader current card's supplier/invoice task is explicitly changed +to this support-search side result in [TASK.json](TASK.json). + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p112-demand-kernel +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p112-demand-kernel/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p112-demand-kernel/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p112-demand-kernel --check-source-history +``` + +Other machines can substitute their CPython 3.12 path. Expected scientific +marker: `PASS_P112_DEMAND_KERNEL`, with 262,928 complete demands, 1,141 hit +signatures and 280 retained rows. Each registered normal/optimized command +has a 300-second limit. No optional dependency or solver is required. + +The verifier rebuilds every clique with a bitset prefix enumeration and a +separate literal-coordinate tuple enumeration. It checks every original +domination implication, every retained witness and pairwise nondominance. +It exhausts 16,384 binary multiplicity vectors, adds 256 integer vectors, and +checks 3,456 toy equivalence cases. Positive coordinate and known deficient-cap +controls, eight coordinate omissions and six malformed-certificate/domain +controls exercise the screen. A toy case prevents calling pairwise +nondominance full linear-program irredundancy. + +`verify.py --emit` regenerates the certificate on stdout. Normal replay compares +its complete canonical JSON and prints a generated receipt bound to all eight +package-file hashes. No receipt is handwritten. The only live inputs are the +two exact pinned PR1422 JSON files declared in [VERIFY.json](VERIFY.json). +No predecessor executable is imported or replayed. Source/question provenance, +Git blobs and SHA256 hashes are in [SOURCES.json](SOURCES.json). + +## Limits and open obligations + +The theorem concerns the complete cap-based rank-demand screen for exactly +these 14 rectangles. Arbitrary repeated occurrences and independent whole-term +transposes are covered. Actual coefficient zeros or further support trims may +create stricter demands; the frozen cap kernel does not replace that changed +screen. Adding a rectangle or changing caps requires rebuilding the quotient. + +The 280-row family is pairwise nondominated. No smallest-family, facet, +linear-program irredundancy or complete COPY floor is claimed. Passing it does +not provide coefficients or a decoder. No new runtime percentage is claimed. +Physical/native realization, access, dirty restoration, precision/tape, stock, +compiler closure, a complete signed invoice and outer integration are unrun. +The selected frontier and its five framework assumptions are unchanged. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Can nonnegative combinations of other inequalities remove any of the 280 + retained rows? Start with one row and a rational Farkas certificate. Such a + calculation is not supplied, so pairwise nondominance does not settle it. +- Can changed caps pass the complete screen below COPY64 and admit exact + coefficients? Specify the new alphabet and rebuild the complete quotient + before synthesis. This fixed kernel and a support-level pass supply neither + those coefficients nor a fully charged physical construction. + +## Credit and overlap + +Credit Jeremy Diviney / PR1422 for the explicit smaller-family question, complete +clique guard, pinned geometry and saved support caps; Cinna Davis / PR1347 and +PR1323 for the support model and geometry; Navinor, David Arias, Hanson Sun, +DreamingOfClouds, themilkman216 and the retained E8/label/decoder lineage. +Equal-row quotienting and monotone inequality dominance are classical. The +exact smaller system and its finite certificate are the contribution here. +All predecessor files and credits remain unchanged. Apache-2.0 for new material. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361613) +precedes the computation. Live open/account PRs, recent handoffs and local +reservations, main README quantity/formula searches, merged searches and the +cached overlap report were checked. The cache covered 369 open PRs and 6,284 +Discussion records with complete pagination, but only 107 local notes against +8,917 at HEAD. Sparse notes, unpublished work and arbitrary historical code +remain outside that scan. No search absence is a proof of novelty. + +PR5088's changed two-star dictionary and PR5064's changed-completion search +have different alphabets and coefficient objectives. Neither is repriced or +validated here. This result concerns the fixed PR1422 cap-screen inequalities. + +## Verifier constraints + +Functions are shorter than 60 lines. The verifier uses no recursion, subprocess, +network, dynamic evaluation or output files. It caps the geometry at 120 vertices, +cliques at 300,000, alphabet at 16 factors, and each JSON/source read at one MiB. +All loops have bounds from these caps; the actual alphabet has 14 factors. +Unexpected capacity exhaustion raises an error rather than truncating coverage. + +Power-of-ten rule 3 deviation: CPython allocates integers and containers during +checking. The largest live collections are the bounded clique sets and the +current tuple-enumeration level, each capped by 300,000; signature storage is +at most 65,536 rows. These are one-shot exact finite checks, with ordinary scoped +file handles. Fixed allocation would require a separate runtime implementation. +Rule 9 deviation: six rejection callbacks have fixed named local targets and +finite fixtures; unexpected exceptions propagate. Both registered commands use +`-W error` and explicit guards, including under `-O`. No standalone linter was +available; syntax and AST function-length checks supplement those diagnostics. diff --git a/research/p112-farkas-kernel/sources/RESULT-6425.json b/research/p112-farkas-kernel/sources/RESULT-6425.json new file mode 100644 index 0000000000..e18f92e001 --- /dev/null +++ b/research/p112-farkas-kernel/sources/RESULT-6425.json @@ -0,0 +1,1493 @@ +{ + "alphabet": [ + [ + "0xb0d020bb0d020b002801022918080", + "0xffffffff0000000000000003fffffc" + ], + [ + "0x3c3c3c3c3c3c3c3c3fc0f0f03c03c0", + "0x3c3c3c3c3c3c3c3c3fc0f0f03c03c0" + ], + [ + "0xc84c80c83213203214008042898100", + "0xc3c3c3c3c3c3c3c33fc0f0f03c03c0" + ], + [ + "0x3cc3c33cc33c3cc33fcf0f03c03c00", + "0x3cc3c33cc33c3cc33fcf0f03c03c00" + ], + [ + "0xffffffff00000003fffffc", + "0xffffffff00000003fffffc" + ], + [ + "0x92492092924920921204080099a000", + "0xc33c3cc33cc3c33c3fcf0f03c03c00" + ], + [ + "0xffff0000ffff00000ffff003c03c", + "0xffff0000ffff00000ffff003c03c" + ], + [ + "0x7100008ee700001800069690028028", + "0x8e181871187171e725896962596594" + ], + [ + "0x244db224b224dbb229459a629a69a4", + "0x8ee7188e188e7118258699625a5a58" + ], + [ + "0x8e000071180000e700096960014014", + "0x7118188ee7717118258696925aa5a8" + ], + [ + "0xffffffff0000000000000003fffffc", + "0xffffffff0000000000000003fffffc" + ], + [ + "0xff0000ffff0000ff000ffff003c03c", + "0xff0000ffff0000ff000ffff003c03c" + ], + [ + "0xc3c3c3c3c3c3c3c33fc0f0f03c03c0", + "0xc3c3c3c3c3c3c3c33fc0f0f03c03c0" + ], + [ + "0xc33c3cc33cc3c33c3fcf0f03c03c00", + "0xc33c3cc33cc3c33c3fcf0f03c03c00" + ] + ], + "claim_type": "finite certificate and scoped equivalence proof", + "cliques_sha256": "45ab61f97a8751af935b9be1e4c6d5e01557e57b9de604fe6a0089d93b419bf9", + "complete_demands": 262928, + "coordinate_indices": [ + 4, + 10, + 11, + 6, + 12, + 1, + 3, + 13 + ], + "domination_sha256": "5cf7db565816b6146c5222b6e7a70f9ffaf137f75f8e4e22c6284fc941532d55", + "kernel": [ + [ + "0x5a", + 4, + "0x18240000000000000000" + ], + [ + "0xc0a", + 1, + "0x100000000000000000000000" + ], + [ + "0xc50", + 1, + "0x4" + ], + [ + "0xc51", + 2, + "0x8020" + ], + [ + "0xd0a", + 2, + "0x40000100000000000000000000000" + ], + [ + "0xd50", + 2, + "0x4010" + ], + [ + "0xe8a", + 2, + "0x100000200000000000000000000000" + ], + [ + "0xedb", + 6, + "0x180000240000000000010008" + ], + [ + "0xf8a", + 3, + "0x100000240000000000000000000000" + ], + [ + "0xf8b", + 4, + "0x180000240000000000000000000000" + ], + [ + "0xfd0", + 3, + "0x4030" + ], + [ + "0xfd1", + 4, + "0xc030" + ], + [ + "0xfda", + 5, + "0x100024000000000000004020" + ], + [ + "0x1412", + 2, + "0x40200" + ], + [ + "0x1448", + 2, + "0x201000000000000000000000000" + ], + [ + "0x145f", + 6, + "0x201000010200000000000040200" + ], + [ + "0x1513", + 4, + "0x3000c0" + ], + [ + "0x1516", + 4, + "0xc0300" + ], + [ + "0x1549", + 4, + "0x8142000000000000000000000000" + ], + [ + "0x154c", + 4, + "0x4281000000000000000000000000" + ], + [ + "0x155b", + 6, + "0x102000008040000000000100080" + ], + [ + "0x155e", + 6, + "0x4080000008040000000000080100" + ], + [ + "0x1818", + 2, + "0x8100000000000000" + ], + [ + "0x1842", + 1, + "0x10000000" + ], + [ + "0x1942", + 2, + "0x1080000000" + ], + [ + "0x1a98", + 3, + "0x4000008100000000000000" + ], + [ + "0x1a9c", + 4, + "0x4200008100000000000000" + ], + [ + "0x1ac2", + 2, + "0x2080000000" + ], + [ + "0x1ada", + 5, + "0x108004000004010000000" + ], + [ + "0x1ade", + 6, + "0x108204000004010000000" + ], + [ + "0x1bc2", + 3, + "0x3080000000" + ], + [ + "0x1bc6", + 4, + "0x30c0000000" + ], + [ + "0x1c52", + 3, + "0x10200020" + ], + [ + "0x1c59", + 4, + "0x42000000008100000000000000" + ], + [ + "0x1c5c", + 4, + "0x81000000004200000000000000" + ], + [ + "0x1c9b", + 3, + "0x100000000000000200080" + ], + [ + "0x1c9e", + 3, + "0x4000000000000000040100" + ], + [ + "0x1d1a", + 3, + "0x40100000000000000200000" + ], + [ + "0x1d4a", + 3, + "0x40200100000000000000000000000" + ], + [ + "0x1d58", + 3, + "0x1000000000000000000004010" + ], + [ + "0x1e1b", + 3, + "0x100000000200080" + ], + [ + "0x1e1e", + 3, + "0x4000000000040100" + ], + [ + "0x1e9b", + 4, + "0x100000208000004000000000000000" + ], + [ + "0x1eca", + 3, + "0x1200000000000000080000000" + ], + [ + "0x1edf", + 7, + "0x1080000204000004000040008" + ], + [ + "0x1f9a", + 4, + "0x100000200000000100000000000200" + ], + [ + "0x1f9b", + 6, + "0x100000208000004000000000100040" + ], + [ + "0x1f9e", + 6, + "0x100000200200000100000000080200" + ], + [ + "0x1fca", + 4, + "0x40200100000000000000010000000" + ], + [ + "0x1fcb", + 6, + "0x48002100000000000001080000000" + ], + [ + "0x1fce", + 6, + "0x40280100000000000008010000000" + ], + [ + "0x1fd2", + 4, + "0x10200030" + ], + [ + "0x1fd3", + 6, + "0x30300030" + ], + [ + "0x1fd6", + 6, + "0xc00c0030" + ], + [ + "0x1fd8", + 4, + "0x1000000004000000000020008" + ], + [ + "0x1fd9", + 6, + "0x42000000008100000000020008" + ], + [ + "0x1fdb", + 7, + "0x1200000084000001000100008" + ], + [ + "0x1fdc", + 6, + "0x81000000004200000000020008" + ], + [ + "0x1fde", + 7, + "0x40200000080100008000080008" + ], + [ + "0x2418", + 2, + "0x401000" + ], + [ + "0x2442", + 2, + "0x1004000000000000000000000000" + ], + [ + "0x2462", + 3, + "0x1024000000000000000000000000" + ], + [ + "0x2463", + 4, + "0x1824000000000000000000000000" + ], + [ + "0x247a", + 5, + "0x20000020080000000001000400" + ], + [ + "0x247b", + 6, + "0x820000010040000000000802000" + ], + [ + "0x2518", + 3, + "0x1000c00" + ], + [ + "0x2519", + 4, + "0x3000c00" + ], + [ + "0x2542", + 3, + "0x2018000000000000000000000000" + ], + [ + "0x2543", + 4, + "0x2418000000000000000000000000" + ], + [ + "0x255a", + 5, + "0x10000020080000000000401000" + ], + [ + "0x255b", + 6, + "0x410000010040000000002000800" + ], + [ + "0x2812", + 2, + "0x2400000000000000" + ], + [ + "0x2848", + 2, + "0x20400000000" + ], + [ + "0x2912", + 3, + "0x800002400000000000000" + ], + [ + "0x2932", + 4, + "0x1800002400000000000000" + ], + [ + "0x295a", + 5, + "0x4082000080100000000" + ], + [ + "0x297a", + 6, + "0x1004082000080100000000" + ], + [ + "0x2ada", + 5, + "0x410000800080100000000" + ], + [ + "0x2afa", + 6, + "0x410200800080100000000" + ], + [ + "0x2bc8", + 3, + "0x30400000000" + ], + [ + "0x2be8", + 4, + "0x30c00000000" + ], + [ + "0x2c1b", + 3, + "0x80400000000000000001000" + ], + [ + "0x2c3a", + 3, + "0x100000000400000001000000" + ], + [ + "0x2c4a", + 3, + "0x4200000000000010000000000" + ], + [ + "0x2c52", + 3, + "0x4000000000800000000000008" + ], + [ + "0x2c58", + 3, + "0x101000010" + ], + [ + "0x2d1a", + 4, + "0x40400000000000001000800" + ], + [ + "0x2d3a", + 5, + "0x40000100000000400000001000800" + ], + [ + "0x2d3b", + 6, + "0x40000101000000400000001000800" + ], + [ + "0x2d52", + 4, + "0x4000000000800000000020008" + ], + [ + "0x2d72", + 5, + "0x24000000000800000000020008" + ], + [ + "0x2d73", + 6, + "0x24000000001800000000020008" + ], + [ + "0x2d7b", + 7, + "0x4101004000000080000004800" + ], + [ + "0x2dca", + 4, + "0x2010040000000000000200000000" + ], + [ + "0x2dd8", + 4, + "0x400020c00" + ], + [ + "0x2eca", + 4, + "0x4200000000000010400000000" + ], + [ + "0x2ed3", + 4, + "0x1000000000002400000000000020" + ], + [ + "0x2eea", + 5, + "0x100004200000000000010400000000" + ], + [ + "0x2eeb", + 6, + "0x100804200000000000010400000000" + ], + [ + "0x2ef3", + 6, + "0x1800000000002400000000008020" + ], + [ + "0x2efb", + 7, + "0x4100000200800080000400008" + ], + [ + "0x2f4a", + 4, + "0x42010000000000000010000000000" + ], + [ + "0x2f58", + 4, + "0x80000004c00" + ], + [ + "0x2f9b", + 6, + "0x80000202000000800000002000400" + ], + [ + "0x2fca", + 5, + "0x2010040000000000080200000000" + ], + [ + "0x2fcb", + 6, + "0x42010080000000000010400000000" + ], + [ + "0x2fd2", + 5, + "0x18000000000400000000020008" + ], + [ + "0x2fd3", + 6, + "0x18000000002400000000020008" + ], + [ + "0x2fd8", + 5, + "0x301000030" + ], + [ + "0x2fd9", + 6, + "0x303000030" + ], + [ + "0x2fda", + 6, + "0x4200000100800010000000008" + ], + [ + "0x2fdb", + 7, + "0x4200000100800010002000008" + ], + [ + "0x300a", + 1, + "0x400000000000" + ], + [ + "0x302a", + 2, + "0xa000000000000" + ], + [ + "0x3050", + 1, + "0x20000000000000000" + ], + [ + "0x3070", + 2, + "0x40800000000000000000" + ], + [ + "0x307e", + 6, + "0x42240006000000000000" + ], + [ + "0x310a", + 3, + "0x20c00000000000" + ], + [ + "0x312e", + 4, + "0xf000000000000" + ], + [ + "0x3150", + 3, + "0x80420000000000000000" + ], + [ + "0x315a", + 5, + "0x24810000800000000000" + ], + [ + "0x3174", + 4, + "0x42810000000000000000" + ], + [ + "0x341b", + 3, + "0x800000201000" + ], + [ + "0x341e", + 3, + "0x400001000100" + ], + [ + "0x343a", + 3, + "0x400000202000" + ], + [ + "0x344a", + 3, + "0x1001000000000008000000000000" + ], + [ + "0x344b", + 4, + "0x1042000000000000400000000000" + ], + [ + "0x344e", + 4, + "0x1081000000000008000000000000" + ], + [ + "0x3452", + 3, + "0x4000000020000000000200000" + ], + [ + "0x3453", + 4, + "0x4000000020000000000200080" + ], + [ + "0x3456", + 4, + "0x4000000800000000000040100" + ], + [ + "0x3459", + 3, + "0x2000000800000000000000400" + ], + [ + "0x345b", + 5, + "0x1000000080008000001000080" + ], + [ + "0x345c", + 3, + "0x1000002000000000000400000" + ], + [ + "0x345e", + 5, + "0x40000000080000400001000100" + ], + [ + "0x346f", + 6, + "0x1842000000000010400000000000" + ], + [ + "0x3477", + 6, + "0x804000001020000000000200080" + ], + [ + "0x3478", + 3, + "0x1000000800000000000002000" + ], + [ + "0x347f", + 7, + "0x204000040200004000000041000" + ], + [ + "0x351a", + 4, + "0x1000000200c00" + ], + [ + "0x351f", + 6, + "0xc00003000300" + ], + [ + "0x353b", + 6, + "0xc00000303000" + ], + [ + "0x353e", + 6, + "0xc0000000c3000" + ], + [ + "0x354a", + 4, + "0x218000000000000400000000000" + ], + [ + "0x354f", + 6, + "0x2442000000000005000000000000" + ], + [ + "0x3552", + 4, + "0x2010000000020000000000000200" + ], + [ + "0x3557", + 6, + "0x408000002010000000000200080" + ], + [ + "0x3558", + 4, + "0x1000000400000000001000800" + ], + [ + "0x355d", + 6, + "0x280000080020000000002000400" + ], + [ + "0x355f", + 7, + "0x204000004020004000002000080" + ], + [ + "0x356b", + 6, + "0x811800000000000a000000000000" + ], + [ + "0x356e", + 6, + "0x4218000000000010400000000000" + ], + [ + "0x3573", + 6, + "0x1020000080400000000000100040" + ], + [ + "0x3576", + 6, + "0x1020000002010000000000080200" + ], + [ + "0x3579", + 6, + "0x140000040010000000001000800" + ], + [ + "0x357b", + 7, + "0x104000008020020000000400080" + ], + [ + "0x357c", + 6, + "0x4001000001400000000001000800" + ], + [ + "0x357e", + 7, + "0x1040000004010010000000080800" + ], + [ + "0x383a", + 4, + "0x810a000000000000" + ], + [ + "0x3852", + 3, + "0x20400004000000000" + ], + [ + "0x3858", + 3, + "0x80000100080000000000" + ], + [ + "0x386a", + 3, + "0x2004100000000" + ], + [ + "0x393a", + 5, + "0x80000810a000000000000" + ], + [ + "0x393e", + 6, + "0x1800004210400000000000" + ], + [ + "0x3952", + 5, + "0x80020400004020000000" + ], + [ + "0x395a", + 6, + "0x80080108080020000000" + ], + [ + "0x3976", + 6, + "0x402801000008010000000" + ], + [ + "0x397e", + 7, + "0x108801008040010000000" + ], + [ + "0x399e", + 4, + "0x2400000005000000000000" + ], + [ + "0x39ce", + 4, + "0xc08400000000" + ], + [ + "0x39d8", + 4, + "0x180400000000400000000" + ], + [ + "0x39ea", + 4, + "0xc40080000000" + ], + [ + "0x3aca", + 3, + "0x404400000000" + ], + [ + "0x3ada", + 6, + "0x180000400804400000000" + ], + [ + "0x3af8", + 4, + "0x4000008000010400000000" + ], + [ + "0x3afe", + 7, + "0x140200802004100000000" + ], + [ + "0x3b1e", + 4, + "0x2405000000000000" + ], + [ + "0x3b4e", + 4, + "0xc80040000000" + ], + [ + "0x3b58", + 4, + "0x80400100080000000000" + ], + [ + "0x3b6a", + 4, + "0xc04800000000" + ], + [ + "0x3b9a", + 4, + "0x100000420800000000000" + ], + [ + "0x3b9e", + 5, + "0x100002420800000000000" + ], + [ + "0x3bca", + 5, + "0x20003300000000" + ], + [ + "0x3bd8", + 5, + "0x80400100080200000000" + ], + [ + "0x3bee", + 6, + "0xc0cc00000000" + ], + [ + "0x3bfc", + 6, + "0x140800200040100000000" + ], + [ + "0x3c01", + 1, + "0x10000000000000000000000" + ], + [ + "0x3c04", + 1, + "0x400000000000000000000000" + ], + [ + "0x3c0b", + 2, + "0x10000000008000000000000" + ], + [ + "0x3c0e", + 2, + "0x400000000000400000000000" + ], + [ + "0x3c13", + 3, + "0x10000000000000000040200" + ], + [ + "0x3c16", + 3, + "0x400000000000000000200040" + ], + [ + "0x3c1f", + 4, + "0x10000080000000000000000041000" + ], + [ + "0x3c21", + 2, + "0x10000020000000000000000000000" + ], + [ + "0x3c24", + 2, + "0x400000800000000000000000000000" + ], + [ + "0x3c33", + 4, + "0x10000020000000000000000040200" + ], + [ + "0x3c36", + 4, + "0x400000800000000000000000200040" + ], + [ + "0x3c49", + 3, + "0x8040010000000000000000000000" + ], + [ + "0x3c4c", + 3, + "0x201400000000000000000000000" + ], + [ + "0x3c54", + 2, + "0x400000800000000000000000" + ], + [ + "0x3c69", + 4, + "0x18040020000000000000000000000" + ], + [ + "0x3c6c", + 4, + "0x400201800000000000000000000000" + ], + [ + "0x3c75", + 3, + "0x10000020000000000010000" + ], + [ + "0x3c99", + 3, + "0x10000000000000000000000401000" + ], + [ + "0x3c9c", + 3, + "0x400000000000000000000000401000" + ], + [ + "0x3caf", + 3, + "0x20000000006000000000000" + ], + [ + "0x3cc3", + 3, + "0x12008000000000000000000000000" + ], + [ + "0x3cc6", + 3, + "0x402008000000000000000000000000" + ], + [ + "0x3d1b", + 5, + "0x10000044000000000000000040800" + ], + [ + "0x3d1e", + 5, + "0x40000400000000100000000200800" + ], + [ + "0x3d37", + 6, + "0x10000022000001000000000040200" + ], + [ + "0x3d3f", + 7, + "0x10000044000001010000000040800" + ], + [ + "0x3d48", + 3, + "0x201000000000000000200000000" + ], + [ + "0x3d68", + 4, + "0x201000000000000010800000000" + ], + [ + "0x3d77", + 7, + "0x4020000801000008000040008" + ], + [ + "0x3d7f", + 8, + "0x1080000801008040000040008" + ], + [ + "0x3d8f", + 4, + "0x10000080000000009000000000000" + ], + [ + "0x3dab", + 4, + "0x100000020000000020400000000000" + ], + [ + "0x3dbc", + 4, + "0x400000000200000000000000401000" + ], + [ + "0x3dc6", + 4, + "0x402008000000000000008000000000" + ], + [ + "0x3dcb", + 5, + "0x2001000000000020001200000000" + ], + [ + "0x3dce", + 5, + "0x204000000000001008200000000" + ], + [ + "0x3dea", + 5, + "0x100208000000000000440000000000" + ], + [ + "0x3df1", + 4, + "0x20000810000000000000008" + ], + [ + "0x3df8", + 5, + "0x1000000800000040000400008" + ], + [ + "0x3e19", + 3, + "0x10000000000000000401000" + ], + [ + "0x3e1c", + 3, + "0x400000000000000000401000" + ], + [ + "0x3e2f", + 3, + "0x10000000010800000000000" + ], + [ + "0x3e43", + 3, + "0x2008010000000000000000000000" + ], + [ + "0x3e46", + 3, + "0x2008400000000000000000000000" + ], + [ + "0x3e85", + 2, + "0x10000400000000000000000000000" + ], + [ + "0x3ea5", + 4, + "0x420000810000000000000000000000" + ], + [ + "0x3eab", + 3, + "0x10000100000000008000000000000" + ], + [ + "0x3eae", + 3, + "0x100000400000000000400000000000" + ], + [ + "0x3ec7", + 4, + "0x10000400000000000004010000000" + ], + [ + "0x3ecb", + 5, + "0x10040200000000000010010000000" + ], + [ + "0x3ece", + 5, + "0x200001400000000000004200000000" + ], + [ + "0x3ed3", + 5, + "0x10400020000000080000080" + ], + [ + "0x3ed6", + 5, + "0x400400800000000010000100" + ], + [ + "0x3ee6", + 4, + "0x20400000000000004010000000" + ], + [ + "0x3ee7", + 6, + "0x10820400000000000004010000000" + ], + [ + "0x3eef", + 7, + "0x10840200000000010010010000000" + ], + [ + "0x3ef1", + 3, + "0x10040000000000000000020" + ], + [ + "0x3ef4", + 3, + "0x400001000000000000000020" + ], + [ + "0x3ef7", + 7, + "0x800010040002000000080040020" + ], + [ + "0x3eff", + 8, + "0x420000240006000000010008" + ], + [ + "0x3f0f", + 4, + "0x80000010000000009000000000000" + ], + [ + "0x3f2b", + 4, + "0x20000100000000020400000000000" + ], + [ + "0x3f3c", + 4, + "0x400000000200000000401000" + ], + [ + "0x3f46", + 4, + "0x2008400000000000000040000000" + ], + [ + "0x3f4b", + 5, + "0x2001000000000020010020000000" + ], + [ + "0x3f4e", + 5, + "0x204000000000001010040000000" + ], + [ + "0x3f6a", + 5, + "0x208100000000000400800000000" + ], + [ + "0x3f71", + 4, + "0x20000000000810000000000000010" + ], + [ + "0x3f78", + 5, + "0x1000000800000000800400010" + ], + [ + "0x3f8e", + 4, + "0x240000400000000004000000000000" + ], + [ + "0x3f9d", + 6, + "0x10000404000000100000002000800" + ], + [ + "0x3f9f", + 7, + "0x10000080800000108000002000080" + ], + [ + "0x3faf", + 6, + "0x180000420000000020400000000000" + ], + [ + "0x3fb3", + 6, + "0x10000020800000400000000100080" + ], + [ + "0x3fb6", + 6, + "0x400000800800000400000000080100" + ], + [ + "0x3fbb", + 7, + "0x10000104000000401000000100800" + ], + [ + "0x3fbe", + 7, + "0x100000400400000120000000080800" + ], + [ + "0x3fc7", + 6, + "0x12008400000000000001040000000" + ], + [ + "0x3fcf", + 7, + "0x12040080000000001010040000000" + ], + [ + "0x3fd4", + 4, + "0x400000810000000000000008" + ], + [ + "0x3fd7", + 7, + "0x8010000402000008000040008" + ], + [ + "0x3fdd", + 7, + "0x2400000800100020002000008" + ], + [ + "0x3fdf", + 8, + "0x30c3000c00" + ], + [ + "0x3fe9", + 6, + "0x18040020000000000010800000000" + ], + [ + "0x3feb", + 7, + "0x18008100000000008001800000000" + ], + [ + "0x3fec", + 6, + "0x400201800000000000010800000000" + ], + [ + "0x3fee", + 7, + "0x40210800000000010010010000000" + ], + [ + "0x3ff3", + 7, + "0x10020000800400002000100008" + ], + [ + "0x3ff5", + 6, + "0x420000810000000000010008" + ], + [ + "0x3ff6", + 7, + "0x10800000020400004000080008" + ], + [ + "0x3ff9", + 7, + "0x40010000028000040000400008" + ], + [ + "0x3ffb", + 8, + "0x3300303000" + ], + [ + "0x3ffc", + 7, + "0x1400000800200040000400008" + ], + [ + "0x3ffe", + 8, + "0xc3000c3000" + ] + ], + "kernel_by_demand": { + "1": 7, + "2": 21, + "3": 57, + "4": 71, + "5": 34, + "6": 57, + "7": 28, + "8": 5 + }, + "kernel_rows": 280, + "multiplicity_checks": 16640, + "new_kappa": null, + "quotient_sha256": "d1cd0103c426ed1465d88c6f4c973a7d86e3329591efd0489a500689a6aa8a07", + "signature_rows": 1141, + "status": "PASS_P112_DEMAND_KERNEL", + "toy_equivalence_checks": 3456 +} diff --git a/research/p112-farkas-kernel/verify.py b/research/p112-farkas-kernel/verify.py new file mode 100644 index 0000000000..9bf5c3813a --- /dev/null +++ b/research/p112-farkas-kernel/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Exact nonnegative-combination reduction of one frozen280-row real system. + +Source: Nick Petalas/PR6425 and retained PR1422/support lineage. New certificate +generator: ToikY with OpenAI Codex assistance. Simplex/Farkas methods classical. +Apache-2.0. No author executable, optional dependency or floating LP is used. +""" +import argparse +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path +import sys +import time + +HERE = Path(__file__).resolve().parent +MANIFEST_SHA = 'd9d9e3785d6496adf112ccafbe25689057e9a1f28384ca28a536660c9f55f6e9' +DIMENSION, ROWS, OUTSIDE = 14, 280, 8 +CAPS = {'seconds': 120, 'per_target_pivots': 2000, 'total_pivots': 100000, + 'coefficient_bits': 4096} + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), allow_nan=False) + + +def decode(raw): + def unique(items): + out = {} + for key, value in items: + require(key not in out, 'duplicate JSON key') + out[key] = value + return out + def bad(value): + raise ValueError('nonfinite JSON value: ' + value) + return json.loads(raw, object_pairs_hook=unique, parse_constant=bad) + + +def source(): + manifest = (HERE / 'SOURCE-PINS.json').read_bytes() + require(hashlib.sha256(manifest).hexdigest() == MANIFEST_SHA, 'source manifest SHA256') + pins = decode(manifest)['files'] + require(set(pins) == {'README-6425.md', 'RESULT-6425.json'}, 'two frozen source objects') + raw = {} + for name, pin in pins.items(): + data = (HERE / 'sources' / name).read_bytes() + require(len(data) == pin['bytes'], 'source byte length: ' + name) + require(hashlib.sha256(data).hexdigest() == pin['sha256'], 'source SHA256: ' + name) + require(hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() == pin['git_blob'], 'source Git blob: ' + name) + raw[name] = data + obj = decode(raw['RESULT-6425.json']) + require(type(obj.get('kernel_rows')) is int and obj['kernel_rows'] == ROWS, '280 original rows') + require(type(obj.get('alphabet')) is list and len(obj['alphabet']) == DIMENSION, '14-variable source alphabet') + for rectangle in obj['alphabet']: + require(type(rectangle) is list and len(rectangle) == 2, 'source rectangle pair') + for cap in rectangle: + require(type(cap) is str and cap == hex(int(cap, 16)) and int(cap, 16) > 0, 'canonical nonempty cap') + rows = {} + require(type(obj['kernel']) is list and len(obj['kernel']) == ROWS, 'literal kernel array') + for entry in obj['kernel']: + require(type(entry) is list and len(entry) == 3, 'source row/witness schema') + text, demand, witness = entry + require(type(text) is str and text == hex(int(text, 16)), 'canonical source support') + mask = int(text, 16) + require(0 < mask < (1 << DIMENSION) and mask not in rows, 'unique nonempty14-bit support') + require(type(demand) is int and 1 <= demand <= OUTSIDE, 'integer source demand1..8') + require(type(witness) is str and witness == hex(int(witness, 16)) and int(witness, 16) > 0, 'literal source witness identifier') + rows[mask] = demand + return rows + + +def order(mask): + return mask.bit_count(), mask + + +def bits(mask): + return [k for k in range(DIMENSION) if mask & (1 << k)] + + +def dot(mask, x): + return sum((x[k] for k in bits(mask)), F(0)) + + +class Budget: + def __init__(self): + self.started = time.monotonic() + self.total = 0 + self.counts = [] + + def check(self, target_count): + require(time.monotonic() - self.started <= CAPS['seconds'], 'UNKNOWN: exact solver time cap') + require(target_count <= CAPS['per_target_pivots'] and self.total <= CAPS['total_pivots'], 'UNKNOWN: exact solver pivot cap') + + def pivot(self, tableau, count): + self.total += 1 + self.check(count) + require(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length()) <= CAPS['coefficient_bits'] for row in tableau for x in row), 'UNKNOWN: coefficient bit cap') + + +def pivot(tableau, costs, basis, leaving, entering): + factor = tableau[leaving][entering] + row = [x / factor for x in tableau[leaving]] + tableau[leaving] = row + for k in range(len(tableau)): + if k != leaving and tableau[k][entering]: + multiplier = tableau[k][entering] + tableau[k] = [a - multiplier * b for a, b in zip(tableau[k], row)] + multiplier = costs[entering] + increment = multiplier * row[-1] + costs[:] = [a - multiplier * b for a, b in zip(costs, row[:-1])] + basis[leaving] = entering + return increment + + +def packing(mask, demand, donors, rows, budget): + coordinates = bits(mask) + m, n = len(coordinates), len(donors) + tableau = [[F(int(bool(donor & (1 << k)))) for donor in donors] + + [F(int(j == r)) for j in range(m)] + [F(1)] + for r, k in enumerate(coordinates)] + costs = [F(rows[donor]) for donor in donors] + [F(0)] * m + basis, value, count = list(range(n, n + m)), F(0), 0 + while True: + budget.check(count) + weights = {donors[v]: tableau[r][-1] for r, v in enumerate(basis) if v < n and tableau[r][-1]} + require(all(weight > 0 for weight in weights.values()), 'feasible basic weights') + require(value == sum((rows[d] * w for d, w in weights.items()), F(0)), 'exact primal objective accounting') + if value >= demand: + budget.counts.append((mask, count)) + return weights, None + entering = next((j for j, c in enumerate(costs) if j not in basis and c > 0), None) + if entering is None: + dual = [-costs[n + r] for r in range(m)] + require(all(x >= 0 for x in dual), 'dual nonnegative') + require(all(sum((dual[r] for r, k in enumerate(coordinates) if d & (1 << k)), F(0)) >= rows[d] for d in donors), 'dual covers every retained donor') + require(sum(dual, F(0)) == value < demand, 'exact primal-dual optimum and strict gap') + budget.counts.append((mask, count)) + return None, dual + choices = [(row[-1] / row[entering], basis[r], r) for r, row in enumerate(tableau) if row[entering] > 0] + require(choices, 'UNKNOWN: unexpected unbounded nonempty-support packing') + leaving = min(choices)[2] + value += pivot(tableau, costs, basis, leaving, entering) + require(all(row[-1] >= 0 for row in tableau), 'primal feasibility after exact pivot') + count += 1 + budget.pivot(tableau + [costs + [value]], count) + + +def deletion_check(target, multipliers, retained, rows): + require(target in rows and target not in retained, 'deletion target outside retained set') + coverage = [F(0)] * DIMENSION + demand = F(0) + for donor, weight in multipliers.items(): + require(donor in retained and donor in rows and donor != target and weight >= 0, 'nonnegative final-retained donor') + demand += weight * rows[donor] + for k in bits(donor): + coverage[k] += weight + require(all(x <= int(bool(target & (1 << k))) for k, x in enumerate(coverage)), 'Farkas coefficient overflow') + require(demand >= rows[target], 'Farkas demand shortfall') + return coverage, demand + + +def separator_check(target, x, rows): + require(target in rows and len(x) == DIMENSION and all(value >= 0 for value in x), 'nonnegative14-variable separator') + require(all(dot(mask, x) >= demand for mask, demand in rows.items() if mask != target), 'separator violates another original row') + require(dot(target, x) < rows[target], 'separator must strictly violate target') + + +def generate(rows): + retained, deletions, separators = [], [], [] + budget = Budget() + for mask in sorted(rows, key=order): + donors = [d for d in retained if d != mask and d & mask == d] + weights, dual = packing(mask, rows[mask], donors, rows, budget) + if weights is not None: + deletion_check(mask, weights, set(retained), rows) + deletions.append((mask, weights)) + else: + x = [F(OUTSIDE)] * DIMENSION + for k, value in zip(bits(mask), dual): + x[k] = value + separator_check(mask, x, rows) + retained.append(mask) + separators.append((mask, x)) + final = set(retained) + require(len(retained) + len(deletions) == len(rows), 'complete source row partition') + for mask, weights in deletions: + deletion_check(mask, weights, final, rows) + for mask, x in separators: + separator_check(mask, x, rows) + return retained, deletions, separators, budget + + +def rejects(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('corrupted certificate accepted') + + +def controls(rows, retained, deletions, separators): + toy = {1: 1, 2: 1, 3: 2} + weights, dual = packing(3, 2, [1, 2], toy, Budget()) + require(weights == {1: F(1), 2: F(1)} and dual is None, 'nontrivial two-row combination fixture') + deletion_check(3, weights, {1, 2}, toy) + toy = {1: 1, 3: 1} + weights, dual = packing(1, 1, [], toy, Budget()) + require(weights is None and dual == [F(0)], 'restricted support fixture optimum') + x = [F(8)] * DIMENSION + x[0] = F(0) + separator_check(1, x, toy) + outside_error = rejects(lambda: separator_check(1, [F(0)] * DIMENSION, toy)) + target, original = separators[0] + changed = list(original) + k = bits(target)[0] + changed[k] += rows[target] + strict_error = rejects(lambda: separator_check(target, changed, rows)) + result = {'two_row_combination': {'target': '0x3', 'multipliers': [['0x1', '1'], ['0x2', '1']]}, + 'outside_extension_required': {'restricted_zero_point_error': outside_error}, + 'actual_separator_made_target_feasible': {'target': hex(target), 'coordinate': k, 'observed_error': strict_error}} + if deletions: + target, original = deletions[0] + total = sum((rows[d] * w for d, w in original.items()), F(0)) + changed = {d: w * F(rows[target], 2) / total for d, w in original.items()} + error = rejects(lambda: deletion_check(target, changed, set(retained), rows)) + coverage, _total = deletion_check(target, original, set(retained), rows) + factor = F(2) / max(coverage) + excessive = {d: w * factor for d, w in original.items()} + overflow = rejects(lambda: deletion_check(target, excessive, set(retained), rows)) + result['actual_combination_half_demand'] = {'target': hex(target), 'observed_error': error, 'mutant_rhs': str(F(rows[target], 2))} + result['actual_combination_coefficient_overflow'] = {'target': hex(target), 'observed_error': overflow} + return result + + +def run(): + rows = source() + retained, deletions, separators, budget = generate(rows) + return {'schema_version': 1, 'source_manifest_sha256': MANIFEST_SHA, + 'dimension': DIMENSION, 'source_rows': len(rows), + 'retained': [hex(mask) for mask in retained], + 'deletions': [{'target': hex(mask), 'multipliers': [[hex(d), str(w)] for d, w in sorted(weights.items(), key=lambda item: order(item[0]))]} for mask, weights in deletions], + 'separators': [{'target': hex(mask), 'x': list(map(str, x))} for mask, x in separators], + 'counts': {'retained': len(retained), 'deleted': len(deletions), 'strict_separators': len(separators)}, + 'pivot_statistics': {'total': budget.total, 'maximum_per_target': max((n for _mask, n in budget.counts), default=0), + 'per_target': [[hex(mask), n] for mask, n in budget.counts]}, + 'declared_caps': CAPS, 'controls': controls(rows, retained, deletions, separators), + 'method': 'Exact Fraction packing simplex; feasible slack basis and Bland entering/leaving rules, including nonbasic slacks. Early feasible deletion certificates need no optimality claim.', + 'limits': ['Equivalence and irredundancy of this frozen real nonnegative-variable system only; retained separators may be fractional, so integer irredundancy is not claimed.', + 'Original clique census, support geometry and source280-row equivalence remain credited PR6425 premises, not independently replayed here.', + 'No globally smallest arbitrary inequality description, new cap alphabet, coefficients/decoder, physical COPY bound, kappa, native/outer admission or frontier change.']} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = run() + if args.emit: + print(canonical(result)) + else: + path = HERE / 'RESULT.json' + require(path.is_file(), 'retained RESULT.json required') + observed = decode(path.read_bytes()) + require(type(observed) is dict and type(observed.get('schema_version')) is int and observed['schema_version'] == 1, 'typed certificate receipt schema') + require(canonical(observed) == canonical(result), 'strict retained complete certificate') + print('PASS_P112_FARKAS_KERNEL') + + +if __name__ == '__main__': + main()