diff --git a/research/p112-integer-demand-kernel/NOTICE b/research/p112-integer-demand-kernel/NOTICE new file mode 100644 index 0000000000..2329bb2b20 --- /dev/null +++ b/research/p112-integer-demand-kernel/NOTICE @@ -0,0 +1,16 @@ +New integer projection, certificate generation/checking and package metadata: +ToikY with substantial OpenAI Codex assistance. Apache-2.0. + +Three source objects are retained verbatim and authenticated by SOURCE-PINS.json: +- MATRIX-6425.json: Nick Petalas's PR6425 fixed280-row/14-variable P112 kernel. +- REAL-RESULT-6455.json: ToikY/OpenAI Codex PR6455 exact real-domain certificate. +- README-6455.md: PR6455 scope, attribution and open integer-only question. + +Retain credit to Jeremy Diviney/PR1422 for the original smaller-family question, +complete-clique guard, geometry and support caps; Cinna Davis/PR1347/1323, Navinor, +David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the retained +E8/label/decoder lineage. All earlier source headers and credits remain. + +No predecessor executable or scientific clique census is replayed. Weak +compositions/stars-and-bars, monotonicity and finite integer implication are +classical; no general mathematical priority is claimed. diff --git a/research/p112-integer-demand-kernel/ORACLE.json b/research/p112-integer-demand-kernel/ORACLE.json new file mode 100644 index 0000000000..bfe79c8961 --- /dev/null +++ b/research/p112-integer-demand-kernel/ORACLE.json @@ -0,0 +1 @@ +{"checked":{"integer_witnesses":[{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x5a","target_demand":4,"target_lhs":0,"x":[8,0,8,0,0,8,0,8,8,8,8,8,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xc0a","target_demand":1,"target_lhs":0,"x":[8,0,8,0,8,8,8,8,8,8,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xc50","target_demand":1,"target_lhs":0,"x":[8,8,8,8,0,8,0,8,8,8,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xc51","target_demand":2,"target_lhs":1,"x":[0,8,8,8,1,8,0,8,8,8,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xd0a","target_demand":2,"target_lhs":1,"x":[8,1,8,0,8,8,8,8,0,8,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xd50","target_demand":2,"target_lhs":1,"x":[8,8,8,8,1,8,0,8,0,8,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xe8a","target_demand":2,"target_lhs":1,"x":[8,1,8,0,8,8,8,0,8,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xedb","target_demand":6,"target_lhs":4,"x":[0,2,8,0,2,8,0,0,8,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xf8a","target_demand":3,"target_lhs":2,"x":[8,2,8,0,8,8,8,0,0,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xf8b","target_demand":4,"target_lhs":3,"x":[0,3,8,0,8,8,8,0,0,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xfd0","target_demand":3,"target_lhs":2,"x":[8,8,8,8,2,8,0,0,0,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0xfd1","target_demand":4,"target_lhs":3,"x":[0,8,8,8,3,8,0,0,0,0,0,0,8,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1412","target_demand":2,"target_lhs":0,"x":[8,0,8,8,0,8,8,8,8,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1448","target_demand":2,"target_lhs":0,"x":[8,8,8,0,8,8,0,8,8,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x145f","target_demand":6,"target_lhs":4,"x":[0,2,0,2,0,8,0,8,8,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1513","target_demand":4,"target_lhs":2,"x":[0,2,8,8,0,8,8,8,0,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1516","target_demand":4,"target_lhs":2,"x":[8,2,0,8,0,8,8,8,0,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1549","target_demand":4,"target_lhs":2,"x":[0,8,8,2,8,8,0,8,0,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x154c","target_demand":4,"target_lhs":2,"x":[8,8,0,2,8,8,0,8,0,8,0,8,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1818","target_demand":2,"target_lhs":0,"x":[8,8,8,0,0,8,8,8,8,8,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1842","target_demand":1,"target_lhs":0,"x":[8,0,8,8,8,8,0,8,8,8,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1942","target_demand":2,"target_lhs":1,"x":[8,1,8,8,8,8,0,8,0,8,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1a98","target_demand":3,"target_lhs":2,"x":[8,8,8,2,0,8,8,0,8,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1a9c","target_demand":4,"target_lhs":3,"x":[8,8,0,3,0,8,8,0,8,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1ac2","target_demand":2,"target_lhs":1,"x":[8,1,8,8,8,8,0,0,8,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1ade","target_demand":6,"target_lhs":5,"x":[8,1,0,3,0,8,0,1,8,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1bc2","target_demand":3,"target_lhs":2,"x":[8,2,8,8,8,8,0,0,0,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1bc6","target_demand":4,"target_lhs":3,"x":[8,3,0,8,8,8,0,0,0,0,8,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1c52","target_demand":3,"target_lhs":2,"x":[8,1,8,8,1,8,0,8,8,8,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1c59","target_demand":4,"target_lhs":3,"x":[0,8,8,1,1,8,1,8,8,8,0,0,0,8]},{"origin":"new-integer","other_original_rows_checked":279,"target":"0x1c5c","target_demand":4,"target_lhs":3,"x":[8,8,0,2,1,8,0,8,8,8,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1edf","target_demand":7,"target_lhs":6,"x":[0,0,0,2,2,8,2,0,8,0,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1fcb","target_demand":6,"target_lhs":5,"x":[0,1,8,1,8,8,1,0,2,0,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1fce","target_demand":6,"target_lhs":5,"x":[8,1,0,1,8,8,2,0,1,0,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x1fd3","target_demand":6,"target_lhs":5,"x":[0,1,8,8,2,8,1,0,1,0,0,0,0,8]},{"origin":"new-integer","other_original_rows_checked":279,"target":"0x1fd6","target_demand":6,"target_lhs":5,"x":[8,2,0,8,1,8,1,0,1,0,0,0,0,8]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2418","target_demand":2,"target_lhs":0,"x":[8,8,8,0,0,8,8,8,8,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2442","target_demand":2,"target_lhs":0,"x":[8,0,8,8,8,8,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2462","target_demand":3,"target_lhs":2,"x":[8,2,8,8,8,0,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2463","target_demand":4,"target_lhs":3,"x":[0,3,8,8,8,0,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x247b","target_demand":6,"target_lhs":5,"x":[0,3,8,1,0,0,0,8,8,8,1,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2518","target_demand":3,"target_lhs":2,"x":[8,8,8,2,0,8,8,8,0,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2519","target_demand":4,"target_lhs":3,"x":[0,8,8,3,0,8,8,8,0,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2542","target_demand":3,"target_lhs":2,"x":[8,2,8,8,8,8,0,8,0,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2543","target_demand":4,"target_lhs":3,"x":[0,3,8,8,8,8,0,8,0,8,0,8,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2812","target_demand":2,"target_lhs":0,"x":[8,0,8,8,0,8,8,8,8,8,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2848","target_demand":2,"target_lhs":0,"x":[8,8,8,0,8,8,0,8,8,8,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2912","target_demand":3,"target_lhs":2,"x":[8,2,8,8,0,8,8,8,0,8,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2932","target_demand":4,"target_lhs":3,"x":[8,3,8,8,0,0,8,8,0,8,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x297a","target_demand":6,"target_lhs":5,"x":[8,3,8,1,0,0,0,8,0,8,8,1,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2ada","target_demand":5,"target_lhs":4,"x":[8,2,8,2,0,8,0,0,8,0,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2afa","target_demand":6,"target_lhs":5,"x":[8,3,8,2,0,0,0,0,8,0,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2bc8","target_demand":3,"target_lhs":2,"x":[8,8,8,2,8,8,0,0,0,0,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2be8","target_demand":4,"target_lhs":3,"x":[8,8,8,3,8,0,0,0,0,0,8,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2d3a","target_demand":5,"target_lhs":4,"x":[8,1,8,0,2,0,8,8,1,8,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2d3b","target_demand":6,"target_lhs":5,"x":[0,1,8,1,3,0,8,8,0,8,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2d73","target_demand":6,"target_lhs":5,"x":[0,3,8,8,1,0,1,8,0,8,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2d7b","target_demand":7,"target_lhs":6,"x":[0,2,8,0,2,0,0,8,0,8,0,0,8,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2eca","target_demand":4,"target_lhs":3,"x":[8,1,8,1,8,8,1,0,8,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2ed3","target_demand":4,"target_lhs":3,"x":[0,1,8,8,1,8,1,0,8,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2eea","target_demand":5,"target_lhs":4,"x":[8,1,8,1,8,0,2,0,8,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2eeb","target_demand":6,"target_lhs":5,"x":[0,1,8,1,8,0,3,0,8,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2ef3","target_demand":6,"target_lhs":4,"x":[0,2,8,8,0,0,2,0,8,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2f9b","target_demand":6,"target_lhs":5,"x":[0,1,8,1,1,8,8,0,2,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2fcb","target_demand":6,"target_lhs":5,"x":[0,2,8,1,8,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2fd2","target_demand":5,"target_lhs":4,"x":[8,1,8,8,1,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2fd3","target_demand":6,"target_lhs":5,"x":[0,1,8,8,1,8,2,0,1,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2fd8","target_demand":5,"target_lhs":4,"x":[8,8,8,1,1,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x2fd9","target_demand":6,"target_lhs":5,"x":[0,8,8,1,2,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x300a","target_demand":1,"target_lhs":0,"x":[8,0,8,0,8,8,8,8,8,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x302a","target_demand":2,"target_lhs":1,"x":[8,1,8,0,8,0,8,8,8,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3050","target_demand":1,"target_lhs":0,"x":[8,8,8,8,0,8,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3070","target_demand":2,"target_lhs":1,"x":[8,8,8,8,1,0,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x307e","target_demand":6,"target_lhs":4,"x":[8,2,0,0,2,0,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x310a","target_demand":3,"target_lhs":1,"x":[8,1,8,0,8,8,8,8,0,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x312e","target_demand":4,"target_lhs":3,"x":[8,3,0,0,8,0,8,8,0,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3150","target_demand":3,"target_lhs":1,"x":[8,8,8,8,1,8,0,8,0,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3174","target_demand":4,"target_lhs":3,"x":[8,8,0,8,3,0,0,8,0,8,8,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x344b","target_demand":4,"target_lhs":3,"x":[0,0,8,1,8,8,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x344e","target_demand":4,"target_lhs":3,"x":[8,0,0,1,8,8,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3453","target_demand":4,"target_lhs":3,"x":[0,2,8,8,1,8,0,8,8,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3456","target_demand":4,"target_lhs":3,"x":[8,2,0,8,1,8,0,8,8,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x346f","target_demand":6,"target_lhs":4,"x":[0,2,0,0,8,0,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3477","target_demand":6,"target_lhs":4,"x":[0,2,0,8,0,0,2,8,8,8,0,8,0,0]},{"origin":"new-integer","other_original_rows_checked":279,"target":"0x351f","target_demand":6,"target_lhs":5,"x":[0,1,0,1,2,8,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x353b","target_demand":6,"target_lhs":5,"x":[0,1,8,1,2,0,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x353e","target_demand":6,"target_lhs":5,"x":[8,2,0,1,1,0,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x354f","target_demand":6,"target_lhs":5,"x":[0,1,0,1,8,8,2,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3557","target_demand":6,"target_lhs":5,"x":[0,2,0,8,1,8,1,8,1,8,0,8,0,0]},{"origin":"new-integer","other_original_rows_checked":279,"target":"0x355d","target_demand":6,"target_lhs":5,"x":[0,8,0,2,1,8,1,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3579","target_demand":6,"target_lhs":5,"x":[0,8,8,2,1,0,1,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x357c","target_demand":6,"target_lhs":5,"x":[8,8,0,1,1,0,2,8,1,8,0,8,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x383a","target_demand":4,"target_lhs":3,"x":[8,1,8,1,1,0,8,8,8,8,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3852","target_demand":3,"target_lhs":2,"x":[8,1,8,8,1,8,0,8,8,8,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x393e","target_demand":6,"target_lhs":5,"x":[8,3,0,1,1,0,8,8,0,8,8,0,0,0]},{"origin":"new-integer","other_original_rows_checked":279,"target":"0x3952","target_demand":5,"target_lhs":4,"x":[8,1,8,8,2,8,1,8,0,8,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3976","target_demand":6,"target_lhs":5,"x":[8,1,0,8,1,0,1,8,2,8,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x397e","target_demand":7,"target_lhs":6,"x":[8,2,0,0,2,0,0,8,0,8,8,0,0,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ada","target_demand":6,"target_lhs":5,"x":[8,2,8,2,1,8,0,0,8,0,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3afe","target_demand":7,"target_lhs":6,"x":[8,1,0,1,3,0,1,0,8,0,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3bca","target_demand":5,"target_lhs":4,"x":[8,1,8,1,8,8,1,0,1,0,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3bee","target_demand":6,"target_lhs":5,"x":[8,1,0,1,8,0,1,0,2,0,8,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c01","target_demand":1,"target_lhs":0,"x":[0,8,8,8,8,8,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c04","target_demand":1,"target_lhs":0,"x":[8,8,0,8,8,8,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c21","target_demand":2,"target_lhs":1,"x":[1,8,8,8,8,0,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c24","target_demand":2,"target_lhs":1,"x":[8,8,1,8,8,0,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c33","target_demand":4,"target_lhs":3,"x":[0,1,8,8,0,0,8,8,8,8,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c36","target_demand":4,"target_lhs":3,"x":[8,1,0,8,0,0,8,8,8,8,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c69","target_demand":4,"target_lhs":3,"x":[0,8,8,1,8,0,0,8,8,8,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3c6c","target_demand":4,"target_lhs":3,"x":[8,8,0,1,8,0,0,8,8,8,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3cc3","target_demand":3,"target_lhs":2,"x":[0,1,8,8,8,8,0,0,8,8,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3cc6","target_demand":3,"target_lhs":2,"x":[8,1,0,8,8,8,0,0,8,8,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d37","target_demand":6,"target_lhs":5,"x":[0,3,0,8,0,0,8,8,0,8,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d3f","target_demand":7,"target_lhs":6,"x":[0,1,0,0,2,0,8,8,1,8,0,0,0,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d48","target_demand":3,"target_lhs":2,"x":[8,8,8,2,8,8,0,8,0,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d68","target_demand":4,"target_lhs":3,"x":[8,8,8,3,8,0,0,8,0,8,0,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d77","target_demand":7,"target_lhs":6,"x":[0,2,0,8,2,0,0,8,0,8,0,0,0,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3d8f","target_demand":4,"target_lhs":3,"x":[0,2,0,0,8,8,8,0,0,8,0,0,1,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3dc6","target_demand":4,"target_lhs":3,"x":[8,2,0,8,8,8,0,0,0,8,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3e43","target_demand":3,"target_lhs":2,"x":[0,1,8,8,8,8,0,8,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3e46","target_demand":3,"target_lhs":2,"x":[8,1,0,8,8,8,0,8,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3e85","target_demand":2,"target_lhs":1,"x":[0,8,0,8,8,8,8,0,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ea5","target_demand":4,"target_lhs":2,"x":[0,8,0,8,8,0,8,0,8,0,2,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ec7","target_demand":4,"target_lhs":3,"x":[0,1,0,8,8,8,0,0,8,0,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ecb","target_demand":5,"target_lhs":4,"x":[0,0,8,1,8,8,2,0,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ece","target_demand":5,"target_lhs":4,"x":[8,0,0,1,8,8,2,0,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ed3","target_demand":5,"target_lhs":4,"x":[0,1,8,8,1,8,1,0,8,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ed6","target_demand":5,"target_lhs":4,"x":[8,1,0,8,0,8,0,0,8,0,1,0,1,1]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ee7","target_demand":6,"target_lhs":5,"x":[0,1,0,8,8,0,0,0,8,0,3,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3eef","target_demand":7,"target_lhs":6,"x":[0,2,0,0,8,0,0,0,8,0,2,0,0,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3ef7","target_demand":7,"target_lhs":6,"x":[0,0,0,8,0,0,2,0,8,0,2,0,0,2]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3f0f","target_demand":4,"target_lhs":3,"x":[0,2,0,0,8,8,8,8,0,0,0,0,1,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3f46","target_demand":4,"target_lhs":3,"x":[8,2,0,8,8,8,0,8,0,0,1,0,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3f9d","target_demand":6,"target_lhs":5,"x":[0,8,0,3,0,8,8,0,0,0,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3fb3","target_demand":6,"target_lhs":5,"x":[1,3,8,8,0,0,8,0,0,0,0,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3fb6","target_demand":6,"target_lhs":5,"x":[8,3,1,8,0,0,8,0,0,0,0,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3fc7","target_demand":6,"target_lhs":5,"x":[0,3,0,8,8,8,0,0,0,0,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3fe9","target_demand":6,"target_lhs":5,"x":[0,8,8,3,8,0,0,0,0,0,1,1,0,0]},{"origin":"prior-integral","other_original_rows_checked":279,"target":"0x3fec","target_demand":6,"target_lhs":5,"x":[8,8,0,3,8,0,0,0,0,0,1,1,0,0]}],"new_obstructions":[{"budget":4,"checked_profiles":495,"coordinates":[1,3,4,6,7,9,11,12],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1818",13],["0x1842",5],["0x1a98",9],["0x1ac2",8]],"target":"0x1ada"},{"budget":2,"checked_profiles":45,"coordinates":[0,1,3,4,7,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"target":"0x1c9b"},{"budget":2,"checked_profiles":45,"coordinates":[1,2,3,4,7,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"target":"0x1c9e"},{"budget":2,"checked_profiles":45,"coordinates":[0,1,3,4,9,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"target":"0x1e1b"},{"budget":2,"checked_profiles":45,"coordinates":[1,2,3,4,9,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"target":"0x1e1e"},{"budget":3,"checked_profiles":220,"coordinates":[0,1,3,4,7,9,10,11,12],"expected_profiles":220,"miss_histogram":[["0xc0a",56],["0xe8a",40],["0x1412",80],["0x1818",36],["0x1a98",8]],"target":"0x1e9b"},{"budget":5,"checked_profiles":3003,"coordinates":[0,1,3,4,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc0a",462],["0xd0a",504],["0xe8a",140],["0xf8a",200],["0xf8b",348],["0x1412",633],["0x1513",422],["0x1818",238],["0x1a98",56]],"target":"0x1f9b"},{"budget":5,"checked_profiles":3003,"coordinates":[1,2,3,4,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc0a",462],["0xd0a",504],["0xe8a",140],["0xf8a",200],["0x1412",706],["0x1516",602],["0x1818",252],["0x1a98",77],["0x1a9c",60]],"target":"0x1f9e"},{"budget":5,"checked_profiles":3003,"coordinates":[0,3,4,6,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc50",462],["0xc51",504],["0xd50",224],["0xfd0",240],["0xfd1",300],["0x1448",573],["0x1549",410],["0x1818",234],["0x1a98",56]],"target":"0x1fd9"},{"budget":5,"checked_profiles":3003,"coordinates":[2,3,4,6,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc50",462],["0xd50",504],["0xfd0",280],["0x1448",742],["0x154c",602],["0x1818",264],["0x1a98",83],["0x1a9c",66]],"target":"0x1fdc"},{"budget":4,"checked_profiles":330,"coordinates":[1,3,4,5,6,10,13],"expected_profiles":330,"miss_histogram":[["0x5a",295],["0x2418",13],["0x2442",13],["0x2462",9]],"target":"0x247a"},{"budget":4,"checked_profiles":330,"coordinates":[1,3,4,6,8,11,13],"expected_profiles":330,"miss_histogram":[["0x5a",295],["0x2812",13],["0x2848",13],["0x2912",9]],"target":"0x295a"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,3,4,10,11,13],"expected_profiles":36,"miss_histogram":[["0xc0a",10],["0x2418",19],["0x2812",7]],"target":"0x2c1b"},{"budget":2,"checked_profiles":36,"coordinates":[1,3,4,5,10,11,13],"expected_profiles":36,"miss_histogram":[["0xc0a",10],["0x2418",19],["0x2812",7]],"target":"0x2c3a"},{"budget":2,"checked_profiles":28,"coordinates":[1,3,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc0a",6],["0x2442",15],["0x2848",7]],"target":"0x2c4a"},{"budget":2,"checked_profiles":28,"coordinates":[1,4,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc50",6],["0x2442",15],["0x2812",7]],"target":"0x2c52"},{"budget":2,"checked_profiles":28,"coordinates":[3,4,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc50",6],["0x2418",15],["0x2848",7]],"target":"0x2c58"},{"budget":3,"checked_profiles":120,"coordinates":[1,3,4,8,10,11,13],"expected_profiles":120,"miss_histogram":[["0xc0a",20],["0xd0a",24],["0x2418",42],["0x2518",17],["0x2812",17]],"target":"0x2d1a"},{"budget":3,"checked_profiles":120,"coordinates":[1,4,6,8,10,11,13],"expected_profiles":120,"miss_histogram":[["0xc50",20],["0xd50",24],["0x2442",42],["0x2542",17],["0x2812",17]],"target":"0x2d52"},{"budget":4,"checked_profiles":495,"coordinates":[1,4,5,6,8,10,11,13],"expected_profiles":495,"miss_histogram":[["0xc50",70],["0xd50",80],["0x2442",147],["0x2462",81],["0x2542",20],["0x2812",58],["0x2912",21],["0x2932",18]],"target":"0x2d72"},{"budget":3,"checked_profiles":165,"coordinates":[1,3,6,7,8,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc0a",35],["0xd0a",40],["0x2442",53],["0x2542",20],["0x2848",17]],"target":"0x2dca"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,7,8,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc50",35],["0xd50",40],["0x2418",53],["0x2518",20],["0x2848",17]],"target":"0x2dd8"},{"budget":6,"checked_profiles":12376,"coordinates":[0,1,3,4,5,6,7,9,10,11,13],"expected_profiles":12376,"miss_histogram":[["0x5a",10584],["0xc0a",148],["0xc50",148],["0xc51",244],["0xe8a",184],["0xedb",429],["0x2418",157],["0x2442",157],["0x2462",152],["0x2463",79],["0x247b",22],["0x2812",22],["0x2848",24],["0x2ada",10],["0x2afa",11],["0x2eea",1],["0x2eeb",3],["0x2ef3",1]],"target":"0x2efb"},{"budget":3,"checked_profiles":165,"coordinates":[1,3,6,8,9,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc0a",35],["0xd0a",40],["0x2442",53],["0x2542",20],["0x2848",17]],"target":"0x2f4a"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,8,9,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc50",35],["0xd50",40],["0x2418",53],["0x2518",20],["0x2848",17]],"target":"0x2f58"},{"budget":4,"checked_profiles":715,"coordinates":[1,3,6,7,8,9,10,11,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0xe8a",40],["0xf8a",60],["0x2442",178],["0x2542",70],["0x2848",81],["0x2bc8",12],["0x2eca",8]],"target":"0x2fca"},{"budget":5,"checked_profiles":3003,"coordinates":[1,3,4,6,7,8,9,10,11,13],"expected_profiles":3003,"miss_histogram":[["0x5a",2702],["0xc0a",31],["0xc50",31],["0xd0a",52],["0xd50",52],["0xe8a",8],["0xf8a",46],["0xfd0",36],["0x2418",13],["0x2442",13],["0x2518",11],["0x2542",2],["0x2812",2],["0x2848",2],["0x2912",1],["0x2ada",1]],"target":"0x2fda"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,3,4,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2418",7],["0x300a",3]],"target":"0x341b"},{"budget":2,"checked_profiles":36,"coordinates":[1,2,3,4,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2418",7],["0x300a",3]],"target":"0x341e"},{"budget":2,"checked_profiles":28,"coordinates":[1,3,6,10,12,13],"expected_profiles":28,"miss_histogram":[["0x1448",18],["0x2442",7],["0x300a",3]],"target":"0x344a"},{"budget":2,"checked_profiles":28,"coordinates":[1,4,6,10,12,13],"expected_profiles":28,"miss_histogram":[["0x1412",18],["0x2442",7],["0x3050",3]],"target":"0x3452"},{"budget":2,"checked_profiles":36,"coordinates":[0,3,4,6,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2418",7],["0x3050",3]],"target":"0x3459"},{"budget":4,"checked_profiles":495,"coordinates":[0,1,3,4,6,10,12,13],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1412",13],["0x1448",13],["0x2418",3],["0x2442",3],["0x300a",1],["0x3050",1],["0x344b",1]],"target":"0x345b"},{"budget":2,"checked_profiles":36,"coordinates":[2,3,4,6,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2418",7],["0x3050",3]],"target":"0x345c"},{"budget":4,"checked_profiles":495,"coordinates":[1,2,3,4,6,10,12,13],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1412",13],["0x1448",13],["0x2418",3],["0x2442",3],["0x300a",1],["0x3050",1],["0x344e",1]],"target":"0x345e"},{"budget":6,"checked_profiles":8008,"coordinates":[0,1,2,3,4,5,6,10,12,13],"expected_profiles":8008,"miss_histogram":[["0x5a",6552],["0x1412",356],["0x1448",356],["0x145f",330],["0x2418",88],["0x2442",88],["0x2462",96],["0x2463",60],["0x247b",14],["0x300a",9],["0x302a",13],["0x3050",9],["0x3070",13],["0x307e",19],["0x346f",4],["0x3477",1]],"target":"0x347f"},{"budget":5,"checked_profiles":2002,"coordinates":[0,1,3,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1448",756],["0x1549",600],["0x2442",252],["0x2462",154],["0x2463",90],["0x2542",9],["0x2543",8],["0x300a",49],["0x302a",56],["0x310a",28]],"target":"0x356b"},{"budget":5,"checked_profiles":2002,"coordinates":[1,2,3,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1448",756],["0x154c",600],["0x2442",252],["0x2462",154],["0x2542",18],["0x300a",60],["0x302a",78],["0x310a",54],["0x312e",30]],"target":"0x356e"},{"budget":5,"checked_profiles":2002,"coordinates":[0,1,4,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1412",756],["0x1513",600],["0x2442",252],["0x2462",154],["0x2463",90],["0x2542",9],["0x2543",8],["0x3050",49],["0x3070",56],["0x3150",28]],"target":"0x3573"},{"budget":5,"checked_profiles":2002,"coordinates":[1,2,4,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1412",756],["0x1516",600],["0x2442",252],["0x2462",154],["0x2542",18],["0x3050",60],["0x3070",78],["0x3150",54],["0x3174",30]],"target":"0x3576"},{"budget":2,"checked_profiles":28,"coordinates":[3,4,6,11,12,13],"expected_profiles":28,"miss_histogram":[["0x1818",18],["0x2848",7],["0x3050",3]],"target":"0x3858"},{"budget":2,"checked_profiles":36,"coordinates":[1,3,5,6,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1842",10],["0x2848",19],["0x300a",3],["0x302a",4]],"target":"0x386a"},{"budget":4,"checked_profiles":495,"coordinates":[1,3,4,5,8,11,12,13],"expected_profiles":495,"miss_histogram":[["0x1818",210],["0x2812",111],["0x2912",67],["0x2932",59],["0x300a",19],["0x302a",14],["0x310a",15]],"target":"0x393a"},{"budget":5,"checked_profiles":1287,"coordinates":[1,3,4,6,8,11,12,13],"expected_profiles":1287,"miss_histogram":[["0x5a",1056],["0x1818",65],["0x1842",21],["0x1942",36],["0x2812",28],["0x2848",28],["0x2912",24],["0x300a",4],["0x3050",4],["0x310a",11],["0x3150",8],["0x3952",2]],"target":"0x395a"},{"budget":3,"checked_profiles":220,"coordinates":[1,2,3,6,7,8,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x310a",24]],"target":"0x39ce"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,7,8,11,12,13],"expected_profiles":165,"miss_histogram":[["0x1818",95],["0x2848",37],["0x3050",13],["0x3150",20]],"target":"0x39d8"},{"budget":3,"checked_profiles":220,"coordinates":[1,3,5,6,7,8,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x302a",16],["0x310a",8]],"target":"0x39ea"},{"budget":2,"checked_profiles":45,"coordinates":[1,3,6,7,9,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1842",15],["0x1ac2",12],["0x2848",15],["0x300a",3]],"target":"0x3aca"},{"budget":3,"checked_profiles":220,"coordinates":[3,4,5,6,7,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1818",140],["0x1a98",40],["0x2848",24],["0x3050",10],["0x3070",6]],"target":"0x3af8"},{"budget":3,"checked_profiles":220,"coordinates":[1,2,3,6,8,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x310a",24]],"target":"0x3b4e"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,8,9,11,12,13],"expected_profiles":165,"miss_histogram":[["0x1818",95],["0x2848",37],["0x3050",13],["0x3150",20]],"target":"0x3b58"},{"budget":3,"checked_profiles":220,"coordinates":[1,3,5,6,8,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x302a",16],["0x310a",8]],"target":"0x3b6a"},{"budget":4,"checked_profiles":715,"coordinates":[3,4,6,7,8,9,11,12,13],"expected_profiles":715,"miss_histogram":[["0x1818",350],["0x1a98",100],["0x2848",122],["0x2bc8",27],["0x3050",42],["0x3150",74]],"target":"0x3bd8"},{"budget":1,"checked_profiles":8,"coordinates":[0,1,3,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc0a",4],["0x300a",2],["0x3c01",2]],"target":"0x3c0b"},{"budget":1,"checked_profiles":8,"coordinates":[1,2,3,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc0a",4],["0x300a",2],["0x3c04",2]],"target":"0x3c0e"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,4,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2812",7],["0x3c01",3]],"target":"0x3c13"},{"budget":2,"checked_profiles":36,"coordinates":[1,2,4,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2812",7],["0x3c04",3]],"target":"0x3c16"},{"budget":3,"checked_profiles":220,"coordinates":[0,1,2,3,4,10,11,12,13],"expected_profiles":220,"miss_histogram":[["0xc0a",56],["0x1412",100],["0x1818",44],["0x2418",10],["0x2812",4],["0x300a",3],["0x3c01",3]],"target":"0x3c1f"},{"budget":2,"checked_profiles":36,"coordinates":[0,3,6,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2848",7],["0x3c01",3]],"target":"0x3c49"},{"budget":2,"checked_profiles":36,"coordinates":[2,3,6,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2848",7],["0x3c04",3]],"target":"0x3c4c"},{"budget":1,"checked_profiles":8,"coordinates":[2,4,6,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc50",4],["0x3050",2],["0x3c04",2]],"target":"0x3c54"},{"budget":2,"checked_profiles":45,"coordinates":[0,3,4,7,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c01",3]],"target":"0x3c99"},{"budget":2,"checked_profiles":45,"coordinates":[2,3,4,7,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c04",3]],"target":"0x3c9c"},{"budget":2,"checked_profiles":66,"coordinates":[0,1,2,3,5,7,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc0a",28],["0x300a",13],["0x302a",16],["0x3c01",5],["0x3c21",4]],"target":"0x3caf"},{"budget":4,"checked_profiles":715,"coordinates":[0,1,3,4,8,10,11,12,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0x1412",211],["0x1513",173],["0x1818",50],["0x2418",6],["0x2518",3],["0x2519",4],["0x2912",1],["0x300a",1]],"target":"0x3d1b"},{"budget":4,"checked_profiles":715,"coordinates":[1,2,3,4,8,10,11,12,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0x1412",211],["0x1516",173],["0x1818",50],["0x2418",6],["0x2518",3],["0x2812",2],["0x2912",1],["0x300a",1],["0x310a",2]],"target":"0x3d1e"},{"budget":7,"checked_profiles":50388,"coordinates":[0,1,2,3,4,5,6,8,10,11,12,13],"expected_profiles":50388,"miss_histogram":[["0x5a",41217],["0xc0a",645],["0xc50",645],["0xc51",1040],["0xd0a",1040],["0xd50",312],["0x1412",1077],["0x1448",1077],["0x145f",1127],["0x1513",881],["0x1516",199],["0x1549",632],["0x154c",64],["0x1818",83],["0x1842",21],["0x1942",37],["0x1c52",1],["0x1c5c",2],["0x2418",31],["0x2442",42],["0x2462",49],["0x2463",59],["0x247b",15],["0x2518",9],["0x2519",20],["0x2812",6],["0x2848",6],["0x2912",26],["0x2932",23],["0x2d3b",1],["0x307e",1]],"target":"0x3d7f"},{"budget":3,"checked_profiles":286,"coordinates":[0,1,3,5,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0x300a",29],["0x302a",40],["0x310a",32],["0x3c01",7],["0x3c21",10]],"target":"0x3dab"},{"budget":3,"checked_profiles":286,"coordinates":[2,3,4,5,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1818",196],["0x2418",51],["0x2518",26],["0x3c04",7],["0x3c24",6]],"target":"0x3dbc"},{"budget":4,"checked_profiles":1001,"coordinates":[1,2,3,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x154c",216],["0x1842",22],["0x1942",14],["0x2442",15],["0x2542",3],["0x2848",6],["0x300a",2],["0x310a",3]],"target":"0x3dce"},{"budget":4,"checked_profiles":1001,"coordinates":[1,3,5,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x1842",70],["0x1942",64],["0x2442",63],["0x2462",46],["0x2542",3],["0x2848",18],["0x300a",4],["0x302a",7],["0x310a",4],["0x3d48",1],["0x3d68",1]],"target":"0x3dea"},{"budget":3,"checked_profiles":286,"coordinates":[0,4,5,6,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xc51",84],["0xd50",24],["0x3050",21],["0x3070",30],["0x3150",30],["0x3c01",7],["0x3c21",6]],"target":"0x3df1"},{"budget":4,"checked_profiles":1001,"coordinates":[3,4,5,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc50",210],["0xd50",224],["0x1448",286],["0x1818",166],["0x2418",44],["0x2518",33],["0x2848",18],["0x3050",6],["0x3070",7],["0x3150",4],["0x3d48",1],["0x3d68",2]],"target":"0x3df8"},{"budget":2,"checked_profiles":45,"coordinates":[0,3,4,9,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c01",3]],"target":"0x3e19"},{"budget":2,"checked_profiles":45,"coordinates":[2,3,4,9,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c04",3]],"target":"0x3e1c"},{"budget":2,"checked_profiles":66,"coordinates":[0,1,2,3,5,9,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc0a",28],["0x300a",13],["0x302a",16],["0x3c01",5],["0x3c21",4]],"target":"0x3e2f"},{"budget":3,"checked_profiles":286,"coordinates":[1,2,5,6,7,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1842",84],["0x1ac2",60],["0x2442",95],["0x2462",34],["0x3c04",7],["0x3c24",6]],"target":"0x3ee6"},{"budget":2,"checked_profiles":66,"coordinates":[2,4,5,6,7,9,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc50",28],["0x3050",13],["0x3070",16],["0x3c04",5],["0x3c24",4]],"target":"0x3ef4"},{"budget":3,"checked_profiles":286,"coordinates":[0,1,3,5,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0x300a",29],["0x302a",40],["0x310a",32],["0x3c01",7],["0x3c21",10]],"target":"0x3f2b"},{"budget":3,"checked_profiles":286,"coordinates":[2,3,4,5,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1818",196],["0x2418",51],["0x2518",26],["0x3c04",7],["0x3c24",6]],"target":"0x3f3c"},{"budget":4,"checked_profiles":1001,"coordinates":[1,2,3,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x154c",216],["0x1842",22],["0x1942",14],["0x2442",15],["0x2542",3],["0x2848",6],["0x300a",2],["0x310a",3]],"target":"0x3f4e"},{"budget":4,"checked_profiles":1001,"coordinates":[1,3,5,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x1842",70],["0x1942",64],["0x2442",63],["0x2462",46],["0x2542",3],["0x2848",18],["0x300a",4],["0x302a",7],["0x310a",4],["0x3d48",1],["0x3d68",1]],"target":"0x3f6a"},{"budget":3,"checked_profiles":286,"coordinates":[0,4,5,6,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xc51",84],["0xd50",24],["0x3050",21],["0x3070",30],["0x3150",30],["0x3c01",7],["0x3c21",6]],"target":"0x3f71"},{"budget":4,"checked_profiles":1001,"coordinates":[3,4,5,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc50",210],["0xd50",224],["0x1448",286],["0x1818",166],["0x2418",44],["0x2518",33],["0x2848",18],["0x3050",6],["0x3070",7],["0x3150",4],["0x3d48",1],["0x3d68",2]],"target":"0x3f78"},{"budget":3,"checked_profiles":286,"coordinates":[1,2,3,7,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0xe8a",20],["0xf8a",40],["0x300a",17],["0x310a",34],["0x3c04",7]],"target":"0x3f8e"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,3,4,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1412",3412],["0x1513",2405],["0x1516",585],["0x1818",1083],["0x1a98",313],["0x1a9c",294],["0x2418",51],["0x2518",25],["0x2519",42],["0x2812",12],["0x2912",8],["0x2f9b",3],["0x300a",12],["0x310a",7],["0x351f",6],["0x3c01",3],["0x3e85",2]],"target":"0x3f9f"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,3,4,5,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1412",3412],["0x1513",2405],["0x1818",1417],["0x1a98",403],["0x2418",194],["0x2518",96],["0x2519",92],["0x2812",84],["0x2912",37],["0x2932",60],["0x2d3a",4],["0x2d3b",21],["0x300a",11],["0x302a",10],["0x310a",2],["0x353b",4],["0x3c01",7],["0x3c21",4]],"target":"0x3fbb"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,3,4,5,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0x1412",4006],["0x1516",3322],["0x1818",1501],["0x1a98",466],["0x1a9c",442],["0x2418",169],["0x2518",96],["0x2812",78],["0x2912",40],["0x2932",77],["0x2d3a",11],["0x300a",21],["0x302a",31],["0x310a",10],["0x312e",13],["0x353e",3],["0x3c04",3],["0x3c24",4]],"target":"0x3fbe"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,3,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1448",3412],["0x1549",2405],["0x154c",585],["0x1842",427],["0x1942",284],["0x1ac2",190],["0x1bc2",138],["0x1bc6",293],["0x1fcb",88],["0x1fce",40],["0x2442",145],["0x2542",25],["0x2543",72],["0x2848",65],["0x2bc8",3],["0x2eca",6],["0x2fcb",4],["0x300a",30],["0x310a",14],["0x344b",14],["0x354f",6],["0x3c01",10],["0x3e85",7]],"target":"0x3fcf"},{"budget":3,"checked_profiles":286,"coordinates":[2,4,6,7,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xd50",84],["0xfd0",56],["0x3050",19],["0x3150",34],["0x3c04",9]],"target":"0x3fd4"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,4,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1412",3112],["0x1513",2335],["0x1516",585],["0x1842",427],["0x1942",284],["0x1ac2",210],["0x1bc2",138],["0x1bc6",293],["0x1c52",16],["0x1fd3",56],["0x1fd6",44],["0x2442",109],["0x2542",25],["0x2543",66],["0x2812",56],["0x2912",8],["0x2ed3",6],["0x2fd3",4],["0x3050",20],["0x3150",12],["0x3453",10],["0x3557",6],["0x3c01",10],["0x3e85",7]],"target":"0x3fd7"},{"budget":6,"checked_profiles":18564,"coordinates":[0,2,3,4,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1448",3112],["0x1549",2335],["0x154c",585],["0x1818",1059],["0x1a98",319],["0x1a9c",288],["0x2418",36],["0x2518",25],["0x2519",36],["0x2848",10],["0x2bc8",3],["0x2fd9",3],["0x3050",10],["0x3150",9],["0x355d",4],["0x3c01",3],["0x3e85",2]],"target":"0x3fdd"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,3,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1448",3412],["0x1549",2405],["0x1842",565],["0x1942",414],["0x1ac2",208],["0x1bc2",195],["0x1fcb",168],["0x2442",317],["0x2462",270],["0x2463",130],["0x2848",73],["0x2bc8",18],["0x2be8",44],["0x2eea",11],["0x2eeb",9],["0x300a",9],["0x302a",6],["0x310a",6],["0x3c01",1],["0x3c21",2]],"target":"0x3feb"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,3,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0x1448",4006],["0x154c",3322],["0x1842",565],["0x1942",462],["0x1ac2",244],["0x1bc2",231],["0x1bc6",399],["0x1fce",168],["0x2442",317],["0x2462",270],["0x2848",96],["0x2bc8",19],["0x2be8",54],["0x2eea",31],["0x300a",34],["0x302a",35],["0x310a",16],["0x312e",18],["0x3c04",4],["0x3c24",2]],"target":"0x3fee"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1412",3112],["0x1513",2335],["0x1842",565],["0x1942",414],["0x1ac2",228],["0x1bc2",195],["0x1c52",52],["0x1fd3",120],["0x2442",266],["0x2462",248],["0x2463",123],["0x2812",73],["0x2912",37],["0x2932",48],["0x2ef3",14],["0x3050",2],["0x3070",2],["0x3150",2],["0x3c01",1],["0x3c21",2]],"target":"0x3ff3"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xd50",3168],["0xfd0",1764],["0x1412",4206],["0x1516",3322],["0x1842",565],["0x1942",462],["0x1ac2",304],["0x1bc2",231],["0x1bc6",399],["0x1c52",96],["0x1fd6",156],["0x2442",299],["0x2462",270],["0x2812",96],["0x2912",40],["0x2932",78],["0x3050",28],["0x3070",38],["0x3150",10],["0x3174",16],["0x3976",1],["0x3c04",7],["0x3c24",5]],"target":"0x3ff6"},{"budget":6,"checked_profiles":18564,"coordinates":[0,3,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1448",3112],["0x1549",2335],["0x1818",1393],["0x1a98",409],["0x1c59",16],["0x2418",168],["0x2518",96],["0x2519",86],["0x2848",77],["0x2bc8",18],["0x2be8",45],["0x2fd9",3],["0x3050",31],["0x3070",23],["0x3150",6],["0x3579",10],["0x3c01",7],["0x3c21",4]],"target":"0x3ff9"},{"budget":6,"checked_profiles":18564,"coordinates":[2,3,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xd50",3168],["0xfd0",1764],["0x1448",4206],["0x154c",3322],["0x1818",1561],["0x1a98",496],["0x1a9c",474],["0x1c5c",30],["0x2418",160],["0x2518",96],["0x2848",75],["0x2bc8",19],["0x2be8",51],["0x3050",36],["0x3070",53],["0x3150",16],["0x3174",19],["0x357c",7],["0x3c04",3],["0x3c24",5]],"target":"0x3ffc"}],"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","0x1ade","0x1bc2","0x1bc6","0x1c52","0x1c59","0x1c5c","0x1edf","0x1fcb","0x1fce","0x1fd3","0x1fd6","0x2418","0x2442","0x2462","0x2463","0x247b","0x2518","0x2519","0x2542","0x2543","0x2812","0x2848","0x2912","0x2932","0x297a","0x2ada","0x2afa","0x2bc8","0x2be8","0x2d3a","0x2d3b","0x2d73","0x2d7b","0x2eca","0x2ed3","0x2eea","0x2eeb","0x2ef3","0x2f9b","0x2fcb","0x2fd2","0x2fd3","0x2fd8","0x2fd9","0x300a","0x302a","0x3050","0x3070","0x307e","0x310a","0x312e","0x3150","0x3174","0x344b","0x344e","0x3453","0x3456","0x346f","0x3477","0x351f","0x353b","0x353e","0x354f","0x3557","0x355d","0x3579","0x357c","0x383a","0x3852","0x393e","0x3952","0x3976","0x397e","0x3ada","0x3afe","0x3bca","0x3bee","0x3c01","0x3c04","0x3c21","0x3c24","0x3c33","0x3c36","0x3c69","0x3c6c","0x3cc3","0x3cc6","0x3d37","0x3d3f","0x3d48","0x3d68","0x3d77","0x3d8f","0x3dc6","0x3e43","0x3e46","0x3e85","0x3ea5","0x3ec7","0x3ecb","0x3ece","0x3ed3","0x3ed6","0x3ee7","0x3eef","0x3ef7","0x3f0f","0x3f46","0x3f9d","0x3fb3","0x3fb6","0x3fc7","0x3fe9","0x3fec"]},"dimension":14,"limits":["Fixed original280-row nonnegative-integer system; outside=8 constructs witnesses, not a global cap.","Every new obstruction exhausts all inside totals<=demand-1; strict-subset source premises yield simultaneous implication by induction.","43 real implications and134 integral source points are authenticated credited reuse, not new coverage.","Five-million total profiles,120000 per row,one-MiB inputs and256-bit input integers/rationals are fail-UNKNOWN capacities.","No smallest arbitrary inequality description, changed cap alphabet, COPY floor, decoder, native supplier, kappa or frontier claim."],"method":"Independent iterative vector-budget DFS verifies sealed primary data; literal all279-original-row integer points; no solver or primary/predecessor executable import","negative_controls":{"altered_prior_point":"literal credited prior integral witness","altered_saved_first_miss_histogram":"exact obstruction miss_histogram","altered_saved_profile_count":"exact obstruction checked_profiles","duplicate_key":"duplicate JSON key","false_obstruction":"obstruction has an integer counterexample","literal_vector_DFS_toy":{"count":6,"profiles":[[0,0],[0,1],[0,2],[1,0],[1,1],[2,0]]},"missing_prior_deletion":"exact reused real deletions","negative_point":"nonnegative integer coordinates","nonfinite":"nonfinite JSON number","nonviolating_point":"point must strictly violate target","old_coefficient_overrun":"old coefficient overrun","old_negative_multiplier":"old nonnegative unique retained premise","old_zero_rhs":"old demand implication","other_row_point_violation":"point violates another original inequality","rational_exponent":"rational quotient grammar","row_capacity_UNKNOWN":"row profile capacity exceeded","source_byte_mutation":"source SHA256: MATRIX-6425.json"},"new_integer_points":5,"new_obstructions":98,"primary_certificate_sha256":"f4959ac06a189e817a4fc14c428b9bd02dd9f344f20022cd159d8acfd972fa54","retained_rows":139,"reused_integral_points":134,"reused_real_deletions":43,"schema_version":1,"source_manifest_sha256":"c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64","source_rows":280,"status":"PASS_INDEPENDENT_INTEGER_DEMAND_KERNEL","total_new_obstruction_profiles":336386} diff --git a/research/p112-integer-demand-kernel/PROOF.md b/research/p112-integer-demand-kernel/PROOF.md new file mode 100644 index 0000000000..dfb88bcac5 --- /dev/null +++ b/research/p112-integer-demand-kernel/PROOF.md @@ -0,0 +1,123 @@ +# Exact integer projection of the fixed P112 demand system + +The source matrix has 280 distinct nonempty 14-bit masks `H_t`, each with integer +demand `1 <= d_t <= 8`. Its row is `sum_(k in H_t) x_k >= d_t`. This proof fixes +the common domain `x in Z^14`, `x >= 0`, with no upper bounds. Source objects are +authenticated before parsing. The original clique census and geometry-to-demand +equivalence remain credited PR6425 premises, not new replays. + +## Complete finite projection of a counterexample + +An integer vector violating target `(I,d)` has + + sum_(k in I) x_k <= d-1 <= 7. + +Thus its inside coordinates are one of the finitely many weak compositions with +total at most `B=d-1`. This is a consequence of a target violation, not an assumed +global bound on multiplicities. + +For any such inside assignment, set every coordinate outside `I` to 8. Every +other source row either has support contained in `I`, or has an outside bit. The +latter row has LHS at least 8 and hence satisfies its demand. Distinct masks mean +that a different row contained in `I` is a **proper** subset row. Consequently a +global integer counterexample to the target exists if and only if one of the +inside weak compositions satisfies every proper-subset source row. + +The forward implication follows by restricting any global counterexample. For +the reverse, extend by 8 as above. Each resulting full vector is nevertheless +checked literally against all 279 other original rows before acceptance as a +separating point. No inference from a partial point or solver status is used. + +## Enumeration and coverage + +For `k=|I|`, the number of nonnegative inside vectors of total at most `B` is + + binomial(k+B,k). + +Introduce a slack coordinate equal to `B - sum inside` to obtain ordinary weak +compositions of exactly `B` into `k+1` parts. Stars and bars gives this count. + +The primary traverses coordinate multisets of each total `0..B`; counting the +multiplicity of each coordinate is a bijection to the inside vectors. The +separate checker uses an iterative vector-budget tree: at each coordinate assign +an integer from zero through the remaining budget, then continue with the +remainder. At depth `k`, each inside vector occurs exactly once; leftover budget +is the implicit slack. These are distinct executable enumerations of the same +complete domain. + +For a negative classification, every profile must be visited and fail at least +one proper-subset source inequality. The exact closed-form count and the +histogram of the first failing row are checked. The count or histogram alone is +not the proof of exhaustive rejection: both implementations regenerate all +profiles, and the enumeration bijections justify coverage. Positive search may +stop early only after producing an actual full integer separating point. +Capacity exhaustion is UNKNOWN and nonzero; it must not produce a complete +minimum certificate. + +## One integer-only implication + +One concrete integer-only deletion illustrates the domain change. Target +`0x1ada` has demand 5. One half of each source row `0x5a` (demand 4), `0x1a98` +(demand 3), and `0x1ac2` (demand 2) has **exactly** the target coefficient vector +and RHS `9/2`. Hence its integer LHS is at least `ceil(9/2)=5`. The corresponding +real-domain separator from PR6455 has target LHS `9/2` and satisfies the other +279 rows, so deleting this row over the reals would be unsound. The new complete +projection independently checks all 495 inside integer profiles for this target. +The half-sum/rounding example is explanatory; the full result uses complete +negative projections and literal integer separating points. + +## Reused predecessor evidence + +PR6455 already supplied 43 exact real-domain deletion certificates and 134 +integral separating points. These are validated as data and credited, not new +integer discoveries. Each reused deletion is checked as a nonnegative rational +combination of proper-subset source rows whose coefficient vector is at most +the target and whose RHS is at least its demand. Each reused integral point is +parsed as integral/nonnegative and rechecked against all 279 other original +rows. The new classification resolves the remaining 103 labels. + +No predecessor executable, LP solver or 262,928-clique census is imported or +replayed. The earlier real minimum gives a 237-row candidate integer system; +the 134 literal integral points force at least those 134 rows. These are existing +coverage bounds, not the new answer. + +## Joint deletion and the restricted integer minimum + +Let `R` be the new retained rows. Every deleted row is justified either by a +reused rational implication or by exhaustive rejection of its finite inside +counterexample domain. Both types use only proper-subset original rows as +premises. Induct on support cardinality: an integer solution of `R` satisfies +each earlier proper-subset row, whether retained or already implied. The rational +implication then establishes a reused target. For a new negative target, a +violation would give a visited profile failing one of those already-established +proper-subset rows, a contradiction. Therefore every integer solution of `R` +satisfies all original rows. The converse is immediate because `R` is a +subfamily. Simultaneous deletion has no circular premises. + +Every retained row has a full nonnegative integer point satisfying all 279 +other originals and violating that row. Any original-row subfamily equivalent +to the full integer system must contain that row, since otherwise this point +would satisfy the subfamily. Hence, once all classifications and witnesses pass, +`R` is the unique minimum-cardinality and unique inclusion-minimal equivalent +**subfamily of the original 280 inequalities** over the integer orthant. + +This does not minimize arbitrary new inequalities. The minimum claim concerns +unrestricted integer multiplicities: its witness points need not satisfy an +additional cost/COPY budget or multiplicity cap. The all-orthant equivalence can +still be conjoined with any identical additional constraints on both systems; +the minimum property itself need not persist in that restricted domain. + +## Scope and credit + +This is a source-bound necessary-condition screen. Integer separating points +are inequality counterexamples, not decoders or physical call constructions. +Changed supports require a new matrix and extension bound. Coefficients, full +decoder/COPY pricing, native/access/dirty restoration/precision/tape/stock/compiler +and outer admission remain outside scope; no κ or frontier change follows. + +Credit Nick Petalas/PR6425, Jeremy Diviney/PR1422, Cinna Davis/PR1347/1323 and the +retained E8/label/decoder lineage. Credit ToikY with OpenAI Codex/PR6455 for the +real certificates, literal integral points and explicit integer-domain question. +Weak compositions, monotonicity and finite integer implication are classical. +New code/proof uses substantial OpenAI Codex assistance. Separate AI checking +does not constitute human or formal proof-kernel acceptance. diff --git a/research/p112-integer-demand-kernel/README.md b/research/p112-integer-demand-kernel/README.md new file mode 100644 index 0000000000..9c89a7e17e --- /dev/null +++ b/research/p112-integer-demand-kernel/README.md @@ -0,0 +1,107 @@ +# An exact 139-row integer P112 demand subfamily + +The fixed 280-row, 14-variable P112 demand system has a **unique minimum +139-row original subfamily over nonnegative integers**, with no upper bounds. +This resolves [PR6455](https://github.com/CrocSwap/integer-mult-bounds/pull/6455)'s +integer-only question after its 237-row real-domain minimum. + +The new work removes 98 additional rows by complete integer projections and +finds five new integer separating points. The 43 earlier real-domain deletions +and 134 existing integral points are authenticated, validated and credited reuse. +Thus all 103 previously unresolved labels are decided. Every one of the 139 +retained rows has a full integer point satisfying all 279 other original rows +and violating that row; these force every equivalent original-row subfamily to +contain all 139. No minimum over arbitrary new inequalities is claimed. + +## Why a finite test covers unrestricted integer multiplicities + +For a violated target `(I,d)`, integrality forces the total of the target +coordinates to at most `d-1 <= 7`. Set every outside coordinate to 8: every row +with an outside bit is then satisfied. The remaining constraints have proper +subset supports. Exhausting the inside weak compositions therefore decides +whether a global counterexample exists, despite unrestricted multiplicities. +Support-cardinality induction makes simultaneous old/new deletions sound. +`PROOF.md` states the complete projection, enumeration and minimum arguments. + +For example, half of source rows `0x5a` (demand 4), `0x1a98` (3) and `0x1ac2` +(2) gives exactly the coefficient vector of target `0x1ada` with RHS `9/2`. +Its integer LHS is therefore at least 5, the target's demand. The source's +real separating point has LHS `9/2`, showing why the row was needed over reals. +The new projection checks all 495 inside integer profiles for this target. + +## Replay and evidence + +CPython 3.12 and the standard library suffice; no Git, network, LP solver or +predecessor executable is required for these two package replays. + +```sh +python3.12 -I -W error -B research/p112-integer-demand-kernel/verify.py +python3.12 -I -W error -B research/p112-integer-demand-kernel/oracle.py +``` + +Both also pass with `-O`. Default commands require complete strict retained +JSON; `--emit` prints candidates without overwriting files. All three inert +source objects are authenticated before parsing. The primary uses coordinate +multisets; the separate checker uses iterative vector-budget DFS and imports +no primary or predecessor code. + +All 98 new negative domains exhaust 336,386 profiles, independently regenerated +with exact closed-form counts and first-miss histograms. The primary visits +340,727 profiles across all 103 new targets, including 4,341 positive early-stop +profiles. The separate checker validates positive witnesses directly and does +not reproduce that first-positive search order. It checks 16 rejection cases +and a literal two-dimensional DFS coverage toy. Saved-count/histogram mutations +test receipt drift; they do not remove profiles from the enumerator. + +Primary `profile_sha256` values describe its ordered multiset transcript and +are regenerated by the primary only. The separate checker ignores these +optional order-specific hashes and independently regenerates all mathematical +obstruction fields and histograms. Neither a hash nor a count alone certifies +exhaustion. Profile/time/input capacities reject instead of silently truncating. +`VALIDATION.md` records source identities, actual runs and remaining obligations. + +## Scope and limits + +The result concerns exactly the original PR6425 masks and unrestricted +`Z^14 >= 0`. The inside total bound is derived from violating a particular row; +it is not a global cap on multiplicities. The all-orthant equivalence remains +valid if identical extra constraints are conjoined to both systems. The minimum +claim itself need not persist under a cost/COPY budget or multiplicity caps, +because its separating points may fail those extra constraints. + +The source clique census and geometry-to-demand equivalence are credited +predecessor coverage and are not replayed. Passing the screen produces no +coefficients, decoder, physical calls, COPY floor, paid supplier or κ. Native, +access, dirty restoration, precision/tape, stock, compiler and outer integration +remain open. No selected supplier, native, Lean or Docker replay was run. + +Canonical orientation: main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8, selected PR6030, selected-record SHA256 +`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`. +The broader `complex-rank-shape-decoder` card is explicitly changed to this +integer support-screen implication. Main/overlap are refreshed before submission; +bounded searches and sparse/hidden/unpublished/history gaps are not novelty +certificates. All five selected framework assumptions remain. + +## Open next questions + +1. What is the minimum original-row subfamily under one exact cost/COPY budget? + State that domain first; the unrestricted witness points do not settle it. +2. Can a passing integer vector admit actual coefficients and a fully charged + decoder? Freeze one vector/interface before synthesis and complete pricing. +3. For changed support caps, rebuild the complete quotient and establish its + valid integer projection/extension bound before reducing rows. + +## Credit + +Credit Nick Petalas/PR6425 for the original kernel; Jeremy Diviney/PR1422 for +the guard, geometry/caps and smaller-family question; Cinna Davis/PR1347/1323, +Navinor, David Arias, Hanson Sun, DreamingOfClouds, themilkman216 and the retained +E8/label/decoder lineage. Credit ToikY/OpenAI Codex/PR6455 for the real reduction, +literal integral points and explicit integer-only question. Weak compositions, +monotonicity and integer implication/rounding are classical. + +New work uses substantial OpenAI Codex assistance. Separate AI checking is not +human review or formal proof-kernel acceptance. `NOTICE` and `SOURCE-PINS.json` +retain exact source heads, Git blobs and attribution; predecessor files remain +verbatim. No merge or selected-frontier change is part of this contribution. diff --git a/research/p112-integer-demand-kernel/RESULT.json b/research/p112-integer-demand-kernel/RESULT.json new file mode 100644 index 0000000000..b0fd5808f3 --- /dev/null +++ b/research/p112-integer-demand-kernel/RESULT.json @@ -0,0 +1 @@ +{"controls":{"actual_witness_loses_strict_violation":{"observed_error":"point must strictly violate target","target":"0x5a"},"full_source_obstructions":98,"inclusive_budget_boundary":{"target":"0x3","witness_first_two_coordinates":[1,0]},"incomplete_count_rejection":"complete weak-composition count","self_premise_rejection":"obstruction premise must be a proper source subset","triangle_real_integer_gap":{"checked_profiles":4,"fractional_point":["1/2","1/2","1/2"],"integer_domain_rejection":"literal nonnegative INTEGER witness","target":"0x7"}},"counts":{"new_integer_only_deletions":98,"new_integer_witnesses":5,"retained":139,"reused_integral_witnesses":134,"reused_real_deletions":43},"declared_caps":{"profiles_per_target":200000,"seconds":180,"total_profiles":30000000},"dimension":14,"exhaustion_encoding":"CWR coordinates ascending; total0..budget. SHA256 starts with p112-miss/v1 NUL,target two-byte big-endian,budget byte; each miss is total byte,allocation bytes,first-missed mask two-byte big-endian. Histogram/count/digest alone are not a proof: full negative domains are enumerated.","limits":["Only103previously unresolved integer labels are newly classified;43real deletion certificates and134actual integral separators are validated and reused as predecessor evidence.","Unique minimum subset of the original280named rows on unrestricted nonnegative INTEGER variables; not a minimum arbitrary inequality description, facet theorem or support-alphabet extension.","Equivalence can be conjoined with the same additional constraints, but indispensability/minimum need not survive added budget constraints that exclude these witnesses.","Original clique census, caps, real280-row source equivalence, coefficients/decoder, COPY floor, native/physical/outer admission and kappa remain separate."],"obstructions":[{"budget":4,"checked_profiles":495,"coordinates":[1,3,4,6,7,9,11,12],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1818",13],["0x1842",5],["0x1a98",9],["0x1ac2",8]],"profile_sha256":"f3d17d04dce8f67d319304b24ff6bd511f680702d97ba6d9142c93f62886912c","target":"0x1ada"},{"budget":2,"checked_profiles":45,"coordinates":[0,1,3,4,7,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"profile_sha256":"1f3a931fc208e8ca8f10337e47e2f89dd2c9fb7861d442e32e85d0670d10da7b","target":"0x1c9b"},{"budget":2,"checked_profiles":45,"coordinates":[1,2,3,4,7,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"profile_sha256":"a3feaf5b27d79e65ba48b92972abf6f29104e311b6fd0b3e1d10f7859b420de5","target":"0x1c9e"},{"budget":2,"checked_profiles":45,"coordinates":[0,1,3,4,9,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"profile_sha256":"6f10c9384702396f45f2d3a4c1c9b09c9c2ec1020a9b7a39a3e6ac1e8be3a2cd","target":"0x1e1b"},{"budget":2,"checked_profiles":45,"coordinates":[1,2,3,4,9,10,11,12],"expected_profiles":45,"miss_histogram":[["0xc0a",15],["0x1412",23],["0x1818",7]],"profile_sha256":"217c6198c85e13c6518bbe85ac96b7a2d170dbb019d93d60595e0ab44f4a2b15","target":"0x1e1e"},{"budget":3,"checked_profiles":220,"coordinates":[0,1,3,4,7,9,10,11,12],"expected_profiles":220,"miss_histogram":[["0xc0a",56],["0xe8a",40],["0x1412",80],["0x1818",36],["0x1a98",8]],"profile_sha256":"eba6652fddb0ec03957576b929849d104b18b969996e1dbf9af77c3b6867a350","target":"0x1e9b"},{"budget":5,"checked_profiles":3003,"coordinates":[0,1,3,4,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc0a",462],["0xd0a",504],["0xe8a",140],["0xf8a",200],["0xf8b",348],["0x1412",633],["0x1513",422],["0x1818",238],["0x1a98",56]],"profile_sha256":"e1cec47cf6e34088e0e04d546240a92e5e579cd62644bed8bdf9101d45a018ee","target":"0x1f9b"},{"budget":5,"checked_profiles":3003,"coordinates":[1,2,3,4,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc0a",462],["0xd0a",504],["0xe8a",140],["0xf8a",200],["0x1412",706],["0x1516",602],["0x1818",252],["0x1a98",77],["0x1a9c",60]],"profile_sha256":"dedf069ba83ccfa1cf4abd17555d451d6a7b835591664bf1493aaadf003a6adb","target":"0x1f9e"},{"budget":5,"checked_profiles":3003,"coordinates":[0,3,4,6,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc50",462],["0xc51",504],["0xd50",224],["0xfd0",240],["0xfd1",300],["0x1448",573],["0x1549",410],["0x1818",234],["0x1a98",56]],"profile_sha256":"98be437f4c856cd894ad2cb4fec560d454d9b634670f064bb2c220c5c49e065e","target":"0x1fd9"},{"budget":5,"checked_profiles":3003,"coordinates":[2,3,4,6,7,8,9,10,11,12],"expected_profiles":3003,"miss_histogram":[["0xc50",462],["0xd50",504],["0xfd0",280],["0x1448",742],["0x154c",602],["0x1818",264],["0x1a98",83],["0x1a9c",66]],"profile_sha256":"c93fe90a32911895e453cad38f20ee5d83d2083b59e991574e8b5af22224949a","target":"0x1fdc"},{"budget":4,"checked_profiles":330,"coordinates":[1,3,4,5,6,10,13],"expected_profiles":330,"miss_histogram":[["0x5a",295],["0x2418",13],["0x2442",13],["0x2462",9]],"profile_sha256":"dd2a88a17d0d24645ae583fcce9455d11176d49f913db720fb2606521ad00697","target":"0x247a"},{"budget":4,"checked_profiles":330,"coordinates":[1,3,4,6,8,11,13],"expected_profiles":330,"miss_histogram":[["0x5a",295],["0x2812",13],["0x2848",13],["0x2912",9]],"profile_sha256":"d419cf97eedf814449014458a02cbc71fb8c6d23b414c48beefc0f642683a039","target":"0x295a"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,3,4,10,11,13],"expected_profiles":36,"miss_histogram":[["0xc0a",10],["0x2418",19],["0x2812",7]],"profile_sha256":"de0f8d601212d975b9f58f2f83309cfea72d7251cd787938d1749f8353965c88","target":"0x2c1b"},{"budget":2,"checked_profiles":36,"coordinates":[1,3,4,5,10,11,13],"expected_profiles":36,"miss_histogram":[["0xc0a",10],["0x2418",19],["0x2812",7]],"profile_sha256":"b6f03c971abcb45ae361a418f967e797f447ae608532ab284956a7d910152050","target":"0x2c3a"},{"budget":2,"checked_profiles":28,"coordinates":[1,3,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc0a",6],["0x2442",15],["0x2848",7]],"profile_sha256":"176c0c0bea761a54aaceb17e935ad2ee45f312fec66d9a0082e3fe19e939c9e7","target":"0x2c4a"},{"budget":2,"checked_profiles":28,"coordinates":[1,4,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc50",6],["0x2442",15],["0x2812",7]],"profile_sha256":"ae2fdaf25ffc7d228809a2ce53c3075c58a3f7a65d16946c979a38c312fbf745","target":"0x2c52"},{"budget":2,"checked_profiles":28,"coordinates":[3,4,6,10,11,13],"expected_profiles":28,"miss_histogram":[["0xc50",6],["0x2418",15],["0x2848",7]],"profile_sha256":"5df77b438d328fb2a0742eaad0b13fa09a6a77547ad9a29df052219921602140","target":"0x2c58"},{"budget":3,"checked_profiles":120,"coordinates":[1,3,4,8,10,11,13],"expected_profiles":120,"miss_histogram":[["0xc0a",20],["0xd0a",24],["0x2418",42],["0x2518",17],["0x2812",17]],"profile_sha256":"3f434ba4f6634fddbb2f4e8556fb78fa73b908ba8a6bdc63a52ce3e594f0e03c","target":"0x2d1a"},{"budget":3,"checked_profiles":120,"coordinates":[1,4,6,8,10,11,13],"expected_profiles":120,"miss_histogram":[["0xc50",20],["0xd50",24],["0x2442",42],["0x2542",17],["0x2812",17]],"profile_sha256":"5117fc005564aa2459cd021f08b9a91ebf49d1e318f8c3ce72632b3bd7a67f0e","target":"0x2d52"},{"budget":4,"checked_profiles":495,"coordinates":[1,4,5,6,8,10,11,13],"expected_profiles":495,"miss_histogram":[["0xc50",70],["0xd50",80],["0x2442",147],["0x2462",81],["0x2542",20],["0x2812",58],["0x2912",21],["0x2932",18]],"profile_sha256":"df16203eb4e21121fc383b82305279efd27563baaf3a165e816b16dc479823c9","target":"0x2d72"},{"budget":3,"checked_profiles":165,"coordinates":[1,3,6,7,8,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc0a",35],["0xd0a",40],["0x2442",53],["0x2542",20],["0x2848",17]],"profile_sha256":"da99f71eb38fcdd218b1245a741e82b6773f82f6495e8611e295ce1e5c651ca8","target":"0x2dca"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,7,8,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc50",35],["0xd50",40],["0x2418",53],["0x2518",20],["0x2848",17]],"profile_sha256":"223ebdeadc3717e76c82b9886fd16b502af107f512bc739243c55593577291d6","target":"0x2dd8"},{"budget":6,"checked_profiles":12376,"coordinates":[0,1,3,4,5,6,7,9,10,11,13],"expected_profiles":12376,"miss_histogram":[["0x5a",10584],["0xc0a",148],["0xc50",148],["0xc51",244],["0xe8a",184],["0xedb",429],["0x2418",157],["0x2442",157],["0x2462",152],["0x2463",79],["0x247b",22],["0x2812",22],["0x2848",24],["0x2ada",10],["0x2afa",11],["0x2eea",1],["0x2eeb",3],["0x2ef3",1]],"profile_sha256":"46598b00f87067c68f9e7e72272001a801ddea92ec89dde9d93b5f13151a1e09","target":"0x2efb"},{"budget":3,"checked_profiles":165,"coordinates":[1,3,6,8,9,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc0a",35],["0xd0a",40],["0x2442",53],["0x2542",20],["0x2848",17]],"profile_sha256":"87fce23fb907159dc2832263576e104633bd4ddd729d700423686283e574ed4a","target":"0x2f4a"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,8,9,10,11,13],"expected_profiles":165,"miss_histogram":[["0xc50",35],["0xd50",40],["0x2418",53],["0x2518",20],["0x2848",17]],"profile_sha256":"05f6d44989f81cb7d4886b0a9cc6b6077596531e1dd4b9a8844daa547ddb2aee","target":"0x2f58"},{"budget":4,"checked_profiles":715,"coordinates":[1,3,6,7,8,9,10,11,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0xe8a",40],["0xf8a",60],["0x2442",178],["0x2542",70],["0x2848",81],["0x2bc8",12],["0x2eca",8]],"profile_sha256":"29131462e83b6b862f599ffe207be55863af4132bca735ef9b6820c4c095f37f","target":"0x2fca"},{"budget":5,"checked_profiles":3003,"coordinates":[1,3,4,6,7,8,9,10,11,13],"expected_profiles":3003,"miss_histogram":[["0x5a",2702],["0xc0a",31],["0xc50",31],["0xd0a",52],["0xd50",52],["0xe8a",8],["0xf8a",46],["0xfd0",36],["0x2418",13],["0x2442",13],["0x2518",11],["0x2542",2],["0x2812",2],["0x2848",2],["0x2912",1],["0x2ada",1]],"profile_sha256":"3ce8b4134fa803a4050040bc1a2b3747db1815a54a20e768ba01bb1def897a8e","target":"0x2fda"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,3,4,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2418",7],["0x300a",3]],"profile_sha256":"c40820caf58dc3245682f790fcca9ec85bd88774e198c997d7a14180555fb533","target":"0x341b"},{"budget":2,"checked_profiles":36,"coordinates":[1,2,3,4,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2418",7],["0x300a",3]],"profile_sha256":"bdafc2b5fa5176cf1de642bcd71d8d415e16da2adce26242361da842ad430005","target":"0x341e"},{"budget":2,"checked_profiles":28,"coordinates":[1,3,6,10,12,13],"expected_profiles":28,"miss_histogram":[["0x1448",18],["0x2442",7],["0x300a",3]],"profile_sha256":"878dd4743bbab6a3423cdb08829476000418ebe61c0ed173dcabef0f345ee1a6","target":"0x344a"},{"budget":2,"checked_profiles":28,"coordinates":[1,4,6,10,12,13],"expected_profiles":28,"miss_histogram":[["0x1412",18],["0x2442",7],["0x3050",3]],"profile_sha256":"02706595394aaf242d52a90597fbf8aee06d9355fbdaf07502a143e4e099d7ec","target":"0x3452"},{"budget":2,"checked_profiles":36,"coordinates":[0,3,4,6,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2418",7],["0x3050",3]],"profile_sha256":"9f0b29d7e5397de5e9826462c3609089c654ef306f0d199ba29179a33f3d7862","target":"0x3459"},{"budget":4,"checked_profiles":495,"coordinates":[0,1,3,4,6,10,12,13],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1412",13],["0x1448",13],["0x2418",3],["0x2442",3],["0x300a",1],["0x3050",1],["0x344b",1]],"profile_sha256":"ced29bfc88833f4a25cc2a984a472bbbbff035a910e678d231d2cf74097e7129","target":"0x345b"},{"budget":2,"checked_profiles":36,"coordinates":[2,3,4,6,10,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2418",7],["0x3050",3]],"profile_sha256":"977d7e872bc895309a72978b8bfb5c1e0f17cd1389c326c113b24690f61c2131","target":"0x345c"},{"budget":4,"checked_profiles":495,"coordinates":[1,2,3,4,6,10,12,13],"expected_profiles":495,"miss_histogram":[["0x5a",460],["0x1412",13],["0x1448",13],["0x2418",3],["0x2442",3],["0x300a",1],["0x3050",1],["0x344e",1]],"profile_sha256":"eee493bd0690dcb141e8c4fbd5cc1355401497e639f8b9b1595b630c9b604671","target":"0x345e"},{"budget":6,"checked_profiles":8008,"coordinates":[0,1,2,3,4,5,6,10,12,13],"expected_profiles":8008,"miss_histogram":[["0x5a",6552],["0x1412",356],["0x1448",356],["0x145f",330],["0x2418",88],["0x2442",88],["0x2462",96],["0x2463",60],["0x247b",14],["0x300a",9],["0x302a",13],["0x3050",9],["0x3070",13],["0x307e",19],["0x346f",4],["0x3477",1]],"profile_sha256":"89dea9b4b74c186b40f4836a8300d3e24ec0e704eedd15ef43aa40c432000d7f","target":"0x347f"},{"budget":5,"checked_profiles":2002,"coordinates":[0,1,3,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1448",756],["0x1549",600],["0x2442",252],["0x2462",154],["0x2463",90],["0x2542",9],["0x2543",8],["0x300a",49],["0x302a",56],["0x310a",28]],"profile_sha256":"381242a6bfc5fa00d03d3d22c1ac5849bea164207c964171948c756673924998","target":"0x356b"},{"budget":5,"checked_profiles":2002,"coordinates":[1,2,3,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1448",756],["0x154c",600],["0x2442",252],["0x2462",154],["0x2542",18],["0x300a",60],["0x302a",78],["0x310a",54],["0x312e",30]],"profile_sha256":"56cb8465856fa4ea926e47459bb343bb50f8b2ca1e9f43cc64f257625f401633","target":"0x356e"},{"budget":5,"checked_profiles":2002,"coordinates":[0,1,4,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1412",756],["0x1513",600],["0x2442",252],["0x2462",154],["0x2463",90],["0x2542",9],["0x2543",8],["0x3050",49],["0x3070",56],["0x3150",28]],"profile_sha256":"2a7359241fb57aa38aeb4edf9d09046be7ea507bfe53aea7c919f7a454e294fc","target":"0x3573"},{"budget":5,"checked_profiles":2002,"coordinates":[1,2,4,5,6,8,10,12,13],"expected_profiles":2002,"miss_histogram":[["0x1412",756],["0x1516",600],["0x2442",252],["0x2462",154],["0x2542",18],["0x3050",60],["0x3070",78],["0x3150",54],["0x3174",30]],"profile_sha256":"a6fc69494585ffd8214cbd6ab39a23436c4532ccecfb66ef296a818e146d7d30","target":"0x3576"},{"budget":2,"checked_profiles":28,"coordinates":[3,4,6,11,12,13],"expected_profiles":28,"miss_histogram":[["0x1818",18],["0x2848",7],["0x3050",3]],"profile_sha256":"67c70d4b10a373c7e9e5b2fdfeeee9a783dcdbc2657b89f8f3ad9a72388df033","target":"0x3858"},{"budget":2,"checked_profiles":36,"coordinates":[1,3,5,6,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1842",10],["0x2848",19],["0x300a",3],["0x302a",4]],"profile_sha256":"ab9fe315d2b1fb80a43038805a41f62b06e1483ec7c76f1e1d0b0e34fe39ba2f","target":"0x386a"},{"budget":4,"checked_profiles":495,"coordinates":[1,3,4,5,8,11,12,13],"expected_profiles":495,"miss_histogram":[["0x1818",210],["0x2812",111],["0x2912",67],["0x2932",59],["0x300a",19],["0x302a",14],["0x310a",15]],"profile_sha256":"b6d08d41e496cb9ff0cb2403a4835efad258df6dc02fea655f4cdca58477b888","target":"0x393a"},{"budget":5,"checked_profiles":1287,"coordinates":[1,3,4,6,8,11,12,13],"expected_profiles":1287,"miss_histogram":[["0x5a",1056],["0x1818",65],["0x1842",21],["0x1942",36],["0x2812",28],["0x2848",28],["0x2912",24],["0x300a",4],["0x3050",4],["0x310a",11],["0x3150",8],["0x3952",2]],"profile_sha256":"5b4690abf9c58e70eeba2553e5cfca753d155abd16c92256f14e53c27db4f72c","target":"0x395a"},{"budget":3,"checked_profiles":220,"coordinates":[1,2,3,6,7,8,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x310a",24]],"profile_sha256":"9cdcb54c60c534d33bf4361f69aeb0fb62148aa782646bd91ffcc2fc29066928","target":"0x39ce"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,7,8,11,12,13],"expected_profiles":165,"miss_histogram":[["0x1818",95],["0x2848",37],["0x3050",13],["0x3150",20]],"profile_sha256":"0ffd86a4064b5c0c305ff4dee053b6edbd5682353a7f5b84e2a967dbb400d116","target":"0x39d8"},{"budget":3,"checked_profiles":220,"coordinates":[1,3,5,6,7,8,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x302a",16],["0x310a",8]],"profile_sha256":"9f088d27b3ef18b871cb162c6176d0b74336868b144807629f6d3a1484c2aa90","target":"0x39ea"},{"budget":2,"checked_profiles":45,"coordinates":[1,3,6,7,9,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1842",15],["0x1ac2",12],["0x2848",15],["0x300a",3]],"profile_sha256":"620ca555c0376127efacf610acd9a94229392f59e087deb477ce309b4d015594","target":"0x3aca"},{"budget":3,"checked_profiles":220,"coordinates":[3,4,5,6,7,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1818",140],["0x1a98",40],["0x2848",24],["0x3050",10],["0x3070",6]],"profile_sha256":"91c56cf13f8d6026c8198933f9f7016628503e83e2fd3e9a6414d2f2dfc3c9bd","target":"0x3af8"},{"budget":3,"checked_profiles":220,"coordinates":[1,2,3,6,8,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x310a",24]],"profile_sha256":"a7525d6d18eb1061162a33b05fe4a7296f019b75c531b97d3e88cef53211d2c8","target":"0x3b4e"},{"budget":3,"checked_profiles":165,"coordinates":[3,4,6,8,9,11,12,13],"expected_profiles":165,"miss_histogram":[["0x1818",95],["0x2848",37],["0x3050",13],["0x3150",20]],"profile_sha256":"a5b31d8f2ee4887e41d99e7d77d8bc8ea549f6a5b48a304e7b2be074209e3eff","target":"0x3b58"},{"budget":3,"checked_profiles":220,"coordinates":[1,3,5,6,8,9,11,12,13],"expected_profiles":220,"miss_histogram":[["0x1842",56],["0x1942",60],["0x2848",64],["0x300a",16],["0x302a",16],["0x310a",8]],"profile_sha256":"0cc9e1e3088f2acf3eecc5c57b274c0bbab4ebb2480c2bc0170e6abb3549865f","target":"0x3b6a"},{"budget":4,"checked_profiles":715,"coordinates":[3,4,6,7,8,9,11,12,13],"expected_profiles":715,"miss_histogram":[["0x1818",350],["0x1a98",100],["0x2848",122],["0x2bc8",27],["0x3050",42],["0x3150",74]],"profile_sha256":"839839920c048aca5c9d16096a85baf2fab46c36f122be91190cc8bd10adb52e","target":"0x3bd8"},{"budget":1,"checked_profiles":8,"coordinates":[0,1,3,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc0a",4],["0x300a",2],["0x3c01",2]],"profile_sha256":"d7fbd4d6c5670c761dbf75c3cf2cd6eead14b5a6d4c75eed80a32356e3b01b5b","target":"0x3c0b"},{"budget":1,"checked_profiles":8,"coordinates":[1,2,3,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc0a",4],["0x300a",2],["0x3c04",2]],"profile_sha256":"4a0e2c0c3923051888c260937cc2acb8d6de80cf78394d3e94c828e7971cfa3b","target":"0x3c0e"},{"budget":2,"checked_profiles":36,"coordinates":[0,1,4,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2812",7],["0x3c01",3]],"profile_sha256":"4323fdf906aa156dd6946ed639f6b88e60ea2b09414096110a0f1d951a511b23","target":"0x3c13"},{"budget":2,"checked_profiles":36,"coordinates":[1,2,4,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1412",26],["0x2812",7],["0x3c04",3]],"profile_sha256":"207e206074498d90e3937a5d27775bab3f58152d73de1211584917798355f751","target":"0x3c16"},{"budget":3,"checked_profiles":220,"coordinates":[0,1,2,3,4,10,11,12,13],"expected_profiles":220,"miss_histogram":[["0xc0a",56],["0x1412",100],["0x1818",44],["0x2418",10],["0x2812",4],["0x300a",3],["0x3c01",3]],"profile_sha256":"ee5c45a35be53637742eb1a65dc36a63dfdc28d31e745f6fbe1cdcb9f1125b78","target":"0x3c1f"},{"budget":2,"checked_profiles":36,"coordinates":[0,3,6,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2848",7],["0x3c01",3]],"profile_sha256":"c98078aed73cea85ccdf300ed64e240afd5e0c02befa0648d6541470a7d649f6","target":"0x3c49"},{"budget":2,"checked_profiles":36,"coordinates":[2,3,6,10,11,12,13],"expected_profiles":36,"miss_histogram":[["0x1448",26],["0x2848",7],["0x3c04",3]],"profile_sha256":"1e579e84f93a4229acbc634e96272378ae12d6bb9c068c2e56417e1c789d56a2","target":"0x3c4c"},{"budget":1,"checked_profiles":8,"coordinates":[2,4,6,10,11,12,13],"expected_profiles":8,"miss_histogram":[["0xc50",4],["0x3050",2],["0x3c04",2]],"profile_sha256":"b9abb9fef71a0a70d103723546d0c4fce5075ecf2dd81a3b86169e9dfd2ac6ca","target":"0x3c54"},{"budget":2,"checked_profiles":45,"coordinates":[0,3,4,7,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c01",3]],"profile_sha256":"12855ec7b2d8c481cbfd644d624e3659a85d2e944d915ebf905ada387691607f","target":"0x3c99"},{"budget":2,"checked_profiles":45,"coordinates":[2,3,4,7,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c04",3]],"profile_sha256":"f070171f6ad9242d8990c1dc22dc84e1b55d47a1a7590f39ef2142b230c52c17","target":"0x3c9c"},{"budget":2,"checked_profiles":66,"coordinates":[0,1,2,3,5,7,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc0a",28],["0x300a",13],["0x302a",16],["0x3c01",5],["0x3c21",4]],"profile_sha256":"86f6654fbe55c156ab03f58142f65bf6a26f03c4c8cbe84ea40b1ba0bb2a0fdb","target":"0x3caf"},{"budget":4,"checked_profiles":715,"coordinates":[0,1,3,4,8,10,11,12,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0x1412",211],["0x1513",173],["0x1818",50],["0x2418",6],["0x2518",3],["0x2519",4],["0x2912",1],["0x300a",1]],"profile_sha256":"4211ccb88c19df6fe10f69bea6b3801a20e847728c5969c9a56c36c6b05ace7a","target":"0x3d1b"},{"budget":4,"checked_profiles":715,"coordinates":[1,2,3,4,8,10,11,12,13],"expected_profiles":715,"miss_histogram":[["0xc0a",126],["0xd0a",140],["0x1412",211],["0x1516",173],["0x1818",50],["0x2418",6],["0x2518",3],["0x2812",2],["0x2912",1],["0x300a",1],["0x310a",2]],"profile_sha256":"b99ccf4e7ef52fd5c0c83c039f11dbcf583b54aea666e5b0fb05b3d4278a2756","target":"0x3d1e"},{"budget":7,"checked_profiles":50388,"coordinates":[0,1,2,3,4,5,6,8,10,11,12,13],"expected_profiles":50388,"miss_histogram":[["0x5a",41217],["0xc0a",645],["0xc50",645],["0xc51",1040],["0xd0a",1040],["0xd50",312],["0x1412",1077],["0x1448",1077],["0x145f",1127],["0x1513",881],["0x1516",199],["0x1549",632],["0x154c",64],["0x1818",83],["0x1842",21],["0x1942",37],["0x1c52",1],["0x1c5c",2],["0x2418",31],["0x2442",42],["0x2462",49],["0x2463",59],["0x247b",15],["0x2518",9],["0x2519",20],["0x2812",6],["0x2848",6],["0x2912",26],["0x2932",23],["0x2d3b",1],["0x307e",1]],"profile_sha256":"3a855c58a1b5e7d0b11dbf0c8919afa21e049377646b20e0e2899462ed75c8ce","target":"0x3d7f"},{"budget":3,"checked_profiles":286,"coordinates":[0,1,3,5,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0x300a",29],["0x302a",40],["0x310a",32],["0x3c01",7],["0x3c21",10]],"profile_sha256":"a3b2b39bfeafa2ee307316f74e108b5ac4cd1fbc35f282a7e121ee33d66836b0","target":"0x3dab"},{"budget":3,"checked_profiles":286,"coordinates":[2,3,4,5,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1818",196],["0x2418",51],["0x2518",26],["0x3c04",7],["0x3c24",6]],"profile_sha256":"94d562a7c128c39a2c038346607e28eb701f846725c7c34595ea89681b75e629","target":"0x3dbc"},{"budget":4,"checked_profiles":1001,"coordinates":[1,2,3,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x154c",216],["0x1842",22],["0x1942",14],["0x2442",15],["0x2542",3],["0x2848",6],["0x300a",2],["0x310a",3]],"profile_sha256":"620c85ecd3f531a4a360d7d58e9cddcbd76cab6726454fa6944fca58342bbc28","target":"0x3dce"},{"budget":4,"checked_profiles":1001,"coordinates":[1,3,5,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x1842",70],["0x1942",64],["0x2442",63],["0x2462",46],["0x2542",3],["0x2848",18],["0x300a",4],["0x302a",7],["0x310a",4],["0x3d48",1],["0x3d68",1]],"profile_sha256":"ec355717e71baace4d8846d37e19fceaddef8fd3d3aa2bc2f9beb26512ae6525","target":"0x3dea"},{"budget":3,"checked_profiles":286,"coordinates":[0,4,5,6,7,8,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xc51",84],["0xd50",24],["0x3050",21],["0x3070",30],["0x3150",30],["0x3c01",7],["0x3c21",6]],"profile_sha256":"ec6860a14790c5c1d74f7a0516bfd65466cb9b713b51d0a8ba632bd7cb5a4030","target":"0x3df1"},{"budget":4,"checked_profiles":1001,"coordinates":[3,4,5,6,7,8,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc50",210],["0xd50",224],["0x1448",286],["0x1818",166],["0x2418",44],["0x2518",33],["0x2848",18],["0x3050",6],["0x3070",7],["0x3150",4],["0x3d48",1],["0x3d68",2]],"profile_sha256":"00c1233b7ae126fc99dfb8491ac98784f9e6d79d06d40d217266e73bdc0b71f2","target":"0x3df8"},{"budget":2,"checked_profiles":45,"coordinates":[0,3,4,9,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c01",3]],"profile_sha256":"ed5c6c689a7e5fd4f948b3e8a537660f459cf1699ce0a5b147abed02f020ea67","target":"0x3e19"},{"budget":2,"checked_profiles":45,"coordinates":[2,3,4,9,10,11,12,13],"expected_profiles":45,"miss_histogram":[["0x1818",35],["0x2418",7],["0x3c04",3]],"profile_sha256":"643e10b768b52c5cf4dc4826e24806a7c3e0945512d15b918fcaaff19ce30f22","target":"0x3e1c"},{"budget":2,"checked_profiles":66,"coordinates":[0,1,2,3,5,9,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc0a",28],["0x300a",13],["0x302a",16],["0x3c01",5],["0x3c21",4]],"profile_sha256":"eef0022a5924b783b7761da69ffd446c373722b5e22b3a250c638f4cef924be4","target":"0x3e2f"},{"budget":3,"checked_profiles":286,"coordinates":[1,2,5,6,7,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1842",84],["0x1ac2",60],["0x2442",95],["0x2462",34],["0x3c04",7],["0x3c24",6]],"profile_sha256":"bcfa51a2ff4aa45d9662364c520b0e347edbd9564f7894332f820f21b17971fa","target":"0x3ee6"},{"budget":2,"checked_profiles":66,"coordinates":[2,4,5,6,7,9,10,11,12,13],"expected_profiles":66,"miss_histogram":[["0xc50",28],["0x3050",13],["0x3070",16],["0x3c04",5],["0x3c24",4]],"profile_sha256":"100f15e845a42400f375cb7555d6ccd44ce68170aa344a2e6a9ef2c28fa2f650","target":"0x3ef4"},{"budget":3,"checked_profiles":286,"coordinates":[0,1,3,5,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0x300a",29],["0x302a",40],["0x310a",32],["0x3c01",7],["0x3c21",10]],"profile_sha256":"e5c6a23081080b7e7f0434886dc1f67200fc07ace57093bcaddd8bc187898a60","target":"0x3f2b"},{"budget":3,"checked_profiles":286,"coordinates":[2,3,4,5,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0x1818",196],["0x2418",51],["0x2518",26],["0x3c04",7],["0x3c24",6]],"profile_sha256":"6564b94c06abb62972ec904258c439747ecc32bb28d4bdcf020368aa8125f7aa","target":"0x3f3c"},{"budget":4,"checked_profiles":1001,"coordinates":[1,2,3,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x154c",216],["0x1842",22],["0x1942",14],["0x2442",15],["0x2542",3],["0x2848",6],["0x300a",2],["0x310a",3]],"profile_sha256":"b38e303e115f11f9f4d6ee2eb30c80e5291ff5d39aa6911301725671597a8207","target":"0x3f4e"},{"budget":4,"checked_profiles":1001,"coordinates":[1,3,5,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc0a",210],["0xd0a",224],["0x1448",286],["0x1842",70],["0x1942",64],["0x2442",63],["0x2462",46],["0x2542",3],["0x2848",18],["0x300a",4],["0x302a",7],["0x310a",4],["0x3d48",1],["0x3d68",1]],"profile_sha256":"96f51e3f1db1b05968d3e1296c282b11825fcb962073a6eb2bdc34494a59e6f7","target":"0x3f6a"},{"budget":3,"checked_profiles":286,"coordinates":[0,4,5,6,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xc51",84],["0xd50",24],["0x3050",21],["0x3070",30],["0x3150",30],["0x3c01",7],["0x3c21",6]],"profile_sha256":"c1204a4a1457570e45d6712dd9e2e5f3207b03be9a479c8a1273266d61806d75","target":"0x3f71"},{"budget":4,"checked_profiles":1001,"coordinates":[3,4,5,6,8,9,10,11,12,13],"expected_profiles":1001,"miss_histogram":[["0xc50",210],["0xd50",224],["0x1448",286],["0x1818",166],["0x2418",44],["0x2518",33],["0x2848",18],["0x3050",6],["0x3070",7],["0x3150",4],["0x3d48",1],["0x3d68",2]],"profile_sha256":"14cff69f65205f25f28d8fda5fb7c0ff2d19a0d956d69e142384b8e5cdf8604c","target":"0x3f78"},{"budget":3,"checked_profiles":286,"coordinates":[1,2,3,7,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc0a",84],["0xd0a",84],["0xe8a",20],["0xf8a",40],["0x300a",17],["0x310a",34],["0x3c04",7]],"profile_sha256":"878a19c9f53031ee18e58279eb0e7f9ec1bd1a51aa55210fac4d838dc800fae2","target":"0x3f8e"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,3,4,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1412",3412],["0x1513",2405],["0x1516",585],["0x1818",1083],["0x1a98",313],["0x1a9c",294],["0x2418",51],["0x2518",25],["0x2519",42],["0x2812",12],["0x2912",8],["0x2f9b",3],["0x300a",12],["0x310a",7],["0x351f",6],["0x3c01",3],["0x3e85",2]],"profile_sha256":"b2ed192699a3b2bbac107af284555130c5558b27cd401261ca3b3474a2588420","target":"0x3f9f"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,3,4,5,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1412",3412],["0x1513",2405],["0x1818",1417],["0x1a98",403],["0x2418",194],["0x2518",96],["0x2519",92],["0x2812",84],["0x2912",37],["0x2932",60],["0x2d3a",4],["0x2d3b",21],["0x300a",11],["0x302a",10],["0x310a",2],["0x353b",4],["0x3c01",7],["0x3c21",4]],"profile_sha256":"f78d8f9c76e8f004caaa5281c7026fec78db7b2d1b3964953e3f767fa786b913","target":"0x3fbb"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,3,4,5,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0x1412",4006],["0x1516",3322],["0x1818",1501],["0x1a98",466],["0x1a9c",442],["0x2418",169],["0x2518",96],["0x2812",78],["0x2912",40],["0x2932",77],["0x2d3a",11],["0x300a",21],["0x302a",31],["0x310a",10],["0x312e",13],["0x353e",3],["0x3c04",3],["0x3c24",4]],"profile_sha256":"2ed4ca8b8501aebadb80849348fb372b8da21661b97bbcf8214464116aceb3ad","target":"0x3fbe"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,3,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1448",3412],["0x1549",2405],["0x154c",585],["0x1842",427],["0x1942",284],["0x1ac2",190],["0x1bc2",138],["0x1bc6",293],["0x1fcb",88],["0x1fce",40],["0x2442",145],["0x2542",25],["0x2543",72],["0x2848",65],["0x2bc8",3],["0x2eca",6],["0x2fcb",4],["0x300a",30],["0x310a",14],["0x344b",14],["0x354f",6],["0x3c01",10],["0x3e85",7]],"profile_sha256":"cbde55872d94cfb7fc27f4cbc1797bdc4b492f18e1c2aaef9c9ddc2ba9ef4029","target":"0x3fcf"},{"budget":3,"checked_profiles":286,"coordinates":[2,4,6,7,8,9,10,11,12,13],"expected_profiles":286,"miss_histogram":[["0xc50",84],["0xd50",84],["0xfd0",56],["0x3050",19],["0x3150",34],["0x3c04",9]],"profile_sha256":"3dfa12553a282d1f63eff506e90c3a6b0266e9b5fb567627cefe9fca0d9adbe0","target":"0x3fd4"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,2,4,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1412",3112],["0x1513",2335],["0x1516",585],["0x1842",427],["0x1942",284],["0x1ac2",210],["0x1bc2",138],["0x1bc6",293],["0x1c52",16],["0x1fd3",56],["0x1fd6",44],["0x2442",109],["0x2542",25],["0x2543",66],["0x2812",56],["0x2912",8],["0x2ed3",6],["0x2fd3",4],["0x3050",20],["0x3150",12],["0x3453",10],["0x3557",6],["0x3c01",10],["0x3e85",7]],"profile_sha256":"9176eed5430472fca7dd77083a7383688be0a544e376caab467c7996c0d47789","target":"0x3fd7"},{"budget":6,"checked_profiles":18564,"coordinates":[0,2,3,4,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1448",3112],["0x1549",2335],["0x154c",585],["0x1818",1059],["0x1a98",319],["0x1a9c",288],["0x2418",36],["0x2518",25],["0x2519",36],["0x2848",10],["0x2bc8",3],["0x2fd9",3],["0x3050",10],["0x3150",9],["0x355d",4],["0x3c01",3],["0x3e85",2]],"profile_sha256":"ce3bda7607a4374d06ac0e135eb5c537dc309ad5813fe7d4250bf45c014f3dba","target":"0x3fdd"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,3,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0xf8b",2030],["0x1448",3412],["0x1549",2405],["0x1842",565],["0x1942",414],["0x1ac2",208],["0x1bc2",195],["0x1fcb",168],["0x2442",317],["0x2462",270],["0x2463",130],["0x2848",73],["0x2bc8",18],["0x2be8",44],["0x2eea",11],["0x2eeb",9],["0x300a",9],["0x302a",6],["0x310a",6],["0x3c01",1],["0x3c21",2]],"profile_sha256":"ba386cffd8d8baf3579966460d334d3425d84ee2e8dc76b6d6a0b96dd7174778","target":"0x3feb"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,3,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc0a",3003],["0xd0a",3168],["0xe8a",840],["0xf8a",1260],["0x1448",4006],["0x154c",3322],["0x1842",565],["0x1942",462],["0x1ac2",244],["0x1bc2",231],["0x1bc6",399],["0x1fce",168],["0x2442",317],["0x2462",270],["0x2848",96],["0x2bc8",19],["0x2be8",54],["0x2eea",31],["0x300a",34],["0x302a",35],["0x310a",16],["0x312e",18],["0x3c04",4],["0x3c24",2]],"profile_sha256":"957a36cb831f13668775cd10a84d2a69b31ea688809ec437c0095848e9c0a469","target":"0x3fee"},{"budget":6,"checked_profiles":18564,"coordinates":[0,1,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1412",3112],["0x1513",2335],["0x1842",565],["0x1942",414],["0x1ac2",228],["0x1bc2",195],["0x1c52",52],["0x1fd3",120],["0x2442",266],["0x2462",248],["0x2463",123],["0x2812",73],["0x2912",37],["0x2932",48],["0x2ef3",14],["0x3050",2],["0x3070",2],["0x3150",2],["0x3c01",1],["0x3c21",2]],"profile_sha256":"224c0c632e46e715aac79704a7aeedde3c54d5cd2cff2a02978e12f17a8b3206","target":"0x3ff3"},{"budget":6,"checked_profiles":18564,"coordinates":[1,2,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xd50",3168],["0xfd0",1764],["0x1412",4206],["0x1516",3322],["0x1842",565],["0x1942",462],["0x1ac2",304],["0x1bc2",231],["0x1bc6",399],["0x1c52",96],["0x1fd6",156],["0x2442",299],["0x2462",270],["0x2812",96],["0x2912",40],["0x2932",78],["0x3050",28],["0x3070",38],["0x3150",10],["0x3174",16],["0x3976",1],["0x3c04",7],["0x3c24",5]],"profile_sha256":"c283c01ff490982574f9e20c62d79b11d04c3b1a59a11aad18c31f219c40f42a","target":"0x3ff6"},{"budget":6,"checked_profiles":18564,"coordinates":[0,3,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xc51",3168],["0xd50",1320],["0xfd0",1484],["0xfd1",1750],["0x1448",3112],["0x1549",2335],["0x1818",1393],["0x1a98",409],["0x1c59",16],["0x2418",168],["0x2518",96],["0x2519",86],["0x2848",77],["0x2bc8",18],["0x2be8",45],["0x2fd9",3],["0x3050",31],["0x3070",23],["0x3150",6],["0x3579",10],["0x3c01",7],["0x3c21",4]],"profile_sha256":"e8b38d1174d45935d2669b7dd4fb13967ed6393638d48a61bb28b40eee8f1480","target":"0x3ff9"},{"budget":6,"checked_profiles":18564,"coordinates":[2,3,4,5,6,7,8,9,10,11,12,13],"expected_profiles":18564,"miss_histogram":[["0xc50",3003],["0xd50",3168],["0xfd0",1764],["0x1448",4206],["0x154c",3322],["0x1818",1561],["0x1a98",496],["0x1a9c",474],["0x1c5c",30],["0x2418",160],["0x2518",96],["0x2848",75],["0x2bc8",19],["0x2be8",51],["0x3050",36],["0x3070",53],["0x3150",16],["0x3174",19],["0x357c",7],["0x3c04",3],["0x3c24",5]],"profile_sha256":"63e0d363efe29d243ff3411fd1eac71f85642fa8656e168b2299a69feac92013","target":"0x3ffc"}],"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","0x1ade","0x1bc2","0x1bc6","0x1c52","0x1c59","0x1c5c","0x1edf","0x1fcb","0x1fce","0x1fd3","0x1fd6","0x2418","0x2442","0x2462","0x2463","0x247b","0x2518","0x2519","0x2542","0x2543","0x2812","0x2848","0x2912","0x2932","0x297a","0x2ada","0x2afa","0x2bc8","0x2be8","0x2d3a","0x2d3b","0x2d73","0x2d7b","0x2eca","0x2ed3","0x2eea","0x2eeb","0x2ef3","0x2f9b","0x2fcb","0x2fd2","0x2fd3","0x2fd8","0x2fd9","0x300a","0x302a","0x3050","0x3070","0x307e","0x310a","0x312e","0x3150","0x3174","0x344b","0x344e","0x3453","0x3456","0x346f","0x3477","0x351f","0x353b","0x353e","0x354f","0x3557","0x355d","0x3579","0x357c","0x383a","0x3852","0x393e","0x3952","0x3976","0x397e","0x3ada","0x3afe","0x3bca","0x3bee","0x3c01","0x3c04","0x3c21","0x3c24","0x3c33","0x3c36","0x3c69","0x3c6c","0x3cc3","0x3cc6","0x3d37","0x3d3f","0x3d48","0x3d68","0x3d77","0x3d8f","0x3dc6","0x3e43","0x3e46","0x3e85","0x3ea5","0x3ec7","0x3ecb","0x3ece","0x3ed3","0x3ed6","0x3ee7","0x3eef","0x3ef7","0x3f0f","0x3f46","0x3f9d","0x3fb3","0x3fb6","0x3fc7","0x3fe9","0x3fec"],"reused_real_deletions":["0xfda","0x155b","0x155e","0x1d1a","0x1d4a","0x1d58","0x1eca","0x1f9a","0x1fca","0x1fd2","0x1fd8","0x1fdb","0x1fde","0x255a","0x255b","0x2fdb","0x315a","0x343a","0x3478","0x351a","0x354a","0x3552","0x3558","0x355f","0x357b","0x357e","0x399e","0x3b1e","0x3b9a","0x3b9e","0x3bfc","0x3c75","0x3dcb","0x3eab","0x3eae","0x3ef1","0x3eff","0x3f4b","0x3faf","0x3fdf","0x3ff5","0x3ffb","0x3ffe"],"schema_version":1,"search_statistics":{"new_targets":103,"per_target":[["0x2c4a",28,"exhausted"],["0x2c52",28,"exhausted"],["0x2c58",28,"exhausted"],["0x344a",28,"exhausted"],["0x3452",28,"exhausted"],["0x3858",28,"exhausted"],["0x1c5c",66,"witness"],["0x247a",330,"exhausted"],["0x295a",330,"exhausted"],["0x2c1b",36,"exhausted"],["0x2c3a",36,"exhausted"],["0x2d1a",120,"exhausted"],["0x2d52",120,"exhausted"],["0x341b",36,"exhausted"],["0x341e",36,"exhausted"],["0x3459",36,"exhausted"],["0x345c",36,"exhausted"],["0x386a",36,"exhausted"],["0x3952",150,"witness"],["0x3c0b",8,"exhausted"],["0x3c0e",8,"exhausted"],["0x3c13",36,"exhausted"],["0x3c16",36,"exhausted"],["0x3c49",36,"exhausted"],["0x3c4c",36,"exhausted"],["0x3c54",8,"exhausted"],["0x1ada",495,"exhausted"],["0x1c9b",45,"exhausted"],["0x1c9e",45,"exhausted"],["0x1e1b",45,"exhausted"],["0x1e1e",45,"exhausted"],["0x2d72",495,"exhausted"],["0x2dca",165,"exhausted"],["0x2dd8",165,"exhausted"],["0x2f4a",165,"exhausted"],["0x2f58",165,"exhausted"],["0x345b",495,"exhausted"],["0x345e",495,"exhausted"],["0x393a",495,"exhausted"],["0x395a",1287,"exhausted"],["0x39d8",165,"exhausted"],["0x3aca",45,"exhausted"],["0x3b58",165,"exhausted"],["0x3c99",45,"exhausted"],["0x3c9c",45,"exhausted"],["0x3e19",45,"exhausted"],["0x3e1c",45,"exhausted"],["0x1e9b",220,"exhausted"],["0x2fca",715,"exhausted"],["0x351f",1437,"witness"],["0x355d",1576,"witness"],["0x356b",2002,"exhausted"],["0x356e",2002,"exhausted"],["0x3573",2002,"exhausted"],["0x3576",2002,"exhausted"],["0x39ce",220,"exhausted"],["0x39ea",220,"exhausted"],["0x3af8",220,"exhausted"],["0x3b4e",220,"exhausted"],["0x3b6a",220,"exhausted"],["0x3bd8",715,"exhausted"],["0x3c1f",220,"exhausted"],["0x3d1b",715,"exhausted"],["0x3d1e",715,"exhausted"],["0x1f9b",3003,"exhausted"],["0x1f9e",3003,"exhausted"],["0x1fd6",1112,"witness"],["0x1fd9",3003,"exhausted"],["0x1fdc",3003,"exhausted"],["0x2fda",3003,"exhausted"],["0x347f",8008,"exhausted"],["0x3caf",66,"exhausted"],["0x3dab",286,"exhausted"],["0x3dbc",286,"exhausted"],["0x3dce",1001,"exhausted"],["0x3dea",1001,"exhausted"],["0x3df1",286,"exhausted"],["0x3df8",1001,"exhausted"],["0x3e2f",66,"exhausted"],["0x3ee6",286,"exhausted"],["0x3ef4",66,"exhausted"],["0x3f2b",286,"exhausted"],["0x3f3c",286,"exhausted"],["0x3f4e",1001,"exhausted"],["0x3f6a",1001,"exhausted"],["0x3f71",286,"exhausted"],["0x3f78",1001,"exhausted"],["0x3f8e",286,"exhausted"],["0x3fd4",286,"exhausted"],["0x2efb",12376,"exhausted"],["0x3d7f",50388,"exhausted"],["0x3f9f",18564,"exhausted"],["0x3fbb",18564,"exhausted"],["0x3fbe",18564,"exhausted"],["0x3fcf",18564,"exhausted"],["0x3fd7",18564,"exhausted"],["0x3fdd",18564,"exhausted"],["0x3feb",18564,"exhausted"],["0x3fee",18564,"exhausted"],["0x3ff3",18564,"exhausted"],["0x3ff6",18564,"exhausted"],["0x3ff9",18564,"exhausted"],["0x3ffc",18564,"exhausted"]],"profiles_checked":340727},"source_manifest_sha256":"c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64","source_rows":280,"witnesses":[{"origin":"prior-integral","target":"0x5a","x":[8,0,8,0,0,8,0,8,8,8,8,8,8,8]},{"origin":"prior-integral","target":"0xc0a","x":[8,0,8,0,8,8,8,8,8,8,0,0,8,8]},{"origin":"prior-integral","target":"0xc50","x":[8,8,8,8,0,8,0,8,8,8,0,0,8,8]},{"origin":"prior-integral","target":"0xc51","x":[0,8,8,8,1,8,0,8,8,8,0,0,8,8]},{"origin":"prior-integral","target":"0xd0a","x":[8,1,8,0,8,8,8,8,0,8,0,0,8,8]},{"origin":"prior-integral","target":"0xd50","x":[8,8,8,8,1,8,0,8,0,8,0,0,8,8]},{"origin":"prior-integral","target":"0xe8a","x":[8,1,8,0,8,8,8,0,8,0,0,0,8,8]},{"origin":"prior-integral","target":"0xedb","x":[0,2,8,0,2,8,0,0,8,0,0,0,8,8]},{"origin":"prior-integral","target":"0xf8a","x":[8,2,8,0,8,8,8,0,0,0,0,0,8,8]},{"origin":"prior-integral","target":"0xf8b","x":[0,3,8,0,8,8,8,0,0,0,0,0,8,8]},{"origin":"prior-integral","target":"0xfd0","x":[8,8,8,8,2,8,0,0,0,0,0,0,8,8]},{"origin":"prior-integral","target":"0xfd1","x":[0,8,8,8,3,8,0,0,0,0,0,0,8,8]},{"origin":"prior-integral","target":"0x1412","x":[8,0,8,8,0,8,8,8,8,8,0,8,0,8]},{"origin":"prior-integral","target":"0x1448","x":[8,8,8,0,8,8,0,8,8,8,0,8,0,8]},{"origin":"prior-integral","target":"0x145f","x":[0,2,0,2,0,8,0,8,8,8,0,8,0,8]},{"origin":"prior-integral","target":"0x1513","x":[0,2,8,8,0,8,8,8,0,8,0,8,0,8]},{"origin":"prior-integral","target":"0x1516","x":[8,2,0,8,0,8,8,8,0,8,0,8,0,8]},{"origin":"prior-integral","target":"0x1549","x":[0,8,8,2,8,8,0,8,0,8,0,8,0,8]},{"origin":"prior-integral","target":"0x154c","x":[8,8,0,2,8,8,0,8,0,8,0,8,0,8]},{"origin":"prior-integral","target":"0x1818","x":[8,8,8,0,0,8,8,8,8,8,8,0,0,8]},{"origin":"prior-integral","target":"0x1842","x":[8,0,8,8,8,8,0,8,8,8,8,0,0,8]},{"origin":"prior-integral","target":"0x1942","x":[8,1,8,8,8,8,0,8,0,8,8,0,0,8]},{"origin":"prior-integral","target":"0x1a98","x":[8,8,8,2,0,8,8,0,8,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1a9c","x":[8,8,0,3,0,8,8,0,8,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1ac2","x":[8,1,8,8,8,8,0,0,8,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1ade","x":[8,1,0,3,0,8,0,1,8,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1bc2","x":[8,2,8,8,8,8,0,0,0,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1bc6","x":[8,3,0,8,8,8,0,0,0,0,8,0,0,8]},{"origin":"prior-integral","target":"0x1c52","x":[8,1,8,8,1,8,0,8,8,8,0,0,0,8]},{"origin":"prior-integral","target":"0x1c59","x":[0,8,8,1,1,8,1,8,8,8,0,0,0,8]},{"origin":"new-integer","target":"0x1c5c","x":[8,8,0,2,1,8,0,8,8,8,0,0,0,8]},{"origin":"prior-integral","target":"0x1edf","x":[0,0,0,2,2,8,2,0,8,0,0,0,0,8]},{"origin":"prior-integral","target":"0x1fcb","x":[0,1,8,1,8,8,1,0,2,0,0,0,0,8]},{"origin":"prior-integral","target":"0x1fce","x":[8,1,0,1,8,8,2,0,1,0,0,0,0,8]},{"origin":"prior-integral","target":"0x1fd3","x":[0,1,8,8,2,8,1,0,1,0,0,0,0,8]},{"origin":"new-integer","target":"0x1fd6","x":[8,2,0,8,1,8,1,0,1,0,0,0,0,8]},{"origin":"prior-integral","target":"0x2418","x":[8,8,8,0,0,8,8,8,8,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2442","x":[8,0,8,8,8,8,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2462","x":[8,2,8,8,8,0,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2463","x":[0,3,8,8,8,0,0,8,8,8,0,8,8,0]},{"origin":"prior-integral","target":"0x247b","x":[0,3,8,1,0,0,0,8,8,8,1,8,8,0]},{"origin":"prior-integral","target":"0x2518","x":[8,8,8,2,0,8,8,8,0,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2519","x":[0,8,8,3,0,8,8,8,0,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2542","x":[8,2,8,8,8,8,0,8,0,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2543","x":[0,3,8,8,8,8,0,8,0,8,0,8,8,0]},{"origin":"prior-integral","target":"0x2812","x":[8,0,8,8,0,8,8,8,8,8,8,0,8,0]},{"origin":"prior-integral","target":"0x2848","x":[8,8,8,0,8,8,0,8,8,8,8,0,8,0]},{"origin":"prior-integral","target":"0x2912","x":[8,2,8,8,0,8,8,8,0,8,8,0,8,0]},{"origin":"prior-integral","target":"0x2932","x":[8,3,8,8,0,0,8,8,0,8,8,0,8,0]},{"origin":"prior-integral","target":"0x297a","x":[8,3,8,1,0,0,0,8,0,8,8,1,8,0]},{"origin":"prior-integral","target":"0x2ada","x":[8,2,8,2,0,8,0,0,8,0,8,0,8,0]},{"origin":"prior-integral","target":"0x2afa","x":[8,3,8,2,0,0,0,0,8,0,8,0,8,0]},{"origin":"prior-integral","target":"0x2bc8","x":[8,8,8,2,8,8,0,0,0,0,8,0,8,0]},{"origin":"prior-integral","target":"0x2be8","x":[8,8,8,3,8,0,0,0,0,0,8,0,8,0]},{"origin":"prior-integral","target":"0x2d3a","x":[8,1,8,0,2,0,8,8,1,8,0,0,8,0]},{"origin":"prior-integral","target":"0x2d3b","x":[0,1,8,1,3,0,8,8,0,8,0,0,8,0]},{"origin":"prior-integral","target":"0x2d73","x":[0,3,8,8,1,0,1,8,0,8,0,0,8,0]},{"origin":"prior-integral","target":"0x2d7b","x":[0,2,8,0,2,0,0,8,0,8,0,0,8,2]},{"origin":"prior-integral","target":"0x2eca","x":[8,1,8,1,8,8,1,0,8,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2ed3","x":[0,1,8,8,1,8,1,0,8,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2eea","x":[8,1,8,1,8,0,2,0,8,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2eeb","x":[0,1,8,1,8,0,3,0,8,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2ef3","x":[0,2,8,8,0,0,2,0,8,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2f9b","x":[0,1,8,1,1,8,8,0,2,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2fcb","x":[0,2,8,1,8,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2fd2","x":[8,1,8,8,1,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2fd3","x":[0,1,8,8,1,8,2,0,1,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2fd8","x":[8,8,8,1,1,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","target":"0x2fd9","x":[0,8,8,1,2,8,1,0,1,0,0,0,8,0]},{"origin":"prior-integral","target":"0x300a","x":[8,0,8,0,8,8,8,8,8,8,8,8,0,0]},{"origin":"prior-integral","target":"0x302a","x":[8,1,8,0,8,0,8,8,8,8,8,8,0,0]},{"origin":"prior-integral","target":"0x3050","x":[8,8,8,8,0,8,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","target":"0x3070","x":[8,8,8,8,1,0,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","target":"0x307e","x":[8,2,0,0,2,0,0,8,8,8,8,8,0,0]},{"origin":"prior-integral","target":"0x310a","x":[8,1,8,0,8,8,8,8,0,8,8,8,0,0]},{"origin":"prior-integral","target":"0x312e","x":[8,3,0,0,8,0,8,8,0,8,8,8,0,0]},{"origin":"prior-integral","target":"0x3150","x":[8,8,8,8,1,8,0,8,0,8,8,8,0,0]},{"origin":"prior-integral","target":"0x3174","x":[8,8,0,8,3,0,0,8,0,8,8,8,0,0]},{"origin":"prior-integral","target":"0x344b","x":[0,0,8,1,8,8,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","target":"0x344e","x":[8,0,0,1,8,8,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","target":"0x3453","x":[0,2,8,8,1,8,0,8,8,8,0,8,0,0]},{"origin":"prior-integral","target":"0x3456","x":[8,2,0,8,1,8,0,8,8,8,0,8,0,0]},{"origin":"prior-integral","target":"0x346f","x":[0,2,0,0,8,0,2,8,8,8,0,8,0,0]},{"origin":"prior-integral","target":"0x3477","x":[0,2,0,8,0,0,2,8,8,8,0,8,0,0]},{"origin":"new-integer","target":"0x351f","x":[0,1,0,1,2,8,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x353b","x":[0,1,8,1,2,0,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x353e","x":[8,2,0,1,1,0,8,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x354f","x":[0,1,0,1,8,8,2,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x3557","x":[0,2,0,8,1,8,1,8,1,8,0,8,0,0]},{"origin":"new-integer","target":"0x355d","x":[0,8,0,2,1,8,1,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x3579","x":[0,8,8,2,1,0,1,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x357c","x":[8,8,0,1,1,0,2,8,1,8,0,8,0,0]},{"origin":"prior-integral","target":"0x383a","x":[8,1,8,1,1,0,8,8,8,8,8,0,0,0]},{"origin":"prior-integral","target":"0x3852","x":[8,1,8,8,1,8,0,8,8,8,8,0,0,0]},{"origin":"prior-integral","target":"0x393e","x":[8,3,0,1,1,0,8,8,0,8,8,0,0,0]},{"origin":"new-integer","target":"0x3952","x":[8,1,8,8,2,8,1,8,0,8,8,0,0,0]},{"origin":"prior-integral","target":"0x3976","x":[8,1,0,8,1,0,1,8,2,8,8,0,0,0]},{"origin":"prior-integral","target":"0x397e","x":[8,2,0,0,2,0,0,8,0,8,8,0,0,2]},{"origin":"prior-integral","target":"0x3ada","x":[8,2,8,2,1,8,0,0,8,0,8,0,0,0]},{"origin":"prior-integral","target":"0x3afe","x":[8,1,0,1,3,0,1,0,8,0,8,0,0,0]},{"origin":"prior-integral","target":"0x3bca","x":[8,1,8,1,8,8,1,0,1,0,8,0,0,0]},{"origin":"prior-integral","target":"0x3bee","x":[8,1,0,1,8,0,1,0,2,0,8,0,0,0]},{"origin":"prior-integral","target":"0x3c01","x":[0,8,8,8,8,8,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3c04","x":[8,8,0,8,8,8,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3c21","x":[1,8,8,8,8,0,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3c24","x":[8,8,1,8,8,0,8,8,8,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3c33","x":[0,1,8,8,0,0,8,8,8,8,1,1,0,0]},{"origin":"prior-integral","target":"0x3c36","x":[8,1,0,8,0,0,8,8,8,8,1,1,0,0]},{"origin":"prior-integral","target":"0x3c69","x":[0,8,8,1,8,0,0,8,8,8,1,1,0,0]},{"origin":"prior-integral","target":"0x3c6c","x":[8,8,0,1,8,0,0,8,8,8,1,1,0,0]},{"origin":"prior-integral","target":"0x3cc3","x":[0,1,8,8,8,8,0,0,8,8,1,0,0,0]},{"origin":"prior-integral","target":"0x3cc6","x":[8,1,0,8,8,8,0,0,8,8,1,0,0,0]},{"origin":"prior-integral","target":"0x3d37","x":[0,3,0,8,0,0,8,8,0,8,1,1,0,0]},{"origin":"prior-integral","target":"0x3d3f","x":[0,1,0,0,2,0,8,8,1,8,0,0,0,2]},{"origin":"prior-integral","target":"0x3d48","x":[8,8,8,2,8,8,0,8,0,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3d68","x":[8,8,8,3,8,0,0,8,0,8,0,0,0,0]},{"origin":"prior-integral","target":"0x3d77","x":[0,2,0,8,2,0,0,8,0,8,0,0,0,2]},{"origin":"prior-integral","target":"0x3d8f","x":[0,2,0,0,8,8,8,0,0,8,0,0,1,0]},{"origin":"prior-integral","target":"0x3dc6","x":[8,2,0,8,8,8,0,0,0,8,1,0,0,0]},{"origin":"prior-integral","target":"0x3e43","x":[0,1,8,8,8,8,0,8,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3e46","x":[8,1,0,8,8,8,0,8,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3e85","x":[0,8,0,8,8,8,8,0,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3ea5","x":[0,8,0,8,8,0,8,0,8,0,2,0,0,0]},{"origin":"prior-integral","target":"0x3ec7","x":[0,1,0,8,8,8,0,0,8,0,1,1,0,0]},{"origin":"prior-integral","target":"0x3ecb","x":[0,0,8,1,8,8,2,0,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3ece","x":[8,0,0,1,8,8,2,0,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3ed3","x":[0,1,8,8,1,8,1,0,8,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3ed6","x":[8,1,0,8,0,8,0,0,8,0,1,0,1,1]},{"origin":"prior-integral","target":"0x3ee7","x":[0,1,0,8,8,0,0,0,8,0,3,1,0,0]},{"origin":"prior-integral","target":"0x3eef","x":[0,2,0,0,8,0,0,0,8,0,2,0,0,2]},{"origin":"prior-integral","target":"0x3ef7","x":[0,0,0,8,0,0,2,0,8,0,2,0,0,2]},{"origin":"prior-integral","target":"0x3f0f","x":[0,2,0,0,8,8,8,8,0,0,0,0,1,0]},{"origin":"prior-integral","target":"0x3f46","x":[8,2,0,8,8,8,0,8,0,0,1,0,0,0]},{"origin":"prior-integral","target":"0x3f9d","x":[0,8,0,3,0,8,8,0,0,0,1,1,0,0]},{"origin":"prior-integral","target":"0x3fb3","x":[1,3,8,8,0,0,8,0,0,0,0,1,0,0]},{"origin":"prior-integral","target":"0x3fb6","x":[8,3,1,8,0,0,8,0,0,0,0,1,0,0]},{"origin":"prior-integral","target":"0x3fc7","x":[0,3,0,8,8,8,0,0,0,0,1,1,0,0]},{"origin":"prior-integral","target":"0x3fe9","x":[0,8,8,3,8,0,0,0,0,0,1,1,0,0]},{"origin":"prior-integral","target":"0x3fec","x":[8,8,0,3,8,0,0,0,0,0,1,1,0,0]}]} diff --git a/research/p112-integer-demand-kernel/SOURCE-PINS.json b/research/p112-integer-demand-kernel/SOURCE-PINS.json new file mode 100644 index 0000000000..fe77c76b93 --- /dev/null +++ b/research/p112-integer-demand-kernel/SOURCE-PINS.json @@ -0,0 +1,28 @@ +{ + "files": { + "MATRIX-6425.json": { + "git_blob": "e18f92e001b8ce9d44287760516bf6ea002bcbcd", + "repository": "petalas/integer-mult-bounds", + "commit": "092dcbd13d1263e691ad29f34fbf286fea1fac2c", + "path": "research/p112-demand-kernel/RESULT.json", + "bytes": 22234, + "sha256": "f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89" + }, + "REAL-RESULT-6455.json": { + "git_blob": "1ee2f6269556d155b5d265b8c1a0ace6b0e13e22", + "repository": "ToikY/integer-mult-bounds", + "commit": "7fdae743973bebb77daf4508d05655dc1e8915c7", + "path": "research/p112-farkas-kernel/RESULT.json", + "bytes": 31660, + "sha256": "b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704" + }, + "README-6455.md": { + "git_blob": "27aea79adbd206d95ffe94f01fa69d8ca478ab5e", + "repository": "ToikY/integer-mult-bounds", + "commit": "7fdae743973bebb77daf4508d05655dc1e8915c7", + "path": "research/p112-farkas-kernel/README.md", + "bytes": 5522, + "sha256": "dd2849071a27cf4fa8023a8d3cba767199afeb977cc7e5c5acab361e5006804d" + } + } +} diff --git a/research/p112-integer-demand-kernel/SOURCES.json b/research/p112-integer-demand-kernel/SOURCES.json new file mode 100644 index 0000000000..d2f056059e --- /dev/null +++ b/research/p112-integer-demand-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 metadata is provenance only. Runtime closure is three inert source data/documents plus the new certificate, all package-local and independently authenticated. No predecessor executable or clique census is run." +} diff --git a/research/p112-integer-demand-kernel/TASK.json b/research/p112-integer-demand-kernel/TASK.json new file mode 100644 index 0000000000..2578764d0b --- /dev/null +++ b/research/p112-integer-demand-kernel/TASK.json @@ -0,0 +1,103 @@ +{ + "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 PR6455 README next-question1 (TASK entry2): determine the integer-only demand subfamily, rather than synthesize a full rank-shape supplier. The earlier237-row real result leaves103labels unresolved on the integer orthant after43real deletions and134integral witnesses. Reused coverage is checked and credited, not counted as new.", + "actual_scope": "Complete integer-only classification of the fixed280original P112 demand inequalities over unrestricted nonnegative integer14-vectors, via exact finite projection and literal separating points.", + "bottleneck_link": "Integer multiplicities describe whole support terms. An equivalent smaller necessary-condition screen can simplify support search; it supplies neither coefficients nor a paid physical construction.", + "budget_minutes": 60, + "stop_rule": "One fixed integer-system result or precise UNKNOWN/partial handoff on capacity exhaustion. Freeze science by2026-11-03T00:59:00Z, reserve at least15minutes for verification/handoff and stop by01:14:00Z. No new alphabets, coefficient synthesis, decoder/COPY pricing or source clique census.", + "outcome": "completed", + "evidence": "98new integer obstructions exhaust336386profiles in independent vectorDFS;5new integer points plus134credited points force139retained rows.43credited realdeletions are validated. Complete280partition, strict normal/Oreceipts, semanticcontrols and source-bound projection/induction proof; no source executable/census.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance for implementation, proof and packaging. Separate checker code/enumeration and static review are AI corroboration, not independent human or formal-kernel acceptance.", + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363170", + "source_heads": { + "original6425": "092dcbd13d1263e691ad29f34fbf286fea1fac2c", + "real6455": "7fdae743973bebb77daf4508d05655dc1e8915c7" + }, + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "overlap": { + "open_pr_bodies": 425, + "nearest_work": [ + "PR6455 real237minimum+43implications+134integralpoints; integer-onlyminimumexplicitlyuncomputed", + "PR6425 original280kernel and source clique equivalence", + "PR6430 compatibilityreplay usesanother P112 screen", + "PR5767 suppliedLPcertificate semantics, no solverorintegerclassification" + ], + "limits": "Non-atomic pages deduplicated with freshfirstpage;15allstatequeries includingtruncated100resultbroadquery;6458PR404unknown;sparse/hidden/unpublished/arbitraryhistory gaps remain." + }, + "open_questions": [ + { + "question": "What is the smallest original-row subfamily after adding a concrete COPY/cost upper budget?", + "why_it_matters": "All-orthant equivalence remains valid after conjunction, but the unrestricted separating points may violate the budget, so its minimum need not persist.", + "first_step": "State one exact cost/budget constraint and derive a new complete counterexample projection respecting it.", + "blocked_by": "No extra cost domain is included in this fixed orthant result." + }, + { + "question": "Can a passing integer vector admit actual coefficients and a fully charged decoder?", + "why_it_matters": "Rank-demand inequalities are necessary conditions and do not construct coefficients or pay native/access/restoration/precision/stock/compiler/outer costs.", + "first_step": "Freeze one passing vector and its support/caller interface before coefficient synthesis and full pricing.", + "blocked_by": "Coefficient and physical supplier construction are outside this session." + }, + { + "question": "Does a changed cap alphabet admit the same type of finite integer projection?", + "why_it_matters": "Changing supports changes masks and can change maximum demand and the valid outside extension.", + "first_step": "Rebuild the complete changed quotient and verify the new domain and extension bound before reducing rows.", + "blocked_by": "Only the exact14source rectangles are in scope." + } + ] +} diff --git a/research/p112-integer-demand-kernel/VALIDATION.md b/research/p112-integer-demand-kernel/VALIDATION.md new file mode 100644 index 0000000000..170c223276 --- /dev/null +++ b/research/p112-integer-demand-kernel/VALIDATION.md @@ -0,0 +1,58 @@ +# Validation and credited reuse + +Three inert source objects were frozen before scientific execution: + +- Original PR6425 head `092dcbd13d1263e691ad29f34fbf286fea1fac2c` matrix: + Git blob `e18f92e001b8ce9d44287760516bf6ea002bcbcd`, SHA256 + `f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89`. +- Parent PR6455 head `7fdae743973bebb77daf4508d05655dc1e8915c7` real result: + Git blob `1ee2f6269556d155b5d265b8c1a0ace6b0e13e22`, SHA256 + `b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704`. +- Parent README: Git blob `27aea79adbd206d95ffe94f01fa69d8ca478ab5e`, + SHA256 `dd2849071a27cf4fa8023a8d3cba767199afeb977cc7e5c5acab361e5006804d`. +- Three-source manifest SHA256 + `c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64`. + +The 43 old real deletion certificates and 134 actual integral predecessor +points are rechecked as data, not counted as new results. No predecessor +executable, LP or clique census is imported/replayed. The original geometry +and complete-clique equivalence remain credited predecessor claims when +composing this literal matrix result with the larger support screen. + +The primary first execution passed. Normal/optimized emissions and strict +defaults passed with identical JSON and empty stderr. Primary certificate: +50,830 bytes, SHA256 +`f4959ac06a189e817a4fc14c428b9bd02dd9f344f20022cd159d8acfd972fa54`. +It contains 98 new integer obstructions, five new integer points, 139 retained +rows, and the explicit prior-coverage partition. Across all 103 new targets it +visits 340,727 profiles, including 4,341 positive early-stop profiles. + +The independent checker was written before reading the new primary code or +result, then consumes the sealed result as untrusted certificate data. It uses +iterative vector-budget DFS instead of multiset enumeration, independently +regenerates all 336,386 profiles in 98 negative domains, and checks all 139 +integer points against all 279 other source rows. Its first execution passed; +normal/optimized emissions were byte-identical and both strict defaults passed. +Independent receipt: 48,964 bytes, SHA256 +`5a0ea35df19ee7cc72607fbb4ec8ca51a95ffa1cdea1e73e40214311a5dd47a1`. + +There were no scientific execution failures. Before the first independent run, +static review renamed two control labels to describe altered saved counts and +histograms accurately. These controls do not mutate DFS traversal. The checker +has 16 rejection cases plus a separate literal two-dimensional coverage toy. +Its core obstruction comparison intentionally ignores the primary's optional +ordered transcript SHA256; that hash is primary-only provenance. Acceptance +rests on complete regenerated profiles, proper-subset failures, direct integer +points and the written coverage/induction proof. + +An explanatory exact half-sum for target `0x1ada` was checked against the frozen +matrix: the three donor demands 4, 3 and 2 give RHS `9/2` and exactly the target +coefficient vector. Integer rounding gives demand 5. This example is not used +as a substitute for any complete obstruction check. + +All assertions used for acceptance are explicit exceptions and remain active +under optimized Python. `--emit` writes stdout only. Package, source/commit +mode/history, read-only cold export, external artifact corruption, static +review and exact-head hosted CI are distinct obligations recorded in session +receipts and public handoff. No physical supplier, coefficient synthesis, +cost-constrained minimum, κ or selected-frontier update is asserted. diff --git a/research/p112-integer-demand-kernel/VERIFY.json b/research/p112-integer-demand-kernel/VERIFY.json new file mode 100644 index 0000000000..f15b97739c --- /dev/null +++ b/research/p112-integer-demand-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": "Authenticate3frozen sources, validate/reuse43realcertificates and134actualintegralpoints, classifyremaining103 with bounded multiset weak compositions, verify full integer witnesses/allnegative coverage, and strictly compare complete retained RESULT. No predecessor code/census." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 300, + "checks": "Independent vector-budget DFS regenerates every new negative finite obstruction and its exact coverage/histogram; direct source/rational reuse and all279-row integer point checks, semantic controls and strict complete ORACLE receipt. No primarycode imports or LPsolver." + } + ] +} diff --git a/research/p112-integer-demand-kernel/oracle.py b/research/p112-integer-demand-kernel/oracle.py new file mode 100644 index 0000000000..79137abdf7 --- /dev/null +++ b/research/p112-integer-demand-kernel/oracle.py @@ -0,0 +1,393 @@ +#!/usr/bin/env python3 +"""Independent vector-DFS checking of a sealed integer-demand certificate. + +The source matrix and real certificates are inert authenticated data. This +checker imports no predecessor or primary executable and uses no solver. +Prior real deletions and integral points retain their authors' credit. +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 = 'c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64' +PINS = { + 'MATRIX-6425.json': (22234, 'f8d15306112914af299acca8720779fbc9f6f07bb1336c51e99304fdea5caf89', + 'e18f92e001b8ce9d44287760516bf6ea002bcbcd'), + 'REAL-RESULT-6455.json': (31660, 'b477f2a8d144ed884c78ee29ac76fd88c95b076eb2dd290ef2431dd7e4969704', + '1ee2f6269556d155b5d265b8c1a0ace6b0e13e22'), + 'README-6455.md': (5522, 'dd2849071a27cf4fa8023a8d3cba767199afeb977cc7e5c5acab361e5006804d', + '27aea79adbd206d95ffe94f01fa69d8ca478ab5e'), +} +DIMENSION, ROWS = 14, 280 +MAX_BYTES = 1024 * 1024 +MAX_ROW_PROFILES, MAX_TOTAL_PROFILES = 120000, 5000000 + + +class CapacityError(ValueError): + pass + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def capacity(ok, message): + if not ok: + raise CapacityError(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 bad(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=bad, parse_float=floating) + + +def read(path): + with path.open('rb') as handle: + raw = handle.read(MAX_BYTES+1) + capacity(len(raw) <= MAX_BYTES, 'input exceeds one-MiB capacity') + return raw + + +def authenticate(values, manifest): + require(hashlib.sha256(manifest).hexdigest() == MANIFEST_SHA, 'source manifest SHA256') + require(set(values) == set(PINS), 'exact three-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, 'bounded hex mask') + try: + number = int(value, 16) + except ValueError: + raise ValueError('invalid hex mask') from None + require(value == hex(number) and 0 < number < 1 << DIMENSION, 'canonical nonempty 14-bit mask') + return number + + +def rational(value): + require(type(value) is str and len(value) <= 512, 'bounded rational string') + require(re.fullmatch(r'-?(?:0|[1-9][0-9]*)(?:/[1-9][0-9]*)?', value) is not None, 'rational quotient grammar') + number = Fraction(value) + capacity(abs(number.numerator).bit_length() <= 256 and number.denominator.bit_length() <= 256, + 'rational exceeds 256-bit input capacity') + require(str(number) == value, 'canonical rational') + return number + + +def matrix(raw): + source = decode(raw) + require(type(source) is dict and source.get('kernel_rows') == ROWS, '280 source rows') + require(type(source.get('alphabet')) is list and len(source['alphabet']) == DIMENSION, '14 source columns') + records = source.get('kernel') + require(type(records) is list and len(records) == ROWS, 'source kernel records') + rows = {} + for record in records: + require(type(record) is list and len(record) == 3, 'source row shape') + number = mask(record[0]) + require(number not in rows and type(record[1]) is int and 1 <= record[1] <= 8, 'source demand/unique mask') + rows[number] = record[1] + return dict(sorted(rows.items())) + + +def dot(number, vector): + return sum(value for column, value in enumerate(vector) if number >> column & 1) + + +def integer_point(target, vector, rows): + require(type(vector) is list and len(vector) == DIMENSION, '14 integer coordinates') + require(all(type(value) is int and value >= 0 for value in vector), 'nonnegative integer coordinates') + capacity(all(value.bit_length() <= 256 for value in vector), 'point exceeds 256-bit input capacity') + require(dot(target, vector) < rows[target], 'point must strictly violate target') + require(all(dot(other, vector) >= demand for other, demand in rows.items() if other != target), + 'point violates another original inequality') + return {'target': hex(target), 'x': vector, 'target_lhs': dot(target, vector), + 'target_demand': rows[target], 'other_original_rows_checked': ROWS-1} + + +def old_deletion(record, retained, rows): + target = mask(record['target']) + require(target in rows and target not in retained, 'old deletion target') + terms = record['multipliers'] + require(type(terms) is list and 1 <= len(terms) <= ROWS, 'old 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, 'old multiplier pair') + donor, weight = mask(term[0]), rational(term[1]) + require(donor in retained and donor not in used and weight >= 0, 'old nonnegative unique retained premise') + require(weight == 0 or donor != target and donor & target == donor, 'old strict-subset premise') + used.add(donor) + rhs += weight*rows[donor] + for column in range(DIMENSION): + coefficients[column] += weight*(donor >> column & 1) + require(all(value <= (target >> k & 1) for k, value in enumerate(coefficients)), 'old coefficient overrun') + require(rhs >= rows[target], 'old demand implication') + return target + + +def prior_data(raw, rows): + prior = decode(raw) + require(type(prior) is dict and prior.get('dimension') == DIMENSION and prior.get('source_rows') == ROWS, 'prior dimensions') + retained = {mask(value) for value in prior['retained']} + require(len(retained) == 237 and retained <= rows.keys(), '237 prior retained rows') + removed = [old_deletion(record, retained, rows) for record in prior['deletions']] + require(len(removed) == 43 and len(set(removed)) == 43 and set(removed) == rows.keys()-retained, '43 prior real deletions') + require(type(prior.get('separators')) is list and len(prior['separators']) == 237, '237 prior separator records') + integral, seen = {}, set() + for record in prior['separators']: + target = mask(record['target']) + require(target in retained and target not in seen, 'distinct prior separator target') + seen.add(target) + require(type(record['x']) is list and len(record['x']) == DIMENSION, 'prior separator dimension') + vector = [rational(value) for value in record['x']] + if all(value.denominator == 1 for value in vector): + converted = [value.numerator for value in vector] + integer_point(target, converted, rows) + integral[target] = converted + require(len(integral) == 134, '134 actual integral prior points') + return set(removed), integral + + +def profiles(width, budget): + """Every nonnegative vector with sum<=budget has one root-to-leaf path.""" + pending = [(0, budget, ())] + while pending: + column, remaining, prefix = pending.pop() + if column == width: + yield prefix + else: + for value in range(remaining+1): + pending.append((column+1, remaining-value, prefix+(value,))) + + +def first_miss(vector, constraints): + for number, demand, columns in constraints: + if sum(vector[column] for column in columns) < demand: + return number + return None + + +def obstruction(target, rows, budget_limit=MAX_ROW_PROFILES): + coordinates = [column for column in range(DIMENSION) if target >> column & 1] + budget = rows[target]-1 + expected = math.comb(len(coordinates)+budget, len(coordinates)) + capacity(expected <= budget_limit, 'row profile capacity exceeded') + constraints = [(number, demand, tuple(k for k, column in enumerate(coordinates) if number >> column & 1)) + for number, demand in rows.items() if number != target and number & target == number] + histogram, checked = {}, 0 + for vector in profiles(len(coordinates), budget): + checked += 1 + capacity(checked <= expected, 'enumerator exceeded closed-form coverage') + missed = first_miss(vector, constraints) + require(missed is not None, 'obstruction has an integer counterexample') + histogram[missed] = histogram.get(missed, 0)+1 + require(checked == expected, 'enumerator incomplete closed-form coverage') + return {'target': hex(target), 'coordinates': coordinates, 'budget': budget, + 'expected_profiles': expected, 'checked_profiles': checked, + 'miss_histogram': [[hex(number), count] for number, count in sorted(histogram.items())]} + + +def partition(certificate, rows, old_removed, old_points): + require(type(certificate) is dict, 'certificate object') + for key, value in [('schema_version', 1), ('dimension', DIMENSION), ('source_rows', ROWS)]: + require(type(certificate.get(key)) is int and certificate[key] == value, 'typed '+key) + require(certificate.get('source_manifest_sha256') == MANIFEST_SHA, 'certificate source binding') + require(type(certificate.get('retained')) is list, 'retained list') + ordered = [mask(value) for value in certificate['retained']] + retained = set(ordered) + require(len(ordered) == len(retained) and old_points.keys() <= retained <= rows.keys(), 'retained distinct/prior coverage') + require(type(certificate.get('reused_real_deletions')) is list, 'reused deletion list') + reused = [mask(value) for value in certificate['reused_real_deletions']] + require(len(reused) == 43 and set(reused) == old_removed, 'exact reused real deletions') + require(type(certificate.get('obstructions')) is list and type(certificate.get('witnesses')) is list, 'obstruction/witness lists') + removed = [mask(record['target']) for record in certificate['obstructions']] + require(len(set(removed)) == len(removed), 'distinct obstruction targets') + require(not(retained & old_removed or retained & set(removed) or old_removed & set(removed)), 'disjoint partition') + require(retained | old_removed | set(removed) == rows.keys(), 'complete 280-row partition') + expected = sum(math.comb(number.bit_count()+rows[number]-1, number.bit_count()) for number in removed) + capacity(expected <= MAX_TOTAL_PROFILES, 'total profile capacity exceeded') + return retained + + +def positive_checks(records, retained, rows, old_points): + require(len(records) == len(retained), 'positive witness count') + checked, seen = [], set() + for record in records: + require(type(record) is dict, 'positive witness record') + target = mask(record.get('target')) + require(target in retained and target not in seen, 'unique retained witness') + seen.add(target) + if target in old_points: + require(record.get('origin') == 'prior-integral' and record.get('x') == old_points[target], 'literal credited prior integral witness') + else: + require(record.get('origin') == 'new-integer', 'new integer witness origin') + point = integer_point(target, record.get('x'), rows) + point['origin'] = record['origin'] + checked.append(point) + return sorted(checked, key=lambda item: mask(item['target'])) + + +def verify_certificate(certificate, rows, old_removed, old_points): + retained = partition(certificate, rows, old_removed, old_points) + points = positive_checks(certificate['witnesses'], retained, rows, old_points) + negative = [] + for record in certificate['obstructions']: + target = mask(record['target']) + expected = obstruction(target, rows) + same_obstruction(record, expected) + negative.append(expected) + return {'retained': [hex(value) for value in sorted(retained)], + 'integer_witnesses': points, 'new_obstructions': sorted(negative, key=lambda item: mask(item['target']))} + + +def same_obstruction(record, expected): + for key, value in expected.items(): + require(key in record and canonical(record[key]) == canonical(value), 'exact obstruction '+key) + + +def reject(callback, expected): + try: + callback() + except ValueError as error: + require(expected in str(error), 'unexpected rejection reason: '+str(error)) + return str(error) + raise ValueError('negative control accepted: '+expected) + + +def prior_negative_controls(sources, rows): + prior = decode(sources['REAL-RESULT-6455.json']) + retained = {mask(value) for value in prior['retained']} + result = {} + bad = deepcopy(prior['deletions'][0]) + bad['multipliers'][0][1] = '-1' + result['old_negative_multiplier'] = reject(lambda: old_deletion(bad, retained, rows), 'old nonnegative') + bad = deepcopy(prior['deletions'][0]) + bad['multipliers'][0][1] = str(rational(bad['multipliers'][0][1])+2) + result['old_coefficient_overrun'] = reject(lambda: old_deletion(bad, retained, rows), 'old coefficient overrun') + bad = deepcopy(prior['deletions'][0]) + for term in bad['multipliers']: + term[1] = '0' + result['old_zero_rhs'] = reject(lambda: old_deletion(bad, retained, rows), 'old demand implication') + return result + + +def negative_controls(certificate, rows, old_removed, old_points, sources, manifest, checked): + result = {} + retained = {mask(value) for value in certificate['retained']} + bad = deepcopy(certificate['witnesses']) + bad[0]['x'][0] = -1 + result['negative_point'] = reject(lambda: integer_point(mask(bad[0]['target']), bad[0]['x'], rows), 'nonnegative integer coordinates') + target = mask(certificate['witnesses'][0]['target']) + result['nonviolating_point'] = reject(lambda: integer_point(target, [8]*DIMENSION, rows), 'strictly violate target') + result['other_row_point_violation'] = reject(lambda: integer_point(target, [0]*DIMENSION, rows), 'another original inequality') + target = min(old_points) + result['false_obstruction'] = reject(lambda: obstruction(target, rows), 'integer counterexample') + result['row_capacity_UNKNOWN'] = reject(lambda: obstruction(target, rows, 0), 'profile capacity') + bad = deepcopy(certificate) + bad['reused_real_deletions'].pop() + result['missing_prior_deletion'] = reject(lambda: partition(bad, rows, old_removed, old_points), 'exact reused real deletions') + bad = deepcopy(certificate['witnesses']) + prior_index = next(i for i, record in enumerate(bad) if mask(record['target']) in old_points) + bad[prior_index]['x'] = list(bad[prior_index]['x']) + bad[prior_index]['x'][0] += 1 + result['altered_prior_point'] = reject(lambda: positive_checks(bad, retained, rows, old_points), 'literal credited prior') + altered = dict(sources) + altered['MATRIX-6425.json'] = b'X'+sources['MATRIX-6425.json'][1:] + result['source_byte_mutation'] = reject(lambda: authenticate(altered, manifest), 'source SHA256') + result['duplicate_key'] = reject(lambda: decode('{"x":1,"x":2}'), 'duplicate JSON key') + result['nonfinite'] = reject(lambda: decode('{"x":1e999}'), 'nonfinite JSON') + result['rational_exponent'] = reject(lambda: rational('1e999999'), 'quotient grammar') + if checked['new_obstructions']: + expected_record = checked['new_obstructions'][0] + bad = deepcopy(expected_record) + bad['checked_profiles'] -= 1 + result['altered_saved_profile_count'] = reject(lambda: same_obstruction(bad, expected_record), 'exact obstruction checked_profiles') + bad = deepcopy(expected_record) + bad['miss_histogram'][0][1] += 1 + result['altered_saved_first_miss_histogram'] = reject(lambda: same_obstruction(bad, expected_record), 'exact obstruction miss_histogram') + else: + result['obstruction_mutation_scope'] = 'Not applicable: no new obstruction certificate exists.' + expected = {(0, 0), (0, 1), (0, 2), (1, 0), (1, 1), (2, 0)} + observed = list(profiles(2, 2)) + require(len(observed) == math.comb(4, 2) and set(observed) == expected, 'literal vector-DFS toy coverage') + result['literal_vector_DFS_toy'] = {'profiles': sorted(observed), 'count': len(observed)} + result.update(prior_negative_controls(sources, rows)) + return result + + +def compute(): + manifest = read(ROOT/'SOURCE-PINS.json') + sources = {name: read(ROOT/'sources'/name) for name in PINS} + authenticate(sources, manifest) + rows = matrix(sources['MATRIX-6425.json']) + old_removed, old_points = prior_data(sources['REAL-RESULT-6455.json'], rows) + raw = read(ROOT/'RESULT.json') + certificate = decode(raw) + checked = verify_certificate(certificate, rows, old_removed, old_points) + controls = negative_controls(certificate, rows, old_removed, old_points, sources, manifest, checked) + return {'schema_version': 1, 'status': 'PASS_INDEPENDENT_INTEGER_DEMAND_KERNEL', + 'source_manifest_sha256': MANIFEST_SHA, 'primary_certificate_sha256': hashlib.sha256(raw).hexdigest(), + 'dimension': DIMENSION, 'source_rows': ROWS, 'retained_rows': len(checked['retained']), + 'reused_real_deletions': len(old_removed), 'reused_integral_points': len(old_points), + 'new_obstructions': len(checked['new_obstructions']), + 'total_new_obstruction_profiles': sum(record['checked_profiles'] for record in checked['new_obstructions']), + 'new_integer_points': len(checked['integer_witnesses'])-len(old_points), + 'method': 'Independent iterative vector-budget DFS verifies sealed primary data; literal all279-original-row integer points; no solver or primary/predecessor executable import', + 'checked': checked, 'negative_controls': controls, + 'limits': ['Fixed original280-row nonnegative-integer system; outside=8 constructs witnesses, not a global cap.', + 'Every new obstruction exhausts all inside totals<=demand-1; strict-subset source premises yield simultaneous implication by induction.', + '43 real implications and134 integral source points are authenticated credited reuse, not new coverage.', + 'Five-million total profiles,120000 per row,one-MiB inputs and256-bit input integers/rationals are fail-UNKNOWN capacities.', + 'No smallest arbitrary inequality description, changed cap alphabet, COPY floor, decoder, native supplier, kappa or frontier claim.']} + + +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(read(ROOT/'ORACLE.json')) + require(canonical(retained) == canonical(result), 'strict complete oracle receipt drift') + print('PASS_INDEPENDENT_INTEGER_DEMAND_KERNEL') + + +if __name__ == '__main__': + try: + main() + except CapacityError as error: + print('UNKNOWN: '+str(error), file=sys.stderr) + sys.exit(1) + except (ValueError, KeyError, TypeError, OSError) as error: + print('FAIL: '+str(error), file=sys.stderr) + sys.exit(1) diff --git a/research/p112-integer-demand-kernel/sources/MATRIX-6425.json b/research/p112-integer-demand-kernel/sources/MATRIX-6425.json new file mode 100644 index 0000000000..e18f92e001 --- /dev/null +++ b/research/p112-integer-demand-kernel/sources/MATRIX-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-integer-demand-kernel/sources/README-6455.md b/research/p112-integer-demand-kernel/sources/README-6455.md new file mode 100644 index 0000000000..27aea79adb --- /dev/null +++ b/research/p112-integer-demand-kernel/sources/README-6455.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-integer-demand-kernel/sources/REAL-RESULT-6455.json b/research/p112-integer-demand-kernel/sources/REAL-RESULT-6455.json new file mode 100644 index 0000000000..1ee2f62695 --- /dev/null +++ b/research/p112-integer-demand-kernel/sources/REAL-RESULT-6455.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-integer-demand-kernel/verify.py b/research/p112-integer-demand-kernel/verify.py new file mode 100644 index 0000000000..9bc05980d1 --- /dev/null +++ b/research/p112-integer-demand-kernel/verify.py @@ -0,0 +1,324 @@ +#!/usr/bin/env python3 +"""Finite integer-only classification of one frozen280-row demand system. + +Nick Petalas/6425, ToikY/6455 and PR1422/support lineage retain their credit. +New finite certificate: ToikY with OpenAI Codex assistance. Apache-2.0. +No source executable, LP, floating arithmetic or optional dependency is used. +""" +import argparse +from collections import Counter +from fractions import Fraction as F +import hashlib +from itertools import combinations_with_replacement +import json +from math import comb +from pathlib import Path +import time + +HERE = Path(__file__).resolve().parent +MANIFEST_SHA = 'c326b2a83adb02af94954c3904ee6e59822bf5fd274c847851abdcb63c1b9c64' +DIM, NROWS, OUTSIDE = 14, 280, 8 +CAPS = {'seconds': 180, 'total_profiles': 30000000, 'profiles_per_target': 200000} + + +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): + result = {} + for key, value in items: + require(key not in result, 'duplicate JSON key') + result[key] = value + return result + def bad(value): + raise ValueError('nonfinite JSON: ' + value) + return json.loads(raw, object_pairs_hook=unique, parse_constant=bad) + + +def authenticated(): + raw_manifest = (HERE / 'SOURCE-PINS.json').read_bytes() + require(hashlib.sha256(raw_manifest).hexdigest() == MANIFEST_SHA, 'source manifest SHA256') + pins = decode(raw_manifest)['files'] + require(set(pins) == {'MATRIX-6425.json', 'REAL-RESULT-6455.json', 'README-6455.md'}, 'three exact source files') + raw = {} + for name, pin in pins.items(): + value = (HERE / 'sources' / name).read_bytes() + require(len(value) == pin['bytes'], 'source byte length: ' + name) + require(hashlib.sha256(value).hexdigest() == pin['sha256'], 'source SHA256: ' + name) + require(hashlib.sha1(b'blob ' + str(len(value)).encode() + b'\0' + value).hexdigest() == pin['git_blob'], 'source Git blob: ' + name) + raw[name] = value + return decode(raw['MATRIX-6425.json']), decode(raw['REAL-RESULT-6455.json']) + + +def mask_value(text): + require(type(text) is str, 'hex support string') + mask = int(text, 16) + require(0 < mask < (1 << DIM) and text == hex(mask), 'canonical nonempty14-bit support') + return mask + + +def rational(text): + require(type(text) is str, 'canonical Fraction string') + value = F(text) + require(str(value) == text, 'canonical Fraction representation') + return value + + +def bits(mask): + return [k for k in range(DIM) if mask & (1 << k)] + + +def order(mask): + return mask.bit_count(), mask + + +def dot(mask, x): + return sum(x[k] for k in bits(mask)) + + +def matrix_rows(obj): + require(type(obj.get('kernel_rows')) is int and obj['kernel_rows'] == NROWS, '280 original rows') + require(type(obj.get('alphabet')) is list and len(obj['alphabet']) == DIM, '14 source variables') + require(type(obj.get('kernel')) is list and len(obj['kernel']) == NROWS, 'literal source kernel') + rows = {} + for entry in obj['kernel']: + require(type(entry) is list and len(entry) == 3, 'source kernel row schema') + mask = mask_value(entry[0]) + require(mask not in rows, 'unique source support') + demand = entry[1] + require(type(demand) is int and 1 <= demand <= OUTSIDE, 'source demand1..8') + require(type(entry[2]) is str and entry[2] == hex(int(entry[2], 16)) and int(entry[2], 16) > 0, 'source witness identifier') + rows[mask] = demand + return rows + + +def real_separator(target, x, rows): + require(target in rows and len(x) == DIM and all(value >= 0 for value in x), 'nonnegative real point') + require(all(dot(mask, x) >= demand for mask, demand in rows.items() if mask != target), 'point misses another original row') + require(dot(target, x) < rows[target], 'point must strictly violate target') + + +def integer_separator(target, x, rows): + require(type(x) is list and len(x) == DIM and all(type(value) is int and value >= 0 for value in x), 'literal nonnegative INTEGER witness') + real_separator(target, x, rows) + + +def validate_old_deletions(parent, retained, rows): + deleted = [] + require(type(parent['deletions']) is list and len(parent['deletions']) == 43, '43 legacy real deletions') + for record in parent['deletions']: + target = mask_value(record['target']) + require(target in rows and target not in retained and target not in deleted, 'legacy deletion partition') + coverage, demand, seen = [F(0)] * DIM, F(0), set() + require(type(record['multipliers']) is list and record['multipliers'], 'nonempty legacy multiplier list') + for raw_donor, raw_weight in record['multipliers']: + donor, weight = mask_value(raw_donor), rational(raw_weight) + require(donor in retained and donor not in seen and donor != target and donor & target == donor and weight >= 0, 'proper-subset nonnegative legacy donor') + seen.add(donor) + demand += weight * rows[donor] + for k in bits(donor): + coverage[k] += weight + require(all(v <= int(bool(target & (1 << k))) for k, v in enumerate(coverage)) and demand >= rows[target], 'legacy Farkas combination') + deleted.append(target) + require(set(deleted) | retained == set(rows), 'complete prior real partition') + return sorted(deleted) + + +def parent_data(parent, rows): + require(type(parent.get('dimension')) is int and parent['dimension'] == DIM and type(parent.get('source_rows')) is int and parent['source_rows'] == NROWS, 'parent dimensions') + require(type(parent.get('retained')) is list and len(parent['retained']) == 237, '237 legacy real retained rows') + sequence = [mask_value(text) for text in parent['retained']] + retained = set(sequence) + require(len(retained) == 237 and retained <= set(rows), 'unique legacy retained masks') + deleted = validate_old_deletions(parent, retained, rows) + require(type(parent['separators']) is list and len(parent['separators']) == 237, 'all237 legacy separators') + integral, all_points = {}, {} + for record in parent['separators']: + target = mask_value(record['target']) + require(target in retained and target not in all_points and type(record['x']) is list, 'legacy separator target') + x = [rational(text) for text in record['x']] + real_separator(target, x, rows) + all_points[target] = x + if all(value.denominator == 1 for value in x): + point = [int(value) for value in x] + integer_separator(target, point, rows) + integral[target] = point + require(set(all_points) == retained and len(integral) == 134, '134 actual prior integral points') + unresolved = sorted(retained - set(integral), key=order) + require(len(unresolved) == 103, '103 integer-only questions beyond predecessor') + return deleted, integral, unresolved + + +class Budget: + def __init__(self): + self.started = time.monotonic() + self.profiles = 0 + + def check(self): + require(time.monotonic() - self.started <= CAPS['seconds'], 'UNKNOWN: finite classification time cap') + require(self.profiles <= CAPS['total_profiles'], 'UNKNOWN: finite classification profile cap') + + def tick(self): + self.profiles += 1 + require(self.profiles <= CAPS['total_profiles'], 'UNKNOWN: finite classification profile cap') + if self.profiles % 1024 == 0: + self.check() + + +def obstruction_shape(record, rows): + target = mask_value(record['target']) + coordinates, bound = bits(target), rows[target] - 1 + expected = comb(len(coordinates) + bound, len(coordinates)) + require(record['coordinates'] == coordinates and record['budget'] == bound, 'obstruction domain') + require(type(record['expected_profiles']) is int and record['expected_profiles'] == expected and type(record['checked_profiles']) is int and record['checked_profiles'] == expected, 'complete weak-composition count') + total, seen = 0, set() + for raw_mask, count in record['miss_histogram']: + premise = mask_value(raw_mask) + require(premise in rows and premise != target and premise & target == premise and premise not in seen, 'obstruction premise must be a proper source subset') + require(type(count) is int and count > 0, 'positive miss count') + seen.add(premise) + total += count + require(total == expected, 'miss histogram covers complete domain') + + +def classify(target, rows, budget): + coordinates, bound = bits(target), rows[target] - 1 + expected = comb(len(coordinates) + bound, len(coordinates)) + require(expected <= CAPS['profiles_per_target'], 'UNKNOWN: target domain cap') + proper = [(mask, rows[mask], tuple(int(bool(mask & (1 << k))) for k in range(DIM))) + for mask in sorted(rows) if mask != target and mask & target == mask] + histogram, checked = Counter(), 0 + transcript = hashlib.sha256(b'p112-miss/v1\0' + target.to_bytes(2, 'big') + bytes((bound,))) + budget.check() + for total in range(bound + 1): + for allocation in combinations_with_replacement(coordinates, total): + budget.tick() + checked += 1 + missing = next((mask for mask, demand, members in proper if total < demand or sum(members[k] for k in allocation) < demand), None) + if missing is None: + x = [OUTSIDE] * DIM + for k in coordinates: + x[k] = 0 + for k in allocation: + x[k] += 1 + integer_separator(target, x, rows) + return x, None, checked + histogram[missing] += 1 + transcript.update(bytes((total,)) + bytes(allocation) + missing.to_bytes(2, 'big')) + require(checked == expected, 'actual complete weak-composition enumeration') + record = {'target': hex(target), 'coordinates': coordinates, 'budget': bound, + 'expected_profiles': expected, 'checked_profiles': checked, + 'miss_histogram': [[hex(mask), count] for mask, count in sorted(histogram.items())], + 'profile_sha256': transcript.hexdigest()} + obstruction_shape(record, rows) + budget.check() + return None, record, checked + + +def generate(rows, parent): + legacy, integral, unresolved = parent_data(parent, rows) + witnesses = {mask: {'target': hex(mask), 'x': x, 'origin': 'prior-integral'} for mask, x in integral.items()} + obstructions, statistics, budget = [], [], Budget() + for target in unresolved: + x, obstruction, checked = classify(target, rows, budget) + statistics.append([hex(target), checked, 'witness' if x is not None else 'exhausted']) + if x is not None: + witnesses[target] = {'target': hex(target), 'x': x, 'origin': 'new-integer'} + else: + obstructions.append(obstruction) + removed = {mask_value(record['target']) for record in obstructions} + retained = set(witnesses) + require(not(retained & set(legacy) or retained & removed or set(legacy) & removed), 'disjoint complete classification') + require(retained | set(legacy) | removed == set(rows), 'all280 original rows classified') + require(134 <= len(retained) <= 237 and len(witnesses) - 134 + len(obstructions) == 103, 'new-only classification counts') + for target, witness in witnesses.items(): + integer_separator(target, witness['x'], rows) + for record in obstructions: + obstruction_shape(record, rows) + budget.check() + return legacy, witnesses, sorted(obstructions, key=lambda record: int(record['target'], 16)), statistics, budget + + +def rejects(action): + try: + action() + except ValueError as error: + return str(error) + raise ValueError('invalid proof object accepted') + + +def controls(rows, witnesses, obstructions): + triangle = {3: 1, 5: 1, 6: 1, 7: 2} + x, obstruction, _checked = classify(7, triangle, Budget()) + require(x is None and obstruction['checked_profiles'] == 4, 'triangle integer-only obstruction') + fractional = [F(0)] * DIM + fractional[:3] = [F(1, 2)] * 3 + real_separator(7, fractional, triangle) + integer_error = rejects(lambda: integer_separator(7, fractional, triangle)) + boundary = {1: 1, 3: 2} + x, obstruction2, _checked = classify(3, boundary, Budget()) + require(obstruction2 is None and dot(3, x) == 1, 'inclusive d-1 boundary witness') + corrupted = dict(obstruction) + corrupted['checked_profiles'] -= 1 + count_error = rejects(lambda: obstruction_shape(corrupted, triangle)) + corrupted = dict(obstruction) + corrupted['miss_histogram'] = [['0x7', 4]] + circular_error = rejects(lambda: obstruction_shape(corrupted, triangle)) + target = min(witnesses) + changed = list(witnesses[target]['x']) + changed[bits(target)[0]] += rows[target] + strict_error = rejects(lambda: integer_separator(target, changed, rows)) + return {'triangle_real_integer_gap': {'target': '0x7', 'checked_profiles': 4, + 'fractional_point': ['1/2', '1/2', '1/2'], 'integer_domain_rejection': integer_error}, + 'inclusive_budget_boundary': {'target': '0x3', 'witness_first_two_coordinates': x[:2]}, + 'incomplete_count_rejection': count_error, 'self_premise_rejection': circular_error, + 'actual_witness_loses_strict_violation': {'target': hex(target), 'observed_error': strict_error}, + 'full_source_obstructions': len(obstructions)} + + +def run(): + source_matrix, parent = authenticated() + rows = matrix_rows(source_matrix) + legacy, witnesses, obstructions, statistics, budget = generate(rows, parent) + retained = sorted(witnesses) + return {'schema_version': 1, 'source_manifest_sha256': MANIFEST_SHA, + 'dimension': DIM, 'source_rows': len(rows), 'retained': list(map(hex, retained)), + 'reused_real_deletions': list(map(hex, legacy)), + 'witnesses': [witnesses[mask] for mask in retained], 'obstructions': obstructions, + 'counts': {'retained': len(retained), 'reused_real_deletions': len(legacy), + 'reused_integral_witnesses': 134, 'new_integer_witnesses': len(retained) - 134, + 'new_integer_only_deletions': len(obstructions)}, + 'search_statistics': {'new_targets': 103, 'profiles_checked': budget.profiles, 'per_target': statistics}, + 'declared_caps': CAPS, 'controls': controls(rows, witnesses, obstructions), + 'exhaustion_encoding': 'CWR coordinates ascending; total0..budget. SHA256 starts with p112-miss/v1 NUL,target two-byte big-endian,budget byte; each miss is total byte,allocation bytes,first-missed mask two-byte big-endian. Histogram/count/digest alone are not a proof: full negative domains are enumerated.', + 'limits': ['Only103previously unresolved integer labels are newly classified;43real deletion certificates and134actual integral separators are validated and reused as predecessor evidence.', + 'Unique minimum subset of the original280named rows on unrestricted nonnegative INTEGER variables; not a minimum arbitrary inequality description, facet theorem or support-alphabet extension.', + 'Equivalence can be conjoined with the same additional constraints, but indispensability/minimum need not survive added budget constraints that exclude these witnesses.', + 'Original clique census, caps, real280-row source equivalence, coefficients/decoder, COPY floor, native/physical/outer admission and kappa remain separate.']} + + +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 integer certificate receipt') + require(canonical(observed) == canonical(result), 'strict retained complete integer certificate') + print('PASS_P112_INTEGER_DEMAND_KERNEL') + + +if __name__ == '__main__': + main()