From f2c20bc4d82558bb4ff280a49814e70778816e96 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 1/6] Research: flag-9 I-G/2 end-cut side-correction bill attains +2 (no new kappa) Price entry (23,4) on the published native word at terminal transport 3489. T/S/T48 attain +2 rank mass; private-copy P costs +1. Feeder X58:333 at leave 745 blocks all 25 zero-mass insertion classes, consistent with open #3614. Prepared by Wentao Li with substantial AI assistance. --- .../CERTIFICATE.json | 1899 +++++++++++++++++ .../CORRECTION-RECIPES.json | 306 +++ .../MASTER-HANDOFF.md | 47 + .../p104-flag9-side-correction-bill/NOTICE.md | 19 + .../p104-flag9-side-correction-bill/PROOF.md | 85 + .../p104-flag9-side-correction-bill/README.md | 113 + .../SOURCES.json | 119 ++ .../p104-flag9-side-correction-bill/TASK.json | 102 + .../VERIFY.json | 52 + .../p104-flag9-side-correction-bill/build.py | 79 + .../independent.py | 272 +++ .../test_package.py | 148 ++ .../p104-flag9-side-correction-bill/verify.py | 615 ++++++ 13 files changed, 3856 insertions(+) create mode 100644 research/p104-flag9-side-correction-bill/CERTIFICATE.json create mode 100644 research/p104-flag9-side-correction-bill/CORRECTION-RECIPES.json create mode 100644 research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md create mode 100644 research/p104-flag9-side-correction-bill/NOTICE.md create mode 100644 research/p104-flag9-side-correction-bill/PROOF.md create mode 100644 research/p104-flag9-side-correction-bill/README.md create mode 100644 research/p104-flag9-side-correction-bill/SOURCES.json create mode 100644 research/p104-flag9-side-correction-bill/TASK.json create mode 100644 research/p104-flag9-side-correction-bill/VERIFY.json create mode 100644 research/p104-flag9-side-correction-bill/build.py create mode 100644 research/p104-flag9-side-correction-bill/independent.py create mode 100644 research/p104-flag9-side-correction-bill/test_package.py create mode 100644 research/p104-flag9-side-correction-bill/verify.py diff --git a/research/p104-flag9-side-correction-bill/CERTIFICATE.json b/research/p104-flag9-side-correction-bill/CERTIFICATE.json new file mode 100644 index 0000000000..b8f8238c85 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/CERTIFICATE.json @@ -0,0 +1,1899 @@ +{ + "basis_head": 196, + "bill": { + "P": { + "Y23_final_X4": "0", + "Y23_final_row_is_identity": false, + "added_rank_by_register": { + "C": 1 + }, + "added_vs_published": { + "events": 5, + "rank_mass": 1, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y23" + ], + "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": false, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1075, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 9, + "erase": 9, + "zero": 9 + }, + "profile_delta_vs_published": { + "1": 1 + }, + "rank_mass": 2369, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y23", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 3, + "transport_occurrences": 1411 + }, + "S": { + "Y23_final_X4": "0", + "Y23_final_row_is_identity": false, + "added_rank_by_register": { + "X4": 2 + }, + "added_vs_published": { + "events": 3, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 2 + }, + "changed_final_rows": [ + "Y23" + ], + "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": false, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1076, + "2": 58, + "3": 86, + "4": 104, + "5": 48, + "6": 24, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_published": { + "1": 2 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y23", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 3, + "transport_occurrences": 1412 + }, + "T": { + "Y23_final_X4": "0", + "Y23_final_row_is_identity": false, + "added_rank_by_register": { + "Y23": 2 + }, + "added_vs_published": { + "events": 2, + "rank_mass": 2, + "scalar_adds": 1, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y23" + ], + "correction_adds": 1, + "correction_charts": [ + 9 + ], + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4060, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": false, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1075, + "2": 58, + "3": 86, + "4": 104, + "5": 47, + "6": 25, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_published": { + "1": 1, + "5": -1, + "6": 1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y23", + "scalar_adds": 2625, + "target_frame_before_correction_rank": 3, + "transport_occurrences": 1411 + }, + "T48": { + "Y23_final_X4": "0", + "Y23_final_row_is_identity": true, + "added_rank_by_register": { + "Y23": 2 + }, + "added_vs_published": { + "events": 49, + "rank_mass": 2, + "scalar_adds": 48, + "transport_occurrences": 1 + }, + "changed_final_rows": [ + "Y23" + ], + "correction_adds": 48, + "correction_charts": [ + 9 + ], + "distinct_native_edges": 741, + "endpoint_adapters": 208, + "events": 4107, + "head_in_correction_charts": true, + "head_in_source_frame_before_correction": true, + "head_in_target_frame_before_correction": false, + "native_validate_coefficient_zero": "PASS", + "paid_profile": { + "1": 1075, + "2": 58, + "3": 86, + "4": 104, + "5": 47, + "6": 25, + "7": 8, + "8": 8 + }, + "private_events": { + "copy": 8, + "erase": 8, + "zero": 8 + }, + "profile_delta_vs_published": { + "1": 1, + "5": -1, + "6": 1 + }, + "rank_mass": 2370, + "real_word_rejected_by_unchanged_checker_at": "full physical boundary endpoint Y23", + "scalar_adds": 2672, + "target_frame_before_correction_rank": 3, + "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-flag9-side-correction-bill", + "corrections": { + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X4 into C at the full chart, descend C to Y23's final hyperplane, deliver, discard", + "splices": [ + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ], + [ + "zero", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "copy", + "C", + "X4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "C", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 1 + ], + [ + "add", + "Y23", + "C", + "1/2", + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ] + ], + [ + "erase", + "C", + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ] + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + } + ] + }, + "S": { + "route": "source detour: Y23 takes its published terminal transport, X4 descends to Y23's final hyperplane for one ADD and returns to the full chart before its next read at 3695", + "splices": [ + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ], + [ + "transport", + "X4", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 1 + ], + [ + "add", + "Y23", + "X4", + "1/2", + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ] + ], + [ + "transport", + "X4", + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + } + ] + }, + "T": { + "route": "end-cut target lift on the published word: Y23 leaves [447,127,192] for the full chart, takes the entry from X4 there, then descends to its final hyperplane", + "splices": [ + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 6 + ], + [ + "add", + "Y23", + "X4", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y23", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + } + ] + }, + "T48": { + "route": "whole Y23 row of I - G/2 on the same end-cut lift: every off-diagonal source entry -G[23,s]/2 is added while Y23 sits in the full chart", + "splices": [ + { + "events": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + 6 + ], + [ + "add", + "Y23", + "X3", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X4", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X5", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X6", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X13", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X14", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X21", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X22", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X24", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X25", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X26", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X27", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X28", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X29", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X31", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X32", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X36", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X37", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X38", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X39", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X44", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X45", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X46", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X51", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X52", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X53", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X54", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X59", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X60", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X61", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X62", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X63", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X64", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X65", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X66", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X71", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X72", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X73", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X74", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X79", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X80", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X81", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X86", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X87", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X88", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X89", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X95", + "-1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "add", + "Y23", + "X101", + "1/2", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ] + ], + [ + "transport", + "Y23", + [ + 1, + 2, + 4, + 8, + 16, + 32, + 64, + 128, + 256 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 1 + ] + ], + "published": [ + [ + "transport", + "Y23", + [ + 447, + 127, + 192 + ], + [ + 467, + 27, + 196, + 12, + 124, + 3, + 7, + 1 + ], + 5 + ] + ], + "published_range": [ + 3489, + 3490 + ] + } + ] + } + }, + "cut_event": 3489, + "end_cut": { + "attaining_words": [ + "T", + "S", + "T48" + ], + "private_discount_word": "P", + "published_before_chart": [ + 256, + 191, + 127 + ], + "published_detour_added_rank": 2, + "published_detour_via_full_rank": 7, + "published_terminal_transport": [ + 3489, + 5 + ] + }, + "flag_index": 9, + "no_new_kappa": true, + "obstruction": { + "direct_cut_classes": 25, + "direct_first_obstruction": [ + [ + 0, + [ + 77, + "Y24" + ] + ], + [ + 75, + [ + 79, + "Y24" + ] + ], + [ + 76, + [ + 80, + "Y24" + ] + ], + [ + 77, + [ + 2071, + "Y28" + ] + ], + [ + 641, + [ + 2071, + "Y28" + ] + ], + [ + 746, + [ + 746, + "Y23" + ] + ], + [ + 905, + [ + 905, + "Y23" + ] + ], + [ + 1106, + [ + 1106, + "Y23" + ] + ], + [ + 1326, + [ + 1326, + "Y23" + ] + ], + [ + 1614, + [ + 1614, + "Y23" + ] + ], + [ + 1652, + [ + 1652, + "Y23" + ] + ], + [ + 1717, + [ + 1717, + "Y23" + ] + ], + [ + 1806, + [ + 1806, + "Y23" + ] + ], + [ + 1910, + [ + 1910, + "Y23" + ] + ], + [ + 2071, + [ + 2071, + "Y23" + ] + ], + [ + 2161, + [ + 2161, + "Y23" + ] + ], + [ + 2297, + [ + 2297, + "Y23" + ] + ], + [ + 2641, + [ + 2641, + "Y23" + ] + ], + [ + 2827, + [ + 2827, + "Y23" + ] + ], + [ + 3125, + [ + 3125, + "Y23" + ] + ], + [ + 3696, + [ + 3696, + "Y23" + ] + ], + [ + 3803, + [ + 3803, + "Y23" + ] + ], + [ + 3855, + [ + 3855, + "Y23" + ] + ], + [ + 3959, + [ + 3959, + "Y23" + ] + ], + [ + 4010, + [ + 4010, + "Y23" + ] + ] + ], + "entry": { + "correction_coefficient": "1/2", + "diagonal_gram": 2, + "gram": -1, + "source": "X4", + "target": "Y23" + }, + "flag_head_in_target_final": true, + "leave_add_event": [ + "add", + "G7", + "X4", + -2 + ], + "leave_alone_forcing_census": { + "cited_insertion_classes": 25, + "cited_primary_feeder": "X58:333@leave745", + "note": "recomputed on the published word; deferred flag-9 head-step repair not reopened", + "open_pr": 3614, + "package": "research/p104-present-head-side-correction-forcing-census" + }, + "non_private_registers_at_rank_floor": 280, + "outside_head_count": 1, + "private_early_delivery_cuts": 7, + "private_early_first_obstruction": [ + [ + 0, + [ + 77, + "Y24" + ] + ], + [ + 75, + [ + 79, + "Y24" + ] + ], + [ + 76, + [ + 80, + "Y24" + ] + ], + [ + 77, + [ + 2071, + "Y28" + ] + ], + [ + 2071, + [ + 2161, + "Y28" + ] + ], + [ + 2161, + [ + 2297, + "Y28" + ] + ], + [ + 2297, + [ + 2642, + "Y28" + ] + ] + ], + "published_private_lifetimes": [ + 2461, + 2524 + ], + "row_23_offdiagonal_nonzero": 48, + "selected_feeder": { + "carrier_path": [ + [ + 631, + "G7", + "X58" + ], + [ + 729, + "G16", + "X58" + ], + [ + 731, + "G16", + "X35" + ], + [ + 745, + "G7", + "X4" + ] + ], + "from_register": "X58", + "gram_with_target": 0, + "head": 333, + "head_in_target_final": false + }, + "source_forced_full_from": 1613, + "source_forced_rank_at_events": [ + [ + 640, + "G13", + 1 + ], + [ + 745, + "G7", + 2 + ], + [ + 904, + "G16", + 4 + ], + [ + 1105, + "G26", + 7 + ], + [ + 1325, + "G27", + 8 + ], + [ + 1613, + "G13", + 9 + ], + [ + 1651, + "G7", + 9 + ], + [ + 1716, + "G16", + 9 + ], + [ + 1805, + "G26", + 9 + ], + [ + 1909, + "G27", + 9 + ], + [ + 3695, + "Q1", + 9 + ], + [ + 3802, + "Q3", + 9 + ], + [ + 3854, + "Q4", + 9 + ], + [ + 3958, + "Q6", + 9 + ], + [ + 4009, + "Q7", + 9 + ] + ], + "source_leaves_target_final_at": 745, + "source_next_read_after_cut": [ + 3695, + [ + "add", + "Q1", + "X4", + 2 + ] + ], + "source_rank_at_leave": 2 + }, + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "schema_version": 1, + "selected_kappa": "0.001672660197076918" +} diff --git a/research/p104-flag9-side-correction-bill/CORRECTION-RECIPES.json b/research/p104-flag9-side-correction-bill/CORRECTION-RECIPES.json new file mode 100644 index 0000000000..acce30c147 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/CORRECTION-RECIPES.json @@ -0,0 +1,306 @@ +{ + "clifford_exact_sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "compiler_sha256": "9d2fc2d81962ddb0b4dd7d6482d9918a87a6b05759690317dea79939ca5656a3", + "recipes": [ + { + "new": [ + 256, + 160, + 96, + 16, + 8, + 4, + 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, + 8, + 16, + 32, + 1, + 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": [ + 32, + 1, + 2, + 4, + 8, + 16, + 96, + 160, + 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, + 160, + 96, + 16, + 8, + 4, + 2, + 1 + ], + "rank": 1, + "recipe": { + "left": { + "linear_Z4": [ + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "matrix_rows": [ + 2, + 4, + 8, + 16, + 32, + 65, + 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": [ + 160, + 1, + 2, + 4, + 8, + 16, + 128, + 192, + 256 + ], + "offset": 65, + "phase": 0, + "quadratic_rows": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + } + } + }, + { + "new": [ + 256, + 128, + 64, + 32, + 16, + 8, + 4, + 2, + 1 + ], + "old": [ + 256, + 168, + 5 + ], + "rank": 6, + "recipe": { + "left": { + "linear_Z4": [ + 3, + 2, + 3, + 2, + 3, + 2, + 0, + 0, + 0 + ], + "matrix_rows": [ + 65, + 2, + 1, + 132, + 8, + 16, + 32, + 20, + 256 + ], + "offset": 0, + "phase": 0, + "quadratic_rows": [ + 1, + 0, + 20, + 0, + 20, + 0, + 0, + 0, + 0 + ] + }, + "rank": 6, + "right": { + "linear_Z4": [ + 0, + 2, + 0, + 0, + 2, + 0, + 2, + 1, + 0 + ], + "matrix_rows": [ + 1, + 2, + 8, + 16, + 160, + 64, + 4, + 128, + 256 + ], + "offset": 239, + "phase": 3, + "quadratic_rows": [ + 4, + 0, + 1, + 128, + 0, + 128, + 0, + 168, + 0 + ] + } + } + } + ], + "schema_version": 1, + "scope": "Native recipes for the transport edges used by flag-9 end-cut corrections T, S, P and T48 that are absent from the published p104-native-channel recipe set. Lowered with the pinned compile.py / vendor/clifford_exact.py; checked by the published check_native.validate() during replay." +} diff --git a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md new file mode 100644 index 0000000000..c8496036fa --- /dev/null +++ b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md @@ -0,0 +1,47 @@ +# MASTER-HANDOFF — flag-9 end-cut side-correction bill + +## Claim (one sentence) + +On the published P104 native word, flag 9's `I−G/2` entry `(23,4)` (`G=−1` ⇒ `+1/2·X4` into `Y23`) costs exactly **+2** non-private rank mass at the end-cut (attained by T/S/T48); private-copy P costs **+1**; feeder `X58:333` at leave 745 blocks all 25 zero-mass insertion classes (consistent with open #3614). + +## Tip / base + +- Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`) +- Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork; tip filled after push) +- Package: `research/p104-flag9-side-correction-bill/` + +## PASS lines + +```text +PASS_P104_FLAG9_SIDE_CORRECTION_BILL flag=9 entry=(23,4) gram=-1 coefficient=+1/2 zero_mass_placements=0/25 forcing=X58(333)@leave745 strict_min_added_rank=2 T=+1transport+1add+2rank(H1-H5+H6) S=+2transport+1add+2rank(2H1) P=+1transport+1add+1rank(H1)+1private_lifetime T48=+1transport+48add+2rank row23=identity native_validate=4/4 published_end_cut no_new_kappa +PASS_P104_FLAG9_SIDE_CORRECTION_BILL_INDEPENDENT entry=(23,4) coefficient=+1/2 zero_mass_placements=0/25 early_private_deliveries_obstructed=7/7 forcing_head=333(X58)@leave745 T=+2rank S=+2rank P=+1rank T48=+2rank rows_changed=Y23_only row23=identity new_recipes=3 no_new_kappa +PASS_P104_FLAG9_SIDE_CORRECTION_BILL_TESTS cases=14 clean_read_only=1 scanners=2 +PASS_REGISTERED_RESEARCH_PACKAGE research/p104-flag9-side-correction-bill outcome=completed +``` + +## Commands + +```sh +python3.12 -I -B research/p104-flag9-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag9-side-correction-bill +``` + +## Soft-overlap risks + +- Template kinship with open [#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601) / [#3610](https://github.com/CrocSwap/integer-mult-bounds/pull/3610) (T/S/P/T48 / Tend bill shape). **Novelty bar met:** flag-9-specific attaining words on the published chronology, coefficient `+1/2`, cut 3489 / A3, three new recipes `A3→FULL` + `FULL↔F23`, feeder `X58:333@745` with 25/25 obstruction recomputed, private 7/7 early blocks. Not a rename-only clone. +- Open [#3614](https://github.com/CrocSwap/integer-mult-bounds/pull/3614): feeder/obstruction cited as leave-alone and recomputed; no certificate import; does not reopen deferred head-step repair. +- Leave-alone: #3601, #3610, #3614, #3532, #3508, #3443 (chronology cited only). + +## Open questions + +1. Is private-copy P admissible, or must correction lifetimes be uncomputed? +2. If a co-hosted flag-9 repair later lands, does +2 discount? +3. Full-row (~48) forcing census on Y7/Y23/Y59 — #3614 OQ1. + +## Attribution + +Prepared by Wentao Li with substantial AI assistance. +No CrocSwap PR opened by this worker; master publishes. diff --git a/research/p104-flag9-side-correction-bill/NOTICE.md b/research/p104-flag9-side-correction-bill/NOTICE.md new file mode 100644 index 0000000000..3d44999fcf --- /dev/null +++ b/research/p104-flag9-side-correction-bill/NOTICE.md @@ -0,0 +1,19 @@ +# Notice + +This package applies explicit end-cut corrections to the published P104 native +channel word in memory and checks them with the published native checker and a +second scanner. It does not modify frozen upstream sources. The three 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. + +Open [#3614](https://github.com/CrocSwap/integer-mult-bounds/pull/3614), +[#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601), +[#3610](https://github.com/CrocSwap/integer-mult-bounds/pull/3610), +[#3532](https://github.com/CrocSwap/integer-mult-bounds/pull/3532) and +[#3508](https://github.com/CrocSwap/integer-mult-bounds/pull/3508) are +leave-alone citations. The deferred flag-9 head-step repair is not reopened. + +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-flag9-side-correction-bill/PROOF.md b/research/p104-flag9-side-correction-bill/PROOF.md new file mode 100644 index 0000000000..b8ba52b483 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/PROOF.md @@ -0,0 +1,85 @@ +# Proof notes: flag-9 end-cut side-correction bill + +## Setup + +Let `G` be the P104 Gram matrix of the 104 ports. Flag 9 matches source `X4` +to target `Y23` with basis head `196` (#2981; identity checked against the +pinned joint-unit-flags certificate). The published native word has 4,058 +events. `Y23`'s terminal transport is event 3489: + +```text +transport Y23 [447,127,192] → F23 = [467,27,196,12,124,3,7,1] rank 5 +``` + +`G[23,4] = −1`, so the `(23,4)` entry of `I − G/2` is `+1/2`. The channel +leaves `Y23` with coefficient `−1/2` on `X4`; applying the entry zeros that +coefficient. `Y23` is never read as a source, so only that row changes. + +## Corrections + +Each word replaces event 3489. + +- **T.** `Y23: A3 → FULL` (rank 6), `Y23 += (1/2) X4` in FULL, `Y23: FULL → F23` + (rank 1). Added rank mass `(6 + 1) − 5 = 2`. +- **S.** Keep the published transport; `X4: FULL → F23` (rank 1), ADD in F23, + `X4: F23 → FULL` (rank 1). Added rank mass `2`. `X4`'s next read is at + event 3695 in FULL, so the detour restores before that read. +- **P.** Keep the published transport; open one private lifetime on `C` at + FULL, copy `X4`, descend `C` to F23, ADD, erase. Added rank mass `1` on `C`. +- **T48.** Same lift as T, but every off-diagonal nonzero `−G[23,s]/2` is + added in FULL (48 ADDs). Added rank mass `2`; final `Y23` row is + `y23 + x23`. + +## Native validation + +For each word, set every newly inserted ADD coefficient to `0` and run the +published `check_native.validate()` with the published recipe set plus the +three committed new-edge recipes (`A3 → FULL`, `FULL → F23`, `F23 → FULL`). +Chart legality, endpoint adapters and framed-row checks do not depend on the +coefficient. Each coefficient-0 word passes. Each real word fails only at +`full physical boundary endpoint Y23`. Exact rational replay confirms the +row change stated above. + +## Obstruction + +Work in the class that keeps published events and ADD coefficients, keeps +every endpoint frame, may retarget or insert transports, and keeps `C`'s +published private lifetimes `(2461, 2524)`. + +**Leave.** Replay ADDs under least monotone frames (private `C` unconstrained). +At event 745 (`add G7 X4 −2`), `X4`'s frame first leaves `F23`. The outside +head of `X`-singleton origin with `G[23, ·] = 0` is `333` from `X58`, carried +along + +```text +631: G7 ← X58, 729: G16 ← X58, 731: G16 ← X35, 745: G7 ← X4. +``` + +**Classes.** The 25 insertion classes are the cut-points immediately after +every ADD/copy that touches `X4` or `Y23`, plus the start of the word. A +least-frame sweep that forces `X4` and `Y23` to share a frame at each class +obstructs all 25. From class 746 onward the obstruction is immediate at +`Y23` (merged frame already contains `333`). + +**Parity.** Endpoint-restoring non-private nested transports contribute even +rank mass. Hence the strict non-private minimum is exactly 2. T, S and T48 +attain it. + +**Private.** Forcing `Y23` to host head `196` at each of the 7 early delivery +cuts before `C`'s published span is obstructed. Under the inherited +private-copy contract, +1 is therefore the minimum for one added lifetime. + +## Consistency with #3614 + +Open #3614 reports the same primary feeder `X58:333` at leave 745 and the +same 25/25 zero-mass obstruction for entry `(23,4)` on the published word. +This package recomputes those facts from the pinned witness/Gram and does not +import #3614's certificate. It does not reopen the deferred flag-9 head-step +repair. + +## Limits + +- No co-hosted discount is claimed; the deferred repair is leave-alone. +- P's admissibility as a physical correction is open. +- Only the primary flag-9 entry is priced; full-row (~48) census is #3614 OQ1. +- Selected κ is unchanged: `0.001672660197076918`. diff --git a/research/p104-flag9-side-correction-bill/README.md b/research/p104-flag9-side-correction-bill/README.md new file mode 100644 index 0000000000..28a90190e8 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/README.md @@ -0,0 +1,113 @@ +# Flag 9's `I − G/2` entry costs +2 rank mass at the published end-cut (attaining T/S/T48; private P = +1) + +**Exact bill plus a sharp obstruction. No new exponent.** + +Open [#3614](https://github.com/CrocSwap/integer-mult-bounds/pull/3614) +finds that flag 9's primary present-head entry needs non-private +2 on the +published word (feeder `X58:333` at leave 745; 25/25 insertion classes +zero-mass obstructed) but constructs no attaining correction. Merged +[#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) pins the +published chronology `X4 → Y23`, head 196. The deferred flag-9 head-step +repair is not reopened. This package answers #3614's flag-9 bill question on +the **published** native word only. + +## The entry + +`G[23,4] = = −1`, and the channel leaves `X4` in `Y23` with +coefficient `−1/2`. The corresponding entry of `I − G/2` is `+1/2`. Applying +it leaves `Y23` with `X4` coefficient `0`. `Y23` is never read, so the +correction changes no other row. + +## Result + +Every correction below replaces the published terminal `Y23` transport at +event 3489 (`A3 → F23`, rank 5), where `A3 = [447,127,192]` and `F23` is +`Y23`'s final rank-8 frame. + +| Word | Correction | Δ events | Δ ADDs | Δ transports | Δ rank mass | Profile Δ vs published | Edges | +|---|---|---:|---:|---:|---:|---|---:| +| **T** | `Y23: A3→FULL`, `Y23 += X4/2` in FULL, `Y23: FULL→F23` | +2 | +1 | +1 | **+2** | `H1 − H5 + H6` | 741 | +| **S** | published transport, then `X4: FULL→F23`, ADD in F23, `X4: F23→FULL` | +3 | +1 | +2 | **+2** | `2H1` | 742 | +| **P** | one private lifetime: zero `C` at FULL, copy `X4`, `C: FULL→F23`, ADD, erase | +5 | +1 | +1 | **+1** | `H1` | 741 | +| **T48** | T's lift, carrying all 48 off-diagonal entries `−G[23,s]/2` of row 23 | +49 | +48 | +1 | **+2** | `H1 − H5 + H6` | 741 | + +The published `check_native.validate()` runs unchanged on each word with the +inserted coefficients set to `0`. It passes every native edge, including the +three newly lowered `A3 → FULL` and `FULL ↔ F23` recipes, all 208 endpoint +adapters, all 280 framed rows and the restoration of the 72 dirty helpers. +On the real word, the same checker fails only at +`full physical boundary endpoint Y23`. Exact rational replay confirms that +`Y23` is the only row that changes: + +- in T, S and P it changes by exactly `+1/2 X4`; +- in T48, `Y23`'s final row becomes exactly `y23 + x23`, the identity row. + +Head 196 is absent from `Y23`'s before-frame at the cut (it arrives only in +the terminal after-frame, per #3443) and is present in every correction +chart. + +## Obstruction: no zero-mass placement exists + +Insert one correction ADD between `X4` and `Y23` anywhere in the class that +keeps published events/ADDs, endpoint frames, free retarget/insert of +transports, and `C`'s published private lifetimes. Its added rank mass is +never zero. + +- **Forcing leave.** At event 745 (`G7 −= 2·X4`), `X4`'s forced frame leaves + `F23` carrying `X58`'s head `333` along the carrier path + `631: G7 ← X58`, `729: G16 ← X58`, `731: G16 ← X35`, `745: G7 ← X4`. + `G[23,58] = 0`, so `333` lies outside `F23`. +- **Every insertion point.** A least-lower-bound frame sweep checks all 25 + insertion classes; every class is obstructed (before 746 via early forced + hosting of other targets; from 746 on immediately at `Y23`). +- **Parity.** Each nested transport 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. + +This feeder and the 25/25 obstruction match open #3614's leave-alone census +(recomputed here; not imported). + +**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 `X4`: all 7 early delivery classes +before `C`'s published span 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-flag9-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/verify.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/independent.py +python3.12 -I -O -Werror -B research/p104-flag9-side-correction-bill/test_package.py +python3.12 -B scripts/research_package.py --package research/p104-flag9-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 [#3614](https://github.com/CrocSwap/integer-mult-bounds/pull/3614) for +the forcing census / feeder (leave-alone; recomputed), [#3443](https://github.com/CrocSwap/integer-mult-bounds/pull/3443) +for flag 9's published chronology, and open [#3601](https://github.com/CrocSwap/integer-mult-bounds/pull/3601) +/ [#3610](https://github.com/CrocSwap/integer-mult-bounds/pull/3610) as format +priors (leave-alone; scientific novelty is the flag-9 attaining bill). Credit +`research/p104-side-correction-rank-obstruction` for the end-cut round-trip +invoice pattern. 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 the +1 private-copy route P admissible as a physical correction? +2. If a co-hosted flag-9 repair later lands, does the end-cut +2 discount? +3. Full-row forcing census on Y7/Y23/Y59 (~48 sources) — #3614 OQ1. diff --git a/research/p104-flag9-side-correction-bill/SOURCES.json b/research/p104-flag9-side-correction-bill/SOURCES.json new file mode 100644 index 0000000000..6cfb5d19ea --- /dev/null +++ b/research/p104-flag9-side-correction-bill/SOURCES.json @@ -0,0 +1,119 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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 9 identity)" + }, + { + "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 three 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-flag9-audit/README.md", + "usage": "provenance", + "git_blob": "0f216f0e9453cf0c6fc27925f50f4185b75c8d70", + "sha256": "03954e301d5aa90a61b11eeb69788976f1189f625673cc4d38c0aabf4c08102c", + "pin": "base_commit:research/p104-present-head-flag9-audit/README.md", + "credit": "#3443 flag-9 chronology on the published word (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" + } + ], + "leave_alone_citations": [ + { + "open_pr": 3614, + "package": "research/p104-present-head-side-correction-forcing-census", + "role": "feeder X58:333 @ leave 745 and 25/25 zero-mass obstruction on published word; recomputed consistently; not imported" + }, + { + "open_pr": 3601, + "package": "research/p104-flag43-side-correction-bill", + "role": "format prior for T/S/P/T48 bills; leave-alone; not cloned byte-for-byte" + }, + { + "open_pr": 3610, + "package": "research/p104-flag1-side-correction-bill", + "role": "format prior / Tend control pattern; leave-alone" + }, + { + "merged_pr": 3443, + "package": "research/p104-present-head-flag9-audit", + "role": "published chronology X4->Y23 head 196; cited only" + } + ] +} diff --git a/research/p104-flag9-side-correction-bill/TASK.json b/research/p104-flag9-side-correction-bill/TASK.json new file mode 100644 index 0000000000..594fa2a8a9 --- /dev/null +++ b/research/p104-flag9-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-9 entry of the I - G/2 side correction (Y23 += -G[23,4]/2 X4 = +1/2 X4) at the published end-cut (terminal Y23 transport 3489), with no co-hosted repair. Build and natively validate four corrected words on the published word (target lift T, source detour S, one private-copy lifetime P, and the whole Y23 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 25 insertion classes costs zero added rank mass, so the strict minimum is exactly 2. Recompute and cite open #3614's primary feeder X58:333 at leave 745; do not reopen the deferred flag-9 head-step repair.", + "scope_change_reason": "Open #3614's forcing census finds flag 9's primary entry (23,4) needs non-private +2 on the published word (feeder X58:333 at leave 745; 25/25 insertion classes zero-mass obstructed) but constructs no attaining correction. Open #3601/#3610 price flags 43 and 1 at co-hosted repairs; flag 9's head-step repair is deferred. This package answers #3614 OQ2 for flag 9 by building attaining end-cut words on the published chronology (#3443) and confirming the private-copy discount route.", + "bottleneck_link": "On the published word the end-cut correction for flag 9's entry needs a common chart for X4 and Y23. From event 745 on, X4's forced frame contains X58's head 333, while Y23 stays inside its final hyperplane, which excludes 333. The cheapest strict correction therefore pays +2 rank mass, attained by T, S and T48. Only the inherited private-copy contract lowers it to +1. Neither is a supplier. No co-hosted discount is claimed (deferred repair not reopened).", + "budget_minutes": 60, + "stop_rule": "Stop after flag 9: one entry, one target row, one published end-cut (3489), four validated words and the zero-mass obstruction over all insertion classes. Do not touch flags 0, 1 or 43, the other 103 target rows, global hosting, precision or kappa. Do not reopen deferred flag-9 head-step repair or leave-alone #3601/#3610/#3614/#3532/#3508.", + "outcome": "completed", + "evidence": "Flag-9 entry: G[23,4]=-1, so I-G/2 needs +1/2 X4 in Y23. On the published word the corrections replace the terminal Y23 transport at 3489 (A3=[447,127,192] -> F23, rank 5). T: Y23 A3->FULL (rank 6), ADD in FULL, FULL->F23 (rank 1): +2 events, +1 ADD, +1 transport occurrence, +2 rank mass, profile H1-H5+H6 vs published, 741 edges. S: published transport, then X4 FULL->F23, ADD in F23, F23->FULL: +3 events, +1 ADD, +2 transport occurrences, +2 rank mass, profile 2H1, 742 edges. P: zero C at FULL, copy X4, C FULL->F23, 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 23: +49 events, +48 ADDs, +1 transport occurrence, +2 rank mass; Y23's final row is exactly y23 + x23. The unchanged check_native.validate() passes each coefficient-0 word (native edges incl. three newly lowered A3->FULL and FULL<->F23 recipes, 208 adapters, 280 framed rows, 72 dirty helpers) and rejects each real word only at 'full physical boundary endpoint Y23'; exact rational replay changes only Y23's row. Obstruction: at event 745 (G7 -= 2 X4) X4's frame leaves F23 carrying X58's head 333 along carrier path 631:G7<-X58, 729:G16<-X58, 731:G16<-X35, 745:G7<-X4; G[23,58]=0 puts 333 outside Y23's final; a least-lower-bound sweep blocks all 25 insertion classes; 7/7 early private deliveries before C's published span are blocked. Per-register added rank mass is even, so the strict minimum is exactly 2. Feeder/obstruction consistent with open #3614 (leave-alone). 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 X4. 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 X4'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": "If a co-hosted flag-9 repair later lands (after #3532 merges and shared headstep.py), does the end-cut +2 discount at that cut?", + "why_it_matters": "Flag 1's R1 chart made the entry free (+0 vs R1). Flag 9's deferred repair is not reopened here; an analogous R1-style free-ride would be the first co-host discount for this flag.", + "first_step": "After a published co-hosted flag-9 chart exists, re-run the T/E comparison of #3610 at that chart.", + "blocked_by": "research/p104-flag9-head-step-repair remains deferred for soft-overlap with open #3532." + }, + { + "question": "Does every present-head target row need +2 for its strict side-correction entry on the full ~48 off-diagonal sources (beyond #3614's 18-entry sample)?", + "why_it_matters": "A zero-mass entry on Y7/Y23/Y59 would be the first place where a non-private discount exists on the published word.", + "first_step": "Full-row forcing census extension answering #3614 OQ1.", + "blocked_by": "Not attempted here; this package prices only the primary flag-9 entry." + } + ] +} diff --git a/research/p104-flag9-side-correction-bill/VERIFY.json b/research/p104-flag9-side-correction-bill/VERIFY.json new file mode 100644 index 0000000000..e308660b78 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/VERIFY.json @@ -0,0 +1,52 @@ +{ + "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" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Applies end-cut corrections T, S, P and T48 on the published word at event 3489, runs the published check_native.validate() unchanged on each coefficient-0 word (native edges incl. three 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 Y23's endpoint, recomputes bills, profiles, the X58:333 leave at 745 and the least-lower-bound sweep over all 25 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; published target rows equal G/2; each correction changes only Y23 by exactly the stated entry (T48: row becomes y+x); even non-private added mass; direct native check of all three new recipes; forward-sweep obstruction for 25 direct and 7 early private placements; feeder X58:333 at leave 745" + }, + { + "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 flags 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-flag9-side-correction-bill/build.py b/research/p104-flag9-side-correction-bill/build.py new file mode 100644 index 0000000000..5ab6972f6f --- /dev/null +++ b/research/p104-flag9-side-correction-bill/build.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Producer for CERTIFICATE.json and CORRECTION-RECIPES.json (not part of replay). + +Generates the four end-cut corrections on the published word, lowers every +transport edge absent from the published recipe set 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("flag9_side_clifford_pin", root / V.NATIVE / "vendor/clifford_exact.py", CLIFFORD_SHA256) + co = load("flag9_side_native_compile", root / V.NATIVE / "compile.py", COMPILER_SHA256) + witness, fixture, recipes, _flags = V.load_inputs(root) + physical = V.physical_map(recipes) + program = witness["program"] + spec = V.corrections(program, witness["final_frames"], V.ports(fixture)) + known = {(tuple(r["old"]), tuple(r["new"])) for r in recipes["transports"]} + new = {} + for name in spec: + prog = V.apply_splices(program, 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 flag-9 end-cut corrections T, S, P and T48 that are absent from the published p104-native-channel recipe set. 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, + } + # Seed certificate with corrections so receipt() can compare. + seed = {"corrections": spec} + got = V.receipt(root, seed, 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-flag9-side-correction-bill/independent.py b/research/p104-flag9-side-correction-bill/independent.py new file mode 100644 index 0000000000..20e0f0d773 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/independent.py @@ -0,0 +1,272 @@ +#!/usr/bin/env python3 +"""Independent replay of the flag-9 end-cut 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 three +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" +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", +} +MARKER = ( + "PASS_P104_FLAG9_SIDE_CORRECTION_BILL_INDEPENDENT entry=(23,4) coefficient=+1/2 " + "zero_mass_placements=0/25 early_private_deliveries_obstructed=7/7 " + "forcing_head=333(X58)@leave745 T=+2rank S=+2rank P=+1rank T48=+2rank " + "rows_changed=Y23_only row23=identity new_recipes=3 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") + 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("flag9_side_independent_native", root / NATIVE / "vendor/native_verify.py") + N = importlib.util.module_from_spec(spec) + spec.loader.exec_module(N) + + flag = flags["helpers"][9] + need((flag["source"], flag["target"], flag["basis"][0]) == (4, 23, 196), "flag 9") + G = gram_rows(fixture) + need(G(23, 4) == -1 and G(23, 23) == 2 and G(23, 58) == 0, "Gram entries") + program = witness["program"] + rows0, b0 = replay(witness, program) + need((b0["events"], b0["adds"], b0["transports"], b0["rank_mass"]) == (4058, 2624, 1410, 2368), "published 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, "published 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") + f23 = witness["final_frames"]["Y23"] + a3 = [447, 127, 192] + 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(a3), phys(full)), + (phys(full), phys(f23)), + (phys(f23), phys(full)), + }, "new edges are A3->FULL and FULL<->F23") + need(len(new) == 3, "three new recipes") + + 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(program, 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 == ["Y23"], name + " changes only Y23") + if name == "T48": + need(rows["Y23"] == {"Y23": Fraction(1), "X23": Fraction(1)}, "row 23 identity") + else: + need("X4" not in rows["Y23"], name + " entry applied") + diff = {k: rows["Y23"].get(k, 0) - rows0["Y23"].get(k, 0) for k in set(rows["Y23"]) | set(rows0["Y23"])} + need({k: v for k, v in diff.items() if v} == {"X4": Fraction(1, 2)}, name + " exact entry") + c = cert["bill"][name] + need([c["added_vs_published"][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, "base feasible") + ev = sorted({i for i, e in enumerate(program) if e[0] in ("add", "copy") and {"X4", "Y23"} & {e[1], e[2]}}) + cuts = sorted({0} | {i + 1 for i in ev}) + need(len(cuts) == 25, "25 placement classes") + blocked = [lower_sweep(witness, program, (u, ("X4", "Y23"), ())) 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 "Y23" 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, ("Y23",), (196,))) for u in early] + need(len(early) == 7 and all(pblocked), "early private deliveries obstructed") + + # Recompute X58:333 leave at 745. + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + f23c = closure(f23) + leave = None + for i, e in enumerate(program): + 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]])) + if "X4" in (e[1], e[2]) and not cur["X4"] <= f23c: + leave = i + break + need(leave == 745 and 333 in cur["X4"] and 333 not in f23c and 196 in f23c, "333 forced into X4 by 745") + need(witness["initial_frames"]["X58"] == [333], "X58 head") + ob = cert["obstruction"] + need(ob["source_leaves_target_final_at"] == 745, "certificate leave") + need(ob["selected_feeder"]["from_register"] == "X58" and ob["selected_feeder"]["head"] == 333, "certificate feeder") + need(ob["selected_feeder"]["carrier_path"] == [[631, "G7", "X58"], [729, "G16", "X58"], [731, "G16", "X35"], [745, "G7", "X4"]], "carrier path") + need(ob["source_forced_full_from"] == 1613, "certificate full-from") + need(ob["leave_alone_forcing_census"]["open_pr"] == 3614, "cite #3614") + 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-flag9-side-correction-bill/test_package.py b/research/p104-flag9-side-correction-bill/test_package.py new file mode 100644 index 0000000000..b910b74702 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/test_package.py @@ -0,0 +1,148 @@ +#!/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" +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", +] +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_published"].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"]["selected_feeder"].update(head=196)), + "leave_event": cert_edit(lambda d: d["obstruction"].update(source_leaves_target_final_at=640)), + "obstruction_row": cert_edit(lambda d: d["obstruction"]["direct_first_obstruction"].__setitem__(20, [3125, None])), + "duplicate_key": dup_key, + "witness_byte": flip(f"{NATIVE}/inputs/LOWRANK-WITNESS.json", 4096), + "flags_byte": flip("research/p104-joint-unit-flags/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, 5), + "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_FLAG9_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_FLAG9_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-flag9-side-correction-bill/verify.py b/research/p104-flag9-side-correction-bill/verify.py new file mode 100644 index 0000000000..a5c52b7ba0 --- /dev/null +++ b/research/p104-flag9-side-correction-bill/verify.py @@ -0,0 +1,615 @@ +#!/usr/bin/env python3 +"""Read-only replay of the flag-9 I-G/2 end-cut side-correction bill. + +On the published native-channel word, replaces Y23's terminal transport at +event 3489 with four concrete corrections that apply the (23, 4) entry of +I - G/2 (and, for T48, the whole Y23 row). For each corrected word it runs the +published check_native.validate() unchanged on the coefficient-0 copy, replays +the real word with exact rational rows, and confirms that validate() rejects +the real word only at Y23's endpoint. It then recomputes the bills, the +X58:333 forcing leave at event 745 and the least-lower-bound frame sweep that +rules out a zero-added-mass placement (25/25 classes), and compares the +receipt with CERTIFICATE.json. Admission uses need() and stays active under +python -O. Nothing is written. Does not reopen the deferred flag-9 head-step +repair; cites open #3614's feeder/obstruction as leave-alone. +""" + +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" +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", +} +FLAG_INDEX = 9 +CUT = 3489 +SELECTED_KAPPA = "0.001672660197076918" +FULL = [1, 2, 4, 8, 16, 32, 64, 128, 256] +A3 = [447, 127, 192] +PRIVATE_SPAN = (2461, 2524) +MARKER = ( + "PASS_P104_FLAG9_SIDE_CORRECTION_BILL flag=9 entry=(23,4) gram=-1 coefficient=+1/2 " + "zero_mass_placements=0/25 forcing=X58(333)@leave745 strict_min_added_rank=2 " + "T=+1transport+1add+2rank(H1-H5+H6) S=+2transport+1add+2rank(2H1) " + "P=+1transport+1add+1rank(H1)+1private_lifetime T48=+1transport+48add+2rank row23=identity " + "native_validate=4/4 published_end_cut 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 = "flag9_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")) + return witness, fixture, recipes, flags + + +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) + + +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 + + +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(program, final, ps): + f23 = final["Y23"] + cut = program[CUT] + need(cut == ["transport", "Y23", A3, f23, 5], "published terminal Y23 transport at the cut") + coeff = str(Fraction(-gram(ps, 23, 4), 2)) + need(coeff == "1/2", "flag-9 entry coefficient") + row = [["add", "Y23", "X%d" % s, str(Fraction(-gram(ps, 23, s), 2)), FULL] + for s in range(104) if s != 23 and gram(ps, 23, s)] + entry = ["add", "Y23", "X4", coeff, FULL] + + def one(events): + return [{"published_range": [CUT, CUT + 1], "published": [cut], "events": events}] + + return { + "T": { + "route": "end-cut target lift on the published word: Y23 leaves [447,127,192] for the full chart, takes the entry from X4 there, then descends to its final hyperplane", + "splices": one([ + ["transport", "Y23", A3, FULL, 6], + entry, + ["transport", "Y23", FULL, f23, 1], + ]), + }, + "S": { + "route": "source detour: Y23 takes its published terminal transport, X4 descends to Y23's final hyperplane for one ADD and returns to the full chart before its next read at 3695", + "splices": one([ + cut, + ["transport", "X4", FULL, f23, 1], + ["add", "Y23", "X4", coeff, f23], + ["transport", "X4", f23, FULL, 1], + ]), + }, + "P": { + "route": "one added private lifetime under the inherited private-copy contract: copy X4 into C at the full chart, descend C to Y23's final hyperplane, deliver, discard", + "splices": one([ + cut, + ["zero", "C", FULL], + ["copy", "C", "X4", FULL], + ["transport", "C", FULL, f23, 1], + ["add", "Y23", "C", coeff, f23], + ["erase", "C", f23], + ]), + }, + "T48": { + "route": "whole Y23 row of I - G/2 on the same end-cut lift: every off-diagonal source entry -G[23,s]/2 is added while Y23 sits in the full chart", + "splices": one([["transport", "Y23", A3, FULL, 6]] + row + [["transport", "Y23", FULL, f23, 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 + + +def sweep(witness, program, inject=None): + """Least frames of a zero-added-mass repair; C is left unconstrained.""" + 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}) + + +def closure(vectors): + span = {0} + for v in vectors: + if v not in span: + span |= {x ^ v for x in span} + return frozenset(span) + + +def grow(span, vectors): + span = set(span) + for v in vectors: + if v not in span: + span |= {x ^ v for x in span} + return frozenset(span) + + +def forcing_leave(witness, program, src, tgt): + """First ADD that forces src outside tgt's final; list outside X-heads.""" + final = closure(witness["final_frames"][tgt]) + cur = {n: closure(f) for n, f in witness["initial_frames"].items()} + head_of = { + f[0]: n + for n, f in witness["initial_frames"].items() + if n.startswith("X") and len(f) == 1 + } + holders = {head: {n} for head, n in head_of.items()} + for index, event in enumerate(program): + if event[0] != "add" or "C" in (event[1], event[2]): + continue + left, right = event[1], event[2] + for head, regs in list(holders.items()): + if left in regs or right in regs: + holders[head] = regs | {left, right} + merged = grow(cur[left], cur[right]) + cur[left] = cur[right] = merged + if src in (left, right) and not cur[src] <= final: + outside = [] + for head, name in sorted(head_of.items()): + if head in cur[src] and head not in final: + seen = {name} + path = [] + for step, prior in enumerate(program[: index + 1]): + if prior[0] != "add" or "C" in (prior[1], prior[2]): + continue + if set(prior[1:3]) & seen: + seen |= {prior[1], prior[2]} + path.append([step, prior[1], prior[2]]) + if src in seen: + break + outside.append({ + "head": head, + "from_register": name, + "carrier_path": path, + }) + return { + "source_leaves_target_final_at": index, + "source_rank_at_leave": len(cur[src]).bit_length() - 1, + "add_event": event, + "outside_heads": outside, + } + return None + + +def receipt(root, cert, new_recipes): + ck = load_checker(root) + witness, fixture, recipes, flags = load_inputs(root) + helper = flags["helpers"][FLAG_INDEX] + head = helper["basis"][0] + need(("X%d" % helper["source"], "Y%d" % helper["target"], head) == ("X4", "Y23", 196), "flag 9 identity") + ps = ports(fixture) + physical = physical_map(recipes) + program = witness["program"] + final = witness["final_frames"] + need(len(program) == 4058, "published word length") + base = bill(ck.validate(recipes, witness, fixture, False), program) + spec = corrections(program, final, ps) + need(cert.get("corrections") == spec, "committed corrections equal the generated ones") + expected = rows(witness, program) + need(all(not (e[0] in ("add", "copy") and e[2] == "Y23") for e in program), "Y23 is never read") + 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(program, spec[name]["splices"]) + zero = zeroed(prog, len(program), spec[name]["splices"]) + wz = dict(witness) + wz["program"] = zero + cz, used = assemble(recipes, zero, new_recipes, 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["Y23"] + mass0, mass1 = register_mass(program), 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(program) + 1 + hist = {} + for i, e in enumerate(prog[:start]): + if e[0] == "transport": + hist[e[1]] = e[3] + frames_before = {} + for reg in ("Y23", "X4"): + 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, + "Y23_final_X4": str(y.get("X4", Fraction(0))), + "Y23_final_row_is_identity": y == {"Y23": Fraction(1), "X23": 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["Y23"]), + "head_in_source_frame_before_correction": inside([head], frames_before["X4"]), + "target_frame_before_correction_rank": len(frames_before["Y23"]), + "added_vs_published": {k: b[k] - base[k] for k in ("events", "scalar_adds", "transport_occurrences", "rank_mass")}, + "profile_delta_vs_published": delta(base, b), + }) + need(len(used_all) == len(new_recipes), "every committed correction recipe is used") + + f23 = canon(final["Y23"]) + leave = forcing_leave(witness, program, "X4", "Y23") + need(leave is not None, "X4 leaves Y23 final") + zero_gram = [h for h in leave["outside_heads"] if gram(ps, 23, int(h["from_register"][1:])) == 0] + need(zero_gram, "orthogonal feeder head exists") + feeder = next((h for h in zero_gram if h["from_register"] == "X58" and h["head"] == 333), zero_gram[0]) + lb = forced_frames(witness, program, "X4") + full_from = [i for i, _p, r in lb if r == 9][0] + cuts = cut_classes(program, ("X4", "Y23")) + direct = [[u, sweep(witness, program, (u, "X4", "Y23"))] 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, ("Y23",)) if u < PRIVATE_SPAN[0]] + private = [[u, sweep(witness, program, (u, None, "Y23", 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, "published feasible") + nz = [s for s in range(104) if s != 23 and gram(ps, 23, s)] + pub_cut = program[CUT] + next_x4 = [i for i, e in enumerate(program) if i > CUT and e[0] == "add" and e[2] == "X4"][0] + obstruction = { + "entry": { + "target": "Y23", + "source": "X4", + "gram": gram(ps, 23, 4), + "correction_coefficient": str(Fraction(-gram(ps, 23, 4), 2)), + "diagonal_gram": gram(ps, 23, 23), + }, + "row_23_offdiagonal_nonzero": len(nz), + "flag_head_in_target_final": inside([head], f23), + "source_leaves_target_final_at": leave["source_leaves_target_final_at"], + "source_rank_at_leave": leave["source_rank_at_leave"], + "leave_add_event": leave["add_event"][:4], + "selected_feeder": { + "from_register": feeder["from_register"], + "head": feeder["head"], + "gram_with_target": gram(ps, 23, int(feeder["from_register"][1:])), + "head_in_target_final": inside([feeder["head"]], f23), + "carrier_path": feeder["carrier_path"], + }, + "outside_head_count": len(leave["outside_heads"]), + "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), + "source_next_read_after_cut": [next_x4, program[next_x4][:4]], + "non_private_registers_at_rank_floor": sum( + 1 for r in witness["initial_frames"] + if register_mass(program).get(r, 0) == len(canon(final[r])) - len(canon(witness["initial_frames"][r])) + ), + "leave_alone_forcing_census": { + "package": "research/p104-present-head-side-correction-forcing-census", + "open_pr": 3614, + "cited_primary_feeder": "X58:333@leave745", + "cited_insertion_classes": 25, + "note": "recomputed on the published word; deferred flag-9 head-step repair not reopened", + }, + } + end_cut = { + "published_terminal_transport": [CUT, pub_cut[4]], + "published_before_chart": list(canon(pub_cut[2])), + "published_detour_via_full_rank": (9 - len(canon(pub_cut[2]))) + (9 - len(f23)), + "published_detour_added_rank": (9 - len(canon(pub_cut[2]))) + (9 - len(f23)) - pub_cut[4], + "attaining_words": ["T", "S", "T48"], + "private_discount_word": "P", + } + return { + "schema_version": 1, + "claim_id": "p104-flag9-side-correction-bill", + "pinned_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "flag_index": FLAG_INDEX, + "basis_head": head, + "cut_event": CUT, + "corrections": spec, + "bill": {"published": base, **out}, + "obstruction": obstruction, + "end_cut": end_cut, + "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": "Y23", "source": "X4", "gram": -1, + "correction_coefficient": "1/2", "diagonal_gram": 2, + }, "entry") + need(ob["source_leaves_target_final_at"] == 745, "leave event") + need(ob["selected_feeder"]["from_register"] == "X58" and ob["selected_feeder"]["head"] == 333, "X58 feeder") + need(ob["selected_feeder"]["gram_with_target"] == 0 and not ob["selected_feeder"]["head_in_target_final"], "333 orthogonal") + need(ob["flag_head_in_target_final"] and not b["T"]["head_in_target_frame_before_correction"], "head arrives only at terminal after-frame") + need(ob["source_forced_full_from"] == 1613, "X4 forced full from 1613") + need(ob["direct_cut_classes"] == 25 and all(x[1] for x in ob["direct_first_obstruction"]), "25/25 obstructed") + need(ob["private_early_delivery_cuts"] == 7 and all(x[1] for x in ob["private_early_first_obstruction"]), "7/7 early private") + need(ob["non_private_registers_at_rank_floor"] == 280, "rank floor") + need(ob["leave_alone_forcing_census"]["open_pr"] == 3614, "cite #3614") + 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_published"][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 Y23", name + " rejection site") + need(r["changed_final_rows"] == ["Y23"], name + " only Y23 changes") + need(r["head_in_correction_charts"], name + " head in correction charts") + need(b["T"]["profile_delta_vs_published"] == {"1": 1, "5": -1, "6": 1}, "T profile") + need(b["S"]["profile_delta_vs_published"] == {"1": 2}, "S profile") + need(b["P"]["profile_delta_vs_published"] == {"1": 1}, "P profile") + need(b["P"]["private_events"] == {"zero": 9, "copy": 9, "erase": 9}, "P private lifetime") + need(b["T"]["Y23_final_X4"] == b["S"]["Y23_final_X4"] == b["P"]["Y23_final_X4"] == "0", "entry applied") + need(b["T48"]["Y23_final_row_is_identity"], "row 23 becomes y + x") + need(b["T"]["added_rank_by_register"] == {"Y23": 2} and b["S"]["added_rank_by_register"] == {"X4": 2}, "even per-register mass") + need(b["T"]["target_frame_before_correction_rank"] == 3, "correction leaves the rank-3 before-chart") + need(cert["end_cut"]["published_detour_added_rank"] == 2, "end-cut +2") + 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) From 240e1471ae92240c08568c606b15de2bc218e153 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 2/6] Record flag-9 side-correction bill tip SHA and PASS receipt. Prepared by Wentao Li with substantial AI assistance. --- research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md index c8496036fa..6ec2d4bdbb 100644 --- a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md +++ b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md @@ -7,8 +7,10 @@ On the published P104 native word, flag 9's `I−G/2` entry `(23,4)` (`G=−1` ## Tip / base - Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`) -- Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork; tip filled after push) +- Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork) +- Content tip: `f2c20bc4d82558bb4ff280a49814e70778816e96` - Package: `research/p104-flag9-side-correction-bill/` +- All VERIFY commands PASS (including `PASS_REGISTERED_RESEARCH_PACKAGE`). ## PASS lines From c64ebb59f9a5d499a1de3b1cfc73fd99dde08316 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 3/6] Fill branch tip SHA in flag-9 side-correction MASTER-HANDOFF. Prepared by Wentao Li with substantial AI assistance. --- research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md | 1 + 1 file changed, 1 insertion(+) diff --git a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md index 6ec2d4bdbb..230af7c61c 100644 --- a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md +++ b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md @@ -8,6 +8,7 @@ On the published P104 native word, flag 9's `I−G/2` entry `(23,4)` (`G=−1` - Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`) - Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork) +- Tip: `240e1471ae92240c08568c606b15de2bc218e153` - Content tip: `f2c20bc4d82558bb4ff280a49814e70778816e96` - Package: `research/p104-flag9-side-correction-bill/` - All VERIFY commands PASS (including `PASS_REGISTERED_RESEARCH_PACKAGE`). From ca38a607bbfe3b5e6498f58ed9805c165ec43d35 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 4/6] Finalize MASTER-HANDOFF for flag-9 end-cut side-correction bill. Prepared by Wentao Li with substantial AI assistance. --- research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md index 230af7c61c..aab805de04 100644 --- a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md +++ b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md @@ -8,8 +8,7 @@ On the published P104 native word, flag 9's `I−G/2` entry `(23,4)` (`G=−1` - Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`) - Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork) -- Tip: `240e1471ae92240c08568c606b15de2bc218e153` -- Content tip: `f2c20bc4d82558bb4ff280a49814e70778816e96` +- Content tip: `f2c20bc4d82558bb4ff280a49814e70778816e96` (package body) - Package: `research/p104-flag9-side-correction-bill/` - All VERIFY commands PASS (including `PASS_REGISTERED_RESEARCH_PACKAGE`). From 89dbb7ced3b892ce030d31e4027eb9cba73af173 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 5/6] Point MASTER-HANDOFF Tip at prior branch HEAD. Prepared by Wentao Li with substantial AI assistance. From 0c4b73507ba7ed7b992e47b17f2cbcb6e362466b Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Sun, 18 Oct 2026 09:18:08 +0000 Subject: [PATCH 6/6] Restore Tip line in MASTER-HANDOFF. Prepared by Wentao Li with substantial AI assistance. --- research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md | 1 + 1 file changed, 1 insertion(+) diff --git a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md index aab805de04..7410bd2b9a 100644 --- a/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md +++ b/research/p104-flag9-side-correction-bill/MASTER-HANDOFF.md @@ -8,6 +8,7 @@ On the published P104 native word, flag 9's `I−G/2` entry `(23,4)` (`G=−1` - Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90` (CrocSwap `main`) - Branch: `cursor/flag9-side-correction-bill-30d6` (VictorLiwentao fork) +- Tip: `89dbb7ced3b892ce030d31e4027eb9cba73af173` - Content tip: `f2c20bc4d82558bb4ff280a49814e70778816e96` (package body) - Package: `research/p104-flag9-side-correction-bill/` - All VERIFY commands PASS (including `PASS_REGISTERED_RESEARCH_PACKAGE`).