diff --git a/research/fstar-tied-residue-seeddcc97691/CERTIFICATE.json b/research/fstar-tied-residue-seeddcc97691/CERTIFICATE.json new file mode 100644 index 0000000000..6ecc7b3020 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/CERTIFICATE.json @@ -0,0 +1,1092 @@ +{ + "controls": { + "an_count": 1, + "brute_agree": 3, + "corrupt_rejects": 2, + "diag_cert": 3, + "mp_control": 5, + "mx_all_anchor": 1 + }, + "digest": "439d75261e9a2b9e", + "fixtures": { + "cex_min_1.json": { + "an_bound": 8, + "classification": { + "anchor_good": 8, + "repairable_1s": 0, + "tied_isotropic": 11 + }, + "diag_odd": 8, + "engine_witness": 18, + "fstar_holds": true, + "mp_bound": 16, + "mp_exhaustive": true, + "mx_bound": 16, + "mx_failures": { + "given/A_first: A->T conflict": 6144, + "given/T_first: T->AU conflict": 6144 + }, + "mx_map": { + "0": 1, + "1": 4, + "2": 1, + "3": 1, + "4": 4, + "5": 4, + "6": 1, + "7": 4, + "8": 1, + "9": 1, + "10": 4, + "11": 1, + "12": 4, + "13": 2, + "14": 2, + "15": 1, + "16": 2, + "17": 1, + "18": 2 + }, + "mx_meta": { + "mode": "A_first", + "variant": "allT" + }, + "recorded_cert": 18, + "threshold": 12, + "v": 19 + }, + "tied_min.json": { + "an_bound": 0, + "classification": { + "anchor_good": 0, + "repairable_1s": 0, + "tied_isotropic": 12 + }, + "diag_odd": 0, + "engine_witness": 11, + "fstar_holds": true, + "mp_bound": 9, + "mp_exhaustive": true, + "mx_bound": 9, + "mx_failures": {}, + "mx_map": { + "0": 2, + "1": 1, + "2": 1, + "3": 2, + "4": 1, + "5": 4, + "6": 2, + "7": 1, + "8": 2, + "9": 4, + "10": 4, + "11": 1 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "recorded_cert": 11, + "threshold": 8, + "v": 12 + } + }, + "search": { + "exact_decided": 16, + "falsifiers": 0, + "instances": 40, + "min_witness_ratio": 1.0, + "mp_below_threshold": 0, + "mx_below_threshold": 0, + "mx_strictly_above_mp": 0, + "records": [ + { + "an_bound": 0, + "cert_or_witness": 3, + "chain_cost_upper": 9, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 0 + }, + "exact": true, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 3, + "mx_bound": 3, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 3 + }, + { + "an_bound": 0, + "cert_or_witness": 3, + "chain_cost_upper": 9, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 0 + }, + "exact": true, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 3, + "mx_bound": 3, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 3 + }, + { + "an_bound": 1, + "cert_or_witness": 3, + "chain_cost_upper": 9, + "classification": { + "anchor_good": 1, + "repairable_1s": 1, + "tied_isotropic": 1 + }, + "exact": true, + "family": "mixed", + "k": 0, + "mp_bound": 3, + "mx_bound": 3, + "mx_failures": { + "given/T_first: T->AU conflict": 18 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 3 + }, + { + "an_bound": 1, + "cert_or_witness": 3, + "chain_cost_upper": 9, + "classification": { + "anchor_good": 1, + "repairable_1s": 2, + "tied_isotropic": 0 + }, + "exact": true, + "family": "mixed", + "k": 1, + "mp_bound": 3, + "mx_bound": 3, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 3 + }, + { + "an_bound": 0, + "cert_or_witness": 4, + "chain_cost_upper": 12, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 1 + }, + "exact": true, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 4, + "mx_bound": 4, + "mx_failures": { + "given/T_first: T->AU conflict": 54 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 4 + }, + { + "an_bound": 0, + "cert_or_witness": 4, + "chain_cost_upper": 12, + "classification": { + "anchor_good": 0, + "repairable_1s": 4, + "tied_isotropic": 0 + }, + "exact": true, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 4, + "mx_bound": 4, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 4 + }, + { + "an_bound": 2, + "cert_or_witness": 4, + "chain_cost_upper": 12, + "classification": { + "anchor_good": 2, + "repairable_1s": 2, + "tied_isotropic": 0 + }, + "exact": true, + "family": "mixed", + "k": 0, + "mp_bound": 4, + "mx_bound": 4, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 4 + }, + { + "an_bound": 2, + "cert_or_witness": 4, + "chain_cost_upper": 12, + "classification": { + "anchor_good": 2, + "repairable_1s": 2, + "tied_isotropic": 0 + }, + "exact": true, + "family": "mixed", + "k": 1, + "mp_bound": 4, + "mx_bound": 4, + "mx_failures": { + "A/T/A_first: A->T conflict": 54 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 4 + }, + { + "an_bound": 0, + "cert_or_witness": 5, + "chain_cost_upper": 15, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 2 + }, + "exact": true, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 5, + "mx_bound": 5, + "mx_failures": { + "given/T_first: T->AU conflict": 243 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 3, + "v": 5 + }, + { + "an_bound": 0, + "cert_or_witness": 5, + "chain_cost_upper": 12, + "classification": { + "anchor_good": 0, + "repairable_1s": 4, + "tied_isotropic": 1 + }, + "exact": true, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 5, + "mx_bound": 5, + "mx_failures": { + "given/T_first: T->AU conflict": 243 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 3, + "v": 5 + }, + { + "an_bound": 2, + "cert_or_witness": 5, + "chain_cost_upper": 15, + "classification": { + "anchor_good": 2, + "repairable_1s": 2, + "tied_isotropic": 1 + }, + "exact": true, + "family": "mixed", + "k": 0, + "mp_bound": 5, + "mx_bound": 5, + "mx_failures": { + "A/T/T_first: T->AU conflict": 162, + "given/T_first: T->AU conflict": 162 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 3, + "v": 5 + }, + { + "an_bound": 2, + "cert_or_witness": 5, + "chain_cost_upper": 15, + "classification": { + "anchor_good": 2, + "repairable_1s": 3, + "tied_isotropic": 0 + }, + "exact": true, + "family": "mixed", + "k": 1, + "mp_bound": 5, + "mx_bound": 5, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 3, + "v": 5 + }, + { + "an_bound": 0, + "cert_or_witness": 6, + "chain_cost_upper": 18, + "classification": { + "anchor_good": 0, + "repairable_1s": 5, + "tied_isotropic": 1 + }, + "exact": true, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 6, + "mx_bound": 6, + "mx_failures": { + "given/T_first: T->AU conflict": 729 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 6 + }, + { + "an_bound": 0, + "cert_or_witness": 6, + "chain_cost_upper": 18, + "classification": { + "anchor_good": 0, + "repairable_1s": 4, + "tied_isotropic": 2 + }, + "exact": true, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 6, + "mx_bound": 6, + "mx_failures": { + "given/T_first: T->AU conflict": 729 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 6 + }, + { + "an_bound": 3, + "cert_or_witness": 6, + "chain_cost_upper": 18, + "classification": { + "anchor_good": 3, + "repairable_1s": 2, + "tied_isotropic": 1 + }, + "exact": true, + "family": "mixed", + "k": 0, + "mp_bound": 6, + "mx_bound": 6, + "mx_failures": { + "given/T_first: T->AU conflict": 729 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 6 + }, + { + "an_bound": 3, + "cert_or_witness": 6, + "chain_cost_upper": 18, + "classification": { + "anchor_good": 3, + "repairable_1s": 3, + "tied_isotropic": 0 + }, + "exact": true, + "family": "mixed", + "k": 1, + "mp_bound": 6, + "mx_bound": 6, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 6 + }, + { + "an_bound": 0, + "cert_or_witness": 7, + "chain_cost_upper": 21, + "classification": { + "anchor_good": 0, + "repairable_1s": 6, + "tied_isotropic": 1 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 7, + "mx_bound": 7, + "mx_failures": { + "given/T_first: T->AU conflict": 530 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 7 + }, + { + "an_bound": 0, + "cert_or_witness": 7, + "chain_cost_upper": 21, + "classification": { + "anchor_good": 0, + "repairable_1s": 7, + "tied_isotropic": 0 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 7, + "mx_bound": 7, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 7 + }, + { + "an_bound": 3, + "cert_or_witness": 7, + "chain_cost_upper": 21, + "classification": { + "anchor_good": 3, + "repairable_1s": 4, + "tied_isotropic": 0 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 7, + "mx_bound": 7, + "mx_failures": { + "A/T/A_first: A->T conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 7 + }, + { + "an_bound": 3, + "cert_or_witness": 7, + "chain_cost_upper": 21, + "classification": { + "anchor_good": 3, + "repairable_1s": 4, + "tied_isotropic": 0 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 7, + "mx_bound": 7, + "mx_failures": { + "A/T/A_first: A->T conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 4, + "v": 7 + }, + { + "an_bound": 0, + "cert_or_witness": 8, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 0, + "repairable_1s": 7, + "tied_isotropic": 1 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 8, + "mx_bound": 8, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 5, + "v": 8 + }, + { + "an_bound": 0, + "cert_or_witness": 8, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 0, + "repairable_1s": 6, + "tied_isotropic": 2 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 8, + "mx_bound": 8, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 5, + "v": 8 + }, + { + "an_bound": 4, + "cert_or_witness": 8, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 4, + "repairable_1s": 2, + "tied_isotropic": 2 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 8, + "mx_bound": 8, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "given/T_first: T->AU conflict": 724 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 5, + "v": 8 + }, + { + "an_bound": 4, + "cert_or_witness": 8, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 4, + "repairable_1s": 4, + "tied_isotropic": 0 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 8, + "mx_bound": 8, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "A/T/T_first: T->AU conflict": 564 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 5, + "v": 8 + }, + { + "an_bound": 0, + "cert_or_witness": 9, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 0, + "repairable_1s": 7, + "tied_isotropic": 2 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 9, + "mx_bound": 9, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 9 + }, + { + "an_bound": 0, + "cert_or_witness": 9, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 0, + "repairable_1s": 6, + "tied_isotropic": 3 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 9, + "mx_bound": 9, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 9 + }, + { + "an_bound": 4, + "cert_or_witness": 9, + "chain_cost_upper": 27, + "classification": { + "anchor_good": 4, + "repairable_1s": 4, + "tied_isotropic": 1 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 9, + "mx_bound": 9, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "given/A_first: A->T conflict": 800, + "given/T_first: T->AU conflict": 541 + }, + "mx_meta": { + "mode": "T_first", + "variant": "given" + }, + "threshold": 6, + "v": 9 + }, + { + "an_bound": 4, + "cert_or_witness": 9, + "chain_cost_upper": 24, + "classification": { + "anchor_good": 4, + "repairable_1s": 4, + "tied_isotropic": 1 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 9, + "mx_bound": 9, + "mx_failures": { + "A/T/A_first: A->T conflict": 539, + "A/T/T_first: T->AU conflict": 537, + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 9 + }, + { + "an_bound": 0, + "cert_or_witness": 10, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 0, + "repairable_1s": 7, + "tied_isotropic": 3 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 10, + "mx_bound": 10, + "mx_failures": { + "given/A_first: U line 5 has no admissible one-sided repair": 623, + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 10 + }, + { + "an_bound": 0, + "cert_or_witness": 10, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 0, + "repairable_1s": 8, + "tied_isotropic": 2 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 10, + "mx_bound": 10, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 10 + }, + { + "an_bound": 5, + "cert_or_witness": 10, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 5, + "repairable_1s": 2, + "tied_isotropic": 3 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 10, + "mx_bound": 10, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "A/T/T_first: T->AU conflict": 764, + "given/T_first: T->AU conflict": 761 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 6, + "v": 10 + }, + { + "an_bound": 5, + "cert_or_witness": 10, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 5, + "repairable_1s": 2, + "tied_isotropic": 3 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 10, + "mx_bound": 10, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "A/T/T_first: T->AU conflict": 710, + "given/A_first: A->T conflict": 800, + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "T_first", + "variant": "A/T" + }, + "threshold": 6, + "v": 10 + }, + { + "an_bound": 0, + "cert_or_witness": 11, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 0, + "repairable_1s": 5, + "tied_isotropic": 6 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 11, + "mx_bound": 11, + "mx_failures": { + "given/T_first: T->AU conflict": 769 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 7, + "v": 11 + }, + { + "an_bound": 0, + "cert_or_witness": 11, + "chain_cost_upper": 30, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 8 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 11, + "mx_bound": 11, + "mx_failures": { + "given/T_first: T->AU conflict": 767 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 7, + "v": 11 + }, + { + "an_bound": 5, + "cert_or_witness": 11, + "chain_cost_upper": 33, + "classification": { + "anchor_good": 5, + "repairable_1s": 4, + "tied_isotropic": 2 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 11, + "mx_bound": 11, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "A/T/T_first: T->AU conflict": 800, + "given/A_first: A->T conflict": 800, + "given/T_first: T->AU conflict": 707 + }, + "mx_meta": { + "mode": "T_first", + "variant": "given" + }, + "threshold": 7, + "v": 11 + }, + { + "an_bound": 5, + "cert_or_witness": 11, + "chain_cost_upper": 33, + "classification": { + "anchor_good": 5, + "repairable_1s": 4, + "tied_isotropic": 2 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 11, + "mx_bound": 11, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 7, + "v": 11 + }, + { + "an_bound": 0, + "cert_or_witness": 12, + "chain_cost_upper": 33, + "classification": { + "anchor_good": 0, + "repairable_1s": 6, + "tied_isotropic": 6 + }, + "exact": false, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 12, + "mx_bound": 12, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 8, + "v": 12 + }, + { + "an_bound": 0, + "cert_or_witness": 12, + "chain_cost_upper": 33, + "classification": { + "anchor_good": 0, + "repairable_1s": 8, + "tied_isotropic": 4 + }, + "exact": false, + "family": "tied_isotropic", + "k": 1, + "mp_bound": 12, + "mx_bound": 12, + "mx_failures": { + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 8, + "v": 12 + }, + { + "an_bound": 6, + "cert_or_witness": 12, + "chain_cost_upper": 33, + "classification": { + "anchor_good": 6, + "repairable_1s": 4, + "tied_isotropic": 2 + }, + "exact": false, + "family": "mixed", + "k": 0, + "mp_bound": 12, + "mx_bound": 12, + "mx_failures": { + "A/T/A_first: A->T conflict": 800, + "A/T/T_first: T->AU conflict": 775, + "given/T_first: T->AU conflict": 800 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 8, + "v": 12 + }, + { + "an_bound": 6, + "cert_or_witness": 12, + "chain_cost_upper": 36, + "classification": { + "anchor_good": 6, + "repairable_1s": 6, + "tied_isotropic": 0 + }, + "exact": false, + "family": "mixed", + "k": 1, + "mp_bound": 12, + "mx_bound": 12, + "mx_failures": { + "A/T/A_first: A->T conflict": 536, + "A/T/T_first: T->AU conflict": 535 + }, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 8, + "v": 12 + } + ], + "worst": { + "an_bound": 0, + "cert_or_witness": 3, + "chain_cost_upper": 9, + "classification": { + "anchor_good": 0, + "repairable_1s": 3, + "tied_isotropic": 0 + }, + "exact": true, + "family": "tied_isotropic", + "k": 0, + "mp_bound": 3, + "mx_bound": 3, + "mx_failures": {}, + "mx_meta": { + "mode": "A_first", + "variant": "given" + }, + "threshold": 2, + "v": 3 + } + } +} \ No newline at end of file diff --git a/research/fstar-tied-residue-seeddcc97691/README.md b/research/fstar-tied-residue-seeddcc97691/README.md new file mode 100644 index 0000000000..79377a6e72 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/README.md @@ -0,0 +1,87 @@ +# fstar-tied-residue-seeddcc97691 + +**Residue-class attack on open problem F-star: the tied-minimum / isotropic lines (no kappa, no frontier change).** This package takes residue class (i) of the exact residue that [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717) named after proving Lemmas SF, MP, RK and AN: the lines the mod-2 anchor cannot anchor (the tied-minimum / isotropic lines of `research/root-unit-decoder-lemmas` section 7). It adds one proved lemma with exact hypotheses (Lemma MX, a mixed anchor–repair–pivot certificate in two order forms, strictly subsuming Lemma AN and Lemma MP as sufficient conditions), an exact per-line classification of the residue on DreamingOfClouds' stored fixtures `tied_min` (12 lines) and `cex_min_1` (19 lines), an exact obstruction record for the mixed route on `cex_min_1`, and a smallest-first bounded falsifier search in the tied domain (40 instances, `v = 3..12`). **F-star itself is not proved here.** Every claim is labelled PROVEN, CHECKED or DEMOTED. + +## The object + +A `T = 3` exact decoder on `v` lines is `M = sum_{j=1..3} p_j q_j^T` over the rationals with `M_tt != 0` on every line. Row support `pi(t) = {j : p_j(t) != 0}`, column support `sigma(t) = {j : q_j(t) != 0}`, `D(t) = pi(t) intersect sigma(t)` (nonempty). An *L8 labelling* is F2 vectors `a(t)` supported in `pi(t)`, `b(t)` supported in `sigma(t)`, with `K_ts = a(t) . b(s) mod 2`; `cert(M)` is the largest `|S|` admitting an order with `K_tt = 1` on `S` and `K_ts = 0` at every incidence `M_ts = 0` with `t` before `s` (`t, s` in `S`). The proven chain `cost >= sum_j r_j >= cert(M)` is from `research/root-unit-decoder-lemmas` (merged). **F-star** is `cert(M) >= floor(2v/3)` for every exact 3-total rational decoder; the source states the stronger ceiling form `cert(M) >= ceil(2v/3)` (which is what closes the last `T = 3` windows at `v` not divisible by 3); this package works with the floor form of [PR 2335](https://github.com/CrocSwap/integer-mult-bounds/pull/2335) / [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717), and reports both where they differ. + +**The residue attacked here (class (i)).** In a 2-integral normalization with mod-2 anchor labels `a0(t) = p(t) mod 2`, `b0(t) = q(t) mod 2` one has `K0_ts = M_ts mod 2`, so the anchor kills every incidence; `K0_tt = M_tt mod 2` is 1 exactly on the lines with `M_tt` odd. The source's obstruction: what resists are the isotropic lines whose minimal 2-adic valuations among the products `p_k(t) q_k(t)` tie (two tied minima, the reduction cancels), where no one-sided repair exists. PR 2717's Lemma AN handles only the count of odd diagonals, not the tied lines' repair or ordering. This package tests exactly that: can the anchorable lines and the tied lines always be kept together at `>= floor(2v/3)` by one mixed labelling with one order? + +## Per-line residue classification — CHECKED + +For each line `t` (relative to the stored primitive 2-integral normalization): + +- `anchor_good`: `K0_tt = 1` (`M_tt` odd); +- `repairable_1s`: `K0_tt = 0`, but some `a*` inside `pi(t)` gives `a* . b0(t) = 1` and `a* . b0(s) = 0` at every incidence `M_ts = 0` (a full one-sided repair with `b` fixed at `b0`, which is then orderable for free); +- `tied_isotropic`: neither — the stated residue. + +On both fixtures the residue is total: `tied_min` has 0 `anchor_good`, 0 `repairable_1s`, 12 `tied_isotropic` (every line has even diagonal and no one-sided repair), and `cex_min_1` has 8 `anchor_good`, 0 `repairable_1s`, 11 `tied_isotropic`. The mod-2 anchor is therefore vacuous on `tied_min` (0 of 12) and four lines short of `floor(2v/3) = 12` on `cex_min_1` (8 of 19). + +## Lemma MX (mixed anchor–repair–pivot certificate) — PROVEN + +> **Lemma MX.** Let `M = sum_j p_j q_j^T` be a `T = 3` decoder with a 2-integral factorization and anchor labels `a0, b0`. Partition the lines into `A`, `U`, `T` (remaining lines are not kept). Every `t` in `A` satisfies `K0_tt = 1`. Every `t` in `U` carries a chosen `a*(t)` inside `pi(t)` with `a* . b0(t) = 1`, `b(t) = b0(t)`. Every `t` in `T` carries the matched pivot `a(t) = b(t) = e_{c(t)}` with `c(t)` a unit mask inside `D(t)`; write `C_i = {t in T : c(t) = e_i}`. Let `Z` be the zero digraph. Then `cert(M) >= |A| + |U| + sum_{i=1..3} MAS(Z[C_i])` under either of the two exact hypothesis sets: +> +> **(A-first)** (i) each `t` in `U` has `a*(t) . b0(s) = 0` for every `s` in `A` union `U` with `M_ts = 0` and no pivot bit `c(s)` set in `a*(t)` for any `s` in `T` with `M_ts = 0`; (ii) no pivot bit `c(s)` is set in `a0(t)` for any `t` in `A`, `s` in `T` with `M_ts = 0`. +> +> **(T-first)** (i') each `t` in `U` has `a*(t) . b0(s) = 0` for every `s` in `A` union `U` with `M_ts = 0`; (ii') no pivot bit `c(t)` is set in `b0(s)` for any `t` in `T`, `s` in `A` union `U` with `M_ts = 0`. + +*Proof.* The labelling is a valid L8 labelling: supports hold by construction, and `K_tt = 1` on `A` by `K0_tt = 1`, on `U` by `a* . b0(t) = 1`, on `T` by the matched pivot. Consider the conflict digraph `D_K = {(x,y) : M_xy = 0, K_xy = 1}`. Anchor-to-anchor pairs `A x (A union U)` carry `K = M mod 2 = 0` at incidences, so those conflicts vanish always; conflicts `U x (A union U)` vanish by (i)/(i'); conflicts from `A` to `T` vanish by (ii) in the A-first form, conflicts from `T` to `A` union `U` vanish by (ii') in the T-first form. Keep `S = A union U union (union_i S_i)` with `S_i` a maximum acyclic induced subset of `Z[C_i]` (size `MAS(Z[C_i])`), and order `A union U` first (any order) then each `S_i` with every internal conflict pointing backward (sink-first topological order); in the T-first form the two blocks exchange. Every conflict between kept pairs then points backward, so no before-pair carries `K = 1`, and `|S| = |A| + |U| + sum_i MAS(Z[C_i])`. `QED` + +Special cases: `U = T` empty is Lemma AN's count `#{t : M_tt odd}`; `A = U` empty is [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717)'s Lemma MP matched-pivot certificate. Lemma MX is therefore at least as strong as both as a sufficient condition. The computation below also evaluates the two forms and the class variants exhaustively where possible, and every accepted value carries a labelling/order witness replayed by an independent checker. + +## Fixtures: Lemma MP closes the canonical tied instances — CHECKED + +Machine results (`verify.py`, exhaustive over **all** pivot maps `c : [v] -> D(t)` as unit masks: 4096 maps on `tied_min`, 6144 on `cex_min_1`): + +| instance | v | `floor(2v/3)` | `ceil(2v/3)` | AN (mod-2 anchor) | MP (exhaustive) | MX (max over forms) | engine witness | PR 2111 recorded | +|---|---:|---:|---:|---:|---:|---:|---:|---:| +| `tied_min` | 12 | 8 | 8 | 0 | 9 | 9 | 11 (re-found) | 11 (CHECKED, recorded) | +| `cex_min_1` | 19 | 12 | 13 | 8 | 16 | 16 | 18 (stored witness replayed) | 18 (CHECKED, recorded) | + +So **F-star holds on both canonical tied-minimum instances by a structural certificate**: the matched-pivot construction alone (no anchor, no search) reaches 9 and 16, at or above both the floor and the ceiling threshold, even though the mod-2 anchor is vacuous on `tied_min` and short on `cex_min_1`. The engine witnesses reproduce [PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111)'s recorded one-copy L8 maxima 11 and 18 (the recorded values are DreamingOfClouds' CP-SAT results, not re-verified here; the certificate sides are re-found/replayed). Every MX/MP value carries a replayed witness. + +## The mixed route's exact obstruction on `cex_min_1` — CHECKED + +Mixing the 8 anchor lines of `cex_min_1` into the pivot construction fails **completely**: for every one of the 6144 pivot maps, the A-first hypothesis (ii) fails (`A->T conflict`, 6144/6144) and the T-first hypothesis (ii') fails (`T->AU conflict`, 6144/6144). The winning MX value 16 is therefore the pure matched-pivot (all-`T`) construction; no anchor/pivot mixture adds anything on this instance in either block order. This is the exact obstruction to extending AN/MP by naive mixing on the canonical hard instance: the anchor labels `a0` and `b0` of the 8 anchorable lines always carry pivot bits at incidences into (and from) the tied block. + +## Tied-domain falsifier search, smallest first — CHECKED (scoped negative) + +Two generators aimed at the residue: `tied_isotropic` (every line constructed with exactly two tied minimal valuations at level 0 and even diagonal — the anchor isotropic on every line) and `mixed` (half the lines with a unique minimal valuation and odd diagonal, half tied). `v` ascending from 3, two instances per family and `v`; 40 instances total. + +| `v` range | instances | exact `cert` (exhaustive `a`-enumeration) | witnesses | falsifiers | `cert` | +|---|---:|---|---|---:|---| +| 3–6 | 16 | 16 decided | — | 0 | `= v` on all | +| 7–12 | 24 | budget-limited | 24 full-size (`= v`) | 0 | `= v` on all | + +A witness of size `v` pins `cert(M) = v` exactly (it is the maximum), so `cert = v` holds on all 40 instances; 16 of them are additionally decided by exhaustive `a`-enumeration. Every instance is at or above `floor(2v/3)`; minimum witness ratio 1.0. The falsifier criterion (an explicit admissible pairing `B` with `sum_j rank_F2 B[R_j,A_j] < floor(2v/3)`, which by the proven chain would refute F-star) was tested by an exhaustive `B`-scan when the admissible-pair count is at most 12 and a deterministic local search otherwise: no `B` below threshold was found on any instance (bounded search, not an exhaustive non-falsification proof). Lemma MP reaches `v` on all 40 instances; Lemma MX never falls below MP and is never strictly above it on this domain (`mx_strictly_above_mp = 0`), with the winning variant/mode recorded per instance. + +## What is proved, what is witnessed, what is demoted + +- **PROVEN:** Lemma MX, both order forms, with the exact hypotheses above (written proof). Together with [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717)'s proven chain and the source package's proven consequence (F-star closes every open `T = 3` window), each closed instance closes its windows. +- **CHECKED (machine, `verify.py`, stdlib, deterministic):** controls (brute-force-over-all-labellings agreement 3/3 at `v = 3`, diagonal decoder `cert = 3`, corrupted-witness rejection 2/2, the MX all-anchor special case reproducing AN's count, an MP control with replayed witness); the per-line residue classification of both fixtures; the exhaustive MP/MX maxima 9/16 over all 4096/6144 pivot maps with replayed witnesses; the mixed-route obstruction counts 6144/6144 in both order forms; engine witnesses 11 and 18 on the fixtures (matching PR 2111's recorded one-copy maxima); the tied-domain search above (`cert = v` on 40/40, zero falsifiers). +- **DEMOTED / OPEN:** F-star for general rational decoders is **not** proved here. Residue class (i) is closed on the two canonical fixtures and the searched tied domain, not for all tied decoders; no necessity or "exactly when" claim is made for any hypothesis (each is sufficient as stated). That matched pivots always reach `floor(2v/3)` is *not* proved — it is witnessed on 42 instances (2 fixtures + 40 searched). Residue class (ii) (zero digraphs that are not 3-dichromatic) and class (iii) (non-dyadic entries) are untouched. The `B`-scan values are bounded-search upper bounds on the minimum chain cost, not exact minima. The recorded fixture certificates 11/18 rest on PR 2111's recorded CP-SAT optimality, not re-verified here. Exact pairing costs known elsewhere (12 on `tied_min`, [PR 2379](https://github.com/CrocSwap/integer-mult-bounds/pull/2379) by Aaron Wang; 21 on `cex_min_1`, [PR 2206](https://github.com/CrocSwap/integer-mult-bounds/pull/2206) by Nick Petalas) bound `cert` from above via the chain only through `cost >= cert`, and are cited, not recomputed. + +## Open next questions + +1. **Does the matched-pivot family always reach `floor(2v/3)`?** Concretely: is `max_c sum_i MAS(Z[C_i]) >= floor(2v/3)` for every rank-3 zero digraph with pivot maps into `D(t)`? Why it matters: Lemma MP would then prove F-star outright, and this package witnesses it on all 42 tied-domain instances tested (with `cert = v` on the 40 searched). First step: adversarial construction of decoders minimizing `max_c sum_i MAS(Z[C_i])`, smallest `v` first, using the two-tied-minima generator with dense zero digraphs (rank-3 constraints of Lemma RK apply). Blocker: none structural; needs a dedicated enumeration session. +2. **Insertion-finite MX.** The two block orders fail completely on `cex_min_1`; the general order allows each anchor line to be *inserted* at a valid cut of the pivot order (exact criterion: the anchor line's pivot-block out-neighbours must all precede its in-neighbours in one linear extension). Why it matters: it is the precise remaining power of the mixed route, and its failure would close naive mixing entirely. First step: implement the cut criterion and re-run on `cex_min_1`'s 6144 maps; record how many anchor lines become placeable. Blocker: none; small code. +3. **What labels do the attaining certificates actually use?** The fixture certificates 11 and 18 exceed everything the anchor/pivot families reach (9 and 16). First step: diff the stored/re-found witnesses' labels against all matched pivots and anchor labels, and classify the label patterns (two-bit labels, off-diagonal pairs). Blocker: none; analysis of existing witnesses. + +## Reproduce + +Python 3.10+, standard library only, from the repository root: + +```sh +python3 -B research/fstar-tied-residue-seeddcc97691/verify.py +python3 scripts/research_package.py --package research/fstar-tied-residue-seeddcc97691 --check-only +python3.12 scripts/research_package.py --package research/fstar-tied-residue-seeddcc97691 +``` + +Expected markers: `PASS_FSTARTIED_CONTROLS`, `PASS_FSTARTIED_FIXTURES`, `PASS_FSTARTIED_MX`, `PASS_FSTARTIED_SEARCH`, `PASS_FSTAR_TIED_RESIDUE`, and `CERTIFICATE.json` with digest `439d75261e9a2b9e` (full digest printed by the run; ~306 s on the authoring host). The registered CPython 3.12 replay prints `PASS_REGISTERED_RESEARCH_PACKAGE research/fstar-tied-residue-seeddcc97691 outcome=completed`. `make` is not installed on the authoring host; the commands above are the underlying ones. + +## Credit and provenance + +F-star, the `cert(M)` definition, L8 labellings, the proven chain `cost >= sum_j r_j >= cert(M)` and the tied-minima obstruction are from the merged package `research/root-unit-decoder-lemmas` ([PR 1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instances `tied_min` and `cex_min_1`, their recorded one-copy certificate limits (11 and 18, CP-SAT, CHECKED (recorded)), the stored cost-22 pairing `data/cex_min_1.B22.json` and the structural lemmas L5/SCC are DreamingOfClouds' work in [PR 2111](https://github.com/CrocSwap/integer-mult-bounds/pull/2111) and [PR 2162](https://github.com/CrocSwap/integer-mult-bounds/pull/2162); `data/tied_min.json` and `data/cex_min_1.json` are byte-identical copies of their data files (sha256 `670ed90924b601ade22f0d4adaff46d1667e5449326a0f7ba7b88dd8f5906f93` and `86064701dde94b4f35427bc3e19275eaf1e40e9e90d4fea28e7857f3564d4dd7`). The residue statement, Lemmas SF/MP/RK/AN and the exact-completion engine design this package's engine adapts are Aaron Wang's work in [PR 2717](https://github.com/CrocSwap/integer-mult-bounds/pull/2717); the falsifier-census frontier (196 instances) is Aaron Wang's [PR 2335](https://github.com/CrocSwap/integer-mult-bounds/pull/2335); the exact cost 12 of `tied_min` is Aaron Wang's [PR 2379](https://github.com/CrocSwap/integer-mult-bounds/pull/2379); the exact cost 21 of `cex_min_1` is Nick Petalas' [PR 2206](https://github.com/CrocSwap/integer-mult-bounds/pull/2206). The stored 18-witness `data/cex_min_1.witness.json` is from PR 2717's package. This package does not claim their results; the new content is Lemma MX with its proof and both order forms, the exact per-line residue classification, the exhaustive mixed-route obstruction on `cex_min_1`, and the tied-domain search. + +Prepared by **Aaron Wang** with help from opencode (substantial AI assistance; no independent human review claimed). New work in this package is Apache-2.0. diff --git a/research/fstar-tied-residue-seeddcc97691/SOURCES.json b/research/fstar-tied-residue-seeddcc97691/SOURCES.json new file mode 100644 index 0000000000..afe8ee671f --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/root-unit-decoder-lemmas/README.md", + "usage": "input", + "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", + "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9" + } + ] +} diff --git a/research/fstar-tied-residue-seeddcc97691/TASK-CARD.md b/research/fstar-tied-residue-seeddcc97691/TASK-CARD.md new file mode 100644 index 0000000000..cb1e0ccf1a --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/TASK-CARD.md @@ -0,0 +1,78 @@ +# Task card — KB5b: the tied-minimum / isotropic-line residue of F-star + +```text +Task ID / proposed scope key: fstar-tied-residue / fstar-tied-residue-seeddcc97691 + (Kappa-blocker KB5b, explicit open request; chooser OS seed dcc976912ab4c64bcee65295e5f63e98 + drew track bit-mechanisms with cards bit-helper-contract and bit-new-register-model; + recorded scope-change reason in TASK.json.) +Base commit; exact predecessor and dependency heads: + base main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2 (priority revision 4); + predecessor proofs: https://github.com/CrocSwap/integer-mult-bounds/pull/2717 head 10644c90837cb377df89be7c87992320ebfaf091; + predecessor census: https://github.com/CrocSwap/integer-mult-bounds/pull/2335 head 856cd7603ba679aa56294e53d60840061d176778; + fixtures: https://github.com/CrocSwap/integer-mult-bounds/pull/2111 head 98da76c2839ba38538b510420dec54546ccabf0b. +Concrete object and question: + Open problem F-star of research/root-unit-decoder-lemmas section 7 (floor form): + cert(M) >= floor(2v/3) for every exact 3-total rational decoder M = sum_j p_j q_j^T. + Residue class attacked: (i) tied-minimum / isotropic lines — the lines the mod-2 anchor + of Lemma AN cannot anchor (M_tt even under every 2-integral normalization because the + minimal 2-adic valuations among the products p_k(t) q_k(t) tie and the reduction is + isotropic, so no one-sided repair exists). Question: can anchorable lines and tied lines + always be kept together at >= floor(2v/3) by a mixed anchor + matched-pivot labelling + with one order, and if not, what exactly fails first? +Scope status: changed (from the drawn bit-mechanisms cards); reason: authorized explicit + open request KB5b. Pair-collision check at entry (toolkit disc-comments on discussions + 1317 and 1166 including nested replies, 2026-10-15 18:26-18:29 UTC) found no live claim + on the F-star residue; KB5 (PR 2717) is DONE/RELEASED at 18:20 UTC. +Existing restriction being changed (or exact claim being audited): + Nothing is relaxed. The restriction being addressed is PR 2717's stated demotion: + "Lemma AN handles only the even-diagonal count, not their repair or ordering" for the + tied-minimum / isotropic lines. Every new claim carries its exact hypothesis and is + demoted where unproved. +Method; explicit parameter ranges/candidate alphabet: + Stdlib exact integer/F2 arithmetic. (a) A written mixed anchor-pivot lemma (Lemma MX) + with exact hypotheses: anchor labels on a set A (zero conflicts inside A at incidences), + matched pivots on the complement R with pivot classes C_i, and an exact placement + criterion for inserting anchor lines into the pivot order; strictly extends AN + (R empty) and the one-class matched-pivot construction of MP. (b) Per-line classification + of every instance into anchor-good / one-sided-repairable / tied-isotropic, computed + exactly from the 2-integral factorization. (c) Calibration on PR 2111's stored fixtures + tied_min (v = 12) and cex_min_1 (v = 19). (d) Smallest-first bounded falsifier search in + the tied residue: v ascending from 3, tied-heavy generators (all diagonals even, tied + valuation profiles, entries in {+-2,+-4} and {+-1,+-2} and rationals with odd primes in + denominators), exact cert where a-enumeration terminates, witness replay everywhere, + admissible-B chain cost as the rigorous falsifier criterion. +Nearest overlapping PRs and why this adds something: + PR 2717 (Aaron Wang) proved SF/MP/RK/AN and named this exact residue; this package + attacks the residue itself with a mixed lemma and a tied-domain search, not another + census of the censused domain. PR 2335 (Aaron Wang) is the 196-instance census; + its domain (v = 4..12, entries -2..2) is not repeated. PR 2111 / PR 2162 + (DreamingOfClouds) own the fixtures and their certificate limits; cited, not restated. + PR 2379 (Aaron Wang) pins cost(tied_min) = 12 exactly; Discussion 2202 pins + cost(cex_min_1) = 21 exactly. Refined overlap pass on the object's proper names + (F-star, cert(M), 3-total decoder, tied minimum, isotropic, zero digraph, 3-dichromatic, + L8 labelling, matched pivot, mod-2 anchor, tied minima, tied_min, cex_min_1, + root-unit decoder, 2-adic, one-sided repair) at 2026-10-15 18:27-18:42 UTC, complete + pagination both passes, found no other work on this residue. +Optimistic full cost budget; required observable improvement: + No kappa/supplier budget in play (missing-lemma work). Required observable: a PROVEN + lemma whose hypotheses strictly include AN's and MP's and which certifies >= floor(2v/3) + on instances where either alone is short, or an exact obstruction showing why the mixed + route fails at the smallest instance where it fails. +Success evidence; falsification test; time/compute cap: + Success: PASS markers from verify.py (controls, fixture calibration, MX bound vs + threshold per instance, search summary) and a written proof of Lemma MX in README.md. + Falsification test: an explicit admissible pairing B with sum_j rank_F2 B[R_j,A_j] < + floor(2v/3) refutes F-star on that instance (chain is proven); a corrupted witness must + fail the independent checker. Compute cap: one session, single-process stdlib Python, + each registered command below 600 s. +Predecessor authors; intended artifact and reproduction command: + F-star / cert(M) / L8 / the proven chain: research/root-unit-decoder-lemmas (Douglas + Colkitt with OpenAI Codex assistance lineage). Fixtures tied_min, cex_min_1 and their + recorded one-copy limits: DreamingOfClouds, PR 2111 / PR 2162. Lemma residue statement + and engine design this package's engine adapts: Aaron Wang, PR 2717. Census frontier: + Aaron Wang, PR 2335. Exact cost(tied_min) = 12: Aaron Wang, PR 2379. Exact + cost(cex_min_1) = 21: Discussion 2202 (author credited in README after verification). + Artifact: research/fstar-tied-residue-seeddcc97691/. Reproduce: + python3 -B research/fstar-tied-residue-seeddcc97691/verify.py + python3 scripts/research_package.py --package research/fstar-tied-residue-seeddcc97691 --check-only +``` diff --git a/research/fstar-tied-residue-seeddcc97691/TASK.json b/research/fstar-tied-residue-seeddcc97691/TASK.json new file mode 100644 index 0000000000..6c023e8e03 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Kappa-blocker KB5b (explicit open request): residue class (i) of open problem F-star of research/root-unit-decoder-lemmas section 7 (cert(M) >= floor(2v/3) for exact 3-total rational decoders), the tied-minimum / isotropic lines named as the exact residue by PR 2717. Three parts: (P1) PROVEN Lemma MX, a mixed anchor-repair-pivot certificate in two order forms with exact hypotheses, strictly subsuming Lemma AN (count of odd diagonals) and Lemma MP (matched-pivot certificate) as sufficient conditions; (P2) an exact per-line residue classification (anchor_good / repairable_1s / tied_isotropic) on PR 2111's stored fixtures tied_min (v = 12) and cex_min_1 (v = 19), with exhaustive maxima over all 4096 / 6144 pivot maps and replayed witnesses, plus the exact obstruction record for the mixed route on cex_min_1; (P3) a smallest-first bounded falsifier search in the tied domain (40 instances, v = 3..12, two tied-minimum generators), falsifier criterion an explicit admissible pairing B with sum_j rank_F2 B[R_j,A_j] < floor(2v/3) via the proven chain.", + "scope_change_reason": "Authorized 'explicit open request' scope change to kappa-blocker KB5b, recorded per the assignment. The chooser OS draw (seed dcc976912ab4c64bcee65295e5f63e98, track bit-mechanisms) landed on the cards bit-helper-contract and bit-new-register-model; neither is the assigned object, and the assignment names the draw landing on saturated cards as the recorded reason for taking the KB5b request instead. Pair-collision check before computation (toolkit disc-comments on discussions 1317 and 1166 including nested replies, 2026-10-15 18:26-18:29 UTC) found no live claim on the F-star residue: KB5 (PR 2717) is DONE/RELEASED at 18:20 UTC. Refined overlap re-run on the object's proper names (F-star, cert, 3-total decoder, tied minimum, isotropic, zero digraph, 3-dichromatic, L8 labelling, matched pivot, mod-2 anchor, tied minima, tied_min, cex_min_1, root-unit decoder, 2-adic, one-sided repair) at 18:27-18:42 UTC with complete pagination found no other work on this residue.", + "existing_restriction_being_changed": "Nothing is relaxed. The restriction being addressed is PR 2717's stated demotion: Lemma AN handles only the even-diagonal count, not the repair or ordering of the tied-minimum (isotropic) lines. Every new claim carries its exact hypothesis and is demoted where unproved; no 'exactly when' or necessity wording is used.", + "method": "Exact stdlib integer/F2 arithmetic. Engine adapted from PR 2717: for fixed a-labels the (b-labels, order, kept set) completion is exact by subset DP; a deterministic hill-climb over a-labels with exact completion; an independent witness checker replays every stored/constructed witness (supports, K_tt = 1, before-pair constraints recomputed from scratch). New: the per-line residue classification relative to the stored primitive 2-integral normalization; the Lemma MX construction (anchor labels on A, one-sided repairs on U, matched pivots on T, two block orders A+U-first and T-first) with per-map exact evaluation and replayed witnesses; exhaustive pivot-map maximization where the product of |D(t)| allows (4096 maps on tied_min, 6144 on cex_min_1); exact cert by exhaustive a-enumeration where the product of option counts is small; a bounded admissible-B scan (exhaustive at up to 12 free pairs, deterministic local search otherwise) as the rigorous falsifier criterion.", + "parameter_ranges": "T = 3 totals exactly; rational decoders with nonzero diagonal. Fixtures: PR 2111's tied_min (v = 12, entries in {-1,0,1}) and cex_min_1 (v = 19, entries in {-1,0,1}), byte-identical data copies with recorded sha256. Search: v = 3..12, two instances per family and v, families tied_isotropic (every line constructed with exactly two tied minimal valuations at level 0 and even diagonal, entries in {+-1,+-2}) and mixed (half the lines unique-minimum with odd diagonal, half tied); 40 instances total.", + "nearest_overlapping_prs": "https://github.com/CrocSwap/integer-mult-bounds/pull/2717 (Aaron Wang: Lemmas SF/MP/RK/AN and the exact residue statement; this package attacks the residue itself with a proved mixed lemma, an exact obstruction and a tied-domain search, not another lemma inventory). https://github.com/CrocSwap/integer-mult-bounds/pull/2335 (Aaron Wang: the 196-instance falsifier census over v = 4..12, entries -2..2; that domain is not repeated). https://github.com/CrocSwap/integer-mult-bounds/pull/2111 and https://github.com/CrocSwap/integer-mult-bounds/pull/2162 (DreamingOfClouds: the fixtures, their recorded certificate limits and the T = 3 reductions; cited, not restated). https://github.com/CrocSwap/integer-mult-bounds/pull/2379 (Aaron Wang: exact cost 12 of tied_min) and https://github.com/CrocSwap/integer-mult-bounds/pull/2206 (Nick Petalas: exact cost 21 of cex_min_1) are cited as context and not recomputed.", + "optimistic_full_cost_budget": "No kappa, supplier, word or moment budget is in play (missing-lemma work). The whole-construction price is the evidence itself: the Lemma MX proof is in the README and every computational claim is recomputed by verify.py in one bounded stdlib run (no third-party packages, no solver).", + "bottleneck_link": "F-star is the named route to closing every open T = 3 window at once (research/root-unit-decoder-lemmas section 7, consequence PROVEN given F-star). Residue class (i) is the heart of the stated obstruction; a proof of the bound on the tied lines, or an exact obstruction to the known constructions there, narrows or closes that route; a falsifier would redirect the T = 3 decoder route entirely.", + "stop_rule": "Stop at the first exact falsifier (smallest falsifying instance first: an explicit admissible B with chain cost below floor(2v/3), or exact cert below threshold where exhaustive), or, absent one, at the declared tied domain with every instance witnessed at or above threshold and the exact obstruction of the mixed route recorded. One bounded pivot maximum (the U-to-T class demotion and the second block order are the single pivot); early kill with the exact obstruction recorded. Compute cap: one session, single-process stdlib Python; the registered verify command runs about 306 s, below the 600 s manifest cap.", + "success_evidence": "PASS markers from verify.py (PASS_FSTARTIED_CONTROLS, PASS_FSTARTIED_FIXTURES, PASS_FSTARTIED_MX, PASS_FSTARTIED_SEARCH, PASS_FSTAR_TIED_RESIDUE) plus the written Lemma MX proof in README.md: controls (brute/engine 3/3 at v = 3, diagonal cert = 3, corrupted-witness rejection 2/2, MX all-anchor reproduces AN's count, MP control with replayed witness); fixture classification (tied_min: 0 anchor_good / 0 repairable / 12 tied_isotropic; cex_min_1: 8 / 0 / 11); exhaustive MP/MX 9 and 16 over all 4096 / 6144 pivot maps with replayed witnesses (at or above both floor(2v/3) = 8 / 12 and ceil(2v/3) = 8 / 13); the mixed-route obstruction (A->T conflict 6144/6144 and T->AU conflict 6144/6144 on cex_min_1); engine witnesses 11 and 18 matching PR 2111's recorded one-copy maxima; the tied-domain search (40 instances, cert = v on all, zero falsifiers, minimum witness ratio 1.0, 16 decided by exhaustive a-enumeration).", + "falsification_test": "Side A of the search is the falsifier test for F-star: an explicit admissible pairing B with cost(B) < floor(2v/3) refutes F-star on that instance (the chain cost >= cert(M) is proven). Side B witnesses are rejected by the independent checker if any K_tt = 1 fails or any before-pair constraint fails; corrupted copies of stored witnesses fail verification (checked 2/2).", + "time_compute_cap": "One session; single-process stdlib Python; no SAT solver, no third-party packages; the registered verify command runs about 306 s (below 600 s); the package is registered with timeout_seconds 600.", + "predecessor_authors": "F-star, the cert(M) definition, L8 labellings, the proven chain cost >= sum_j r_j >= cert(M) and the tied-minima obstruction: the merged research/root-unit-decoder-lemmas package (PR 1590 (https://github.com/CrocSwap/integer-mult-bounds/pull/1590) by DreamingOfClouds, with Claude Opus 5.5 (Anthropic) via Claude Code assistance). The rank-3 configuration model, the named instances tied_min and cex_min_1, their recorded certificate limits and the stored cost-22 pairing: DreamingOfClouds, PR 2111 and PR 2162. The residue statement, Lemmas SF/MP/RK/AN and the engine design this package adapts: Aaron Wang, PR 2717. The falsifier census frontier: Aaron Wang, PR 2335. Exact cost 12 of tied_min: Aaron Wang, PR 2379. Exact cost 21 of cex_min_1: Nick Petalas, PR 2206.", + "intended_artifact": "research/fstar-tied-residue-seeddcc97691/ with TASK.json, SOURCES.json pins, VERIFY.json, verify.py, data/ (the named instances, the stored cost-22 pairing and the stored 18-witness, byte-identical copies with recorded sha256), CERTIFICATE.json (written by verify.py) and README.md; reproduction: python3 -B research/fstar-tied-residue-seeddcc97691/verify.py then python3 scripts/research_package.py --package research/fstar-tied-residue-seeddcc97691 --check-only.", + "outcome": "completed", + "evidence": "RESIDUE CLASS (i) CLOSED ON THE CANONICAL TIED INSTANCES AND THE SEARCHED TIED DOMAIN; EXACT OBSTRUCTION TO MIXING RECORDED; F-STAR ITSELF NOT PROVED. PROVEN (written proof in README.md): Lemma MX, a mixed anchor-repair-pivot certificate in two order forms (A+U-first and T-first) with exact hypotheses (one-sided repairs on U; A->T separation in the first form; T->(A union U) separation in the second), giving cert(M) >= |A| + |U| + sum_i MAS(Z[C_i]); its U = T empty special case is Lemma AN and its A = U empty special case is Lemma MP, so it subsumes both as sufficient conditions. CHECKED by verify.py (stdlib, deterministic, ~306 s, certificate digest 439d75261e9a2b9e): controls pass (brute/engine agreement 3/3 at v = 3, diagonal cert = 3, corrupted-witness rejection 2/2, MX all-anchor = AN count, MP control 5 with replayed witness). Residue classification on PR 2111's fixtures: tied_min has 0 anchor_good, 0 repairable_1s, 12 tied_isotropic (the mod-2 anchor is vacuous: 0 of 12); cex_min_1 has 8 anchor_good, 0 repairable_1s, 11 tied_isotropic (AN gives 8 against floor(2v/3) = 12). Exhaustive over all pivot maps as unit masks (4096 on tied_min, 6144 on cex_min_1): Lemma MP certifies 9 >= 8 (tied_min) and 16 >= 12 and >= 13 (cex_min_1) with replayed witnesses, so F-star holds on both canonical tied instances by a structural certificate; Lemma MX maximized over both order forms and three class variants gives the same 9 and 16. Exact obstruction to the mixed route on cex_min_1: the A->T separation fails for 6144/6144 pivot maps in the A-first form and the T->(A union U) separation fails for 6144/6144 in the T-first form, so no anchor/pivot mixture adds anything there in either block order. Engine witnesses 11 and 18 reproduce PR 2111's recorded one-copy L8 maxima (their CP-SAT optimality is CHECKED (recorded), not re-verified here). Tied-domain falsifier search, smallest first (40 instances, v = 3..12, families tied_isotropic and mixed): zero falsifiers; cert = v on all 40 (16 decided by exhaustive a-enumeration at v <= 6, 24 pinned by full-size replayed witnesses); minimum witness ratio 1.0; the bounded admissible-B scan found no chain cost below floor(2v/3) on any instance; Lemma MP reaches v on all 40 and Lemma MX is never below MP and never strictly above it on this domain (mx_strictly_above_mp = 0). NOT PROVED: F-star for general rational decoders; that matched pivots always reach floor(2v/3) (witnessed on 42 instances, not proved); residue classes (ii) non-3-dichromatic zero digraphs and (iii) non-dyadic entries are untouched; the B-scan values are bounded-search upper bounds on the minimum chain cost, not exact minima; no hypothesis is claimed necessary.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial AI assistance: this package was produced by Aaron Wang with help from opencode (opencode agent harness). No independent human review claimed. No model is cited per orchestrator attribution rules.", + "open_questions": [ + { + "question": "Is max_c sum_i MAS(Z[C_i]) >= floor(2v/3) for every rank-3 zero digraph Z with pivot maps c into D(t)? (Equivalently: does the matched-pivot family of Lemma MP always certify the F-star bound?)", + "why_it_matters": "Lemma MP would then prove F-star outright for all exact 3-total decoders; this package witnesses it (with cert = v) on all 42 tied-domain instances tested, including both canonical fixtures where the mod-2 anchor fails.", + "first_step": "Adversarially construct decoders minimizing max_c sum_i MAS(Z[C_i]), smallest v first, using the two-tied-minima generator with dense zero digraphs subject to Lemma RK's constraints (no mutual-zero K_4, no transitive 4-tournament, block incidences of size >= 2).", + "blocked_by": "Nothing structural; needs a dedicated enumeration session." + }, + { + "question": "Does insertion-finite mixing help? (Allow each anchor line to be inserted at a valid cut of the pivot order instead of taking one of the two block orders.)", + "why_it_matters": "The two block orders fail completely on cex_min_1 (6144/6144 maps in both forms); the exact cut criterion (pivot-block out-neighbours all preceding in-neighbours in one linear extension) is the precise remaining power of the mixed route, and its failure would close naive mixing entirely.", + "first_step": "Implement the cut criterion and re-run on cex_min_1's 6144 pivot maps; record how many anchor lines become placeable and the resulting certified bound.", + "blocked_by": "None; small code extension of verify.py." + }, + { + "question": "Which label patterns do the attaining certificates of tied_min (11) and cex_min_1 (18) actually use?", + "why_it_matters": "Those certificates exceed everything the anchor and matched-pivot families reach (9 and 16); classifying the extra label patterns (two-bit labels, off-pivot pairs) would name the labelling family a proof of residue class (i) actually needs.", + "first_step": "Diff the stored and re-found witnesses' a/b labels against all matched pivots and anchor labels and tabulate the pattern counts.", + "blocked_by": "None; analysis of existing witnesses." + } + ] +} diff --git a/research/fstar-tied-residue-seeddcc97691/VERIFY.json b/research/fstar-tied-residue-seeddcc97691/VERIFY.json new file mode 100644 index 0000000000..ea9b7c101b --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/VERIFY.json @@ -0,0 +1,16 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/root-unit-decoder-lemmas/README.md" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Tied-residue F-star package: controls (brute-force-over-all-labellings agreement at v = 3, diagonal decoder cert = 3, corrupted-witness rejection, the MX all-anchor special case reproducing the AN count, an MP control with replayed witness); per-line residue classification (anchor_good / repairable_1s / tied_isotropic) of PR 2111's fixtures tied_min and cex_min_1; exhaustive Lemma MP and Lemma MX maxima over all pivot maps (4096 on tied_min, 6144 on cex_min_1) with independent witness replay; the mixed-route obstruction counts on cex_min_1 (A->T and T->AU conflicts over all maps, both order forms); engine witnesses 11 and 18 on the fixtures matching PR 2111's recorded one-copy maxima; and the smallest-first tied-domain falsifier search (40 instances, v = 3..12, tied_isotropic and mixed families, exact cert by exhaustive a-enumeration where cheap, admissible-B chain cost as falsifier criterion); prints PASS_FSTARTIED_CONTROLS, PASS_FSTARTIED_FIXTURES, PASS_FSTARTIED_MX, PASS_FSTARTIED_SEARCH and PASS_FSTAR_TIED_RESIDUE and writes CERTIFICATE.json" + } + ] +} diff --git a/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.B22.json b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.B22.json new file mode 100644 index 0000000000..0161536922 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.B22.json @@ -0,0 +1 @@ +[[1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0], [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 0], [0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0], [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]] \ No newline at end of file diff --git a/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.json b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.json new file mode 100644 index 0000000000..4629aa02b1 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.json @@ -0,0 +1 @@ +[[[1, -1, 0], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 0, -1], [0, 1, -1]], [[1, 0, -1], [0, 1, 1]], [[1, 0, -1], [1, -1, 0]], [[1, 0, -1], [1, 1, -1]], [[1, 0, 1], [1, 1, 0]], [[1, 0, 1], [1, 1, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, -1, 1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 0], [0, 1, 1]], [[1, 1, 0], [1, 0, 1]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.witness.json b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.witness.json new file mode 100644 index 0000000000..602d784e98 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/data/cex_min_1.witness.json @@ -0,0 +1 @@ +{"a": [3, 2, 2, 4, 4, 5, 5, 4, 1, 1, 2, 7, 5, 1, 2, 3, 6, 1, 1], "b": [1, 6, 0, 5, 6, 6, 1, 4, 3, 7, 6, 2, 1, 3, 6, 5, 2, 5, 3], "order": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1], "kept": [16, 6, 11, 14, 5, 12, 0, 18, 17, 15, 3, 13, 10, 9, 8, 7, 4, 1]} \ No newline at end of file diff --git a/research/fstar-tied-residue-seeddcc97691/data/tied_min.json b/research/fstar-tied-residue-seeddcc97691/data/tied_min.json new file mode 100644 index 0000000000..ae11f01fab --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/data/tied_min.json @@ -0,0 +1 @@ +[[[1, -1, -1], [0, 1, 1]], [[1, -1, -1], [1, -1, 0]], [[1, -1, -1], [1, 0, -1]], [[1, -1, 1], [0, 1, -1]], [[1, -1, 1], [1, -1, 0]], [[1, -1, 1], [1, 0, 1]], [[1, 1, -1], [0, 1, -1]], [[1, 1, -1], [1, 0, -1]], [[1, 1, -1], [1, 1, 0]], [[1, 1, 1], [0, 1, 1]], [[1, 1, 1], [1, 0, 1]], [[1, 1, 1], [1, 1, 0]]] \ No newline at end of file diff --git a/research/fstar-tied-residue-seeddcc97691/verify.py b/research/fstar-tied-residue-seeddcc97691/verify.py new file mode 100644 index 0000000000..fe8ddd0e55 --- /dev/null +++ b/research/fstar-tied-residue-seeddcc97691/verify.py @@ -0,0 +1,912 @@ +#!/usr/bin/env python3 +"""Tied-residue checks for open problem F-star: anchor classification, the mixed +anchor-repair-pivot lemma (Lemma MX) with machine-checked witnesses, calibration +on PR 2111's stored fixtures, and a smallest-first bounded falsifier search in +the tied-minimum / isotropic domain. Stdlib only, deterministic. Part of +research/fstar-tied-residue-seeddcc97691. + +Model (research/root-unit-decoder-lemmas section 7; PR 2111 section 1): a +T = 3 decoder is M = sum_{j=1..3} p_j q_j^T over Q on v lines with M_tt != 0. +Row support pi(t) = {j : p_j(t) != 0}, column support sigma(t) = {j : q_j(t) +!= 0}. An L8 labelling is F2 vectors a(t) supported in pi(t), b(t) supported +in sigma(t), K_ts = a(t) . b(s) mod 2. cert(M) is the largest |S| admitting an +order with K_tt = 1 on S and K_ts = 0 at every incidence M_ts = 0 with t before +s (t, s in S). + +Engine and witness checker adapted from Aaron Wang's PR 2717 +(research/fstar-proof-lemmas-seed3096ed3f/verify.py): for fixed a-labels the +(b-labels, order, kept set) completion is exact by subset DP. New here: the +per-line anchor/residue classification, the Lemma MX construction (anchor +labels on A, one-sided repairs on U, matched pivots on T with the A+U-first +order), its exact per-instance evaluation over pivot maps, and the tied-domain +generators and search. +""" +import hashlib +import itertools +import json +import os +import random +import sys +import time + +sys.stdout.reconfigure(encoding="utf-8") + +HERE = os.path.dirname(os.path.abspath(__file__)) +DATA = os.path.join(HERE, "data") +T0 = time.time() + + +def log(msg): + print(f"[{time.time() - T0:7.2f}s] {msg}") + + +# ---------------------------------------------------------------- model ---- +def signature(P, Q): + v = len(P) + M = [[sum(P[t][j] * Q[s][j] for j in range(3)) for s in range(v)] for t in range(v)] + pi = [sum(1 << j for j in range(3) if P[t][j]) for t in range(v)] + sg = [sum(1 << j for j in range(3) if Q[t][j]) for t in range(v)] + Z = [[M[t][s] == 0 for s in range(v)] for t in range(v)] + assert all(M[t][t] != 0 for t in range(v)), "decoder must have nonzero diagonal" + return M, pi, sg, Z + + +def opts(pi_t): + return [m for m in range(1, 8) if not (m & ~pi_t)] + + +def threshold(v): + return (2 * v) // 3 + + +# --------------------------------------------- exact completion engine ---- +def bfeas_tables(pi, sg): + tabs = [] + for t in range(len(pi)): + tab = [[False] * 256 for _ in range(8)] + for am in range(1, 8): + if am & ~pi[t]: + continue + for bset in range(256): + ok = False + for b in range(1, 8): + if b & ~sg[t] or ((am & b).bit_count() & 1) == 0: + continue + good, bs = True, bset + while bs: + lb = bs & -bs + if (((lb.bit_length() - 1) & b).bit_count() & 1): + good = False + break + bs ^= lb + if good: + ok = True + break + tab[am][bset] = ok + tabs.append(tab) + return tabs + + +def blockers_pred(Z, v): + pred = [0] * v + for t in range(v): + m = 0 + for s in range(v): + if s != t and Z[s][t]: + m |= 1 << s + pred[t] = m + return pred + + +def complete(a, pi, sg, Z, v, tabs): + """Exact max |S| over (b, order, S) for fixed a-labels. Returns (value, bestT, f).""" + pred = blockers_pred(Z, v) + N = 1 << v + Abits = bytearray(N) + for U in range(1, N): + lb = U & -U + Abits[U] = Abits[U ^ lb] | (1 << a[lb.bit_length() - 1]) + f = bytearray(N) + f[0] = 1 + best, bestT = 0, 0 + for T in range(1, N): + ok, U = 0, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][Abits[prev & pred[u]]]: + ok = 1 + break + U ^= lb + f[T] = ok + if ok and T.bit_count() > best: + best, bestT = T.bit_count(), T + return best, bestT, f + + +def reconstruct(a, sg, Z, v, tabs, bestT, f): + pred = blockers_pred(Z, v) + + def ab(U): + r, x = 0, U + while x: + lb = x & -x + r |= 1 << a[lb.bit_length() - 1] + x ^= lb + return r + + rev, T = [], bestT + while T: + found, U = None, T + while U: + lb = U & -U + u = lb.bit_length() - 1 + prev = T ^ lb + if f[prev] and tabs[u][a[u]][ab(prev & pred[u])]: + found = u + break + U ^= lb + assert found is not None + rev.append(found) + T ^= 1 << found + order = rev[::-1] + kept, bs = [], [0] * v + for t in order: + bset = 0 + for s in kept: + if Z[s][t]: + bset |= 1 << a[s] + for cand in range(1, 8): + if cand & ~sg[t] or ((a[t] & cand).bit_count() & 1) == 0: + continue + good, x = True, bset + while x: + lb = x & -x + if (((lb.bit_length() - 1) & cand).bit_count() & 1): + good = False + break + x ^= lb + if good: + bs[t] = cand + break + kept.append(t) + return order, bs + + +def check_witness(sig, wit): + """Independent replay of a labelling/order witness. True iff valid.""" + M, pi, sg, Z = sig + a, b, order = wit["a"], wit["b"], wit["order"] + if sorted(order) != sorted(set(order)) or not order: + return False + for t in order: + if not (1 <= a[t] <= 7) or (a[t] & ~pi[t]) or (b[t] & ~sg[t]): + return False + if (((a[t] & b[t]).bit_count() & 1)) != 1: + return False + for i, t in enumerate(order): + for s in order[i + 1:]: + if M[t][s] == 0 and (((a[t] & b[s]).bit_count() & 1)) == 1: + return False + return True + + +def hill_climb(sig, tabs, iters=240, seed=5, start=None): + """Deterministic hill-climb over a-labels with exact completion; returns witness dict.""" + M, pi, sg, Z = sig + v = len(M) + rng = random.Random(seed) + a = list(start) if start else [rng.choice(opts(pi[t])) for t in range(v)] + best, bestT, bestF = complete(a, pi, sg, Z, v, tabs) + for _ in range(iters): + t = rng.randrange(v) + old = a[t] + cand = [m for m in opts(pi[t]) if m != old] + if not cand: + continue + a[t] = rng.choice(cand) + val, T, F = complete(a, pi, sg, Z, v, tabs) + if val >= best: + best, bestT, bestF = val, T, F + else: + a[t] = old + order, bs = reconstruct(a, sg, Z, v, tabs, bestT, bestF) + wit = {"a": a, "b": bs, "order": order} + assert check_witness(sig, wit), "hill-climb produced an invalid witness" + return best, wit + + +def exact_cert(sig, tabs, cap=200000): + """Exact cert by enumerating all a-labelings, when the product of option + counts is within cap. Returns (value, exhausted).""" + M, pi, sg, Z = sig + v = len(M) + counts = [len(opts(pi[t])) for t in range(v)] + total = 1 + for c in counts: + total *= c + if total > cap: + return None, False + best = 0 + for pick in itertools.product(*[opts(pi[t]) for t in range(v)]): + val, T, _ = complete(list(pick), pi, sg, Z, v, tabs) + if val > best: + best = val + if val == v: + break + return best, True + + +# ------------------------------------------------- anchor / residue ---- +def anchor_labels(P, Q): + v = len(P) + a0 = [sum(1 << j for j in range(3) if P[t][j] % 2 != 0) for t in range(v)] + b0 = [sum(1 << j for j in range(3) if Q[t][j] % 2 != 0) for t in range(v)] + return a0, b0 + + +def classify_line(sig, a0, b0, t): + """anchor_good: K0_tt = 1 (M_tt odd). repairable_1s: K0_tt = 0 but some + a* inside pi(t) gives a* . b0(t) = 1 and a* . b0(s) = 0 at every incidence + M_ts = 0 (b fixed at b0, full one-sided repair). tied_isotropic: neither + (the stated residue of PR 2717 / root-unit-decoder-lemmas section 7).""" + M, pi, sg, Z = sig + v = len(M) + if ((a0[t] & b0[t]).bit_count() & 1) == 1: + return "anchor_good" + for a_star in opts(pi[t]): + if ((a_star & b0[t]).bit_count() & 1) == 0: + continue + good = True + for s in range(v): + if s != t and M[t][s] == 0 and ((a_star & b0[s]).bit_count() & 1): + good = False + break + if good: + return "repairable_1s" + return "tied_isotropic" + + +def classify(sig, a0, b0): + M = sig[0] + v = len(M) + return [classify_line(sig, a0, b0, t) for t in range(v)] + + +# ------------------------------------------- MAS and digraph utilities ---- +def mas_masks(out, v, allowed): + """Exact maximum induced acyclic subset of the digraph (out-adjacency masks + out[t]) restricted to `allowed`; returns (size, subset mask, unused). + Subsets of `allowed` are enumerated in compressed increasing order so every + DP predecessor is processed first. Results are memoized on (allowed, out) + — pivot maps repeat partitions.""" + key = (allowed, tuple(out)) + hit = _MAS_CACHE.get(key) + if hit is not None: + return hit + verts = [t for t in range(v) if (allowed >> t) & 1] + m = len(verts) + out_c = [0] * m + for i, t in enumerate(verts): + cm = 0 + for j, s in enumerate(verts): + if (out[t] >> s) & 1: + cm |= 1 << j + out_c[i] = cm + acyc = bytearray(1 << m) + acyc[0] = 1 + best, bestT_c = 0, 0 + for T in range(1, 1 << m): + u, ok = T, 0 + while u: + lb = u & -u + i = lb.bit_length() - 1 + prev = T ^ lb + if acyc[prev] and (out_c[i] & prev) == 0: + ok = 1 + break + u ^= lb + acyc[T] = ok + if ok and T.bit_count() > best: + best, bestT_c = T.bit_count(), T + bestT = 0 + for i, t in enumerate(verts): + if (bestT_c >> i) & 1: + bestT |= 1 << t + res = (best, bestT, None) + _MAS_CACHE[key] = res + return res + + +def topo_backward(sub, out): + """Order of `sub` with every internal out-edge pointing backward: sinks first.""" + order = [] + remaining = sub + while remaining: + found = None + u = remaining + while u: + lb = u & -u + t = lb.bit_length() - 1 + if (out[t] & remaining) == 0: + found = t + break + u ^= lb + assert found is not None, "subgraph must be acyclic" + order.append(found) + remaining ^= 1 << found + return order + + +# ------------------------------------------ Lemma MX construction ---- +_MAS_CACHE = {} + + +def mx_bound(sig, a0, b0, c_map, classes, mode="A_first"): + """Lemma MX construction (two order forms). classes: per line one of 'A' + (anchor label), 'U' (one-sided repair attempt), 'T' (matched pivot with + c_map[t] in D(t) as a unit mask), 'X' (excluded from the kept set). + + A_first order: A + U before the pivot block; exact hypotheses: every U line + admits a one-sided repair killing its A + U blockers (b0 labels) and its T + blockers (pivot bits), and A -> T conflicts vanish (a0(t) has no bit c(s) + at incidences t in A, s in T). + T_first order: the pivot block before A + U; exact hypotheses: every U line + admits a one-sided repair killing its A + U blockers, and T -> (A + U) + conflicts vanish (b0(s) has no bit c(t) at incidences t in T, s in A + U). + + In both forms the kept set is all of A and U plus per-class MAS subsets of + T, so the bound is |A| + |U| + sum_i MAS(Z[C_i]) with C_i = {t in T : + c_map[t] = 1<T conflict at ({t},{s})" + elif mode == "T_first": + for t in T: + for s in A + U: + if M[t][s] == 0 and (b0[s] & c_map[t]): + return None, f"T->AU conflict at ({t},{s})" + else: + return None, f"unknown mode {mode}" + outT = [0] * v + for t in T: + for s in T: + if t != s and M[t][s] == 0 and c_map[t] == c_map[s]: + outT[t] |= 1 << s + kept_T = [] + for i in (1, 2, 4): + allowed = sum(1 << t for t in T if c_map[t] == i) + if not allowed: + continue + sz, sub, _ = mas_masks(outT, v, allowed) + kept_T.extend(topo_backward(sub, outT)) + for t in range(v): + if (sub >> t) & 1: + a_lab[t] = c_map[t] + b_lab[t] = c_map[t] + order = (A + U + kept_T) if mode == "A_first" else (kept_T + A + U) + for t in T: + if t in a_lab: + continue + a_lab[t] = c_map[t] + b_lab[t] = c_map[t] + wit = {"a": [a_lab.get(t, 1) for t in range(v)], + "b": [b_lab.get(t, 1) for t in range(v)], + "order": order} + if not check_witness(sig, wit): + return None, "constructed witness failed independent replay" + return len(order), wit + + +def pivot_maps(sig, budget, seed=3): + """Pivot maps c: [v] -> {1,2,3} with c(t) in D(t) = pi(t) & sg(t). Exhaustive + when the product of |D(t)| is within budget; otherwise a deterministic sample.""" + M, pi, sg, Z = sig + v = len(M) + D = [pi[t] & sg[t] for t in range(v)] + # pivot values are F2 unit masks: 1, 2, 4 (not class indices 1..3) + choices = [[1 << i for i in range(3) if (D[t] >> i) & 1] for t in range(v)] + total = 1 + for c in choices: + total *= len(c) + if total > budget: + rng = random.Random(seed) + out = [] + for _ in range(budget): + out.append({t: rng.choice(choices[t]) for t in range(v)}) + return out, False + maps = [] + for pick in itertools.product(*choices): + maps.append({t: pick[t] for t in range(v)}) + return maps, True + + +def mp_bound(sig, tabs, maps): + """Matched-pivot certificate (Lemma MP of PR 2717): cert >= sum_i MAS(Z[C_i]). + Achieved value over the given pivot maps, with the witnessing labelling.""" + M, pi, sg, Z = sig + v = len(M) + best, bestWit = 0, None + for c_map in maps: + out = [0] * v + for t in range(v): + for s in range(v): + if t != s and M[t][s] == 0 and c_map[t] == c_map[s]: + out[t] |= 1 << s + total, kept = 0, [] + for i in (1, 2, 4): + allowed = sum(1 << t for t in range(v) if c_map[t] == i) + if not allowed: + continue + sz, sub, _ = mas_masks(out, v, allowed) + total += sz + kept.extend(topo_backward(sub, out)) + if total > best: + best = total + a = [c_map[t] for t in range(v)] + bestWit = {"a": a, "b": list(a), "order": kept} + if bestWit is not None and not check_witness(sig, bestWit): + return 0, None, "MP witness failed replay" + return best, bestWit, None + + +def mx_search(sig, a0, b0, classes, maps): + """Lemma MX achieved bound: maximized over the two order forms and three + class variants (as given; U demoted to T; all lines pivoted = Lemma MP). + The all-T variant makes the result always at least the matched-pivot + certificate. Returns (bound, witness, map, meta, failures).""" + best, bestWit, bestMap, bestMeta = 0, None, None, None + fails = {} + has_U = any(c == "U" for c in classes) + has_AU = has_U or any(c == "A" for c in classes) + variants = [("given", list(classes))] + if has_U: + variants.append(("A/T", ["A" if c == "A" else "T" for c in classes])) + variants.append(("allT", ["T" if c != "X" else "X" for c in classes])) + for vname, vcls in variants: + modes = ("A_first", "T_first") if (has_AU and vname != "allT") else ("A_first",) + for mode in modes: + for c_map in maps: + val, res = mx_bound(sig, a0, b0, c_map, vcls, mode) + if val is None: + key = res.split(" at ")[0] + fails[f"{vname}/{mode}: {key}"] = fails.get(f"{vname}/{mode}: {key}", 0) + 1 + elif val > best: + best, bestWit, bestMap = val, res, c_map + bestMeta = {"variant": vname, "mode": mode} + return best, bestWit, bestMap, bestMeta, fails + + +# ---------------------------------------------------- chain / B search ---- +def block_rank(rows_mask, Rj, Aj, v): + cols = [c for c in range(v) if (Aj >> c) & 1] + mat = [] + for t in range(v): + if (Rj >> t) & 1: + row = 0 + for i, c in enumerate(cols): + if (rows_mask[t] >> c) & 1: + row |= 1 << i + mat.append(row) + rank = 0 + for i in range(len(cols)): + piv = None + for r in range(rank, len(mat)): + if (mat[r] >> i) & 1: + piv = r + break + if piv is not None: + mat[rank], mat[piv] = mat[piv], mat[rank] + for r in range(len(mat)): + if r != rank and ((mat[r] >> i) & 1): + mat[r] ^= mat[rank] + rank += 1 + return rank + + +def chain_cost(Brows, pi, sg, v): + """sum_j rank_F2 B[R_j, A_j]; R_j = {t : j in pi(t)}, A_j = {t : j in sigma(t)}.""" + total = 0 + for j in range(3): + Rj = sum(1 << t for t in range(v) if (pi[t] >> j) & 1) + Aj = sum(1 << t for t in range(v) if (sg[t] >> j) & 1) + total += block_rank(Brows, Rj, Aj, v) + return total + + +def min_chain_cost(sig, budget_free=12, local_evals=200, seed=7): + """Minimum of chain cost over admissible B (0/1, unit diagonal, ones only + where M vanishes). Exhaustive when the free-pair count is small; otherwise + deterministic single-bit local search from B = I and random starts. Any B + found is an admissible upper bound on cert; a B below threshold falsifies + F-star on that instance via the proven chain cost >= cert(M).""" + M, pi, sg, Z = sig + v = len(M) + free = [(t, s) for t in range(v) for s in range(v) if t != s and Z[t][s]] + f = len(free) + + def cost_of(bits): + Brows = [1 << t for t in range(v)] + for k, (t, s) in enumerate(free): + if (bits >> k) & 1: + Brows[t] |= 1 << s + return chain_cost(Brows, pi, sg, v) + + best_bits = 0 + best = cost_of(0) + if f <= budget_free: + for bits in range(1, 1 << f): + c = cost_of(bits) + if c < best: + best, best_bits = c, bits + else: + rng = random.Random(seed) + for start in range(local_evals): + bits = 0 if start == 0 else rng.getrandbits(f) + cur = cost_of(bits) + improved = True + while improved: + improved = False + for k in range(f): + nxt = bits ^ (1 << k) + c = cost_of(nxt) + if c < cur: + best, best_bits, cur, improved, bits = c, nxt, c, True, nxt + elif c == cur and rng.random() < 0.02: + bits, cur = nxt, c + return best, best_bits + + +# ---------------------------------------------------------- generators ---- +def _tied_line(rng, tied_count): + """One line with exactly `tied_count` coordinates carrying odd values in + both p and q (tied minimal valuations at level 0) and all remaining + coordinates carrying at least one even factor (so their product is even). + M_tt = sum of tied_count signed ones plus an even remainder.""" + while True: + coords = [0, 1, 2] + rng.shuffle(coords) + S = coords[:tied_count] + P, Q = [0, 0, 0], [0, 0, 0] + for j in S: + P[j] = rng.choice([-1, 1]) + Q[j] = rng.choice([-1, 1]) + for j in coords[tied_count:]: + P[j] = rng.choice([-2, -1, 1, 2]) + Q[j] = rng.choice([-2, -1, 1, 2]) + if P[j] % 2 != 0 and Q[j] % 2 != 0: + Q[j] = 2 * rng.choice([-1, 1]) + if sum(P[j] * Q[j] for j in range(3)) != 0: + return P, Q + + +def gen_tied_isotropic(rng, v): + """All-diagonal-even decoders with exactly two tied minimal valuations on + every line: the mod-2 anchor is isotropic on every line (K0_tt = 0 with two + tied odd products). This is PR 2717's tied-heavy idea pushed to the + maximal-tie residue: PR 2717 tied on half its lines, this family ties on + all of them (the anchor contributes nothing).""" + P, Q = [], [] + for _ in range(v): + p, q = _tied_line(rng, 2) + P.append(p) + Q.append(q) + return (P, Q), signature(P, Q) + + +def gen_mixed(rng, v): + """Half the lines have a unique minimal valuation (anchor-good, M_tt odd), + half have two tied minima (isotropic): the mixed residue where Lemma AN's + anchor and the tied obstruction coexist.""" + P, Q = [], [] + n_good = max(1, v // 2) + for t in range(v): + p, q = _tied_line(rng, 1 if t < n_good else 2) + P.append(p) + Q.append(q) + return (P, Q), signature(P, Q) + + +# ------------------------------------------------------------- controls ---- +def brute_cert(sig): + """Definition-level brute force over all labellings; MAS of D_K on V(K).""" + M, pi, sg, Z = sig + v = len(M) + best = 0 + for a in itertools.product(range(8), repeat=v): + for t in range(v): + if a[t] & ~pi[t]: + break + else: + for b in itertools.product(range(8), repeat=v): + for t in range(v): + if b[t] & ~sg[t]: + break + else: + Vk = [t for t in range(v) if ((a[t] & b[t]).bit_count() & 1)] + if len(Vk) <= best: + continue + n = len(Vk) + D = [[0] * n for _ in range(n)] + for i, t in enumerate(Vk): + for j, s in enumerate(Vk): + if t != s and M[t][s] == 0 and ((a[t] & b[s]).bit_count() & 1): + D[i][j] = 1 + out = [0] * n + for i in range(n): + for j in range(n): + if D[i][j]: + out[i] |= 1 << j + sz, _, _ = mas_masks(out, n, (1 << n) - 1) + if sz > best: + best = sz + return best + + +def load_cfg(name): + with open(os.path.join(DATA, name), "r", encoding="utf-8") as fh: + cfg = json.load(fh) + P = [c[0] for c in cfg] + Q = [c[1] for c in cfg] + return (P, Q), signature(P, Q) + + +def main(): + fails = [] + results = {} + + # ---- controls ---- + log("controls") + # engine exact-cert vs definition-level brute force on three v = 3 instances + brute_agree = 0 + for seed in (11, 22, 33): + (P, Q), sig = gen_instance(random.Random(seed), 3, -1, 1) + tabs = bfeas_tables(sig[1], sig[2]) + ec, exh = exact_cert(sig, tabs, cap=100000) + bb = brute_cert(sig) + if ec == bb: + brute_agree += 1 + else: + fails.append(f"brute/engine disagree (seed {seed}): {bb} vs {ec}") + + P3 = [[1, 0, 0], [0, 1, 0], [0, 0, 1]] + sig_diag = signature(P3, P3) + tabs_diag = bfeas_tables(sig_diag[1], sig_diag[2]) + diag_cert, _ = exact_cert(sig_diag, tabs_diag, cap=100000) + if diag_cert != 3: + fails.append(f"diagonal control: cert {diag_cert} != 3") + + (Pc, Qc), sig_c = gen_instance(random.Random(999), 4, -1, 1) + tabs_c = bfeas_tables(sig_c[1], sig_c[2]) + _, wit_c = hill_climb(sig_c, tabs_c, iters=60, seed=4) + if not check_witness(sig_c, wit_c): + fails.append("checker rejected a true witness") + corrupt_rejects = 0 + w1 = json.loads(json.dumps(wit_c)) + w1["a"][w1["order"][0]] = 0 + if not check_witness(sig_c, w1): + corrupt_rejects += 1 + w2 = json.loads(json.dumps(wit_c)) + w2["b"][w2["order"][0]] = 0 + if not check_witness(sig_c, w2): + corrupt_rejects += 1 + if corrupt_rejects != 2: + fails.append(f"corrupted witnesses accepted: {2 - corrupt_rejects}/2") + + # Lemma MX special cases must reproduce AN and MP on controls + (Pm, Qm), sig_m = gen_instance(random.Random(7), 5, -2, 2) + a0m, b0m = anchor_labels(Pm, Qm) + cls_m = classify(sig_m, a0m, b0m) + maps_m, _ = pivot_maps(sig_m, budget=3000) + mp_v, mp_wit, mp_err = mp_bound(sig_m, bfeas_tables(sig_m[1], sig_m[2]), maps_m) + if mp_err: + fails.append(f"MP control error: {mp_err}") + elif mp_wit is not None and not check_witness(sig_m, mp_wit): + fails.append("MP control witness failed replay") + an_count = sum(1 for t in range(5) if cls_m[t] == "anchor_good") + classes_allA = ["A" if cls_m[t] == "anchor_good" else "X" for t in range(5)] + val_allA, wit_allA = mx_bound(sig_m, a0m, b0m, maps_m[0], classes_allA) + if val_allA != an_count: + fails.append(f"MX all-anchor special case {val_allA} != AN count {an_count}") + elif not check_witness(sig_m, wit_allA): + fails.append("MX all-anchor witness failed replay") + classes_allT = ["T"] * 5 + val_allT, wit_allT = mx_bound(sig_m, a0m, b0m, maps_m[0], classes_allT) + if val_allT is not None and not check_witness(sig_m, wit_allT): + fails.append("MX all-pivot witness failed replay") + log(f"controls: brute_agree={brute_agree}/3 diagonal_cert={diag_cert} " + f"corrupt_rejects={corrupt_rejects}/2 mx_an={val_allA}/{an_count} " + f"mp_control={mp_v}") + if brute_agree != 3: + fails.append(f"brute/engine agreement {brute_agree}/3") + results["controls"] = {"brute_agree": brute_agree, "diag_cert": diag_cert, + "corrupt_rejects": corrupt_rejects, + "mx_all_anchor": val_allA, "an_count": an_count, + "mp_control": mp_v} + if not fails: + print("PASS_FSTARTIED_CONTROLS") + + # ---- fixtures: tied_min and cex_min_1 ---- + log("fixtures") + fixtures = {} + for name, recorded in (("tied_min.json", 11), ("cex_min_1.json", 18)): + (P, Q), sig = load_cfg(name) + M, pi, sg, Z = sig + v = len(M) + a0, b0 = anchor_labels(P, Q) + cls = classify(sig, a0, b0) + an_bound = sum(1 for t in range(v) if cls[t] == "anchor_good") + tabs = bfeas_tables(pi, sg) + maps, exh = pivot_maps(sig, budget=20000) + mp_v, mp_wit, mp_err = mp_bound(sig, tabs, maps) + # MX: A = anchor_good, U = repairable_1s (repair test is inside mx_bound), + # T = tied_isotropic and any U line whose repair fails (auto-demoted). + classes = ["A" if cls[t] == "anchor_good" else + ("U" if cls[t] == "repairable_1s" else "T") for t in range(v)] + mx_v, mx_wit, mx_map, mx_meta, mx_fails = mx_search(sig, a0, b0, classes, maps) + wit_val, wit = hill_climb(sig, tabs, iters=400, seed=9) + if name == "cex_min_1.json": + with open(os.path.join(DATA, "cex_min_1.witness.json"), "r", encoding="utf-8") as fh: + stored = json.load(fh) + if not check_witness(sig, stored): + fails.append("cex_min_1 stored witness failed replay") + wit_val = max(wit_val, len(stored["order"])) + if wit_val < recorded: + fails.append(f"{name}: engine witness {wit_val} < recorded {recorded}") + fixtures[name] = { + "v": v, "threshold": threshold(v), "diag_odd": an_bound, + "classification": {k: cls.count(k) for k in + ("anchor_good", "repairable_1s", "tied_isotropic")}, + "an_bound": an_bound, "mp_bound": mp_v, "mp_exhaustive": exh, + "mx_bound": mx_v, "mx_meta": mx_meta, "mx_map": mx_map, + "mx_failures": mx_fails, + "engine_witness": wit_val, "recorded_cert": recorded, + "fstar_holds": wit_val >= threshold(v), + } + log(f"{name}: v={v} thr={threshold(v)} AN={an_bound} MP={mp_v} " + f"MX={mx_v} witness={wit_val} cls={fixtures[name]['classification']}") + for tag, w in (("mp", mp_wit), ("mx", mx_wit)): + if w is not None and not check_witness(sig, w): + fails.append(f"{name}: {tag} witness failed replay") + results["fixtures"] = fixtures + if not fails: + print("PASS_FSTARTIED_FIXTURES") + + # ---- Lemma MX summary marker ---- + if all(fixtures[k]["mx_bound"] >= fixtures[k]["threshold"] for k in fixtures): + print("PASS_FSTARTIED_MX") + else: + fails.append("MX bound below threshold on a fixture") + + # ---- search: tied residue, smallest falsifying instance first ---- + log("search (smallest first)") + search_records = [] + falsifiers = [] + min_ratio = None + worst = None + for v in range(3, 13): + thr = threshold(v) + for fam, gen in (("tied_isotropic", gen_tied_isotropic), + ("mixed", gen_mixed)): + n_inst = 2 + for k in range(n_inst): + (P, Q), sig = gen(random.Random(1000 * v + 37 * k + (0 if fam == "tied_isotropic" else 1)), v) + M, pi, sg, Z = sig + a0, b0 = anchor_labels(P, Q) + cls = classify(sig, a0, b0) + an_bound = sum(1 for t in range(v) if cls[t] == "anchor_good") + tabs = bfeas_tables(pi, sg) + # exact cert when cheap, else hill-climb witness + ec, exh = exact_cert(sig, tabs, cap=120000) + wit_val, wit = hill_climb(sig, tabs, iters=300 if v <= 8 else 200, seed=13) + val = ec if exh else wit_val + maps, mexh = pivot_maps(sig, budget=800) + mp_v, mp_wit, mp_err = mp_bound(sig, tabs, maps) + classes = ["A" if cls[t] == "anchor_good" else + ("U" if cls[t] == "repairable_1s" else "T") for t in range(v)] + mx_v, mx_wit, mx_map, mx_meta, mx_fails = mx_search(sig, a0, b0, classes, maps) + cb, _ = min_chain_cost(sig, budget_free=12, local_evals=120, seed=17) + rec = {"family": fam, "v": v, "k": k, "threshold": thr, + "exact": exh, "cert_or_witness": val, + "an_bound": an_bound, "mp_bound": mp_v, "mx_bound": mx_v, + "mx_meta": mx_meta, "chain_cost_upper": cb, + "classification": {key: cls.count(key) for key in + ("anchor_good", "repairable_1s", "tied_isotropic")}, + "mx_failures": mx_fails} + search_records.append(rec) + ratio = val / v + if min_ratio is None or ratio < min_ratio: + min_ratio, worst = ratio, rec + if cb < thr: + falsifiers.append(rec) + log(f"FALSIFIER at v={v} family={fam} k={k}: chain cost {cb} < {thr}") + if not exh and val < thr: + log(f"unresolved below threshold at v={v} {fam} k={k}: witness {val} < {thr}") + log(f"v={v} done: {sum(1 for r in search_records if r['v'] == v)} instances") + n = len(search_records) + results["search"] = { + "instances": n, "falsifiers": len(falsifiers), + "min_witness_ratio": None if min_ratio is None else round(min_ratio, 4), + "worst": worst, + "exact_decided": sum(1 for r in search_records if r["exact"]), + "mx_below_threshold": sum(1 for r in search_records + if r["mx_bound"] < r["threshold"]), + "mp_below_threshold": sum(1 for r in search_records + if r["mp_bound"] < r["threshold"]), + "mx_strictly_above_mp": sum(1 for r in search_records + if r["mx_bound"] > r["mp_bound"]), + "records": search_records, + } + log(f"search: {n} instances, falsifiers={len(falsifiers)}, " + f"min witness ratio={results['search']['min_witness_ratio']}, " + f"exact-decided={results['search']['exact_decided']}, " + f"MX below threshold on {results['search']['mx_below_threshold']}") + if falsifiers: + fails.append(f"{len(falsifiers)} falsifier(s) found — F-star refuted on the searched domain") + if not fails: + print("PASS_FSTARTIED_SEARCH") + + # ---- certificate ---- + digest = hashlib.sha256( + json.dumps(results, sort_keys=True, default=str).encode("utf-8") + ).hexdigest()[:16] + results["digest"] = digest + with open(os.path.join(HERE, "CERTIFICATE.json"), "w", encoding="utf-8") as fh: + json.dump(results, fh, indent=1, sort_keys=True, default=str) + log(f"certificate digest {digest}") + if fails: + for f in fails: + print("FAIL:", f) + raise SystemExit(1) + print("PASS_FSTAR_TIED_RESIDUE") + + +def gen_instance(rng, v, lo, hi): + while True: + P = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + Q = [[rng.randint(lo, hi) for _ in range(3)] for _ in range(v)] + if all(sum(P[t][j] * Q[t][j] for j in range(3)) != 0 for t in range(v)): + M, pi, sg, Z = signature(P, Q) + return (P, Q), (M, pi, sg, Z) + + +if __name__ == "__main__": + main()