diff --git a/research/p104-flag43-side-correction-bill/CERTIFICATE.json b/research/p104-flag43-side-correction-bill/CERTIFICATE.json new file mode 100644 index 0000000000..97b6d37d58 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/CERTIFICATE.json @@ -0,0 +1,1963 @@ +{ + "basis_head": 15, + "bill": { + "P": { + "Y59_final_X21": "0", + "Y59_final_row_is_identity": false, + "added_rank_by_register": { + "C": 1 + }, + "added_vs_R0": { + "events": 5, + "rank_mass": 1, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y59" + ], + "correction_adds": 1, + "correction_charts": [ + 8 + ], + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4063, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1072, + "2": 63, + "3": 85, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 9, + "erase": 9, + "zero": 9 + }, + "profile_delta_vs_R0": { + "1": 1 + }, + "profile_delta_vs_published": { + "1": -2, + "2": 5, + "3": -1, + "4": -1 + }, + "rank_mass": 2369, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y59", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 6, + "transport_occurrences": 1411 + }, + "R0": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "paid_profile": { + "1": 1071, + "2": 63, + "3": 85, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + }, + "S": { + "Y59_final_X21": "0", + "Y59_final_row_is_identity": false, + "added_rank_by_register": { + "X21": 2 + }, + "added_vs_R0": { + "events": 3, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 2 + }, + "changed_final_rows": [ + "Y59" + ], + "correction_adds": 1, + "correction_charts": [ + 8 + ], + "distinct_native_edges": 742, + "endpoint_adapters": 208, + "events": 4061, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1073, + "2": 63, + "3": 85, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_R0": { + "1": 2 + }, + "profile_delta_vs_published": { + "1": -1, + "2": 5, + "3": -1, + "4": -1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y59", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 6, + "transport_occurrences": 1412 + }, + "T": { + "Y59_final_X21": "0", + "Y59_final_row_is_identity": false, + "added_rank_by_register": { + "Y59": 2 + }, + "added_vs_R0": { + "events": 2, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y59" + ], + "correction_adds": 1, + "correction_charts": [ + 9 + ], + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4060, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1072, + "2": 62, + "3": 86, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_R0": { + "1": 1, + "2": -1, + "3": 1 + }, + "profile_delta_vs_published": { + "1": -2, + "2": 4, + "4": -1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y59", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 6, + "transport_occurrences": 1411 + }, + "T48": { + "Y59_final_X21": "0", + "Y59_final_row_is_identity": true, + "added_rank_by_register": { + "Y59": 2 + }, + "added_vs_R0": { + "events": 49, + "rank_mass": 2, + "scalar_adds": 48, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y59" + ], + "correction_adds": 48, + "correction_charts": [ + 9 + ], + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4107, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": true, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1072, + "2": 62, + "3": 86, + "4": 103, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_R0": { + "1": 1, + "2": -1, + "3": 1 + }, + "profile_delta_vs_published": { + "1": -2, + "2": 4, + "4": -1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y59", + "scalar_adds": 2672, + "target_frame_before_correction_rank": 6, + "transport_occurrences": 1411 + }, + "published": { + "distinct_native_edges": 740, + "endpoint_adapters": 208, + "events": 4058, + "paid_profile": { + "1": 1074, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "rank_mass": 2368, + "scalar_adds": 2624, + "transport_occurrences": 1410 + } + }, + "claim_id": "p104-flag43-side-correction-bill", + "corrections": { + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X21 into C at the full chart, descend C to Y59's final hyperplane, deliver, discard", + "splices": [ + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ], + [ + "zero", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "copy", + "C", + "X21", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 1 + ], + [ + "add", + "Y59", + "C", + "-1/2", + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ] + ], + [ + "erase", + "C", + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ] + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published_range": [ + 3525, + 3526 + ] + } + ] + }, + "S": { + "route": "source detour: Y59 takes R0's terminal transport, X21 descends to Y59's final hyperplane for one ADD and returns to the full chart before its next read at 3705", + "splices": [ + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ], + [ + "transport", + "X21", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 1 + ], + [ + "add", + "Y59", + "X21", + "-1/2", + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ] + ], + [ + "transport", + "X21", + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published_range": [ + 3525, + 3526 + ] + } + ] + }, + "T": { + "route": "target lift at the co-hosted cut: Y59 leaves the head chart W6 for the full chart, takes the entry from X21 there, then descends to its final hyperplane", + "splices": [ + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ], + [ + "add", + "Y59", + "X21", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y59", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published_range": [ + 3525, + 3526 + ] + } + ] + }, + "T48": { + "route": "whole Y59 row of I - G/2 on the same lift: every off-diagonal source entry -G[59,s]/2 is added while Y59 sits in the full chart", + "splices": [ + { + "events": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 3 + ], + [ + "add", + "Y59", + "X1", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X2", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X3", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X4", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X7", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X8", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X9", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X13", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X15", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X16", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X17", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X21", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X22", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X23", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X27", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X28", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X29", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X35", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X36", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X40", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X44", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X45", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X46", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X47", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X51", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X52", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X53", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X55", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X56", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X57", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X60", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X61", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X62", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X64", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X65", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X66", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X70", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X74", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X75", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X82", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X86", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X90", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X91", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X96", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X97", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X101", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X102", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y59", + "X103", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y59", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y59", + [ + 95, + 447, + 6, + 32, + 20, + 15 + ], + [ + 499, + 27, + 228, + 32, + 112, + 15, + 7, + 1 + ], + 2 + ] + ], + "published_range": [ + 3525, + 3526 + ] + } + ] + } + }, + "cut_event": 3525, + "end_cut_detour": { + "R0_detour_added_rank": 2, + "published_detour_added_rank": 2, + "published_detour_via_full_rank": 5, + "published_terminal_transport": [ + 3525, + 3 + ] + }, + "flag_index": 43, + "no_new_kappa": true, + "obstruction": { + "direct_cut_classes": 28, + "direct_first_obstruction": [ + [ + 0, + [ + 264, + "Y67" + ] + ], + [ + 224, + [ + 265, + "Y67" + ] + ], + [ + 225, + [ + 267, + "Y67" + ] + ], + [ + 226, + [ + 268, + "Y67" + ] + ], + [ + 227, + [ + 268, + "Y67" + ] + ], + [ + 228, + [ + 2103, + "Y96" + ] + ], + [ + 885, + [ + 885, + "Y59" + ] + ], + [ + 1064, + [ + 1064, + "Y59" + ] + ], + [ + 1247, + [ + 1247, + "Y59" + ] + ], + [ + 1518, + [ + 1518, + "Y59" + ] + ], + [ + 1709, + [ + 1709, + "Y59" + ] + ], + [ + 1788, + [ + 1788, + "Y59" + ] + ], + [ + 1873, + [ + 1873, + "Y59" + ] + ], + [ + 2006, + [ + 2006, + "Y59" + ] + ], + [ + 2100, + [ + 2100, + "Y59" + ] + ], + [ + 2192, + [ + 2192, + "Y59" + ] + ], + [ + 2276, + [ + 2276, + "Y59" + ] + ], + [ + 2342, + [ + 2342, + "Y59" + ] + ], + [ + 2394, + [ + 2394, + "Y59" + ] + ], + [ + 2699, + [ + 2699, + "Y59" + ] + ], + [ + 2892, + [ + 2892, + "Y59" + ] + ], + [ + 3077, + [ + 3077, + "Y59" + ] + ], + [ + 3232, + [ + 3232, + "Y59" + ] + ], + [ + 3365, + [ + 3365, + "Y59" + ] + ], + [ + 3706, + [ + 3706, + "Y59" + ] + ], + [ + 3761, + [ + 3761, + "Y59" + ] + ], + [ + 3812, + [ + 3812, + "Y59" + ] + ], + [ + 3864, + [ + 3864, + "Y59" + ] + ] + ], + "entry": { + "correction_coefficient": "-1/2", + "diagonal_gram": 2, + "gram": 1, + "source": "X21", + "target": "Y59" + }, + "feeder_head_in_target_final": false, + "feeder_source_gram_with_target": 0, + "feeder_source_head": [ + 131 + ], + "flag_head_in_target_final": true, + "non_private_registers_at_rank_floor": 280, + "partner_feeder": [ + 625, + [ + "add", + "G9", + "X12", + 2 + ] + ], + "private_early_delivery_cuts": 11, + "private_early_first_obstruction": [ + [ + 0, + [ + 264, + "Y67" + ] + ], + [ + 224, + [ + 265, + "Y67" + ] + ], + [ + 225, + [ + 267, + "Y67" + ] + ], + [ + 226, + [ + 268, + "Y67" + ] + ], + [ + 227, + [ + 268, + "Y67" + ] + ], + [ + 228, + [ + 2103, + "Y96" + ] + ], + [ + 2100, + [ + 2194, + "Y96" + ] + ], + [ + 2192, + [ + 2336, + "Y26" + ] + ], + [ + 2276, + [ + 2387, + "Y56" + ] + ], + [ + 2342, + [ + 2706, + "Y96" + ] + ], + [ + 2394, + [ + 2706, + "Y96" + ] + ] + ], + "published_private_lifetimes": [ + 2461, + 2524 + ], + "row_59_offdiagonal_nonzero": 48, + "source_first_read": [ + 884, + [ + "add", + "G9", + "X21", + -2 + ] + ], + "source_forced_full_from": 1708, + "source_forced_rank_at_events": [ + [ + 884, + "G9", + 2 + ], + [ + 1063, + "G13", + 6 + ], + [ + 1246, + "G17", + 7 + ], + [ + 1517, + "G5", + 8 + ], + [ + 1708, + "G9", + 9 + ], + [ + 1787, + "G13", + 9 + ], + [ + 1872, + "G17", + 9 + ], + [ + 2005, + "G5", + 9 + ], + [ + 3705, + "Q1", + 9 + ], + [ + 3760, + "Q2", + 9 + ], + [ + 3811, + "Q3", + 9 + ], + [ + 3863, + "Q4", + 9 + ] + ] + }, + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "requested_pin": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "schema_version": 1, + "selected_kappa": "0.001672660197076918" +} diff --git a/research/p104-flag43-side-correction-bill/CORRECTION-RECIPES.json b/research/p104-flag43-side-correction-bill/CORRECTION-RECIPES.json new file mode 100644 index 0000000000..d88b6c156e --- /dev/null +++ b/research/p104-flag43-side-correction-bill/CORRECTION-RECIPES.json @@ -0,0 +1,210 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 132, + 68, + 32, + 16, + 8, + 2, + 1 + ], + "old": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 1, + 8, + 16, + 32, + 64, + 128, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 4, + 1, + 2, + 8, + 16, + 32, + 68, + 132, + 256 + ], + "offset": 192, + "phase": 1, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 132, + 68, + 32, + 16, + 8, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 9, + 16, + 32, + 64, + 129, + 1, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + }, + "rank": 1, + "right": { + "linear_Z4": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0 + ], + "matrix_rows": [ + 132, + 1, + 2, + 128, + 8, + 16, + 32, + 192, + 256 + ], + "offset": 9, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by corrections T, S, P and T48 that are absent from the published p104-native-channel recipe set and from #3508's REPAIR-RECIPES.json. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag43-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag43-side-correction-bill/MASTER-HANDOFF.md new file mode 100644 index 0000000000..393cbf5581 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/MASTER-HANDOFF.md @@ -0,0 +1,139 @@ +# Master handoff — `research/p104-flag43-side-correction-bill/` + +## Candidate + +- Branch: `cursor/flag43-side-correction-bill-6707` (VictorLiwentao fork). The + `-6707` suffix is this worker's environment-required branch suffix, not + `-60b9`. +- Content tip: `8838ce9049e3c0beb555b8e1b6d48c9e11be3685`. This commit holds the + full scientific package. Its parent, `39ad54e9…`, adds the package. The content + tip only lowers the test timeout to the 600 s registry cap. +- Packaging tip: the child commit that adds only this handoff file. Read its SHA + with `git rev-parse origin/cursor/flag43-side-correction-bill-6707`. +- Package: `research/p104-flag43-side-correction-bill/` +- Base: CrocSwap main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The requested + pin, `6f100d4bb5083f8c35d96fd95a539811c62f245c`, is an ancestor of this base. + The newer main is required because #3508's R0 package, an input here, merged + after the requested pin. +- Card: `p104-side-correction` (refined), priority revision 6. The card is + byte-identical to the catalogue at the base. +- κ: unchanged at `0.001672660197076918`. +- Author and committer: Wentao Li ``. A hook-injected + co-author trailer was stripped with `git commit-tree`. +- No CrocSwap PR has been opened. + +## Claim + +This answers #3508's open question 2 for flag 43 (`X21` → `Y59`, head `15`). +Since `G[59,21] = 1`, the `I − G/2` entry is `−1/2·X21` into `Y59`. On R0, all +four corrections below replace `Y59`'s terminal transport at 3525, while the +head is still co-hosted: + +- `Y59` is in `W6 = [95,447,6,32,20,15]`; +- `X21` is in FULL; +- both frames span `15`. + +| Word | Δ events | Δ ADDs | Δ transports | Δ rank | Profile Δ vs R0 | +|---|---:|---:|---:|---:|---| +| T: target lift `W6→FULL`, ADD, `FULL→F59` | +2 | +1 | +1 | +2 | `H1 − H2 + H3` | +| S: source detour `X21: FULL→F59→FULL` | +3 | +1 | +2 | +2 | `2H1` | +| P: one private-copy lifetime | +5 | +1 | +1 | +1 | `H1` | +| T48: whole row 59 (48 entries) on T's lift | +49 | +48 | +1 | +2 | `H1 − H2 + H3` | + +In T48, `Y59`'s final row becomes exactly `y59 + x59`. + +Each word is checked in two ways: + +- The unchanged `check_native.validate()` passes each coefficient-0 word. That + covers the two newly lowered `FULL ↔ F59` recipes, 208 adapters, 280 rows and + 72 dirty helpers. +- On the real word, the same checker fails only at `Y59`'s endpoint. Exact + replay confirms that only `Y59` changes. + +**Obstruction.** The class keeps the published events, ADDs, endpoint frames and +`C` lifetimes, and allows transports to be retargeted or inserted. In this +class, no placement of the correction ADD has zero added rank mass: + +- Events 625 and 884 (`G9 += 2·X12`, then `G9 −= 2·X21`) force `X12`'s head + `131` into `X21`'s frame. +- `G[59,12] = 0` puts `131` outside `Y59`'s final hyperplane. +- A least-lower-bound sweep blocks all 28 insertion classes. +- Each non-private register's added mass is even. + +So the strict minimum is exactly +2. The published end-cut detour also costs ++2, so co-hosting gives a rank-mass discount of 0. P's +1 is minimal for one +added private lifetime that copies `X21`, but only under the inherited +private-copy discard. + +## PASS lines + +```text +PASS_P104_FLAG43_SIDE_CORRECTION_BILL flag=43 entry=(59,21) coefficient=-1/2 zero_mass_placements=0/28 forcing=625:X12(131)->884:G9->X21 strict_min_added_rank=2 T=+1transport+1add+2rank(H1-H2+H3) S=+2transport+1add+2rank(2H1) P=+1transport+1add+1rank(H1)+1private_lifetime T48=+1transport+48add+2rank row59=identity cohost_discount=0 native_validate=4/4 no_new_kappa +PASS_P104_FLAG43_SIDE_CORRECTION_BILL_INDEPENDENT entry=(59,21) zero_mass_placements=0/28 early_private_deliveries_obstructed=11/11 T=+2rank S=+2rank P=+1rank T48=+2rank rows_changed=Y59_only row59=identity new_recipes=2 no_new_kappa +PASS_P104_FLAG43_SIDE_CORRECTION_BILL_TESTS cases=14 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag43-side-correction-bill outcome=completed +``` + +## Commands + +```sh +python3.12 -I -B research/p104-flag43-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-side-correction-bill +``` + +Run times: `verify.py` about 31 s, `independent.py` about 2 s, +`test_package.py` about 96 s with 4 workers, and the registry check about 128 s. +The default replay is read-only. Admission goes through `need()`, so it still +fires under `-O`, and the package contains no `assert` statements. Duplicate +JSON keys are rejected. + +## Closest priors (cite only) + +- [#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) (merged). + R0, the co-hosted chart and the class-Z closure. This package answers its + open question 2. +- [#3456](https://github.com/CrocSwap/integer-mult-bounds/pull/3456). Flag 43's + published chronology. It is not reprinted here. +- `research/p104-side-correction-rank-obstruction`. Its end-cut round-trip and + snapshot invoices (+2 rank per target) are compared against T's +2, and found + equal. +- `research/p104-channel-correction-absent` (the channel leaves `1/2`) and + `research/p104-native-channel` (semantics and the private-copy contract). + +## Soft-overlap risks + +- [#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532) (open) is + the flag-1 head-step repair. It is not touched or cited for content. Flags 1 + and 9 and the flag-0 cascade are untouched. +- `p104-side-correction-rank-obstruction` already prices a +2 per-target + detour at the end cut. This package's new content is: + - the co-hosted-cut placement on R0; + - the zero-mass obstruction over every insertion point, together with its + forcing chain; + - the private-copy +1 route; + - the native validation of the corrected words. +- An open-PR search for "side correction", "3508", "flag 43", "I-G/2" and + "co-hosted" found no other PR pricing this entry. + +## Open question + +The headline open question is whether P's private-copy discard is admissible +for a correction. If `C` must be uncomputed, the strict +2 applies to every +corrected target. Two further questions are open: + +- whether the 625/884-type forcing blocks a zero-mass entry for every pair with + `G[t,s] ≠ 0`; +- whether a fused correction that retunes published ADD coefficients (outside + the class) evades the bound. + +See `TASK.json`. + +## Limits + +This covers one entry and one target row at one cut of one finite word. The +theorem covers a single inserted ADD between `X21` and `Y59`. Multi-register +routes that meet `X21` before 884 are not enumerated. There is no global +hosting, precision or supplier, and no κ change. diff --git a/research/p104-flag43-side-correction-bill/NOTICE.md b/research/p104-flag43-side-correction-bill/NOTICE.md new file mode 100644 index 0000000000..8ad37dcf6a --- /dev/null +++ b/research/p104-flag43-side-correction-bill/NOTICE.md @@ -0,0 +1,13 @@ +# Notice + +This package applies explicit corrections to #3508's repaired P104 word R0 in +memory and checks them with the published native checker and a second scanner. +It does not modify frozen upstream sources or #3508's package. The two recipes +in `CORRECTION-RECIPES.json` were lowered with the pinned +`research/p104-native-channel/compile.py` and `vendor/clifford_exact.py` +(PR1991 lineage, Chafik Boukhalfa), whose notices are retained in that package. +Correction T also reuses #3508's committed `W6 -> FULL` recipe. + +Prepared by Wentao Li with substantial AI assistance. +Apache-2.0; predecessor notices and exact source pins are retained in +`SOURCES.json`. diff --git a/research/p104-flag43-side-correction-bill/PROOF.md b/research/p104-flag43-side-correction-bill/PROOF.md new file mode 100644 index 0000000000..0ba0c68312 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/PROOF.md @@ -0,0 +1,212 @@ +# Proof: the flag-43 side-correction entry at R0's co-hosted cut + +## Setup + +The base is CrocSwap main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The +requested pin, `6f100d4b…`, is an ancestor of it. The newer base is used because +#3508's R0 package is one of the inputs. + +Inputs, all hash-pinned: + +- the reviewed #1991 witness, recipes and checker in + `research/p104-native-channel/`; +- the #2981 flag matching (flag 43: `X21 → Y59`, basis head `15`); +- #3508's `CERTIFICATE.json`, which contains the R0 splices, and its + `REPAIR-RECIPES.json`. + +The channel rules are those of `research/p104-native-channel/PROOF.md` §2–§3: + +- A transport is nested and pays `|dim B − dim A|`. +- An ADD or copy needs both registers in the same frame. +- The private register `C` is created by zero, filled by copy and closed by + erase. These are inherited private-copy semantics. + +At the end, each target row of the channel is `y_t + Σ_s G[t,s] x_s / 2`, where +`G[t,s] = ` and `G[t,t] = 2`. The side correction must add +`(I − G/2)x`. Flag 43's entry is `(59, 21)`. Since `G[59,21] = 1`, the entry is +`−1/2`. + +## 1. The corrected words + +Let `F59` be `Y59`'s final frame `[499,27,228,32,112,15,7,1]`. It has rank 8 +and lies inside the hyperplane orthogonal to `Y59`'s physical root. Let FULL be +the rank-9 chart. In R0: + +- `Y59` is in `W6` from event 3363 until 3525; +- 3525 is `Y59: W6 → F59` (rank 2), and `Y59` has no later events; +- `X21` is in FULL from 1518 and has no events between 3364 and 3705; +- `C` has no lifetime after 2524; +- `Y59` is never the source of an ADD or copy. + +Every correction replaces event 3525: + +- **T:** `Y59: W6 → FULL` (rank 3); `Y59 += −1/2·X21` in FULL; + `Y59: FULL → F59` (rank 1). +- **S:** `Y59: W6 → F59` (rank 2); `X21: FULL → F59` (rank 1); + `Y59 += −1/2·X21` in `F59`; `X21: F59 → FULL` (rank 1). +- **P:** `Y59: W6 → F59`; `zero C` in FULL; `copy C ← X21` in FULL; + `C: FULL → F59` (rank 1); `Y59 += −1/2·C` in `F59`; `erase C` in `F59`. +- **T48:** as T, but with all 48 ADDs `Y59 += −G[59,s]/2 · X_s`, one for each + `s ≠ 59` with `G[59,s] ≠ 0`. All 104 sources are in FULL at 3525. + +`W6 → FULL` is #3508's committed recipe, which R0 already uses for `D17` at +3612. `FULL → F59` and `F59 → FULL` are lowered by `build.py` with the pinned +compiler. They are committed in `CORRECTION-RECIPES.json`. + +**Native validation.** `check_native.validate()` hard-codes the `G/2` endpoint +rows, so `verify.py` uses two runs per corrected word: + +1. It runs `validate()` unchanged on the word with each inserted ADD + coefficient set to `0`. This checks: + - every edge's complete Clifford operator, including phase; + - every transport binding and rank; + - the 208 endpoint adapters; + - the full framed induction. Every ADD and copy must be in a common chart, + every endpoint frame must match, and all 280 rows must close, including + the 72 dirty helpers and `C`'s storage. + + All of these conditions are independent of the ADD coefficients. +2. It replays the real word with exact rational rows and compares every final + row with R0's. + +In T, S and P, only `Y59` changes, and its change is exactly `−1/2·X21`. In +T48, `Y59`'s final row is exactly `{Y59: 1, X59: 1}`. As a control, the +unchanged `validate()` rejects each real word with +`full physical boundary endpoint Y59`. + +**Bill.** All counts come from the validated words. R0 equals the published +word in events, ADDs, transport occurrences, rank mass and edge count. + +| | events | ADDs | transports | rank mass | profile Δ vs R0 | added rank by register | +|---|---:|---:|---:|---:|---|---| +| T | 4,060 | 2,625 | 1,411 | 2,370 | `+H1 − H2 + H3` | `Y59: 2` | +| S | 4,061 | 2,625 | 1,412 | 2,370 | `+2H1` | `X21: 2` | +| P | 4,063 | 2,625 | 1,411 | 2,369 | `+H1` | `C: 1` | +| T48 | 4,107 | 2,672 | 1,411 | 2,370 | `+H1 − H2 + H3` | `Y59: 2` | + +P raises the private zero, copy and erase counts from 8 to 9 each. + +Comparing T and S: `T − S = H3 − H2 − H1`. + +- If `H` is convex with `H(0) = 0`, then `H3 − H2 ≥ H2 − H1 ≥ H1`, so + `T − S ≥ 0`: S is weakly cheaper. +- If `H(r) = a + br`, then T is cheaper by `a`, because it uses one fewer + transport occurrence. + +## 2. Obstruction + +**Class Z₁.** A repair is in class Z₁ when it meets all of these conditions: + +1. it keeps the published events in their published order, with the same ADD + and copy registers and coefficients; +2. it inserts exactly one correction ADD between `X21` and `Y59`; +3. it may retarget or insert transports; +4. it keeps every endpoint frame; +5. it keeps `C`'s published private events. + +R0 plus T, S or T48 are in Z₁. + +**Lemma 1 (parity).** Each transport changes rank by exactly its cost, so a +register's path cost is at least `|rank(final) − rank(initial)|` and has the +same parity. All 280 non-private registers are already at that floor in the +published word. So in Z₁, each non-private register's added mass is a +non-negative even integer. It is zero exactly when the register's path is +monotone. + +**Lemma 2 (least frames).** Fix a zero-added-mass repair, in which every +non-private path is monotone. Define `L_r(t)` by a forward sweep: + +- start from the initial frames; +- at each ADD between non-private registers `r` and `p`, set both frames to + `L_r + L_p`. + +`C` is left unconstrained, which is a relaxation. Every feasible repair has +`frame_r(t) ⊇ L_r(t)`. It is infeasible if any `L_r(t) ⊄ final_r`. + +All initial frames except the sources' heads are empty. So `L_r(t)` is the span +of the heads of the sources that reach `(r, t)` through a time-respecting chain +of ADDs. + +**Forcing chain.** Before 884, `G9`'s only source ADD is event 625, +`G9 += 2·X12`, and `X12`'s head is `131`. At 884, `G9 −= 2·X21` equalizes the +two lower bounds: + +```text +L_X21(884) = span{15, 131} +``` + +`X21`'s forced rank grows to `2, 6, 7, 8` at events 884, 1063, 1246 and 1517. +It is 9 from 1708. Because `G[59,12] = 0`, the binary pairing of `131` with +`Y59`'s root is odd, so `131 ∉ F59`. By contrast, `15 ∈ F59`, since +`G[59,21] = 1`. + +**Theorem.** No member of Z₁ has zero added rank mass. Its minimum added rank +mass is exactly 2. + +*Proof.* The sweep gives the same outcome for every insertion point between two +consecutive `X21`/`Y59` ADD events. That leaves 28 insertion classes. For each, +`verify.py` and `independent.py` add the equality `frame_X21(u) = frame_Y59(u)` +to the sweep: + +- **Classes `u ≤ 884`.** The meeting puts `15` into `Y59` from `u` on. The + sweep fails at `Y67` (events 264–268) for `u ≤ 227` and at `Y96` (2103) for + `228 ≤ u ≤ 884`. This is consistent with #3508's closure table. +- **Classes `u ≥ 885`.** The merged frame contains `131` and so is not inside + `F59`. The sweep fails at `u` itself. + +Zero is therefore impossible. By Lemma 1 the minimum is at least 2, and T, S +and T48 attain 2. ∎ + +The theorem covers one inserted ADD between `X21` and `Y59`. A correction routed +through additional inserted ADDs with other non-private registers is not +enumerated here. Any register that meets `X21` after 884 inherits `131` and +cannot later meet `Y59` without adding rank. Routes that meet `X21` before 884 +are not checked. + +**Co-host discount.** On the published word, event 3525 is +`Y59: [95,447,32,20,6] → F59` (rank 3). The end-cut detour through FULL costs +`4 + 1 = 5`, which is +2. On R0 the detour costs `3 + 1 − 2 = +2`. The rank-mass +discount from co-hosting the head is zero. + +**Private route.** Let class Z₁ᴾ be Z₁ with the inserted ADD replaced by one +added private lifetime: zero, copy from `X21` at time `t`, transports, ADD into +`Y59` at time `t′`, erase. + +- If any non-private register adds mass, that costs at least 2. +- Otherwise `C`'s path costs at least 1 unless its copy chart equals its + delivery chart, that is, unless `frame_X21(t) = frame_Y59(t′)`. + - For `t ≥ 885`, that chart contains `131 ∉ F59`. + - For `t ≤ 884`, the lifetime must end before the published lifetimes start + at 2461. Then `Y59` hosts `15` from `t′ < 2461` on. All 11 such delivery + classes fail the sweep, at `Y67`, `Y96`, `Y26` or `Y56`. + +So the minimum over Z₁ᴾ is exactly 1, and P attains it. + +## Controls + +`test_package.py` copies the package and its eight pinned inputs into a +temporary tree and runs both scanners there under `-O`. The clean tree must pass +and stay byte-identical. Fourteen mutations must be rejected by both scanners: + +- five certificate fields, covering the bill, per-register mass, feeder head, + full-from event and one obstruction row; +- a duplicate JSON key; +- a witness byte flip; +- a byte flip in #3508's certificate; +- a phase flip in a new recipe; +- a wrong coefficient; +- an undercharged lift; +- an ADD in the wrong chart; +- an unrestored source; +- an unclosed private lifetime. + +## Limits + +- This covers one entry, one target row and one cut of one finite word. It does + not price the other 103 rows, global hosting, idle children or precision. It + does not supply a supplier and does not change κ. +- Class Z₁ keeps every published ADD and coefficient. A fused correction that + retunes existing deliveries, such as `D17`'s at 3364, is outside it. +- P's +1 depends on the inherited private-copy discard. The native channel + package does not claim that this discard is reversible. +- `H_r` is left symbolic. diff --git a/research/p104-flag43-side-correction-bill/README.md b/research/p104-flag43-side-correction-bill/README.md new file mode 100644 index 0000000000..f11056d48c --- /dev/null +++ b/research/p104-flag43-side-correction-bill/README.md @@ -0,0 +1,133 @@ +# Flag 43's `I − G/2` entry costs +2 rank mass at the co-hosted cut; head co-hosting gives no discount + +**Exact bill plus a sharp obstruction. No new exponent.** + +[#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) (merged) +gives a repair R0 of the published P104 word. In R0, `Y59`'s last update, event +3364, runs in the head chart `W6 = [95,447,6,32,20,15]`. At that point `X21` is +in the full chart and still live. Its open question 2 asks what the `I − G/2` +side correction costs at that co-hosted cut. This package answers that question +for flag 43's entry and for the whole `Y59` row. It cites #3508 and +[#3456](https://github.com/CrocSwap/integer-mult-bounds/pull/3456) without +re-deriving R0 or the published chronology. + +## The entry + +`G[59,21] = = 1`, and the channel leaves `X21` in `Y59` with +coefficient `1/2`. The corresponding entry of `I − G/2` is `−1/2`. Applying it +leaves `Y59` with `X21` coefficient `0`. `Y59` is never read, so the correction +changes no other row. + +## Result + +Every correction below replaces R0's terminal `Y59` transport at event 3525 +(`W6 → F59`, rank 2). Here `F59` is `Y59`'s final rank-8 frame, which is the +hyperplane orthogonal to `Y59`'s root. + +| Word | Correction | Δ events | Δ ADDs | Δ transports | Δ rank mass | Profile Δ vs R0 | Edges | +|---|---|---:|---:|---:|---:|---|---:| +| **T** | `Y59: W6→FULL`, `Y59 −= X21/2` in FULL, `Y59: FULL→F59` | +2 | +1 | +1 | **+2** | `H1 − H2 + H3` | 740 | +| **S** | R0's transport, then `X21: FULL→F59`, ADD in F59, `X21: F59→FULL` | +3 | +1 | +2 | **+2** | `2H1` | 742 | +| **P** | one private lifetime: zero `C` at FULL, copy `X21`, `C: FULL→F59`, ADD, erase | +5 | +1 | +1 | **+1** | `H1` | 741 | +| **T48** | T's lift, carrying all 48 off-diagonal entries `−G[59,s]/2` of row 59 | +49 | +48 | +1 | **+2** | `H1 − H2 + H3` | 740 | + +All four corrections run while the head is co-hosted. Before each correction, +`Y59` is in `W6` and `X21` is in FULL, and both span `15`. Every correction +chart (FULL or `F59`) spans `15` as well. + +The published `check_native.validate()` runs unchanged on each word with the +inserted coefficients set to `0`. It passes every native edge, including the two +newly lowered `FULL ↔ F59` recipes, all 208 endpoint adapters, all 280 framed +rows and the restoration of the 72 dirty helpers. Chart legality does not depend +on the coefficient. On the real word, the same checker fails only at +`full physical boundary endpoint Y59`. Exact rational replay confirms that +`Y59` is the only row that changes: + +- in T, S and P it changes by exactly `−1/2 X21`; +- in T48, `Y59`'s final row becomes exactly `y59 + x59`, the identity row. + +## Obstruction: no zero-mass placement exists + +Consider the class Z of #3508: + +- keep the published events and ADDs in order; +- keep every endpoint frame; +- retarget or insert transports freely; +- keep `C`'s published private lifetimes. + +Insert one correction ADD between `X21` and `Y59` anywhere in this class. Its +added rank mass is never zero. + +- **Forcing chain.** Event 625 is `G9 += 2·X12` and event 884 is `G9 −= 2·X21`. + `X12`'s head is `131`. In any repair where the registers involved add no rank, + `X21`'s frame contains `131` from event 884 on. From event 1708 it is the full + chart. +- **Why that blocks the meeting.** `G[59,12] = 0`, so `131` lies outside `F59`. + `Y59` adds no rank only if every frame it passes through lies inside `F59`. + Two frames that differ cannot host one ADD. +- **Every insertion point.** A least-lower-bound frame sweep checks all 28 + insertion classes. + - Before event 885, the meeting forces `Y59` to host `15` early. #3508's + closure then fails at `Y67` or `Y96`. + - From event 885 on, the merged frame already leaves `F59`. +- **Parity.** Each step changes rank by exactly its cost. So a non-private + register's added mass is even. The strict minimum is therefore exactly + **2**, and T, S and T48 attain it. + +**Co-host discount 0.** On the published word, detouring `Y59`'s terminal +rank-3 transport through FULL costs 4 + 1 = 5, which is also +2. R0's head chart +makes T cheaper in transports than S, but not in rank mass. + +**Private route.** P relies on the inherited private-copy contract, under which +`C` is discarded while still holding a copy. Under that contract +1 is the +minimum for one added lifetime that copies `X21`: + +- if the copy is taken after event 884, it carries `131`, which `Y59` cannot + host; +- if it is taken earlier, it must be delivered before `C`'s published + lifetimes. All 11 such delivery classes are blocked. + +Whether this contract is admissible for a correction is open. + +Selected κ stays `0.001672660197076918`. Details and limits are in +[PROOF.md](PROOF.md). + +## Reproduce + +```sh +python3.12 -I -B research/p104-flag43-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag43-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag43-side-correction-bill +``` + +`verify.py` is read-only. It loads the pinned `check_native.py` by path. Its +admission checks go through `need()`, so they still fire under `-O`. +`independent.py` imports neither `verify.py` nor the native checker. +`test_package.py` corrupts temporary copies and checks that both scanners +reject all 14 corruptions. `build.py` is the producer and is not part of the +replay. + +## Credit + +Credit #3508 for R0 and the co-hosted chart, and #3456 for flag 43's +chronology. Both are cited only. Credit +`research/p104-side-correction-rank-obstruction` for the end-cut round-trip and +snapshot invoices this package compares against. Credit Nick Petalas / #2981 +for the flag matching. Credit the reviewed #1991 native channel (Chafik +Boukhalfa) for the witness, checker and compiler, and Rohan Arun / PR1972 for +the scalar channel. Prepared by Wentao Li with substantial AI assistance. + +## Open next questions + +1. Is P's private-copy discard admissible for a correction, or must `C` be + uncomputed? If it must, the strict +2 applies. +2. Does the same forcing pattern block a zero-mass entry for every + `(t, s)` pair with `G[t,s] ≠ 0`? If it does, strict per-target corrections + need 208 extra rank mass in total. +3. Can a fused correction that changes published ADD coefficients, outside + class Z (for example by retuning `D17`'s delivery at 3364), apply the entry + with no added rank? + +[TASK.json](TASK.json) gives first steps and blockers. diff --git a/research/p104-flag43-side-correction-bill/SOURCES.json b/research/p104-flag43-side-correction-bill/SOURCES.json new file mode 100644 index 0000000000..1f5011b96a --- /dev/null +++ b/research/p104-flag43-side-correction-bill/SOURCES.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "requested_base_commit": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "base_note": "#3508's R0 package (an input) merged after the requested pin, so the package is based on the newer CrocSwap main that contains it; the requested pin is an ancestor of the base.", + "upstream": "CrocSwap/integer-mult-bounds", + "files": [ + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "credit": "Reviewed #1991 native channel witness (PR1972 word)" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + "credit": "P104 fixture used by the published native checker" + }, + { + "path": "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "usage": "input", + "git_blob": "ab129678c2df4f0d39b02b88457d02c37de0d9b6", + "sha256": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + "credit": "Published native recipes (Chafik Boukhalfa, PR1991)" + }, + { + "path": "research/p104-native-channel/check_native.py", + "usage": "input", + "git_blob": "f8e54afbf146cd6f250063bcb1b9dabf0cbc42ea", + "sha256": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + "credit": "Published native checker; its validate() is run unchanged on each coefficient-0 corrected word" + }, + { + "path": "research/p104-native-channel/vendor/native_verify.py", + "usage": "input", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "credit": "Independent native interpreter used by check_native.py and by independent.py" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "credit": "Nick Petalas, PR #2981 flag matching (flag 43 identity)" + }, + { + "path": "research/p104-flag43-head-step-repair/CERTIFICATE.json", + "usage": "input", + "git_blob": "40474165349a3f3b61b7e1f0b92d3fe295deea47", + "sha256": "6ce05cee77b6641e9875a0fd07059fb2b41de7733b6e770dc673426f70f764b1", + "credit": "#3508 repair R0 splices (leave-alone prior; cited, not re-derived)" + }, + { + "path": "research/p104-flag43-head-step-repair/REPAIR-RECIPES.json", + "usage": "input", + "git_blob": "c69754769465b6ab432bb7fdff635bbc2e507f07", + "sha256": "d6dd5a7aade3206dcf7ccd9876dd143627b9d91ba8a41d7f71df26b437b988fd", + "credit": "#3508 new-edge recipes used by R0 (W6->FULL is reused by correction T)" + }, + { + "path": "research/p104-native-channel/compile.py", + "usage": "provenance", + "git_blob": "840d7608d6795d12ba174620279f88d8a6f727b4", + "sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "pin": "base_commit:research/p104-native-channel/compile.py", + "credit": "Native compiler used by build.py to lower the two new edges" + }, + { + "path": "research/p104-native-channel/vendor/clifford_exact.py", + "usage": "provenance", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "pin": "base_commit:research/p104-native-channel/vendor/clifford_exact.py", + "credit": "Exact Clifford lowering used by build.py" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c", + "pin": "base_commit:research/p104-native-channel/PROOF.md", + "credit": "Binary-frame semantics: nested transports, adds only in a common chart, owned private lifetimes, paid rank per transport" + }, + { + "path": "research/p104-side-correction-rank-obstruction/README.md", + "usage": "provenance", + "git_blob": "7266bdce51f11bf1ee646b34516b79b76e939b33", + "sha256": "5a54ed54cae2cd08517f787e4085f8a3dfeda6c03a330e9e8e3bc88c01158f7a", + "pin": "base_commit:research/p104-side-correction-rank-obstruction/README.md", + "credit": "Prior end-cut side-correction invoices (round-trip/snapshot detours, +2 rank per target); compared, not re-run" + }, + { + "path": "research/p104-present-head-flag43-audit/README.md", + "usage": "provenance", + "git_blob": "0901bd238c813a8cd523c485d1e2dacb4847cff3", + "sha256": "7b751f75d8b84a236c6e1de8bb3d0cc94924cb1e2ae53badb4eb4a941b29dea2", + "pin": "base_commit:research/p104-present-head-flag43-audit/README.md", + "credit": "#3456 flag-43 chronology (leave-alone prior; cited only)" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "pin": "base_commit:docs/research/agent-task-catalog.json", + "credit": "Priority revision 6 task catalogue at the pinned base" + } + ] +} diff --git a/research/p104-flag43-side-correction-bill/TASK.json b/research/p104-flag43-side-correction-bill/TASK.json new file mode 100644 index 0000000000..d5436550df --- /dev/null +++ b/research/p104-flag43-side-correction-bill/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "selected_kappa": "0.001672660197076918", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Price the flag-43 entry of the I - G/2 side correction (Y59 += -G[59,21]/2 X21 = -1/2 X21) at #3508's co-hosted cut, where R0 holds Y59 in the head chart [95,447,6,32,20,15] after its last update 3364 and X21 in the full chart. Build and natively validate four corrected words on R0 (target lift T, source detour S, one private-copy lifetime P, and the whole Y59 row T48), give their exact before/after bills, and prove the matching obstruction: in the class that keeps the published events and ADDs, keeps endpoint frames, may retarget or insert transports, and keeps the private register C's published lifetimes, no placement of the correction ADD at any of the 28 insertion classes costs zero added rank mass, so the strict minimum is exactly 2.", + "scope_change_reason": "#3508 (merged) answers #3456's head-step question with R0 and leaves the I - G/2 side correction at the co-hosted chart open (its open question 2). This package answers that question for the single flag-43 entry and its target row; it cites #3508/#3456 as leave-alone priors and does not re-derive R0 or the published chronology.", + "bottleneck_link": "Head co-hosting at the target update does not discount the side correction. The flag-43 entry needs one common chart for X21 and Y59, and in every zero-added-mass repair X21's forced frame contains X12's head 131 from event 884 on (and is full from 1708), while Y59 stays inside its final hyperplane, which excludes 131. The cheapest strict correction therefore pays +2 rank mass, the same as the end-cut detour on the published word. Only the inherited private-copy contract lowers it to +1. Neither is a supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after flag 43: one entry, one target row, one cut (R0's 3525 terminal transport), four validated words and the zero-mass obstruction over all insertion classes. Do not touch flags 0, 1 or 9, the other 103 target rows, global hosting, precision or kappa.", + "outcome": "completed", + "evidence": "Flag-43 entry: G[59,21]=1, so I-G/2 needs -1/2 X21 in Y59. On R0 the corrections replace R0's terminal Y59 transport at 3525. T: Y59 W6->FULL (rank 3), ADD in FULL, FULL->F59 (rank 1): +2 events, +1 ADD, +1 transport occurrence, +2 rank mass, profile H1-H2+H3 vs R0, 740 edges. S: R0's transport, then X21 FULL->F59, ADD in F59, F59->FULL: +3 events, +1 ADD, +2 transport occurrences, +2 rank mass, profile 2H1, 742 edges. P: zero C at FULL, copy X21, C FULL->F59, ADD, erase: +5 events, +1 ADD, +1 transport occurrence, +1 rank mass, profile H1, private lifetimes 8->9, 741 edges. T48: the T lift carrying all 48 off-diagonal entries of row 59: +49 events, +48 ADDs, +1 transport occurrence, +2 rank mass; Y59's final row is exactly y59 + x59. The unchanged check_native.validate() passes each coefficient-0 word (native edges incl. two newly lowered FULL<->F59 recipes, 208 adapters, 280 framed rows, 72 dirty helpers) and rejects each real word only at 'full physical boundary endpoint Y59'; exact rational replay changes only Y59's row. Obstruction: event 625 (G9 += 2 X12, head 131) and 884 (G9 -= 2 X21) force 131 into X21's frame in any monotone repair; G[59,12]=0 puts 131 outside Y59's final hyperplane; a least-lower-bound sweep blocks all 28 insertion classes (before 885 via Y59's forced head hosting: Y67/Y96; from 885 on immediately). Per-register added rank mass is even, so the strict minimum is exactly 2. The published end-cut detour also costs +2: co-host discount 0. Selected kappa unchanged.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "no_new_kappa": true, + "open_questions": [ + { + "question": "Is the +1 private-copy route P admissible as a physical correction, or must every side-correction lifetime be reversibly uncomputed?", + "why_it_matters": "P is cheaper than every strict route only because the inherited private-copy contract lets C be discarded while it holds a copy of X21. If that contract is not admissible for corrections, the strict bound of +2 per corrected target applies.", + "first_step": "Price an uncompute of C (copy back to zero in X21's chart before the erase) and compare its rank cost with S.", + "blocked_by": "The native channel package labels the private-copy semantics as inherited and makes no reversibility claim." + }, + { + "question": "Does the X12 -> G9 -> X21 forcing pattern block a zero-mass entry for every other present-head flag and for the other off-diagonal entries of row 59?", + "why_it_matters": "If every target row needs +2, the end-cut invoice of 208 extra rank mass is forced for strict per-target corrections. A row with a zero-mass entry would be the first place where co-hosting buys a discount.", + "first_step": "Run this package's sweep() for every (target, source) pair with G[t,s] != 0 on the published word and record the first forcing source head outside the target's final hyperplane.", + "blocked_by": "Flags 1 and 9 are subjects of other open/deferred work; this package treats flag 43 only." + }, + { + "question": "Can a fused correction that changes published ADD coefficients (outside the class used here) apply the entry without added rank mass, e.g. by retuning the 3364 delivery from D17?", + "why_it_matters": "The obstruction keeps every published ADD. D17 already delivers X21 into Y59 at 3364 through the private C descent; changing that delivery would change other target rows too.", + "first_step": "Compute the span of D17/Y103 rows available in the head chart W6 during 3363-3525 and test whether -1/2 X21 lies in it modulo restored helpers.", + "blocked_by": "Not attempted here." + } + ] +} diff --git a/research/p104-flag43-side-correction-bill/VERIFY.json b/research/p104-flag43-side-correction-bill/VERIFY.json new file mode 100644 index 0000000000..d286571e05 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/VERIFY.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", + "research/p104-native-channel/NATIVE-RECIPES.json.gz", + "research/p104-native-channel/check_native.py", + "research/p104-native-channel/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-flag43-head-step-repair/CERTIFICATE.json", + "research/p104-flag43-head-step-repair/REPAIR-RECIPES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Builds #3508's R0 from its pinned splices, applies corrections T, S, P and T48, runs the published check_native.validate() unchanged on each coefficient-0 word (native edges incl. two committed new-edge recipes, 208 endpoint adapters, all 280 framed rows and dirty-helper restorations), replays the real words with exact rational rows, confirms the unchanged checker rejects each real word only at Y59's endpoint, recomputes bills, profiles, the 625/884 forcing chain and the least-lower-bound sweep over all 28 insertion classes, and requires equality with CERTIFICATE.json" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "Separately written replay with XOR-closure frames and exact rational rows: common-chart ADD/copy, nested transports paying their gap, owned private lifetimes, endpoint frames; R0 target rows equal G/2; each correction changes only Y59 by exactly the stated entry (T48: row becomes y+x); even non-private added mass; direct native check of both new recipes; forward-sweep obstruction for 28 direct and 11 early private placements" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Temp-tree clean pass with byte-identical tree; 14 rejections by both scanners under -O: certificate bill/obstruction corruptions, duplicate JSON key, witness and #3508 certificate byte flips, new-recipe phase corruption, wrong coefficient, undercharged lift, wrong common chart, unrestored source and unclosed private lifetime" + } + ] +} diff --git a/research/p104-flag43-side-correction-bill/build.py b/research/p104-flag43-side-correction-bill/build.py new file mode 100644 index 0000000000..f521e48e4d --- /dev/null +++ b/research/p104-flag43-side-correction-bill/build.py @@ -0,0 +1,78 @@ +#!/usr/bin/env python3 +"""Producer for CERTIFICATE.json and CORRECTION-RECIPES.json (not part of replay). + +Generates the four corrections on #3508's R0, lowers every transport edge that +is absent from both the published recipe set and #3508's REPAIR-RECIPES.json +with the pinned native compiler, and writes the receipt computed by verify.py. +Refuses to overwrite existing outputs unless --force is given. +""" + +import argparse +import hashlib +import importlib.util +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import verify as V # noqa: E402 + +COMPILER_SHA256 = "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3" +CLIFFORD_SHA256 = "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + + +def load(name, path, digest): + raw = path.read_bytes() + V.need(hashlib.sha256(raw).hexdigest() == digest, "pinned compiler module: " + str(path)) + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--force", action="store_true") + args = ap.parse_args() + for name in ("CERTIFICATE.json", "CORRECTION-RECIPES.json"): + V.need(args.force or not (HERE / name).exists(), name + " exists") + root = V.ROOT + load("flag43_side_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag43_side_native_compile", root / V.NATIVE / "compile.py", COMPILER_SHA256) + witness, fixture, recipes, _flags, repair, repair_recipes = V.load_inputs(root) + physical = V.physical_map(recipes) + r0 = V.apply_splices(witness["program"], repair["repairs"]["R0"]["splices"]) + spec = V.corrections(r0, witness["final_frames"], V.ports(fixture)) + known = {(tuple(r["old"]), tuple(r["new"])) for r in recipes["transports"]} + known |= {(tuple(r["old"]), tuple(r["new"])) for r in repair_recipes} + new = {} + for name in spec: + prog = V.apply_splices(r0, spec[name]["splices"]) + for e in prog: + if e[0] != "transport": + continue + key = (physical(e[2]), physical(e[3])) + if key in known or key in new: + continue + actual = co.CE.canonical_frame(9, key[0]).adjoint().then(co.CE.canonical_frame(9, key[1])) + record, _ = co.CE.lower_child(actual) + V.need(record["rank"] == e[4], "native rank equals frame gap") + new[key] = {"old": list(key[0]), "new": list(key[1]), "rank": e[4], "recipe": record} + recs = [new[k] for k in sorted(new)] + payload = { + "schema_version": 1, + "scope": "Native recipes for the transport edges used by corrections T, S, P and T48 that are absent from the published p104-native-channel recipe set and from #3508's REPAIR-RECIPES.json. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay.", + "compiler_sha256": COMPILER_SHA256, + "clifford_exact_sha256": CLIFFORD_SHA256, + "recipes": recs, + } + got = V.receipt(root, {"corrections": spec}, recs) + (HERE / "CORRECTION-RECIPES.json").write_text(json.dumps(payload, indent=1, sort_keys=True) + "\n") + (HERE / "CERTIFICATE.json").write_text(json.dumps(got, indent=2, sort_keys=True) + "\n") + print("WROTE", len(recs), "new recipes") + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag43-side-correction-bill/independent.py b/research/p104-flag43-side-correction-bill/independent.py new file mode 100644 index 0000000000..33085ee321 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/independent.py @@ -0,0 +1,261 @@ +#!/usr/bin/env python3 +"""Independent replay of the flag-43 side-correction bill. + +Imports neither verify.py nor check_native.py. Frames are XOR-closed sets of +compressed labels. Every corrected word is replayed with exact rational rows +under the channel rules (common-chart ADD and copy, nested transports paying +their frame gap, owned private lifetimes, endpoint frames). The four +committed new-edge recipes are checked directly with the pinned independent +Gaussian interpreter. The forced-frame obstruction is recomputed by a forward +sweep over closure sets. Key receipts are compared with CERTIFICATE.json. +""" + +import gzip +import hashlib +import importlib.util +import itertools +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +REPAIR = "research/p104-flag43-head-step-repair" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/inputs/P104-FIXTURE.json": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + f"{REPAIR}/CERTIFICATE.json": "6ce05cee77b6641e9875a0fd07059fb2b41de7733b6e770dc673426f70f764b1", + f"{REPAIR}/REPAIR-RECIPES.json": "d6dd5a7aade3206dcf7ccd9876dd143627b9d91ba8a41d7f71df26b437b988fd", +} +MARKER = ( + "PASS_P104_FLAG43_SIDE_CORRECTION_BILL_INDEPENDENT entry=(59,21) zero_mass_placements=0/28 " + "early_private_deliveries_obstructed=11/11 T=+2rank S=+2rank P=+1rank T48=+2rank " + "rows_changed=Y59_only row59=identity new_recipes=2 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def strict(pairs): + out = {} + for k, v in pairs: + need(k not in out, "duplicate JSON key: " + str(k)) + out[k] = v + return out + + +def read(root, rel, gz=False): + raw = (root / rel).read_bytes() + if rel in PINS: + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pin: " + rel) + return json.loads(gzip.decompress(raw) if gz else raw, object_pairs_hook=strict) + + +def closure(vectors): + s = {0} + for v in vectors: + if v not in s: + s |= {x ^ v for x in s} + return frozenset(s) + + +def dim(s): + return len(s).bit_length() - 1 + + +def splice(program, rows): + out = list(program) + for row in sorted(rows, key=lambda r: -r["published_range"][0]): + a, b = row["published_range"] + need(out[a:b] == row["published"], "splice anchor") + out[a:b] = row["events"] + return out + + +def gram_rows(fixture): + lines = set() + for i, j in itertools.combinations(range(8), 2): + for s in (-1, 1): + v = [0] * 8 + v[i], v[j] = 2, 2 * s + lines.add(tuple(v)) + for s in itertools.product((-1, 1), repeat=7): + if s.count(-1) % 2 == 0: + lines.add((1,) + s) + gone = {tuple(r) for r in fixture["F0"] + fixture["C"]} + ps = [r for r in sorted(lines) if r not in gone] + return lambda t, s: sum(x * y for x, y in zip(ps[t], ps[s])) // 4 + + +def replay(witness, program): + frames = {n: closure(f) for n, f in witness["initial_frames"].items()} + rows = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + paid, adds, private = {}, 0, {"zero": 0, "copy": 0, "erase": 0} + mass = {} + for e in program: + op = e[0] + if op == "transport": + _, r, a, b, k = e + fa, fb = closure(a), closure(b) + need(frames[r] == fa, "transport starts at live frame") + need(fa <= fb or fb <= fa, "nested transport") + need(abs(dim(fb) - dim(fa)) == k and k > 0, "rank equals frame gap") + frames[r] = fb + paid[k] = paid.get(k, 0) + 1 + mass[r] = mass.get(r, 0) + k + elif op == "zero": + need(e[1] == "C" and "C" not in frames, "owned private zero") + frames["C"], rows["C"] = closure(e[2]), {} + private["zero"] += 1 + elif op == "erase": + need(frames.get("C") == closure(e[2]), "owned private erase") + frames.pop("C") + rows.pop("C") + private["erase"] += 1 + elif op == "copy": + need(not rows["C"] and frames["C"] == frames[e[2]] == closure(e[3]), "common-chart copy") + rows["C"] = dict(rows[e[2]]) + private["copy"] += 1 + else: + need(op == "add", "known opcode") + _, dst, src, a, f = e + need(dst != src and frames[dst] == frames[src] == closure(f), "common-chart add") + for k, v in rows[src].items(): + z = rows[dst].get(k, Fraction(0)) + Fraction(a) * v + if z: + rows[dst][k] = z + else: + rows[dst].pop(k, None) + adds += 1 + need("C" not in frames, "private storage closed") + for n, f in witness["final_frames"].items(): + need(frames[n] == closure(f), "endpoint frame " + n) + return rows, {"events": len(program), "adds": adds, "transports": sum(paid.values()), + "rank_mass": sum(k * v for k, v in paid.items()), "profile": paid, + "private": private, "mass": mass} + + +def lower_sweep(witness, program, inject=None): + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + fin = {n: closure(f) for n, f in witness["final_frames"].items()} + for i in range(len(program) + 1): + if inject is not None and i == inject[0]: + regs = inject[1] + m = frozenset().union(*[cur[r] for r in regs]) if len(regs) > 1 else cur[regs[0]] + m = closure(set(m) | set(inject[2])) + for r in regs: + cur[r] = m + if not m <= fin[r]: + return i, r + if i == len(program): + return None + e = program[i] + if e[0] == "add" and "C" not in (e[1], e[2]): + m = closure(set(cur[e[1]]) | set(cur[e[2]])) + cur[e[1]] = cur[e[2]] = m + for r in (e[1], e[2]): + if not m <= fin[r]: + return i, r + + +def main(root=ROOT): + witness = read(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json") + fixture = read(root, f"{NATIVE}/inputs/P104-FIXTURE.json")["section4_explicit_P104"] + recipes = read(root, f"{NATIVE}/NATIVE-RECIPES.json.gz", gz=True) + flags = read(root, "research/p104-joint-unit-flags/CERTIFICATE.json") + repair = read(root, f"{REPAIR}/CERTIFICATE.json") + cert = json.loads((HERE / "CERTIFICATE.json").read_bytes(), object_pairs_hook=strict) + new = json.loads((HERE / "CORRECTION-RECIPES.json").read_bytes(), object_pairs_hook=strict)["recipes"] + raw = (root / NATIVE / "vendor/native_verify.py").read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[f"{NATIVE}/vendor/native_verify.py"], "interpreter pin") + spec = importlib.util.spec_from_file_location("flag43_side_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + flag = flags["helpers"][43] + need((flag["source"], flag["target"], flag["basis"][0]) == (21, 59, 15), "flag 43") + G = gram_rows(fixture) + need(G(59, 21) == 1 and G(59, 59) == 2 and G(59, 12) == 0, "Gram entries") + program = witness["program"] + r0 = splice(program, repair["repairs"]["R0"]["splices"]) + rows0, b0 = replay(witness, r0) + need((b0["events"], b0["adds"], b0["transports"], b0["rank_mass"]) == (4058, 2624, 1410, 2368), "R0 bill") + for t in range(104): + y = rows0["Y%d" % t] + want = {"Y%d" % t: Fraction(1)} + want.update({"X%d" % s: Fraction(G(t, s), 2) for s in range(104) if G(t, s)}) + need(y == want, "R0 target row G/2") + + iso = recipes["label_isometry"] + dual, orth = iso["compressed_dual_gram"], iso["orthonormal_basis_compressed"] + + def to_phys(x): + dx = sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(dual)) + return sum((((v & dx).bit_count()) & 1) << j for j, v in enumerate(orth)) + + for rec in new: + need(rec["rank"] == abs(len(rec["old"]) - len(rec["new"])) == rec["recipe"]["rank"], "recipe rank") + N.equal(N.recipe(rec["recipe"]), N.adjoint(N.frame(tuple(rec["old"]), 9)) + N.frame(tuple(rec["new"]), 9), "new native edge") + f59 = witness["final_frames"]["Y59"] + full = [1 << k for k in range(9)] + phys = lambda f: closure(to_phys(x) for x in f) + keys = {(closure(r["old"]), closure(r["new"])) for r in new} + need(keys == {(phys(full), phys(f59)), (phys(f59), phys(full))}, "new edges are FULL<->F59") + + want_add = {"T": (2, 1, 1, 2), "S": (3, 1, 2, 2), "P": (5, 1, 1, 1), "T48": (49, 48, 1, 2)} + for name, (ev, ad, tr, rm) in want_add.items(): + prog = splice(r0, cert["corrections"][name]["splices"]) + rows, b = replay(witness, prog) + got = (b["events"] - 4058, b["adds"] - 2624, b["transports"] - 1410, b["rank_mass"] - 2368) + need(got == (ev, ad, tr, rm), name + " added bill") + changed = sorted(k for k in rows0 if rows[k] != rows0[k]) + need(changed == ["Y59"], name + " changes only Y59") + if name == "T48": + need(rows["Y59"] == {"Y59": Fraction(1), "X59": Fraction(1)}, "row 59 identity") + else: + need("X21" not in rows["Y59"], name + " entry applied") + diff = {k: rows["Y59"].get(k, 0) - rows0["Y59"].get(k, 0) for k in set(rows["Y59"]) | set(rows0["Y59"])} + need({k: v for k, v in diff.items() if v} == {"X21": Fraction(-1, 2)}, name + " exact entry") + c = cert["bill"][name] + need([c["added_vs_R0"][k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == [ev, ad, tr, rm], name + " certificate bill") + dm = {r: b["mass"].get(r, 0) - b0["mass"].get(r, 0) for r in set(b["mass"]) | set(b0["mass"])} + dm = {r: v for r, v in dm.items() if v} + need(all(v % 2 == 0 for r, v in dm.items() if r != "C"), name + " even non-private mass") + need(c["added_rank_by_register"] == dm, name + " per-register mass") + need(cert["bill"]["P"]["private_events"] == {"zero": 9, "copy": 9, "erase": 9}, "P lifetime") + + need(lower_sweep(witness, program) is None and lower_sweep(witness, r0) is None, "base feasible") + ev = sorted({i for i, e in enumerate(program) if e[0] in ("add", "copy") and {"X21", "Y59"} & {e[1], e[2]}}) + cuts = sorted({0} | {i + 1 for i in ev}) + need(len(cuts) == 28, "28 placement classes") + blocked = [lower_sweep(witness, program, (u, ("X21", "Y59"), ())) for u in cuts] + need(all(blocked), "no zero-mass direct placement") + need([[u, list(x)] for u, x in zip(cuts, blocked)] == cert["obstruction"]["direct_first_obstruction"], "obstruction table") + yev = sorted({i for i, e in enumerate(program) if e[0] in ("add", "copy") and "Y59" in (e[1], e[2])}) + early = [u for u in sorted({0} | {i + 1 for i in yev}) if u < 2461] + pblocked = [lower_sweep(witness, program, (u, ("Y59",), (15,))) for u in early] + need(len(early) == 11 and all(pblocked), "early private deliveries obstructed") + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + for i, e in enumerate(program[:885]): + if e[0] == "add" and "C" not in (e[1], e[2]): + cur[e[1]] = cur[e[2]] = closure(set(cur[e[1]]) | set(cur[e[2]])) + need(131 in cur["X21"] and 15 in cur["X21"] and 131 not in closure(f59) and 15 in closure(f59), "131 forced into X21 by 884") + need(witness["initial_frames"]["X12"] == [131], "X12 head") + ob = cert["obstruction"] + need(ob["partner_feeder"][0] == 625 and ob["source_first_read"][0] == 884, "certificate forcing events") + need(ob["feeder_source_head"] == witness["initial_frames"]["X12"] and ob["feeder_source_gram_with_target"] == G(59, 12), "certificate feeder") + need(ob["source_forced_full_from"] == 1708 and 9 not in [r for i, _p, r in ob["source_forced_rank_at_events"] if i < 1708], "certificate full-from") + need(cert["selected_kappa"] == "0.001672660197076918" and cert["no_new_kappa"] is True, "kappa") + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT) diff --git a/research/p104-flag43-side-correction-bill/test_package.py b/research/p104-flag43-side-correction-bill/test_package.py new file mode 100644 index 0000000000..7b3bf1fc78 --- /dev/null +++ b/research/p104-flag43-side-correction-bill/test_package.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Behavioural tests: corruption, negative controls and read-only replay. + +Each case copies the package and its pinned inputs into a temporary tree, +mutates one thing and runs both scanners there under python -O. The scanners +must reject every mutation; the clean tree must pass and stay byte-identical. +""" + +import concurrent.futures +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG = HERE.relative_to(ROOT).as_posix() +NATIVE = "research/p104-native-channel" +REPAIR = "research/p104-flag43-head-step-repair" +COPY = [ + f"{NATIVE}/inputs/LOWRANK-WITNESS.json", + f"{NATIVE}/inputs/P104-FIXTURE.json", + f"{NATIVE}/NATIVE-RECIPES.json.gz", + f"{NATIVE}/check_native.py", + f"{NATIVE}/vendor/native_verify.py", + "research/p104-joint-unit-flags/CERTIFICATE.json", + f"{REPAIR}/CERTIFICATE.json", + f"{REPAIR}/REPAIR-RECIPES.json", +] +SCANNERS = ("verify.py", "independent.py") + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def tree(base): + for rel in COPY: + (base / rel).parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / rel, base / rel) + shutil.copytree(HERE, base / PKG, ignore=shutil.ignore_patterns("__pycache__")) + return base + + +def run(base, scanner): + p = subprocess.run([sys.executable, "-I", "-O", "-Werror", "-B", str(base / PKG / scanner), str(base)], + capture_output=True, text=True, timeout=600) + return p.returncode, p.stdout + p.stderr + + +def digest(base): + return {p.relative_to(base).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(base.rglob("*")) if p.is_file()} + + +def edit_json(path, fn): + data = json.loads(path.read_text()) + fn(data) + path.write_text(json.dumps(data, indent=2, sort_keys=True) + "\n") + + +def cert_edit(fn): + return lambda base: edit_json(base / PKG / "CERTIFICATE.json", fn) + + +def splice_events(name): + return lambda d: d["corrections"][name]["splices"][0]["events"] + + +def set_event(name, k, field, value): + def fn(d): + splice_events(name)(d)[k][field] = value + return cert_edit(fn) + + +def drop_event(name, k): + def fn(d): + del splice_events(name)(d)[k] + return cert_edit(fn) + + +def dup_key(base): + p = base / PKG / "CERTIFICATE.json" + text = p.read_text() + p.write_text(text.replace('"schema_version": 1', '"schema_version": 1,\n "schema_version": 1', 1)) + + +def flip(rel, offset): + def fn(base): + p = base / rel + raw = bytearray(p.read_bytes()) + raw[offset] ^= 1 + p.write_bytes(bytes(raw)) + return fn + + +def recipe_phase(base): + p = base / PKG / "CORRECTION-RECIPES.json" + data = json.loads(p.read_text()) + left = data["recipes"][0]["recipe"]["left"] + left["phase"] = (left["phase"] + 1) % 4 + p.write_text(json.dumps(data, indent=1, sort_keys=True) + "\n") + + +CASES = { + "bill_T_rank_mass": cert_edit(lambda d: d["bill"]["T"]["added_vs_R0"].update(rank_mass=0)), + "bill_P_profile": cert_edit(lambda d: d["bill"]["P"]["added_rank_by_register"].update(C=0)), + "feeder_head": cert_edit(lambda d: d["obstruction"].update(feeder_source_head=[15])), + "full_from": cert_edit(lambda d: d["obstruction"].update(source_forced_full_from=1517)), + "obstruction_row": cert_edit(lambda d: d["obstruction"]["direct_first_obstruction"].__setitem__(23, [3365, None])), + "duplicate_key": dup_key, + "witness_byte": flip(f"{NATIVE}/inputs/LOWRANK-WITNESS.json", 4096), + "repair_certificate_byte": flip(f"{REPAIR}/CERTIFICATE.json", 2048), + "recipe_phase": recipe_phase, + "T_wrong_coefficient": set_event("T", 1, 3, "-1/4"), + "T_undercharged_lift": set_event("T", 0, 4, 2), + "S_wrong_chart": set_event("S", 2, 4, [1, 2, 4, 8, 16, 32, 64, 128, 256]), + "S_source_not_restored": drop_event("S", 3), + "P_private_not_erased": drop_event("P", 5), +} + + +def case(name): + with tempfile.TemporaryDirectory() as tmp: + base = tree(Path(tmp)) + CASES[name](base) + results = [run(base, s) for s in SCANNERS] + return name, [code != 0 for code, _ in results] + + +def main(): + with tempfile.TemporaryDirectory() as tmp: + base = tree(Path(tmp)) + before = digest(base) + for s in SCANNERS: + code, out = run(base, s) + need(code == 0 and "PASS_P104_FLAG43_SIDE_CORRECTION_BILL" in out, "clean pass: " + s + "\n" + out) + need(digest(base) == before, "scanners are read-only") + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool: + results = dict(pool.map(case, CASES)) + for name, rejected in sorted(results.items()): + need(all(rejected), "mutation accepted: %s %s" % (name, rejected)) + print("PASS_P104_FLAG43_SIDE_CORRECTION_BILL_TESTS cases=%d clean_read_only=1 scanners=%d" % (len(CASES), len(SCANNERS))) + + +if __name__ == "__main__": + main() diff --git a/research/p104-flag43-side-correction-bill/verify.py b/research/p104-flag43-side-correction-bill/verify.py new file mode 100644 index 0000000000..ba575bfcbf --- /dev/null +++ b/research/p104-flag43-side-correction-bill/verify.py @@ -0,0 +1,551 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-43 side-correction bill at R0's co-hosted cut. + +Builds #3508's repair R0 from its committed splices, then applies four +corrections that add the (59, 21) entry of I - G/2 (and, for T48, the whole +Y59 row) after R0's last Y59 update. For each corrected word it runs the +published check_native.validate() unchanged on the coefficient-0 copy (chart +legality, native edges, endpoint adapters and all 280 framed rows do not +depend on the inserted coefficient), replays the real word with exact rational +rows, and confirms that validate() rejects the real word only at Y59's +endpoint. It then recomputes the bills, the forcing chain and the +least-lower-bound frame sweep that rules out a zero-added-mass placement, and +compares the receipt with CERTIFICATE.json. Admission uses need() and stays +active under python -O. Nothing is written. +""" + +import copy +import gzip +import hashlib +import importlib.util +import itertools +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +NATIVE = "research/p104-native-channel" +REPAIR = "research/p104-flag43-head-step-repair" +PINS = { + f"{NATIVE}/inputs/LOWRANK-WITNESS.json": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + f"{NATIVE}/inputs/P104-FIXTURE.json": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", + f"{NATIVE}/NATIVE-RECIPES.json.gz": "a1c4d83d3d5fe1338e99b59272e8cf5d43244c33888597da340b2aa7fef5b3e8", + f"{NATIVE}/check_native.py": "e67b874a061a4a28007b9a0fabaf30c8db4a587b1e1c7dd9396c77ff1e3a9fe6", + f"{NATIVE}/vendor/native_verify.py": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "research/p104-joint-unit-flags/CERTIFICATE.json": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + f"{REPAIR}/CERTIFICATE.json": "6ce05cee77b6641e9875a0fd07059fb2b41de7733b6e770dc673426f70f764b1", + f"{REPAIR}/REPAIR-RECIPES.json": "d6dd5a7aade3206dcf7ccd9876dd143627b9d91ba8a41d7f71df26b437b988fd", +} +FLAG_INDEX = 43 +CUT = 3525 +SELECTED_KAPPA = "0.001672660197076918" +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] +W6 = [95, 447, 6, 32, 20, 15] +PRIVATE_SPAN = (2461, 2524) +MARKER = ( + "PASS_P104_FLAG43_SIDE_CORRECTION_BILL flag=43 entry=(59,21) coefficient=-1/2 " + "zero_mass_placements=0/28 forcing=625:X12(131)->884:G9->X21 strict_min_added_rank=2 " + "T=+1transport+1add+2rank(H1-H2+H3) S=+2transport+1add+2rank(2H1) " + "P=+1transport+1add+1rank(H1)+1private_lifetime T48=+1transport+48add+2rank row59=identity " + "cohost_discount=0 native_validate=4/4 no_new_kappa" +) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pairs_unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "duplicate JSON key: " + str(key)) + out[key] = value + return out + + +def loads(raw): + return json.loads(raw, object_pairs_hook=pairs_unique) + + +def pinned_bytes(root, rel): + raw = (root / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PINS[rel], "pinned input changed: " + rel) + return raw + + +def load_checker(root): + pinned_bytes(root, f"{NATIVE}/check_native.py") + pinned_bytes(root, f"{NATIVE}/vendor/native_verify.py") + name = "flag43_side_check_native" + spec = importlib.util.spec_from_file_location(name, root / NATIVE / "check_native.py") + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def load_inputs(root): + witness = loads(pinned_bytes(root, f"{NATIVE}/inputs/LOWRANK-WITNESS.json")) + fixture = loads(pinned_bytes(root, f"{NATIVE}/inputs/P104-FIXTURE.json"))["section4_explicit_P104"] + recipes = loads(gzip.decompress(pinned_bytes(root, f"{NATIVE}/NATIVE-RECIPES.json.gz"))) + flags = loads(pinned_bytes(root, "research/p104-joint-unit-flags/CERTIFICATE.json")) + repair = loads(pinned_bytes(root, f"{REPAIR}/CERTIFICATE.json")) + repair_recipes = loads(pinned_bytes(root, f"{REPAIR}/REPAIR-RECIPES.json"))["recipes"] + return witness, fixture, recipes, flags, repair, repair_recipes + + +# --- GF(2) frames ----------------------------------------------------------- + +def canon(values): + piv = {} + for x in values: + while x: + j = x.bit_length() - 1 + if j in piv: + x ^= piv[j] + else: + piv[j] = x + break + for j in sorted(piv): + for k in piv: + if k > j and piv[k] >> j & 1: + piv[k] ^= piv[j] + return tuple(piv[j] for j in sorted(piv, reverse=True)) + + +def join(a, b): + return canon(tuple(a) + tuple(b)) + + +def inside(a, b): + return len(join(a, b)) == len(canon(b)) + + +def physical_map(recipes): + iso = recipes["label_isometry"] + dual = iso["compressed_dual_gram"] + orth = iso["orthonormal_basis_compressed"] + mv = lambda rows, x: sum((((row & x).bit_count()) & 1) << i for i, row in enumerate(rows)) + dot = lambda a, b: (a & mv(dual, b)).bit_count() & 1 + convert = lambda x: sum(dot(x, v) << j for j, v in enumerate(orth)) + return lambda frame: canon(convert(x) for x in frame) + + +# --- roots ------------------------------------------------------------------- + +def ports(fixture): + lines = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + v = [0] * 8 + v[i], v[j] = 2, 2 * sign + lines.add(tuple(v)) + for signs in itertools.product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + lines.add((1, *signs)) + removed = {tuple(r) for r in fixture["F0"] + fixture["C"]} + out = [r for r in sorted(lines) if r not in removed] + need(len(out) == 104, "P104 ports") + return out + + +def gram(ps, t, s): + return sum(x * y for x, y in zip(ps[t], ps[s])) // 4 + + +# --- schedules --------------------------------------------------------------- + +def apply_splices(program, splices): + out = list(program) + last = len(program) + 1 + for row in sorted(splices, key=lambda r: -r["published_range"][0]): + start, stop = row["published_range"] + need(0 <= start < stop <= len(program) and stop <= last, "ordered disjoint splices") + need(len(row["published"]) == stop - start, "splice covers its range") + for k, old in enumerate(row["published"]): + need(program[start + k] == old, "splice binds event %d" % (start + k)) + out[start:stop] = copy.deepcopy(row["events"]) + last = start + return out + + +def corrections(r0, final, ps): + f59 = final["Y59"] + cut = r0[CUT] + need(cut == ["transport", "Y59", W6, f59, 2], "R0 terminal Y59 transport at the cut") + row = [["add", "Y59", "X%d" % s, str(Fraction(-gram(ps, 59, s), 2)), FULL] + for s in range(104) if s != 59 and gram(ps, 59, s)] + + def one(events): + return [{"published_range": [CUT, CUT + 1], "published": [cut], "events": events}] + return { + "T": { + "route": "target lift at the co-hosted cut: Y59 leaves the head chart W6 for the full chart, takes the entry from X21 there, then descends to its final hyperplane", + "splices": one([ + ["transport", "Y59", W6, FULL, 3], + ["add", "Y59", "X21", "-1/2", FULL], + ["transport", "Y59", FULL, f59, 1], + ]), + }, + "S": { + "route": "source detour: Y59 takes R0's terminal transport, X21 descends to Y59's final hyperplane for one ADD and returns to the full chart before its next read at 3705", + "splices": one([ + cut, + ["transport", "X21", FULL, f59, 1], + ["add", "Y59", "X21", "-1/2", f59], + ["transport", "X21", f59, FULL, 1], + ]), + }, + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X21 into C at the full chart, descend C to Y59's final hyperplane, deliver, discard", + "splices": one([ + cut, + ["zero", "C", FULL], + ["copy", "C", "X21", FULL], + ["transport", "C", FULL, f59, 1], + ["add", "Y59", "C", "-1/2", f59], + ["erase", "C", f59], + ]), + }, + "T48": { + "route": "whole Y59 row of I - G/2 on the same lift: every off-diagonal source entry -G[59,s]/2 is added while Y59 sits in the full chart", + "splices": one([["transport", "Y59", W6, FULL, 3]] + row + [["transport", "Y59", FULL, f59, 1]]), + }, + } + + +def zeroed(program, base_len, splices): + out = copy.deepcopy(program) + start = splices[0]["published_range"][0] + stop = start + len(out) - base_len + 1 + for i in range(start, stop): + if out[i][0] == "add": + out[i][3] = "0" + return out + + +def assemble(recipes, program, extra, physical): + pub = {(tuple(r["old"]), tuple(r["new"])): r for r in recipes["transports"]} + more = {} + for r in extra: + key = (tuple(r["old"]), tuple(r["new"])) + need(key not in more and key not in pub, "extra recipes are unique new edges") + more[key] = r + edges = {} + for i, e in enumerate(program): + if e[0] == "transport": + edges.setdefault((physical(e[2]), physical(e[3])), []).append(i) + used = set() + out = [] + for key in sorted(edges): + if key in pub: + rec = dict(pub[key]) + else: + need(key in more, "missing native recipe for edge") + rec = dict(more[key]) + used.add(key) + rec["events"] = edges[key] + out.append(rec) + profile = {} + for rec in out: + profile[rec["rank"]] = profile.get(rec["rank"], 0) + len(rec["events"]) + c = dict(recipes) + c["transports"] = out + c["paid_profile"] = {str(k): v for k, v in sorted(profile.items())} + return c, used + + +def bill(result, program): + profile = {str(k): v for k, v in sorted(result["paid_profile"].items())} + return { + "events": len(program), + "scalar_adds": result["scalar_events"]["add"], + "private_events": {k: result["scalar_events"].get(k, 0) for k in ("zero", "copy", "erase")}, + "transport_occurrences": sum(profile.values()), + "rank_mass": result["rank_mass"], + "paid_profile": profile, + "distinct_native_edges": result["transports"], + "endpoint_adapters": result["intrinsic_endpoint_adapters"], + } + + +def delta(a, b): + out = {} + for k in sorted({int(x) for x in a["paid_profile"]} | {int(x) for x in b["paid_profile"]}): + d = b["paid_profile"].get(str(k), 0) - a["paid_profile"].get(str(k), 0) + if d: + out[str(k)] = d + return out + + +def rows(witness, program): + state = {n: {n: Fraction(1)} for n in witness["initial_frames"]} + for e in program: + if e[0] == "zero": + state[e[1]] = {} + elif e[0] == "erase": + state.pop(e[1]) + elif e[0] == "copy": + state[e[1]] = dict(state[e[2]]) + elif e[0] == "add": + _, dst, src, a, _f = e + for name, v in list(state[src].items()): + z = state[dst].get(name, Fraction(0)) + Fraction(a) * v + if z: + state[dst][name] = z + else: + state[dst].pop(name, None) + return state + + +def register_mass(program): + out = {} + for e in program: + if e[0] == "transport": + out[e[1]] = out.get(e[1], 0) + e[4] + return out + + +# --- least monotone lower bounds --------------------------------------------- + +def sweep(witness, program, inject=None): + """Least frames of a zero-added-mass repair; C is left unconstrained. + + inject = (u, a, b): registers a and b share one frame just before event u. + inject = (u, None, b, frame): register b contains `frame` from event u on. + Returns the first event/register whose forced frame leaves its final frame. + """ + init = {k: canon(v) for k, v in witness["initial_frames"].items()} + final = {k: canon(v) for k, v in witness["final_frames"].items()} + cur = dict(init) + for i in range(len(program) + 1): + if inject and i == inject[0]: + if inject[1] is None: + cur[inject[2]] = join(cur[inject[2]], inject[3]) + touched = (inject[2],) + else: + m = join(cur[inject[1]], cur[inject[2]]) + cur[inject[1]] = cur[inject[2]] = m + touched = inject[1:3] + for r in touched: + if not inside(cur[r], final[r]): + return [i, r] + if i == len(program): + break + e = program[i] + if e[0] == "add" and "C" not in e[1:3]: + m = join(cur[e[1]], cur[e[2]]) + cur[e[1]] = cur[e[2]] = m + for r in e[1:3]: + if not inside(m, final[r]): + return [i, r] + return None + + +def forced_frames(witness, program, reg): + init = {k: canon(v) for k, v in witness["initial_frames"].items()} + cur = dict(init) + out = [] + for i, e in enumerate(program): + if e[0] == "add" and "C" not in e[1:3]: + m = join(cur[e[1]], cur[e[2]]) + cur[e[1]] = cur[e[2]] = m + if reg in e[1:3]: + out.append([i, e[1] if e[2] == reg else e[2], len(m)]) + return out + + +def cut_classes(program, regs): + ev = [i for i, e in enumerate(program) if e[0] in ("add", "copy") and set(regs) & {e[1], e[2]}] + return sorted({0} | {i + 1 for i in ev}) + + +# --- receipt ----------------------------------------------------------------- + +def receipt(root, cert, new_recipes): + ck = load_checker(root) + witness, fixture, recipes, flags, repair, repair_recipes = load_inputs(root) + helper = flags["helpers"][FLAG_INDEX] + head = helper["basis"][0] + need(("X%d" % helper["source"], "Y%d" % helper["target"], head) == ("X21", "Y59", 15), "flag 43 identity") + need(repair["claim_id"] == "p104-flag43-head-step-repair", "R0 source") + ps = ports(fixture) + physical = physical_map(recipes) + program = witness["program"] + final = witness["final_frames"] + r0 = apply_splices(program, repair["repairs"]["R0"]["splices"]) + need(len(r0) == len(program), "R0 keeps the event count") + w0 = dict(witness) + w0["program"] = r0 + c0, _ = assemble(recipes, r0, repair_recipes, physical) + base = bill(ck.validate(c0, w0, fixture, False), r0) + pub = bill(ck.validate(recipes, witness, fixture, False), program) + spec = corrections(r0, final, ps) + need(cert.get("corrections") == spec, "committed corrections equal the generated ones") + expected = rows(witness, r0) + need(all(not (e[0] in ("add", "copy") and e[2] == "Y59") for e in r0), "Y59 is never read") + extra = list(repair_recipes) + list(new_recipes) + new_keys = {(tuple(r["old"]), tuple(r["new"])) for r in new_recipes} + need(len(new_keys) == len(new_recipes), "unique correction recipes") + used_all = set() + out = {} + for name in ("T", "S", "P", "T48"): + prog = apply_splices(r0, spec[name]["splices"]) + zero = zeroed(prog, len(r0), spec[name]["splices"]) + wz = dict(witness) + wz["program"] = zero + cz, used = assemble(recipes, zero, extra, physical) + used_all |= used & new_keys + res = ck.validate(cz, wz, fixture, False) + b = bill(res, prog) + wr = dict(witness) + wr["program"] = prog + try: + ck.validate(cz, wr, fixture, False) + except ValueError as exc: + rejection = str(exc) + else: + rejection = None + got = rows(witness, prog) + changed = sorted(k for k in expected if got.get(k) != expected[k]) + y = got["Y59"] + mass0, mass1 = register_mass(r0), register_mass(prog) + added_mass = {r: mass1.get(r, 0) - mass0.get(r, 0) for r in sorted(set(mass0) | set(mass1)) + if mass1.get(r, 0) != mass0.get(r, 0)} + start = CUT + stop = CUT + len(prog) - len(r0) + 1 + frames_before = {} + hist = {} + for i, e in enumerate(prog[:start]): + if e[0] == "transport": + hist[e[1]] = e[3] + for reg in ("Y59", "X21"): + frames_before[reg] = list(canon(hist.get(reg, witness["initial_frames"][reg]))) + corr_adds = [e for e in prog[start:stop] if e[0] == "add"] + out[name] = dict(b) + out[name].update({ + "native_validate_coefficient_zero": "PASS", + "real_word_rejected_by_unchanged_checker_at": rejection, + "changed_final_rows": changed, + "Y59_final_X21": str(y.get("X21", Fraction(0))), + "Y59_final_row_is_identity": y == {"Y59": Fraction(1), "X59": Fraction(1)}, + "correction_adds": len(corr_adds), + "correction_charts": sorted({len(canon(e[4])) for e in corr_adds}), + "head_in_correction_charts": all(inside([head], e[4]) for e in corr_adds), + "added_rank_by_register": added_mass, + "head_in_target_frame_before_correction": inside([head], frames_before["Y59"]), + "head_in_source_frame_before_correction": inside([head], frames_before["X21"]), + "target_frame_before_correction_rank": len(frames_before["Y59"]), + "added_vs_R0": {k: b[k] - base[k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")}, + "profile_delta_vs_R0": delta(base, b), + "profile_delta_vs_published": delta(pub, b), + }) + need(len(used_all) == len(new_recipes), "every committed correction recipe is used") + + # Forcing chain and the zero-added-mass obstruction. + init = witness["initial_frames"] + f59 = canon(final["Y59"]) + first_read = [i for i, e in enumerate(program) if e[0] == "add" and e[2] == "X21"][0] + partner = program[first_read][1] + feeders = [i for i, e in enumerate(program[:first_read]) + if e[0] == "add" and e[1] == partner and e[2].startswith("X")] + need(len(feeders) == 1, "one source feeds the partner before the first read") + feeder = feeders[0] + src12 = program[feeder][2] + head12 = canon(init[src12]) + lb = forced_frames(witness, program, "X21") + full_from = [i for i, _p, r in lb if r == 9][0] + cuts = cut_classes(program, ("X21", "Y59")) + direct = [[u, sweep(witness, program, (u, "X21", "Y59"))] for u in cuts] + need(all(x[1] for x in direct), "every direct placement is obstructed") + early = [u for u in cut_classes(program, ("Y59",)) if u < PRIVATE_SPAN[0]] + private = [[u, sweep(witness, program, (u, None, "Y59", canon([head])))] for u in early] + need(all(x[1] for x in private), "every early private delivery is obstructed") + need(sweep(witness, program) is None and sweep(witness, r0) is None, "published and R0 feasible") + nz = [s for s in range(104) if s != 59 and gram(ps, 59, s)] + pub_cut = program[CUT] + obstruction = { + "entry": {"target": "Y59", "source": "X21", "gram": gram(ps, 59, 21), "correction_coefficient": str(Fraction(-gram(ps, 59, 21), 2)), "diagonal_gram": gram(ps, 59, 59)}, + "row_59_offdiagonal_nonzero": len(nz), + "source_first_read": [first_read, program[first_read][:4]], + "partner_feeder": [feeder, program[feeder][:4]], + "feeder_source_head": list(head12), + "feeder_source_gram_with_target": gram(ps, 59, int(src12[1:])), + "feeder_head_in_target_final": inside(head12, f59), + "flag_head_in_target_final": inside([head], f59), + "source_forced_rank_at_events": lb, + "source_forced_full_from": full_from, + "direct_cut_classes": len(cuts), + "direct_first_obstruction": direct, + "private_early_delivery_cuts": len(private), + "private_early_first_obstruction": private, + "published_private_lifetimes": list(PRIVATE_SPAN), + "non_private_registers_at_rank_floor": sum( + 1 for r in init if register_mass(program).get(r, 0) == len(canon(final[r])) - len(canon(init[r]))), + } + end_cut_detour = { + "published_terminal_transport": [CUT, pub_cut[4]], + "published_detour_via_full_rank": (9 - len(canon(pub_cut[2]))) + (9 - len(f59)), + "published_detour_added_rank": (9 - len(canon(pub_cut[2]))) + (9 - len(f59)) - pub_cut[4], + "R0_detour_added_rank": out["T"]["added_vs_R0"]["rank_mass"], + } + return { + "schema_version": 1, + "claim_id": "p104-flag43-side-correction-bill", + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "requested_pin": "6f100d4bb5083f8c35d96fd95a539811c62f245c", + "flag_index": FLAG_INDEX, + "basis_head": head, + "cut_event": CUT, + "corrections": spec, + "bill": {"published": pub, "R0": base, **out}, + "obstruction": obstruction, + "end_cut_detour": end_cut_detour, + "selected_kappa": SELECTED_KAPPA, + "no_new_kappa": True, + } + + +def admit(root, cert, new_recipes): + got = json.loads(json.dumps(receipt(root, cert, new_recipes))) + need(got == cert, "receipt differs from committed certificate") + b, ob = cert["bill"], cert["obstruction"] + need(ob["entry"] == {"target": "Y59", "source": "X21", "gram": 1, "correction_coefficient": "-1/2", "diagonal_gram": 2}, "entry") + need(ob["source_first_read"][0] == 884 and ob["partner_feeder"][0] == 625, "forcing chain events") + need(ob["feeder_source_head"] == [131] and ob["feeder_source_gram_with_target"] == 0, "X12 head orthogonal to r59") + need(not ob["feeder_head_in_target_final"] and ob["flag_head_in_target_final"], "131 outside, 15 inside F59") + need(ob["source_forced_full_from"] == 1708, "X21 forced full from 1708") + need(ob["direct_cut_classes"] == 28 and all(x[1] for x in ob["direct_first_obstruction"]), "28/28 obstructed") + need(ob["non_private_registers_at_rank_floor"] == 280, "rank floor") + for name, want in (("T", [2, 1, 1, 2]), ("S", [3, 1, 2, 2]), ("P", [5, 1, 1, 1]), ("T48", [49, 48, 1, 2])): + r = b[name] + need([r["added_vs_R0"][k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")] == want, name + " bill") + need(r["native_validate_coefficient_zero"] == "PASS", name + " native") + need(r["real_word_rejected_by_unchanged_checker_at"] == "full physical boundary endpoint Y59", name + " rejection site") + need(r["changed_final_rows"] == ["Y59"], name + " only Y59 changes") + need(r["head_in_target_frame_before_correction"] and r["head_in_source_frame_before_correction"], name + " co-hosted") + need(b["T"]["profile_delta_vs_R0"] == {"1": 1, "2": -1, "3": 1}, "T profile") + need(b["S"]["profile_delta_vs_R0"] == {"1": 2}, "S profile") + need(b["P"]["profile_delta_vs_R0"] == {"1": 1}, "P profile") + need(b["P"]["private_events"] == {"zero": 9, "copy": 9, "erase": 9}, "P private lifetime") + need(b["T"]["Y59_final_X21"] == b["S"]["Y59_final_X21"] == b["P"]["Y59_final_X21"] == "0", "entry applied") + need(b["T48"]["Y59_final_row_is_identity"], "row 59 becomes y + x") + need(b["T"]["added_rank_by_register"] == {"Y59": 2} and b["S"]["added_rank_by_register"] == {"X21": 2}, "even per-register mass") + need(b["T"]["target_frame_before_correction_rank"] == 6, "correction leaves the rank-6 head chart") + need(cert["end_cut_detour"]["published_detour_added_rank"] == cert["end_cut_detour"]["R0_detour_added_rank"] == 2, "co-host discount zero") + need(cert["selected_kappa"] == SELECTED_KAPPA and cert["no_new_kappa"] is True, "kappa unchanged") + return got + + +def main(root=ROOT): + cert = loads((HERE / "CERTIFICATE.json").read_bytes()) + new_recipes = loads((HERE / "CORRECTION-RECIPES.json").read_bytes())["recipes"] + admit(root, cert, new_recipes) + print(MARKER) + + +if __name__ == "__main__": + main(Path(sys.argv[1]).resolve() if len(sys.argv) > 1 else ROOT)