diff --git a/research/r439-frame272-seed06/CERTIFICATE.json b/research/r439-frame272-seed06/CERTIFICATE.json new file mode 100644 index 0000000000..8f75369cf0 --- /dev/null +++ b/research/r439-frame272-seed06/CERTIFICATE.json @@ -0,0 +1,1455 @@ +{ + "F2_matrix": [ + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 1, + 0, + 0, + 1, + 1 + ], + [ + 1, + 1, + 1, + 0, + 1, + 1 + ], + [ + 1, + 0, + 1, + 1, + 1, + 1 + ], + [ + 1, + 0, + 1, + 1, + 0, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ] + ], + "boolean_inputs": 64, + "columns": 661, + "controls_rejected": [ + "drop circuit gate", + "reverse circuit operand", + "F2-neutral positive-cost inflation", + "dropped cleanup", + "nonliteral original cleanup", + "illegal lower frame", + "missing dirty compensation", + "dropped exported frame272 ADD", + "dropped exported ERASE" + ], + "frame": 272, + "guarded_minimum": 12, + "independent_guard_exclusion": { + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "excluded_gate_counts": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "guard_pruned_edges": 1587210, + "layers": [ + 1, + 13, + 105, + 616, + 2774, + 10015, + 29147, + 67281, + 126047, + 194071, + 248807, + 270500 + ], + "valid_subtraction_edges": 4416636, + "visited_states": 949377 + }, + "independent_optimality": { + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ], + "edges_from_completed_layers": 4163706, + "layers": [ + 1, + 14, + 125, + 830, + 4209, + 16312, + 48192, + 104127, + 162909, + 186564, + 163664, + 111454 + ], + "minimum": 11, + "visited_states": 798401 + }, + "interface_conclusions": { + "C_is_U_inverse": true, + "J_identity": true, + "K_equals_D": true, + "U_block_form": true + }, + "interface_hypotheses": { + "H1_no_target_feeds_z": true, + "H2_D_frame0_targets_from_helpers": true, + "H3_A_z_only_scatter_targets_B_split": true, + "H4_C_literal_reverse_at_full": true, + "H5_V_identity": true + }, + "kappa_claim": "none; unchanged paid rank profile, no hosted replay", + "labels": { + "frames": 636, + "gram_det": 1, + "labels": 111, + "lattice_rank": 8, + "punctured": 9, + "root_lines": 120 + }, + "native_records": { + "original": { + "adds": 24305, + "adds_by_phase": { + "1": 18085, + "2": 2130, + "3": 527, + "4": 934, + "5": 2629 + }, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 27234, + "records_sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + "replacement": { + "adds": 24283, + "adds_by_phase": { + "1": 18085, + "2": 2119, + "3": 527, + "4": 934, + "5": 2618 + }, + "copies": 9, + "erasures": 9, + "moves": 2911, + "paid_histogram": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "rank_mass": 5129, + "records": 27212, + "records_sha256": "84debd2bad02692f2741bb7065df6a1ffccc4fa729ad426550fe1315d0df0604" + } + }, + "new_gates": 12, + "new_phase_gates": { + "A": 2064, + "B": 712, + "C": 2563, + "D": 111 + }, + "old_gates": 23, + "old_phase_gates": { + "A": 2075, + "B": 712, + "C": 2574, + "D": 111 + }, + "overlap_comparison": { + "composition_claim": "No complete shortened prior word composed; full-word replay uses PR589 only", + "frame_local_gate_count_difference_vs_pr936_with_cleanup": 12, + "reverse_comparisons": [ + { + "dominated": true, + "increased_entries": [], + "pr": 589, + "prior_cap_dominated_by_pr589": true + }, + { + "dominated": true, + "increased_entries": [], + "pr": 904, + "prior_cap_dominated_by_pr589": true + }, + { + "dominated": true, + "increased_entries": [], + "pr": 936, + "prior_cap_dominated_by_pr589": true + }, + { + "dominated": true, + "increased_entries": [], + "pr": 952, + "prior_cap_dominated_by_pr589": true + } + ], + "sources": { + "candidate_comparison": { + "adds": 12, + "by_prior": [ + { + "forward_add_saving": 11, + "paired_cleanup_add_saving": 22, + "pr": 589, + "prior_cap_dominated_by_pr589": true, + "reverse_entrywise_dominated": true + }, + { + "forward_add_saving": 8, + "paired_cleanup_add_saving": 16, + "pr": 904, + "prior_cap_dominated_by_pr589": true, + "reverse_entrywise_dominated": true + }, + { + "forward_add_saving": 6, + "paired_cleanup_add_saving": 12, + "pr": 936, + "prior_cap_dominated_by_pr589": true, + "reverse_entrywise_dominated": true + }, + { + "forward_add_saving": 6, + "paired_cleanup_add_saving": 12, + "pr": 952, + "prior_cap_dominated_by_pr589": true, + "reverse_entrywise_dominated": true + } + ], + "composition_claim": "Only local frame transfers and paired gate counts are compared. No complete prior candidate word was composed or replayed by this package.", + "reverse_positive_transfer": [ + [ + 1, + 1, + 2, + 0, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + 1, + 1, + 3, + 2, + 1, + 1 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 0, + 1, + 2, + 0, + 1, + 1 + ] + ] + }, + "comparison_only": true, + "format": "r439-frame272-overlap-v1", + "frame": 272, + "positive_transfer": [ + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 3, + 2, + 2, + 3, + 1 + ], + [ + 1, + 3, + 3, + 2, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 4, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ] + ], + "prior_result": "PR904 saves three forward gates, PR936 a further two; PR952 accepts no frame272 replacement and leaves 18 gates. Its bounded Boolean nominations do not prove a fixed positive-transfer minimum.", + "registers": [ + 242, + 294, + 296, + 302, + 316, + 501 + ], + "scope": "Comparison of frame 272 only. All versions preserve its exact positive integer transfer. No prior whole-word circuit is imported, and no saving is claimed for composition with prior packages.", + "versions": [ + { + "adds": 23, + "author": "DreamingOfClouds", + "head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 3, + 0 + ], + [ + 3, + 5 + ], + [ + 3, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 5 + ] + ], + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "pr": 589, + "reverse_positive_transfer": [ + [ + 27, + 3, + 12, + 6, + 5, + 26 + ], + [ + 5, + 1, + 2, + 1, + 1, + 5 + ], + [ + 10, + 1, + 5, + 2, + 2, + 10 + ], + [ + 7, + 1, + 3, + 2, + 1, + 7 + ], + [ + 4, + 0, + 2, + 1, + 1, + 4 + ], + [ + 26, + 3, + 12, + 6, + 5, + 27 + ] + ], + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "start": 725, + "stop": 748 + }, + { + "adds": 20, + "author": "Gareth Davidson (@bitplane)", + "certificate_path": "research/r439-four-wire-prefix/CERTIFICATE.json", + "certificate_sha256": "e29dcde966ccfffdc83b25685729a59745e8c3938af8770a38d850e5e8fc7495", + "head": "883a0bdf7792693e57c16be660824b57aacfbe05", + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "parent_frame_start": 725, + "path": "research/r439-four-wire-prefix/candidate.json.gz", + "pr": 904, + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 10, + 3, + 8, + 4, + 3, + 11 + ] + ], + "selected_frame272_windows": [ + { + "frame": 272, + "new": [ + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ] + ], + "old": [ + [ + 1, + 0 + ], + [ + 1, + 3 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ] + ], + "registers": [ + 294, + 296, + 302, + 316 + ], + "saving": 1, + "section": "A", + "start": 733, + "stop": 737 + }, + { + "frame": 272, + "new": [ + [ + 1, + 3 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "old": [ + [ + 2, + 0 + ], + [ + 2, + 3 + ], + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 3 + ] + ], + "registers": [ + 242, + 296, + 302, + 501 + ], + "saving": 2, + "section": "A", + "start": 743, + "stop": 748 + } + ], + "sha256": "9946eaacc69f05a91ad18ca16e57cd4f78db3e0d5b23939f691c96b4a4098a2f", + "start": 710, + "stop": 730 + }, + { + "adds": 18, + "author": "Ross Richardson (@RossRichardson)", + "certificate_path": "research/r439-five-wire-prefix/CERTIFICATE.json", + "certificate_sha256": "6ce5015e9afc4db6d3742df433561ab9d1173b63f72da95178c76b6a0a973fea", + "head": "0679fb6e1e4c91f573ae07ab1d0ea273b13c74e3", + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "parent_frame_start": 710, + "path": "research/r439-five-wire-prefix/candidate.json.gz", + "pr": 936, + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 4, + 1, + 4, + 2, + 1, + 5 + ] + ], + "selected_frame272_windows": [ + { + "frame": 272, + "new": [ + [ + 4, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ], + [ + 4, + 1 + ] + ], + "old": [ + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 3 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ] + ], + "registers": [ + 294, + 296, + 302, + 316, + 501 + ], + "saving": 2, + "section": "A", + "start": 714, + "stop": 721 + } + ], + "sha256": "3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091", + "start": 695, + "stop": 713 + }, + { + "adds": 18, + "author": "Gareth Davidson (@bitplane)", + "certificate_path": "research/r439-six-wire-boolean/CERTIFICATE.json", + "certificate_sha256": "aaa5f126fe0e4938df985c00bb47d1ce17da0eb8b20ae983813b66c02de07841", + "frame272_search_record": { + "distinct_programs": 1970, + "end": 713, + "frame": 272, + "guarded_programs": 0, + "new": null, + "nomination": null, + "old": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "saved_A": 0, + "shorter_programs": 670, + "start": 695, + "trials": 2880, + "wires": [ + 242, + 294, + 296, + 302, + 316, + 501 + ] + }, + "head": "11d24706f06e95271804c9438869546724c67aab", + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "path": "research/r439-six-wire-boolean/candidate.json.gz", + "pr": 952, + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 4, + 1, + 4, + 2, + 1, + 5 + ] + ], + "sha256": "5c67c7949c07a89ea8394a936a155585d22e6b258997df73e36e7be47fc84cb0", + "start": 692, + "stop": 710 + } + ] + }, + "this_frame272_adds": 12 + }, + "physical_frame_paths_sha256": "caa79b5c63fa8db44f7e2d86984e4ac9bc8665dff441166e305fb3f09a9683ea", + "positive_matrices": { + "forward": { + "original": [ + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 3, + 2, + 2, + 3, + 1 + ], + [ + 1, + 3, + 3, + 2, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 4, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ] + ], + "replacement": [ + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 3, + 2, + 2, + 3, + 1 + ], + [ + 1, + 3, + 3, + 2, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 4, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ] + ] + }, + "reverse": { + "original": [ + [ + 27, + 3, + 12, + 6, + 5, + 26 + ], + [ + 5, + 1, + 2, + 1, + 1, + 5 + ], + [ + 10, + 1, + 5, + 2, + 2, + 10 + ], + [ + 7, + 1, + 3, + 2, + 1, + 7 + ], + [ + 4, + 0, + 2, + 1, + 1, + 4 + ], + [ + 26, + 3, + 12, + 6, + 5, + 27 + ] + ], + "replacement": [ + [ + 1, + 1, + 2, + 0, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + 1, + 1, + 3, + 2, + 1, + 1 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 0, + 1, + 2, + 0, + 1, + 1 + ] + ] + } + }, + "reconstructed_word_sha256": "6bde730c8e7489aa0f54c68245dcd4e163f5a715ddc9bd2a467352d796a8a365", + "saved_with_cleanup": 22, + "status": "PASS_R439_FRAME272" +} diff --git a/research/r439-frame272-seed06/CLAIM.json b/research/r439-frame272-seed06/CLAIM.json new file mode 100644 index 0000000000..3ddd969b4a --- /dev/null +++ b/research/r439-frame272-seed06/CLAIM.json @@ -0,0 +1,22 @@ +{ + "status": "claimed locally", + "track": "bit supplier", + "assignment_seed": 6, + "randomness": "First OS RandomNumberGenerator UInt32 draw, rejection sampled below 4294967200 then reduced modulo 100", + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "claimed_at": "2026-10-13T08:49:00-07:00", + "expected_finish": "2026-10-13T09:23:00-07:00", + "object": "PR589 R439 phase-A frame 272, selected as 266 + seed modulo 60", + "method": "Exact nonnegative integer row-subtraction graph for the full six-wire transfer; independent minimum and finite word checks, including literal cleanup and positive bounds", + "stopping_rule": "One object; at most 1000000 states in first graph enumeration. If capped, report bounded coverage rather than optimality. Permit one evidence-driven method pivot on this same object.", + "expected_deliverable": "Source-pinned finite circuit construction or scoped minimum/negative result with reproducible verifier, negative controls and clear inherited obligations; no assumed new kappa", + "candidates_considered": [ + "Whole frame 272 positive-transfer factorization: selected because bounded Boolean/window searches do not certify its integer-transfer minimum", + "Phase-B frame 506 factorization beyond the single-write class: deferred because the phase-B blocks have many concurrent constructions", + "R439 restored helper/target sharing: deferred because PR965/967/980 and related work actively occupy that mechanism" + ], + "coordination": "Curiosity Bot live issue listing at selection showed only issues 913 and 650, no pinned sprint coordination issue; claim recorded locally", + "overlap_inspected": [589, 886, 891, 904, 925, 936, 952, 965, 967, 973, 978, 980], + "prior_negative_results": "PR886 closes fixed-word frame-only improvements; PR891 closes stated single-write classes for phase B. This task changes a phase-A gate sequence and checks a distinct exact integer-transfer class.", + "delegation_scope": "Only frame272 nomination, independent minimum/comparison, and finite verification of that same replacement" +} diff --git a/research/r439-frame272-seed06/HANDOFF.json b/research/r439-frame272-seed06/HANDOFF.json new file mode 100644 index 0000000000..6f654d4503 --- /dev/null +++ b/research/r439-frame272-seed06/HANDOFF.json @@ -0,0 +1,209 @@ +{ + "assignment_seed": 6, + "attribution": "GitHub @woklerx, substantial OpenAI Codex assistance; predecessor and concurrent credit inNOTICE.md", + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "branch": "research/frame272-seed06-review", + "claim_update_policy": "After publication, the original local CLAIM.json is updated once with the result and PR URL; this immutable submission retains the original claim plus this completed receipt.", + "initial_inventory_sha256": "81a0da6dc6a8c7cf00417e67800519b5d4f4f5401b72ca37b1137b69b3a687d6", + "initial_open_pr_count": 707, + "metadata_refreshed_at": "2026-10-13T16:15:53.260117+00:00", + "native_reproduce": "python -I -B research/r439-frame272-seed06/native.py", + "native_requirements": "C++17 compiler and Boost headers; CXX and BOOST_INCLUDE; MSVC developer shell on Windows", + "new_arrivals": [ + { + "headRefOid": "607294b05e534087d934bb3a7fcb46e89f9b9851", + "number": 1000, + "title": "Research audit: elementary rational T37 support certificate (no new kappa)", + "updatedAt": "2026-10-13T16:15:19Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1000" + }, + { + "headRefOid": "fd38a824adb3a5c60c101a86c950a6d590454adf", + "number": 999, + "title": "Research: bounded target accumulation saves additional complex primitives (no new kappa)", + "updatedAt": "2026-10-13T16:13:31Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/999" + }, + { + "headRefOid": "66b777bf2b0160ed926572ff8714ac7b7bba0859", + "number": 998, + "title": "Scoped negative result: complex single lifts cannot lower P112 copy cost", + "updatedAt": "2026-10-13T16:09:02Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/998" + }, + { + "headRefOid": "b3fda8d59436103b195069a6328cbf5d74f73bc0", + "number": 997, + "title": "Recursive-interface construction: signed Hadamard batch saves 126 leaf calls (no new kappa)", + "updatedAt": "2026-10-13T16:10:07Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/997" + }, + { + "headRefOid": "d61f23298228b0b54fb24d997e5a81c30c886ece", + "number": 996, + "title": "Research note: reconcile prime-subset ceilings across assemblies (no new kappa)", + "updatedAt": "2026-10-13T16:09:48Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/996" + }, + { + "headRefOid": "93a8127b990f9755d0c80e729b40c969d6c611e4", + "number": 995, + "title": "Independent verification: uniform U8 supporting inequality (no new kappa)", + "updatedAt": "2026-10-13T16:07:39Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/995" + }, + { + "headRefOid": "b2a47e14f7189969a8a8d0e5f0a44be69898f514", + "number": 994, + "title": "Research consolidation: PR946 frozen-pin inventory and restoration replay (no new kappa)", + "updatedAt": "2026-10-13T16:07:34Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/994" + }, + { + "headRefOid": "76b71ff5bea1088fb5019dea25fe89698287e673", + "number": 993, + "title": "Research note: exact incident-safe parity frame dimensions (no new kappa)", + "updatedAt": "2026-10-13T16:07:24Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/993" + }, + { + "headRefOid": "0efdfc28b1eb71c91c012ca1e1945baeeebce7bb", + "number": 992, + "title": "Research audit: sharp T37 integrality penalties (no new kappa)", + "updatedAt": "2026-10-13T16:09:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/992" + }, + { + "headRefOid": "69f989511a3f0c6f7a26da1c1608b265fbb1668a", + "number": 991, + "title": "Independent T37 schedule and targeted payload/binding verification (same \u03ba as #942)", + "updatedAt": "2026-10-13T16:06:46Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/991" + }, + { + "headRefOid": "1c3ddf6bbbe1d8f0227de6726bb8273b2cb03711", + "number": 990, + "title": "Research construction: eight-query private native shear batch (no new kappa)", + "updatedAt": "2026-10-13T16:06:24Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/990" + }, + { + "headRefOid": "101103e56e3effdb268ce90110c6caa4c6885671", + "number": 989, + "title": "Finite bit construction: compose four R439 blocks, saving 72 ADDs (no new kappa)", + "updatedAt": "2026-10-13T16:05:11Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/989" + }, + { + "headRefOid": "9892e3e9f883fc39966e6d16bcd4e349597afeb4", + "number": 988, + "title": "Independent verification: complete U8 terminal-cone census (no new kappa)", + "updatedAt": "2026-10-13T16:04:17Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/988" + }, + { + "headRefOid": "0beb9476d10308e6693a886be78b36df8fa0a288", + "number": 987, + "title": "Draft: conditional \u03ba = 0.001662039077758742 \u2014 U10 (two new triangle-hybrid slots) on PR942's T37 owners", + "updatedAt": "2026-10-13T16:14:24Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/987" + }, + { + "headRefOid": "12470750d68b13b88e91277cacf95efddab95a59", + "number": 986, + "title": "Research: exact 12/13 frame281 boundary and two fewer ADDs (no new kappa)", + "updatedAt": "2026-10-13T15:58:37Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/986" + }, + { + "headRefOid": "9df42a99dd8497b6e7d46cd2507bb89071372640", + "number": 985, + "title": "Research: dirty arbitrary-stride cyclic inverse on two tapes (no new kappa)", + "updatedAt": "2026-10-13T15:58:18Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/985" + }, + { + "headRefOid": "51b8bce91ab21e1fffa42a907c5de3439551decb", + "number": 984, + "title": "Research note: scale deferral saves 66 beyond one JP8 fan-in block (no new kappa)", + "updatedAt": "2026-10-13T15:50:58Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/984" + }, + { + "headRefOid": "5eca5b435d2ce172edf6ffb85694c7efa31bf114", + "number": 982, + "title": "Research: output-borrowed fanout with an exact scratch/work tradeoff (no new kappa)", + "updatedAt": "2026-10-13T15:50:06Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/982" + } + ], + "pinned_coordination_issues": [], + "refreshed_inventory_sha256": "dce5938bce662bac711ad8a30d4b2b322401e345a022b88075bb0aa1e37d6b90", + "refreshed_open_pr_count": 695, + "remaining_obligations": "No whole hosted invoice, outer assembly, selected cold replay, all-size compiler or full Lean multiplication theorem; inherited physical and analytic hypotheses remain", + "reproduce": "python -I -B research/r439-frame272-seed06/verify.py", + "result": "Frame272 23-to-12 ADD replacement; full local word 24305-to-24283; exact fixed-transfer minimum11 and reverse-compatible minimum12; no new kappa", + "review_entry": "README.md", + "reviewed_dependencies": { + "p904": { + "author": { + "login": "bitplane" + }, + "headRefOid": "883a0bdf7792693e57c16be660824b57aacfbe05", + "number": 904, + "state": "MERGED", + "title": "Bit supplier: save 254 R439 ADDs with four-wire prefix resynthesis (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/904" + }, + "p925": { + "author": { + "login": "RossRichardson" + }, + "headRefOid": "eb85d40a1ba80c2f776481fbeed1bae8cf04cfde", + "number": 925, + "state": "MERGED", + "title": "Finite bit construction: R439 frame 267 reaches a 12-ADD positive-transfer minimum (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/925" + }, + "p936": { + "author": { + "login": "RossRichardson" + }, + "headRefOid": "0679fb6e1e4c91f573ae07ab1d0ea273b13c74e3", + "number": 936, + "state": "MERGED", + "title": "Finite bit construction: five-wire prefixes save 340 further ADDs beyond PR904 (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/936" + }, + "p952": { + "author": { + "login": "bitplane" + }, + "headRefOid": "11d24706f06e95271804c9438869546724c67aab", + "number": 952, + "state": "MERGED", + "title": "Finite bit construction: whole six-wire synthesis saves 38 further ADDs beyond PR936 (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/952" + } + }, + "specific_overlap_conclusions": { + "PR904_PR936_PR952": "Same-frame source-bound/transcribed comparison shows23->20->18->18; new exact guarded12, full-word replay usesPR589, not a sum of unrelated candidate savings", + "PR986": "Different frame281 and source transfer, related12/13 boundary; credit concurrent distinction, no dependency or priority claim", + "PR989": "Composition of phase-B507/508/519/524, distinct object; native compiler adapter adapted with exact Git head and observed checkout digests retained" + }, + "status": "completed research contribution; prepared for one focused PR", + "track": "bit supplier", + "validation": { + "finite_controls": 9, + "formal_columns": [ + 883, + 1327, + 1549 + ], + "full_make_verify": "not run; standalone additions, GNU make unavailable; unrelated historical regeneration avoided", + "hosted_ci": "not claimed", + "native_omitted_bridge_controls": 96, + "package_tests": 11, + "selected_record": "PASS" + } +} diff --git a/research/r439-frame272-seed06/INDEPENDENT-GUARD.json b/research/r439-frame272-seed06/INDEPENDENT-GUARD.json new file mode 100644 index 0000000000..a877eaac94 --- /dev/null +++ b/research/r439-frame272-seed06/INDEPENDENT-GUARD.json @@ -0,0 +1,46 @@ +{ + "excluded_gate_counts": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "layers": [ + 1, + 13, + 105, + 616, + 2774, + 10015, + 29147, + 67281, + 126047, + 194071, + 248807, + 270500 + ], + "visited_states": 949377, + "valid_subtraction_edges": 4416636, + "guard_pruned_edges": 1587210, + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ] +} diff --git a/research/r439-frame272-seed06/INDEPENDENT-MINIMUM.json b/research/r439-frame272-seed06/INDEPENDENT-MINIMUM.json new file mode 100644 index 0000000000..7fbd8c6aca --- /dev/null +++ b/research/r439-frame272-seed06/INDEPENDENT-MINIMUM.json @@ -0,0 +1,32 @@ +{ + "minimum": 11, + "layers": [ + 1, + 14, + 125, + 830, + 4209, + 16312, + 48192, + 104127, + 162909, + 186564, + 163664, + 111454 + ], + "visited_states": 798401, + "edges_from_completed_layers": 4163706, + "completed_expansion_depths": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10 + ] +} diff --git a/research/r439-frame272-seed06/LICENSE b/research/r439-frame272-seed06/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/r439-frame272-seed06/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/r439-frame272-seed06/NATIVE-ENVIRONMENT.json b/research/r439-frame272-seed06/NATIVE-ENVIRONMENT.json new file mode 100644 index 0000000000..b8357f2157 --- /dev/null +++ b/research/r439-frame272-seed06/NATIVE-ENVIRONMENT.json @@ -0,0 +1,161 @@ +{ + "boost_header_sha256": { + "C:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include\\boost\\multiprecision\\cpp_int.hpp": "4099045e8ac3e3507779c08980272b261a86498a23a4d0bb0786849f5424595a", + "C:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include\\boost\\version.hpp": "26446b268b3ece5640f913db846f6541f8e6c3dd6fcedfc8aec92669c222443c" + }, + "boost_include": "C:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include", + "boost_version_header": "// Boost version.hpp configuration header file ------------------------------//\n\n// (C) Copyright John maddock 1999. Distributed under the Boost\n// Software License, Version 1.0. (See accompanying file\n// LICENSE_1_0.txt or copy at http://www.boost.org/LICENSE_1_0.txt)\n\n// See http://www.boost.org/libs/config for documentation\n\n#ifndef BOOST_VERSION_HPP\n#define BOOST_VERSION_HPP\n\n//\n// Caution: this is the only Boost header that is guaranteed\n// to change with every Boost release. Including this header\n// will cause a recompile every time a new Boost version is\n// used.\n//\n// BOOST_VERSION % 100 is the patch level\n// BOOST_VERSION / 100 % 1000 is the minor version\n// BOOST_VERSION / 100000 is the major version\n\n#define BOOST_VERSION 108800\n\n//\n// BOOST_LIB_VERSION must be defined to be the same as BOOST_VERSION\n// but as a *string* in the form \"x_y[_z]\" where x is the major version\n// number, y is the minor version number, and z is the patch level if not 0.\n// This is used by to select which library version to link to.\n\n#define BOOST_LIB_VERSION \"1_88\"\n\n#endif\n", + "commands": { + "compile-columns2": [ + "cl", + "/nologo", + "/O2", + "/std:c++17", + "/EHsc", + "/DHDIM=8", + "/DNCOPY=9", + "/DVPORTS=111", + "/DRHELP=439", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\portable-include", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers", + "/IC:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include", + "/DKPAIRS=2", + "/Fe:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns2.exe", + "/Fo:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns2.obj", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers\\columns_k.cpp" + ], + "compile-columns4": [ + "cl", + "/nologo", + "/O2", + "/std:c++17", + "/EHsc", + "/DHDIM=8", + "/DNCOPY=9", + "/DVPORTS=111", + "/DRHELP=439", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\portable-include", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers", + "/IC:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include", + "/DKPAIRS=4", + "/Fe:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns4.exe", + "/Fo:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns4.obj", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers\\columns_k.cpp" + ], + "compile-columns5": [ + "cl", + "/nologo", + "/O2", + "/std:c++17", + "/EHsc", + "/DHDIM=8", + "/DNCOPY=9", + "/DVPORTS=111", + "/DRHELP=439", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\portable-include", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers", + "/IC:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include", + "/DKPAIRS=5", + "/Fe:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns5.exe", + "/Fo:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns5.obj", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers\\columns_k.cpp" + ], + "compile-legality": [ + "cl", + "/nologo", + "/O2", + "/std:c++17", + "/EHsc", + "/DHDIM=8", + "/DNCOPY=9", + "/DVPORTS=111", + "/DRHELP=439", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\portable-include", + "/IF:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers", + "/IC:\\Users\\wilds\\AppData\\Local\\rattler\\cache\\pkgs\\libboost-headers-1.88.0-h57928b3_7\\Library\\include", + "/Fe:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\legality.exe", + "/Fo:F:\\MEESEEKS MATH\\frame272-native-final\\bin\\legality.obj", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\checkers\\legality_h.cpp" + ], + "original-cohort": [ + "C:\\Users\\wilds\\AppData\\Local\\Programs\\Python\\Python314\\python.exe", + "-I", + "-B", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\regression\\stage_cohort.py", + "F:\\MEESEEKS MATH\\frame272-native-final\\local\\original\\records", + "F:\\MEESEEKS MATH\\frame272-native-final\\local\\original\\records", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cin", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout" + ], + "original-columns2": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns2.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\columns2.json" + ], + "original-columns4": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns4.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\columns4.json" + ], + "original-columns5": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns5.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\columns5.json" + ], + "original-legality": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\legality.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cin", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout", + "F:\\MEESEEKS MATH\\frame272-native-final\\original\\cout\\legality.json" + ], + "replacement-cohort": [ + "C:\\Users\\wilds\\AppData\\Local\\Programs\\Python\\Python314\\python.exe", + "-I", + "-B", + "F:\\MEESEEKS MATH\\integer-mult-bounds\\research\\e8-bit-carrier-skeleton\\code\\bit\\regression\\stage_cohort.py", + "F:\\MEESEEKS MATH\\frame272-native-final\\local\\replacement\\records", + "F:\\MEESEEKS MATH\\frame272-native-final\\local\\replacement\\records", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cin", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout" + ], + "replacement-columns2": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns2.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\columns2.json" + ], + "replacement-columns4": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns4.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\columns4.json" + ], + "replacement-columns5": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\columns5.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\COHORT249-RECORDS.bin", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\columns5.json" + ], + "replacement-legality": [ + "F:\\MEESEEKS MATH\\frame272-native-final\\bin\\legality.exe", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cin", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout", + "F:\\MEESEEKS MATH\\frame272-native-final\\replacement\\cout\\legality.json" + ] + }, + "compiler_command": [ + "cl" + ], + "compiler_path": "C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\Hostx64\\x64\\cl.exe", + "compiler_sha256": "b0a1818ebae6da7f18230a84e76ce839212584ac4c2ab55b97a0d5268085da57", + "compiler_version_output": "Microsoft (R) C/C++ Optimizing Compiler Version 19.51.36260 for x64\nCopyright (C) Microsoft Corporation. All rights reserved.\n\nCompiler Passes:\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\cl.exe: Version 19.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\c1.dll: Version 19.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\c1xx.dll: Version 19.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\c2.dll: Version 19.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\c1xx.dll: Version 19.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\link.exe: Version 14.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\mspdb140.dll: Version 14.51.36260.0\n C:\\Program Files\\Microsoft Visual Studio\\18\\Community\\VC\\Tools\\MSVC\\14.51.36231\\bin\\HostX64\\x64\\1033\\clui.dll: Version 19.51.36260.0\n\ncl : Command line error D8003 : missing source filename\n", + "platform": "Windows-11-10.0.26300-SP0", + "python": "3.14.5 (tags/v3.14.5:5607950, May 10 2026, 10:43:50) [MSC v.1944 64 bit (AMD64)]", + "python_executable": "C:\\Users\\wilds\\AppData\\Local\\Programs\\Python\\Python314\\python.exe", + "runner_predecessor": { + "checkout_difference": "Output encoding/newline and source-pin JSON hash normalization only; pinned-source conventions retained here.", + "git_source_sha256": "bc8d7d09c4e47e7bdd6b758bd0593614e78448b0a849cd83ef150baee44daf04", + "head": "101103e56e3effdb268ce90110c6caa4c6885671", + "observed_checkout_sha256": "387ac33c3b34f65604381ad21bda7780f1fbdf6154555cdfb0b6bd7b40ed18fa", + "path": "research/r439-four-block-composition/native.py", + "pr": 989 + }, + "source_pins_canonical_sha256": "3c67e4dfe7c80abe9bdeca2762958e5bd6caa1477a957f9995cfa122f43b4a60" +} diff --git a/research/r439-frame272-seed06/NATIVE.json b/research/r439-frame272-seed06/NATIVE.json new file mode 100644 index 0000000000..9449a7a0f3 --- /dev/null +++ b/research/r439-frame272-seed06/NATIVE.json @@ -0,0 +1,1202 @@ +{ + "original": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24305, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27234, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "global_live_registers": 1549, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 267355, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121525, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "global_live_registers": 1327, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24305, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24305, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9528119495320518471870892800", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1113070", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218745, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24305, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + }, + "replacement": { + "legality": { + "all_final_frames_pass": true, + "common_frame_ADDs": 24283, + "containment_pairs_checked": 2386, + "copies": 9, + "donor_intersections": 0, + "erasures": 9, + "max_inherited_integer_abs": 2, + "nested_MOVEs": 2911, + "new_frame_ids_collision": false, + "nondegeneracy_checked_by_separate_exact_bank_audit": true, + "old_max_frame_id": 635, + "paid_histogram": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "rank_mass": 5129, + "records": 27212, + "scope": "Independent chronological geometry/copy/source-owner audit. F2 all-column replay is in the separately freshly compiled transform receipt; address transform theorem and bank completion remain separate.", + "selected_helpers": 0, + "selected_pairs": 0, + "source_owner_intersections": 0, + "status": "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE" + }, + "stages": { + "11": { + "bridge_additions": 2664, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1549, + "fresh_center_copies": 99, + "global_live_registers": 1549, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24283, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24283, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + }, + { + "omit_bridge": 18, + "rejected": true + }, + { + "omit_bridge": 19, + "rejected": true + }, + { + "omit_bridge": 20, + "rejected": true + }, + { + "omit_bridge": 21, + "rejected": true + }, + { + "omit_bridge": 22, + "rejected": true + }, + { + "omit_bridge": 23, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9352086094409118902010547200", + "reverse_fresh_center_copies": 45, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1102740", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 267113, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 8 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 9 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 10 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "5": { + "bridge_additions": 666, + "copied_center_original_source_immutable": true, + "five_stage_additions": 121415, + "formal_columns_checked": 883, + "fresh_center_copies": 45, + "global_live_registers": 883, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24283, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24283, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9352086094409118902010547200", + "reverse_fresh_center_copies": 18, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1102740", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 4 + } + ], + "status": "PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + }, + "9": { + "bridge_additions": 1998, + "copied_center_original_source_immutable": true, + "formal_columns_checked": 1327, + "fresh_center_copies": 81, + "global_live_registers": 1327, + "independent_dirty_registers": 439, + "local_odd_scalar_additions": 24283, + "local_raw_H": [ + [ + 1, + 1323 + ], + [ + 2, + 1342 + ], + [ + 3, + 79 + ], + [ + 4, + 44 + ], + [ + 5, + 102 + ], + [ + 6, + 11 + ], + [ + 7, + 19 + ] + ], + "local_registers": 661, + "local_scalar_additions": 24283, + "negative_controls": [ + { + "omit_bridge": 0, + "rejected": true + }, + { + "omit_bridge": 1, + "rejected": true + }, + { + "omit_bridge": 2, + "rejected": true + }, + { + "omit_bridge": 3, + "rejected": true + }, + { + "omit_bridge": 4, + "rejected": true + }, + { + "omit_bridge": 5, + "rejected": true + }, + { + "omit_bridge": 6, + "rejected": true + }, + { + "omit_bridge": 7, + "rejected": true + }, + { + "omit_bridge": 8, + "rejected": true + }, + { + "omit_bridge": 9, + "rejected": true + }, + { + "omit_bridge": 10, + "rejected": true + }, + { + "omit_bridge": 11, + "rejected": true + }, + { + "omit_bridge": 12, + "rejected": true + }, + { + "omit_bridge": 13, + "rejected": true + }, + { + "omit_bridge": 14, + "rejected": true + }, + { + "omit_bridge": 15, + "rejected": true + }, + { + "omit_bridge": 16, + "rejected": true + }, + { + "omit_bridge": 17, + "rejected": true + } + ], + "new_Q_categories": [ + 28, + 29 + ], + "payload_prefix_bits": 93, + "payload_prefix_upper": "9352086094409118902010547200", + "reverse_fresh_center_copies": 36, + "scope": "All independent physical input columns over F2, including all arbitrary helper dirt, restored; external copied-center work closes to zero. New cohort scalar lift uses actual signed coefficients and computed cancellation-free bounds; unchanged source527 signed decoder remains separate defining evidence. Physical projector routing and paid rank/bank receipts are independently bound, not inferred from scalar check.", + "signed_lift_prefix": [ + { + "bits": 16, + "cancellation_free_signed_row_l1_upper": "49347", + "reverse": false + }, + { + "bits": 21, + "cancellation_free_signed_row_l1_upper": "1102740", + "reverse": true + } + ], + "signed_reverse_semantics": "Reverse ADD coefficient negated; reverse DISCARD is fresh COPY from recorded unchanged original center; reverse COPY is DISCARD. Each such block is inverse over every commutative coefficient ring, by elementary-shear induction.", + "stage_additions": 218547, + "stages": [ + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 0 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 1 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 2 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 3 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 4 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 5 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 6 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": true, + "stage": 7 + }, + { + "fresh_copies": 9, + "scalar_additions": 24283, + "signed_inverse": false, + "stage": 8 + } + ], + "status": "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" + } + } + } +} diff --git a/research/r439-frame272-seed06/NOTICE.md b/research/r439-frame272-seed06/NOTICE.md new file mode 100644 index 0000000000..8c4a082fcb --- /dev/null +++ b/research/r439-frame272-seed06/NOTICE.md @@ -0,0 +1,43 @@ +# Attribution and license + +This frame-272 contribution was prepared for GitHub contributor **woklerx** +with substantial **OpenAI Codex** assistance in research, implementation, +independent algorithmic checking, documentation and review. Delegated agents +remained within the one claimed frame. Independent implementations here do +not mean independent human peer review. New material is Apache-2.0, under the +repository license reproduced in `LICENSE`. + +The exact positive-transfer search, flat-matrix minimum check and full-word +verification approach adapt **Ross Richardson's PR925** (`r439-frame267-seed01`), +which in turn credits **mtpsl's PR691** R420 quad-13 method and earlier native +verification work. Source adaptation is marked in the code. This work changes +the mathematical object to frame 272 and adds a separate reverse-compatible +minimum, proved by an independent augmented-pair traversal. + +The PR589 bit word and tuning are by **DreamingOfClouds**, on **eumemic's PR555** +and the PR543/545/510 supplier lineage. The retained geometry/interface checker +is eumemic's, the scalar-record exporter is **Dylan Crow's**, with **Zhihao Chen** +and the native verification contributors credited by the original packages. +These inputs are consumed unchanged and pinned in `SOURCES.json`. + +The native runner's Windows/GCC compiler adapter follows concurrent **PR989**, +head `101103e56e3effdb268ce90110c6caa4c6885671`, with its source digest retained +in `native.py` and `NATIVE-ENVIRONMENT.json`. That runner credits **Krishnendu +Purohit (@Deftsalt-debug)**, **Ali Romman's PR688**, and **Ross Richardson's** +environment-reporting adaptation. We use the existing compiler and headers; +the mathematical checkers themselves are unchanged. + +Same-object comparisons credit **Gareth Davidson's PR904** four-wire rewriting, +**Ross Richardson's PR936** five-wire rewriting, and **Gareth Davidson's PR952** +six-wire Boolean search. Their accepted frame-272 circuits already reduced +23 gates to 18. Their exact local sources and the scope of our comparison +are retained in `OVERLAP.json`; their entire candidate words are not composed +or newly certified here. + +Concurrent **PR986** treats a different frame-281 transfer and its 12/13 +boundary. It is related independent research, not an input to this circuit; +we do not claim priority for the general reverse-admission distinction. + +The selected-bound context credits **Jonathan Capalbo's PR942** T37 composition +and its retained **Chafik Boukhalfa, Jeremy Kothe, Hao Yan**, supplier and review +lineage. That selected construction is not modified by this package. diff --git a/research/r439-frame272-seed06/OVERLAP.json b/research/r439-frame272-seed06/OVERLAP.json new file mode 100644 index 0000000000..b9124f412c --- /dev/null +++ b/research/r439-frame272-seed06/OVERLAP.json @@ -0,0 +1,981 @@ +{ + "format": "r439-frame272-overlap-v1", + "comparison_only": true, + "frame": 272, + "registers": [ + 242, + 294, + 296, + 302, + 316, + 501 + ], + "positive_transfer": [ + [ + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 1, + 3, + 2, + 2, + 3, + 1 + ], + [ + 1, + 3, + 3, + 2, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 3, + 1 + ], + [ + 1, + 4, + 3, + 3, + 4, + 1 + ], + [ + 0, + 1, + 1, + 1, + 1, + 1 + ] + ], + "versions": [ + { + "pr": 589, + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f", + "start": 725, + "stop": 748, + "adds": 23, + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 3, + 0 + ], + [ + 3, + 5 + ], + [ + 3, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 5 + ] + ], + "author": "DreamingOfClouds", + "head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46", + "reverse_positive_transfer": [ + [ + 27, + 3, + 12, + 6, + 5, + 26 + ], + [ + 5, + 1, + 2, + 1, + 1, + 5 + ], + [ + 10, + 1, + 5, + 2, + 2, + 10 + ], + [ + 7, + 1, + 3, + 2, + 1, + 7 + ], + [ + 4, + 0, + 2, + 1, + 1, + 4 + ], + [ + 26, + 3, + 12, + 6, + 5, + 27 + ] + ] + }, + { + "pr": 904, + "path": "research/r439-four-wire-prefix/candidate.json.gz", + "sha256": "9946eaacc69f05a91ad18ca16e57cd4f78db3e0d5b23939f691c96b4a4098a2f", + "start": 710, + "stop": 730, + "adds": 20, + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "author": "Gareth Davidson (@bitplane)", + "head": "883a0bdf7792693e57c16be660824b57aacfbe05", + "certificate_path": "research/r439-four-wire-prefix/CERTIFICATE.json", + "certificate_sha256": "e29dcde966ccfffdc83b25685729a59745e8c3938af8770a38d850e5e8fc7495", + "parent_frame_start": 725, + "selected_frame272_windows": [ + { + "frame": 272, + "new": [ + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ] + ], + "old": [ + [ + 1, + 0 + ], + [ + 1, + 3 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ] + ], + "registers": [ + 294, + 296, + 302, + 316 + ], + "saving": 1, + "section": "A", + "start": 733, + "stop": 737 + }, + { + "frame": 272, + "new": [ + [ + 1, + 3 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ] + ], + "old": [ + [ + 2, + 0 + ], + [ + 2, + 3 + ], + [ + 2, + 1 + ], + [ + 1, + 0 + ], + [ + 1, + 3 + ] + ], + "registers": [ + 242, + 296, + 302, + 501 + ], + "saving": 2, + "section": "A", + "start": 743, + "stop": 748 + } + ], + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 10, + 3, + 8, + 4, + 3, + 11 + ] + ] + }, + { + "pr": 936, + "path": "research/r439-five-wire-prefix/candidate.json.gz", + "sha256": "3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091", + "start": 695, + "stop": 713, + "adds": 18, + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "author": "Ross Richardson (@RossRichardson)", + "head": "0679fb6e1e4c91f573ae07ab1d0ea273b13c74e3", + "certificate_path": "research/r439-five-wire-prefix/CERTIFICATE.json", + "certificate_sha256": "6ce5015e9afc4db6d3742df433561ab9d1173b63f72da95178c76b6a0a973fea", + "parent_frame_start": 710, + "selected_frame272_windows": [ + { + "frame": 272, + "new": [ + [ + 4, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ], + [ + 4, + 1 + ] + ], + "old": [ + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 3 + ], + [ + 2, + 0 + ], + [ + 0, + 3 + ], + [ + 1, + 0 + ] + ], + "registers": [ + 294, + 296, + 302, + 316, + 501 + ], + "saving": 2, + "section": "A", + "start": 714, + "stop": 721 + } + ], + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 4, + 1, + 4, + 2, + 1, + 5 + ] + ] + }, + { + "pr": 952, + "path": "research/r439-six-wire-boolean/candidate.json.gz", + "sha256": "5c67c7949c07a89ea8394a936a155585d22e6b258997df73e36e7be47fc84cb0", + "start": 692, + "stop": 710, + "adds": 18, + "ops": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "author": "Gareth Davidson (@bitplane)", + "head": "11d24706f06e95271804c9438869546724c67aab", + "certificate_path": "research/r439-six-wire-boolean/CERTIFICATE.json", + "certificate_sha256": "aaa5f126fe0e4938df985c00bb47d1ce17da0eb8b20ae983813b66c02de07841", + "frame272_search_record": { + "distinct_programs": 1970, + "end": 713, + "frame": 272, + "guarded_programs": 0, + "new": null, + "nomination": null, + "old": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 3 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 5, + 2 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 2, + 0 + ], + [ + 3, + 2 + ] + ], + "saved_A": 0, + "shorter_programs": 670, + "start": 695, + "trials": 2880, + "wires": [ + 242, + 294, + 296, + 302, + 316, + 501 + ] + }, + "reverse_positive_transfer": [ + [ + 11, + 3, + 8, + 4, + 3, + 10 + ], + [ + 3, + 1, + 2, + 1, + 1, + 3 + ], + [ + 2, + 1, + 1, + 0, + 0, + 2 + ], + [ + 3, + 1, + 3, + 2, + 1, + 3 + ], + [ + 2, + 0, + 2, + 1, + 1, + 2 + ], + [ + 4, + 1, + 4, + 2, + 1, + 5 + ] + ] + } + ], + "scope": "Comparison of frame 272 only. All versions preserve its exact positive integer transfer. No prior whole-word circuit is imported, and no saving is claimed for composition with prior packages.", + "prior_result": "PR904 saves three forward gates, PR936 a further two; PR952 accepts no frame272 replacement and leaves 18 gates. Its bounded Boolean nominations do not prove a fixed positive-transfer minimum.", + "candidate_comparison": { + "adds": 12, + "reverse_positive_transfer": [ + [ + 1, + 1, + 2, + 0, + 1, + 0 + ], + [ + 1, + 1, + 2, + 1, + 1, + 1 + ], + [ + 0, + 1, + 1, + 0, + 0, + 0 + ], + [ + 1, + 1, + 3, + 2, + 1, + 1 + ], + [ + 0, + 0, + 2, + 1, + 1, + 0 + ], + [ + 0, + 1, + 2, + 0, + 1, + 1 + ] + ], + "by_prior": [ + { + "pr": 589, + "forward_add_saving": 11, + "paired_cleanup_add_saving": 22, + "reverse_entrywise_dominated": true, + "prior_cap_dominated_by_pr589": true + }, + { + "pr": 904, + "forward_add_saving": 8, + "paired_cleanup_add_saving": 16, + "reverse_entrywise_dominated": true, + "prior_cap_dominated_by_pr589": true + }, + { + "pr": 936, + "forward_add_saving": 6, + "paired_cleanup_add_saving": 12, + "reverse_entrywise_dominated": true, + "prior_cap_dominated_by_pr589": true + }, + { + "pr": 952, + "forward_add_saving": 6, + "paired_cleanup_add_saving": 12, + "reverse_entrywise_dominated": true, + "prior_cap_dominated_by_pr589": true + } + ], + "composition_claim": "Only local frame transfers and paired gate counts are compared. No complete prior candidate word was composed or replayed by this package." + } +} diff --git a/research/r439-frame272-seed06/PROOF.md b/research/r439-frame272-seed06/PROOF.md new file mode 100644 index 0000000000..065f3e03ee --- /dev/null +++ b/research/r439-frame272-seed06/PROOF.md @@ -0,0 +1,101 @@ +# Exact finite statement and complete local cost + +Let `P(g)` be the positive integer transfer of a sequence of operations +`row[d] += row[s]`, `d != s`, starting from the 6-by-6 identity. The six ordered +registers are `[242,294,296,302,316,501]`. Let `M` be `P` of the source-bound +PR589 phase-A slice `[725:748)`, and let `R` be `P` of that slice in reverse +order. Exact matrices are retained in `CERTIFICATE.json`. + +**Finite proposition.** Among sequences on these same six ordered registers +with no extra wires and positive transfer exactly `M`, the minimum length is +11. With the additional constraint `P(reverse(g)) <= R` entrywise, the minimum +length is 12. Repeated destinations, repeated donors and arbitrary interleaving +are permitted. The class does not fix a single-write order or a factor split. +It excludes circuits with a different positive transfer, extra wires, +subtraction gates and altered frames. + +## Why the exhaustive graph proves a minimum + +Every positive-addition circuit starts at identity and only increases entries, +so every intermediate matrix is entrywise at least identity. Removing its last +operation subtracts the source row from the destination row. Retain precisely +those predecessors that are still entrywise at least identity. Every circuit +therefore gives a path in this graph. Conversely a path to identity reverses to +a valid positive-addition circuit. Each subtraction strictly reduces total +entry mass, since the source row has a positive diagonal. The target has mass +66, so every backward path has length at most 60; sentinel 999 exceeds every +finite distance. The graph is finite without an empirical cutoff assumption. + +`search.py` exhausts the predecessor closure and uses a memoized distance +recurrence. `optimality.py` shares no nomination code or stored distances: it +stores flat matrices and performs breadth-first traversal. Identity first +appears at depth 11 after all earlier layers are complete. The explicit +unconstrained 11-gate witness independently gives the upper bound. + +For the reverse restriction, augment a state with a second matrix, initialized +at identity. Each last-gate removal is the next operation in the reversed +circuit, so apply that positive addition to the second matrix. Its entries +never decrease. If an entry exceeds `R`, no continuation can satisfy the +constraint. This is a valid monotone prune, not a heuristic. + +The independent checker explores these matrix pairs breadth first without +using the searcher's distance-to-identity pruning. It completely enumerates +all reachable admissible pairs through depth 11 and finds no identity first +component. Merging identical pairs is safe: all possible continuations depend +only on the two matrices, and a later visit to the same pair cannot give a +shorter accepted circuit. Together with the checked 12-gate witness this proves +the guarded minimum. Neither verifier reports a minimum on budget exhaustion. + +The final witness is selected under the tighter reversed-transfer cap of the +PR936 18-gate frame. That cap is itself no larger than `R`; the verifier checks +both comparisons directly. The baseline-cap exclusion of all lengths through +11 also excludes them under the tighter cap. Hence the 12-gate witness is +minimal under either of these two stated caps. + +## Substitution and accounting + +The literal witness, in local register indices and execution order, is: + +```text +(3,1), (1,4), (4,3), (5,4), (5,2), (1,5), +(0,4), (0,2), (1,0), (2,1), (4,2), (3,2). +``` + +Exact positive-transfer equality implies equality over F2 for every incoming +state; no helper is assumed zero. Since the replaced slice is contiguous, +all subsequent observations see the same values. Cleanup is rebuilt as the +literal full-frame reverse of all non-target-destination gates in A followed +by B. Elementary XOR gates are involutions, so that reverse restores arbitrary +source/helper dirt. The unchanged H1-H5 checker also validates the whole-word +interface, rather than relying on the local argument alone. + +Every original block register still touches the same frame. The verifier +compares all 661 ordered frame paths. No helper, allocation, frame change, +source access, COPY/ERASE, or recursive child is introduced. The complete +scalar invoice, including the required cleanup, is: + +| Charge | Original | Replacement | +|---|---:|---:| +| D ADDs | 18,085 | 18,085 | +| A ADDs | 2,130 | 2,119 | +| Scatter ADDs | 527 | 527 | +| B ADDs | 934 | 934 | +| C ADDs | 2,629 | 2,618 | +| **All ADDs** | **24,305** | **24,283** | +| MOVEs | 2,911 | 2,911 | +| COPY / ERASE pairs | 9 | 9 | +| Dirty helpers | 439 | 439 | +| Paid rank mass | 5,129 | 5,129 | + +The forward positive block endpoint is identical; its reversed endpoint is +entrywise smaller or equal. Within either positive block each coordinate is +monotone, so its endpoint bounds all its prefixes. Surrounding positive maps +preserve entrywise comparison. Thus the replacement does not increase the +inherited positive envelopes. This is a local algebraic preservation argument; +the package's emitted scalar records are also replayed explicitly. + +This result changes finite scalar work, not the paid recursive histogram or +the selected kappa. It does not supply a full hosted construction, an all-size +compiler, a new analytic transfer argument or a formal proof of multiplication. +Source/compiler, geometry, hosting, precision/tape and analytic assumptions +remain those of the pinned supplier. diff --git a/research/r439-frame272-seed06/README.md b/research/r439-frame272-seed06/README.md new file mode 100644 index 0000000000..0688433e49 --- /dev/null +++ b/research/r439-frame272-seed06/README.md @@ -0,0 +1,135 @@ +# R439 frame 272: a 12-ADD circuit and the cost of reverse domination + +**Finite bit-supplier construction and exact scoped minima; no new kappa.** +The complete phase-A frame-272 circuit of PR589 takes **23 ADDs**. This package +replaces it with **12**, including a literal reverse cleanup in the full word: +**24,305 -> 24,283 exported ADDs**. No helper, frame, copy, source-access operation +or recursive child is added. All 661 register frame paths and the paid rank +histogram are preserved. + +The exact minima expose a useful distinction. On the same six ordered wires, +the fixed positive integer transfer needs **11 ADDs** without a reverse guard, +but **12 ADDs** when its reversed positive transfer must be entrywise at most +the selected circuit's reversed transfer. Both lower bounds are independently +recomputed. This is a minimum in a stated finite circuit class, not unrestricted +XOR optimality or a proof of the full multiplication theorem. + +The research base is `407d52ff15b2217b6e22bce44728b4c3907b6515`. At that commit +the selected certificate is PR942/T37 with unchanged PR589 on PR555, conditional +`kappa = 1661960547713947/10^18 = 0.001661960547713947`. The exact supplier and +selected-source pins are in [SOURCES.json](SOURCES.json). Older frontiers in +dependency READMEs are historical. + +## Reproduce + +From the repository root, using Python 3.11+ and the standard library: + +```sh +python -I -B research/r439-frame272-seed06/verify.py +``` + +Expected final line: + +```text +PASS_R439_FRAME272 gates=23->12 native_adds=24305->24283 columns=661 rank_mass=5129 controls=9 +``` + +The command regenerates the bounded nomination, independently checks both +minima, reconstructs and verifies the full finite word, interprets the actual +exported records, and rejects nine mathematical mutations. The `native_adds` +field counts exported native-format records; it does not assert that a C++ +multistage checker ran. Use `--output /absolute/new/path` to keep both decoded +words and complete record streams. Existing output directories are refused. +The default uses a temporary directory and modifies no repository file. + +```sh +python -I -B research/r439-frame272-seed06/test_package.py -v +``` + +For the unchanged native legality and 5/9/11-stage checks, install no Python +dependencies; use an existing C++17 compiler and Boost headers: + +```sh +BOOST_INCLUDE=/path/to/boost CXX=c++ python -I -B research/r439-frame272-seed06/native.py +``` + +On Windows use an x64 Visual Studio developer shell, `CXX=cl`, and the same +Boost include-root setting. This freshly compiles the original checkers and +checks both complete words: **883 / 1,327 / 1,549 formal columns**, all **96 +omitted-bridge controls**, unchanged paid resources and nonincreasing positive +bounds. The expected final status is `PASS_R439_FRAME272_NATIVE`. Only elapsed +time and temporary stream paths are removed from the compared native receipts. + +`--write-certificate` explicitly regenerates only this package's certificate. +Gzip container bytes are not used to establish regenerated mathematical equality; +the receipt binds canonical decoded words and the actual record stream. + +## Evidence and comparison + +The object is exactly phase A `[725:748)`, frame 272, with physical registers +`[242,294,296,302,316,501]`. The original block is contiguous and has no external +observer. The replacement preserves its entire integer transfer on arbitrary +incoming values, hence its Boolean transfer on arbitrary helper dirt. + +The discovery graph exhausts **868,423 states / 5,005,248 edges**. A separate +flat-matrix breadth-first implementation adapted from PR925 reaches identity at depth 11 +after **798,401 states**, fully expanding depths 0 through 10. An independent +augmented pair-state traversal rules out every reverse-compatible circuit of +length at most 11 with **949,377 states**. The explicit 12-gate circuit supplies +the guarded upper bound. Budget exhaustion raises an error and cannot produce +an optimality receipt. See [PROOF.md](PROOF.md). + +Gareth Davidson's PR904 reduces this same frame from 23 to 20 gates; Ross +Richardson's PR936 reduces it further to 18. Gareth Davidson's PR952 leaves it +at 18 after 1,970 distinct nominations, of which 670 are shorter and none pass +its guards. All these versions have the same positive integer transfer. +[OVERLAP.json](OVERLAP.json) retains the actual prior windows and full local +gate lists, whose algebra is rechecked. Historical PR904/952 hashes and heads +are retained provenance metadata, not newly validated source bindings. The +PR589 word and PR936 comparison word are pinned and checked as execution inputs. +Our exhaustive fixed-transfer +class provides new evidence beyond those bounded window/Boolean searches. + +The final 12-gate circuit also has a reversed positive transfer dominated by +the prior 18-gate frame. Its local saving over that frame is six forward gates +and six cleanup gates. We replay the complete PR589-based word here, not a +composition with the complete PR936/PR952 candidates, and do not add their +whole-word savings to this package's result. + +## Scope and validation + +The original H1-H5 interface checker passes, including literal cleanup and all +661 dirty-input columns. An independent set-valued interpreter checks every +exported MOVE, ADD, COPY and ERASE, the nine copy lifecycles, final states and +paid rank mass 5,129. The 64 local Boolean inputs are also exhaustively checked. +The original forward integer transfer is unchanged and the reversed transfer +is entrywise dominated, so the corresponding positive prefix bounds carry over. + +The selected frontier is not changed. The C++ legality and 5/9/11-stage checks +pass locally on both words. This package does not execute the whole hosted +invoice, outer assembly, selected cold replay or full Lean theorem. +All inherited all-size/compiler, common-label and mutable +source realization, whole-call hosting, precision/tape, analytic transfer and +bit-interface obligations remain. [VALIDATION.md](VALIDATION.md) distinguishes +the checks actually run from those remaining. + +The final queue refresh also identified concurrent PR986's different frame-281 +12/13 boundary and PR989's four phase-B block composition. They are separate +objects and are credited without claiming priority for the general distinction +between scalar minima and reverse-envelope admission. The Windows native runner +adapts PR989's compiler interface at its exact recorded head. + +The first OS-random assignment was **6**, selecting the bit-supplier track; +`266 + (6 mod 60)` chose this phase-A frame. [CLAIM.json](CLAIM.json) records +three candidate tasks, scope and stopping rules. Live GitHub inspection found +no pinned coordination issue, so the claim was recorded locally. The final +overlap refresh is retained in [HANDOFF.json](HANDOFF.json). + +## Attribution + +Prepared for GitHub contributor **@woklerx** with substantial **OpenAI Codex** +assistance, including delegated circuit-search and verification agents. Ross +Richardson's PR925 supplies the predecessor exact-transfer and finite-verifier +method; Gareth Davidson's PR904/952 and Ross Richardson's PR936 supply the +explicit comparison circuits. See [NOTICE.md](NOTICE.md) for the retained +supplier and checker lineage. Apache-2.0. No independent human review is claimed. diff --git a/research/r439-frame272-seed06/SOURCES.json b/research/r439-frame272-seed06/SOURCES.json new file mode 100644 index 0000000000..74aa27ee5f --- /dev/null +++ b/research/r439-frame272-seed06/SOURCES.json @@ -0,0 +1,130 @@ +{ + "base_commit": "407d52ff15b2217b6e22bce44728b4c3907b6515", + "context_inputs": [ + "CONTRIBUTING.md", + "certificates/selected-result.json", + "docs/research/current-status.md", + "docs/research/pr-ledger.md", + "docs/research/community-batch952-review.md", + "research/community-frontier942-audit/ASSEMBLY.json", + "research/community-frontier942-audit/SELECTED-SOURCE.json", + "research/e8-bit-p111-tuned/tune/README.md", + "research/r439-frame267-seed01/search.py", + "research/r439-frame267-seed01/verify.py", + "research/r439-frame267-seed01/optimality.py", + "research/r439-frame267-seed01/PROOF.md", + "research/r439-frame267-seed01/native.py" + ], + "context_policy": "Historical orientation pins at base commit; only execution inputs are required by finite verifier. Native pins reserved for optional replay.", + "execution_inputs": [ + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "research/e8-bit-p111-tuned/code/xcheck_p.py", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py", + "research/r439-five-wire-prefix/candidate.json.gz" + ], + "files": { + "CONTRIBUTING.md": { + "git_blob": "acda5f534dd9e54eb80479cd15ccc12fafe39792", + "sha256": "1cae543effcabab91dab7f78423ee9283e60fb504f10848483d153331cd72bc4" + }, + "certificates/selected-result.json": { + "git_blob": "3d7529d77a5f22d8c6f64f98bd5a0e71b8eee892", + "sha256": "1d35283cb0ce3f8db1f285683933517f9e87475d295e2b6316399ad9928c81c3" + }, + "docs/research/community-batch952-review.md": { + "git_blob": "512ce9f18b32007bea71452eb5f3eb85c4d577ad", + "sha256": "04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b" + }, + "docs/research/current-status.md": { + "git_blob": "28925b5905e93e5d473916a3e236f1821b2d61d6", + "sha256": "9ef8355371d93f344e0462796d515d40a065c4f19534a8540b8d959b51a02aaa" + }, + "docs/research/pr-ledger.md": { + "git_blob": "91660fa11ad9a5a985274ba2d16f8219fdc09422", + "sha256": "53984538c660ecc35d09da30f9383d9731e21561e3d3d05d792e39dff1214f79" + }, + "research/community-frontier942-audit/ASSEMBLY.json": { + "git_blob": "9e71e9c1a1c1cbd1979f0c7bac87495322cbfad0", + "sha256": "4b2894956e594e408e111d806c842f2ed2c32aefcadff93fad69ff0b46f1991a" + }, + "research/community-frontier942-audit/SELECTED-SOURCE.json": { + "git_blob": "7bb22cec9e1150f81c2d695c73d9f5fe4c847f84", + "sha256": "1cd8dfde15919d1c3df9796b262e67898143d9793d2b86ee7b0a47fc903654c9" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp": { + "git_blob": "42bb232fbec4de703e70cc13dc2f39a3b43a3a01", + "sha256": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp": { + "git_blob": "82d69f7c5d044c9887c96b90c97f5639083ecd14", + "sha256": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63" + }, + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp": { + "git_blob": "cb1233c7e96b1aa8bbf4d2e4165d75ab0dca64b9", + "sha256": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3" + }, + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": { + "git_blob": "3632d370486a02f5456f7643ced03f8c925b2350", + "sha256": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3" + }, + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py": { + "git_blob": "f6d7afe3e623208c4207b6a683a1e3e49249e31c", + "sha256": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a" + }, + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h": { + "git_blob": "fc5664e929d9a81d9b4926bee049a93330be86ec", + "sha256": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99" + }, + "research/e8-bit-p111-tuned/code/xcheck_p.py": { + "git_blob": "184f5dcf94a486cc7db91ca4db5865916bf26009", + "sha256": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e" + }, + "research/e8-bit-p111-tuned/tune/README.md": { + "git_blob": "5b1554369682c8344d4f0767111d9b2b35eecbec", + "sha256": "46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d" + }, + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": { + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + "research/r439-five-wire-prefix/candidate.json.gz": { + "git_blob": "513cc674f2962973db5bfa41deafccc541b2aa6c", + "sha256": "3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091" + }, + "research/r439-frame267-seed01/PROOF.md": { + "git_blob": "ef5ece17981ae0174acca60c3e5cc921ce5f643f", + "sha256": "1592e55447e7d5bf0eb8d732d3fdba1d661f8539c137f719754b0b86828696b7" + }, + "research/r439-frame267-seed01/native.py": { + "git_blob": "7a8b5eeacb1784aa2090aa18139dcf10fa0c7e7f", + "sha256": "102a891ce20e43e309bd8ffe2ab5270c2897aedd95ab820dea39b162b6b71f6b" + }, + "research/r439-frame267-seed01/optimality.py": { + "git_blob": "93067b9df53cc28535e8d9a5c9dc1728c6bc8b16", + "sha256": "096422e0f5aec874461814de815df724a5bb10cf24d58e3145cc7fa1992c97ad" + }, + "research/r439-frame267-seed01/search.py": { + "git_blob": "48db43e1d70f1f3f056ac8b0dffbf9501cb2d567", + "sha256": "10eaa07ea45c791733e33bb04ee7c2587ae68c538db92ba22103879a5a7448c7" + }, + "research/r439-frame267-seed01/verify.py": { + "git_blob": "cb97be7c6c2d093345f9cdd81b7b16f6c7db5da9", + "sha256": "cd0bdd6981e7698c2a248ff8774cba7a4c4cad7c0e7482a493b088c309a3f44a" + } + }, + "native_inputs": [ + "research/e8-bit-carrier-skeleton/code/bit/regression/stage_cohort.py", + "research/e8-bit-carrier-skeleton/code/bit/checkers/legality_h.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/columns_k.cpp", + "research/e8-bit-carrier-skeleton/code/bit/checkers/json.hpp", + "research/e8-bit-carrier-skeleton/portable-include/bits/stdc++.h" + ], + "selected_kappa": "1661960547713947/1000000000000000000", + "selected_pr942_head": "1960cfa919a0945d0ca4cb14ea96237000037903", + "selected_source_binding": { + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": true, + "research/e8-bit-p111-tuned/code/xcheck_p.py": true, + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz": true + }, + "supplier_pr589_head": "a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46" +} diff --git a/research/r439-frame272-seed06/VALIDATION.md b/research/r439-frame272-seed06/VALIDATION.md new file mode 100644 index 0000000000..f67ab9c3cd --- /dev/null +++ b/research/r439-frame272-seed06/VALIDATION.md @@ -0,0 +1,50 @@ +# Executed validation and remaining obligations + +Executed on 2026-10-13 with CPython 3.14.5 (Windows x64), MSVC 19.51 and +Boost 1.88.0. `NATIVE-ENVIRONMENT.json` records compiler/header hashes and the +literal native commands. Regenerated gzip headers are excluded from +mathematical equality; exact hashes still bind immutable input archives. + +| Check | Observed result | +|---|---| +| Complete finite verifier, final witness | PASS, 66.010 seconds | +| Exact transfer minimum | 11; independent BFS 798,401 states | +| Exact reverse-compatible minimum | 12; independent exclusion 949,377 states | +| Whole PR589-based local word | 661 columns; H1-H5 and all interface conclusions pass | +| Literal exported instructions | ADDs 24,305 -> 24,283; 2,911 MOVEs; 9 COPY/ERASE pairs | +| Paid profile | Unchanged; rank mass 5,129 | +| Mathematical mutations | All 9 rejected | +| Package tests | 11 passed in 122.432 seconds | +| Fresh C++ legality | Both words pass source-owner, geometry and lifecycle checks | +| Fresh C++ 5/9/11-stage checks | Both words pass 883/1,327/1,549 formal columns | +| Omitted-bridge controls | All 96 rejected across both words | +| Selected-record integrity | `scripts/verify_selected_result.py` passes at recorded base | + +The package tests include a minimal offline copy with only four execution +inputs, in a path with spaces, under `python -I -O -B`; altered certificate and +source rejection; stale cleanup that is scalar-valid but violates H4; malformed +gate/wire and overlap-window rejection; incorrect minima and exhausted budgets; +and preservation of an existing output directory. Independent search receipts +are embedded in `CERTIFICATE.json`; the two small `INDEPENDENT-*.json` files +retain the same separately obtained lower-bound receipts. + +Initial nomination found an 11-gate word with a larger reverse map. It was not +presented as admitted. An exhaustive guarded search established the 12-gate +floor, and the final 12-gate ordering also meets the tighter PR936 reverse cap. +Both final verifier and native replay use that final source-bound ordering. +The earlier 12-gate ordering was checked during development but is not the +packaged witness. No failed receipt was edited into a pass. + +The submitted changes are confined to `research/r439-frame272-seed06/`. +`upstream/`, all consumed suppliers, the selected certificate and global +generators are unchanged. The repository-wide `make verify` and selected cold +replay were not run: this standalone research package does not replace their +inputs, GNU make was not available in the local Windows shell, and their +historical suites regenerate unrelated artifacts. The affected finite and +native checks above were run directly. Hosted Linux CI, a full hosted invoice, +outer assembly and the full Lean multiplication theorem are not claimed. + +All-size/compiler, physical realization, common-label/mutable-source, +whole-call hosting, precision/tape and analytic assumptions remain inherited. +The exact finite minima and executable evidence do not remove those obligations +or produce a new kappa. diff --git a/research/r439-frame272-seed06/WITNESS.json b/research/r439-frame272-seed06/WITNESS.json new file mode 100644 index 0000000000..fbf2746c1d --- /dev/null +++ b/research/r439-frame272-seed06/WITNESS.json @@ -0,0 +1,258 @@ +{ + "assignment_seed": 6, + "dead_end_distance": 999, + "distance_histogram": { + "0": 1, + "1": 13, + "10": 170901, + "11": 131522, + "12": 67957, + "13": 21526, + "14": 3592, + "15": 318, + "16": 24, + "17": 2, + "2": 113, + "3": 733, + "4": 3559, + "5": 13002, + "6": 36321, + "7": 75746, + "8": 122830, + "9": 162075, + "999": 58188 + }, + "edges": 5005248, + "frame": 272, + "minimum": 11, + "original": [ + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 1 + ], + [ + 0, + 4 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 1 + ], + [ + 5, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 4, + 0 + ], + [ + 4, + 5 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 1, + 0 + ], + [ + 1, + 5 + ], + [ + 3, + 0 + ], + [ + 3, + 5 + ], + [ + 3, + 2 + ], + [ + 2, + 0 + ], + [ + 2, + 5 + ] + ], + "overlap_selection": { + "found": true, + "length": 12, + "pr": 936, + "prunes": 100, + "states": 233, + "word_sha256": "3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091" + }, + "phase": "A", + "registers": [ + 242, + 294, + 296, + 302, + 316, + 501 + ], + "replacement": [ + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 4, + 3 + ], + [ + 5, + 4 + ], + [ + 5, + 2 + ], + [ + 1, + 5 + ], + [ + 0, + 4 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 2, + 1 + ], + [ + 4, + 2 + ], + [ + 3, + 2 + ] + ], + "reverse_guard": { + "attempts": [ + { + "found": false, + "length": 11, + "prunes": 11, + "states": 30 + }, + { + "found": true, + "length": 12, + "prunes": 0, + "states": 13 + } + ], + "found": true, + "minimum": 12, + "prunes": 11, + "states": 43 + }, + "start": 725, + "states": 868423, + "stop": 748, + "unconstrained_replacement": [ + [ + 3, + 2 + ], + [ + 3, + 1 + ], + [ + 1, + 4 + ], + [ + 4, + 3 + ], + [ + 5, + 4 + ], + [ + 1, + 5 + ], + [ + 0, + 4 + ], + [ + 1, + 0 + ], + [ + 4, + 1 + ], + [ + 3, + 1 + ], + [ + 2, + 1 + ] + ] +} diff --git a/research/r439-frame272-seed06/native.py b/research/r439-frame272-seed06/native.py new file mode 100644 index 0000000000..3d1aa2fb4a --- /dev/null +++ b/research/r439-frame272-seed06/native.py @@ -0,0 +1,194 @@ +#!/usr/bin/env python3 +"""Fresh native legality and 5/9/11-stage checks for the frame-272 replacement. + +Current frame-272 adaptation: GitHub @woklerx, substantial OpenAI Codex assistance. +The Windows compiler adapter is adapted from PR989 at +101103e56e3effdb268ce90110c6caa4c6885671, +research/r439-four-block-composition/native.py. That predecessor is +adapted from Krishnendu Purohit (@Deftsalt-debug)'s r439-block1-schedule/native.py, +which credits Ali Romman / PR688's r420-two-block-composition/native.py. +Environment reporting follows Ross Richardson's r439-frame524-seed13/native.py. +These predecessors and this contribution include substantial OpenAI Codex +assistance. Apache-2.0; original checker/exporter source notices are retained. + +Requires Python 3, a C++17 compiler and Boost headers; installs nothing. Linux: + BOOST_INCLUDE=/usr/include CXX=c++ python3 native.py --output /tmp/r439-native +Windows: run from an x64 Visual Studio developer shell with CXX=cl and set +BOOST_INCLUDE to the directory containing boost/multiprecision/cpp_int.hpp. +GCC/Clang are also supported. A literal compiler path containing spaces is valid. +Use --write-receipt once to save NATIVE.json and NATIVE-ENVIRONMENT.json; a normal +run independently regenerates all records and compares the mathematical receipt. +""" +import argparse +import importlib.util +import json +import os +from pathlib import Path +import platform +import shlex +import shutil +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +PREDECESSOR = {"pr": 989, "head": "101103e56e3effdb268ce90110c6caa4c6885671", + "path": "research/r439-four-block-composition/native.py", + "git_source_sha256": "bc8d7d09c4e47e7bdd6b758bd0593614e78448b0a849cd83ef150baee44daf04", + "observed_checkout_sha256": "387ac33c3b34f65604381ad21bda7780f1fbdf6154555cdfb0b6bd7b40ed18fa", + "checkout_difference": "Output encoding/newline and source-pin JSON hash normalization only; pinned-source conventions retained here."} +spec = importlib.util.spec_from_file_location("frame272_verifier", HERE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +def run(out, write): + pins = json.loads((HERE / "SOURCES.json").read_text()) + package = verify.ROOT / "research/e8-bit-carrier-skeleton" + bit = package / "code/bit" + checkers = bit / "checkers" + required = [p.relative_to(verify.ROOT).as_posix() for p in + (bit / "regression/stage_cohort.py", checkers / "legality_h.cpp", + checkers / "columns_k.cpp", checkers / "json.hpp", + package / "portable-include/bits/stdc++.h")] + verify.need(pins["native_inputs"] == required, "native input coverage mismatch") + for path in required: + verify.need(verify.sha((verify.ROOT / path).read_bytes()) == pins["files"][path]["sha256"], + "native source hash mismatch: " + path) + raw_compiler = os.environ.get("CXX", "c++") + compiler = ([raw_compiler] if Path(raw_compiler).is_file() else + shlex.split(raw_compiler, posix=os.name != "nt")) + if os.name == "nt": + compiler = [part.strip('"') for part in compiler] + verify.need(bool(compiler), "CXX must name a C++17 compiler") + executable = shutil.which(compiler[0]) + verify.need(executable is not None, "CXX compiler not found: " + compiler[0]) + boost = Path(os.environ.get("BOOST_INCLUDE", "/usr/include")).resolve() + boost_headers = [boost / "boost/version.hpp", boost / "boost/multiprecision/cpp_int.hpp"] + verify.need(all(p.is_file() for p in boost_headers), "Set BOOST_INCLUDE to a Boost header root") + local = out / "local" + local.mkdir() + verify.run(local, False) + certificate = json.loads((HERE / "CERTIFICATE.json").read_text()) + bindir = out / "bin" + bindir.mkdir() + msvc = Path(compiler[0]).stem.lower() in ("cl", "clang-cl") + includes = [package / "portable-include", checkers, boost] + definitions = ["HDIM=8", "NCOPY=9", "VPORTS=111", "RHELP=439"] + flags = (["/nologo", "/O2", "/std:c++17", "/EHsc"] if msvc else ["-O2", "-std=c++17"]) + flags += [("/D" if msvc else "-D") + x for x in definitions] + flags += [("/I" if msvc else "-I") + str(x) for x in includes] + commands = {} + + def call(name, command): + commands[name] = list(map(str, command)) + with (out / (name + ".log")).open("w") as log: + subprocess.run(commands[name], check=True, cwd=bindir, stdout=log, stderr=subprocess.STDOUT) + + def compile_checker(name, source, extra=()): + binary = bindir / (name + (".exe" if os.name == "nt" else "")) + output = ["/Fe:" + str(binary), "/Fo:" + str(bindir / (name + ".obj"))] if msvc else ["-o", binary] + call("compile-" + name, compiler + flags + list(extra) + output + [checkers / source]) + return binary + + def receipt(path): + data = json.loads(path.read_text()) + # Only execution time and the temporary absolute stream pathname vary. + data.pop("seconds", None) + data.pop("local_scalar_stream", None) + return data + + legality_binary = compile_checker("legality", "legality_h.cpp") + column_binaries = {pairs: compile_checker("columns" + str(pairs), "columns_k.cpp", + [("/D" if msvc else "-D") + "KPAIRS=" + str(pairs)]) for pairs in (2, 4, 5)} + results = {} + for name, additions in (("original", 24305), ("replacement", 24283)): + records = local / name / "records" + cin, cout = out / name / "cin", out / name / "cout" + call(name + "-cohort", [sys.executable, "-I", "-B", bit / "regression/stage_cohort.py", + records, records, cin, cout]) + call(name + "-legality", [legality_binary, cin, cout, cout / "legality.json"]) + legality = receipt(cout / "legality.json") + verify.need(legality["status"] == "PASS_INDEPENDENT_COHORT_LEGALITY_SOURCE_OWNERS_AND_LIFECYCLE", + "native legality did not pass") + verify.need(legality["rank_mass"] == 5129 and legality["copies"] == legality["erasures"] == 9 + and legality["common_frame_ADDs"] == additions, "native legality price mismatch") + results[name] = {"legality": legality, "stages": {}} + for pairs in (2, 4, 5): + path = cout / ("columns" + str(pairs) + ".json") + call(name + "-columns" + str(pairs), [column_binaries[pairs], cout / "COHORT249-RECORDS.bin", path]) + data = receipt(path) + status = ("PASS_NEW_COHORT249_ALL_FIVE_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL" if pairs == 2 else + "PASS_NEW_COHORT249_ALL_BRIDGED_STAGE_FORMAL_COLUMNS_AND_PREFIX_BILL") + verify.need(data["status"] == status, "native columns did not pass") + verify.need(data["formal_columns_checked"] == 222 * pairs + 439, "column coverage mismatch") + controls = data["negative_controls"] + verify.need(len(controls) == 6 * (pairs - 1) and all(c["rejected"] for c in controls), + "native bridge control failed") + expected = certificate["native_records"][name] + verify.need(data["local_scalar_additions"] == expected["adds"] == additions, + "native/Python count mismatch") + results[name]["stages"][str(2 * pairs + 1)] = data + for stages in ("5", "9", "11"): + old, new = (results[name]["stages"][stages] for name in ("original", "replacement")) + verify.need(old["local_raw_H"] == new["local_raw_H"] and + old["local_scalar_additions"] - new["local_scalar_additions"] == 22, + "native paid profile or saving mismatch") + verify.need(int(new["payload_prefix_upper"]) <= int(old["payload_prefix_upper"]), + "native prefix increased") + verify.need(int(new["payload_prefix_bits"]) <= int(old["payload_prefix_bits"]), + "native prefix bit count increased") + verify.need(len(old["signed_lift_prefix"]) == len(new["signed_lift_prefix"]) == 2, + "native signed prefix coverage mismatch") + for before, after in zip(old["signed_lift_prefix"], new["signed_lift_prefix"]): + verify.need(before["reverse"] == after["reverse"] and + int(after["cancellation_free_signed_row_l1_upper"]) <= + int(before["cancellation_free_signed_row_l1_upper"]) and + int(after["bits"]) <= int(before["bits"]), + "native signed prefix bound increased") + verify.need(new["copied_center_original_source_immutable"] is True, + "native copied center source changed") + old_legality, new_legality = (results[name]["legality"] for name in ("original", "replacement")) + for key in ("paid_histogram", "rank_mass", "copies", "erasures", "nested_MOVEs"): + verify.need(old_legality[key] == new_legality[key], "native legality resource changed: " + key) + verify.need(new_legality["max_inherited_integer_abs"] <= old_legality["max_inherited_integer_abs"], + "native inherited integer bound increased") + path = HERE / "NATIVE.json" + if write: + path.write_text(json.dumps(results, indent=2, sort_keys=True) + "\n", encoding="utf-8", newline="\n") + version = subprocess.run(compiler + (["/Bv"] if msvc else ["--version"]), + capture_output=True, text=True) + environment = {"runner_predecessor": PREDECESSOR, "python": sys.version, "python_executable": sys.executable, + "platform": platform.platform(), "compiler_command": compiler, + "compiler_path": str(Path(executable).resolve()), + "compiler_sha256": verify.sha(Path(executable).read_bytes()), + "compiler_version_output": version.stdout + version.stderr, + "boost_include": str(boost), + "boost_header_sha256": {str(p): verify.sha(p.read_bytes()) for p in boost_headers}, + "boost_version_header": boost_headers[0].read_text(), + "source_pins_canonical_sha256": verify.sha(verify.canonical( + json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")))), + "commands": commands} + (HERE / "NATIVE-ENVIRONMENT.json").write_text(json.dumps(environment, indent=2, sort_keys=True) + "\n", + encoding="utf-8", newline="\n") + else: + verify.need(results == json.loads(path.read_text()), "native receipt mismatch") + print("PASS_R439_FRAME272_NATIVE words=2 saving=22 stages=5,9,11 columns=883,1327,1549 bridge_controls=96") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="fresh directory for logs and execution artifacts") + parser.add_argument("--write-receipt", action="store_true") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve(), args.write_receipt) + else: + with tempfile.TemporaryDirectory(prefix="r439-frame272-native-") as temporary: + run(Path(temporary), args.write_receipt) + + +if __name__ == "__main__": + main() diff --git a/research/r439-frame272-seed06/optimality.py b/research/r439-frame272-seed06/optimality.py new file mode 100644 index 0000000000..52229c2340 --- /dev/null +++ b/research/r439-frame272-seed06/optimality.py @@ -0,0 +1,162 @@ +"""Independent exact minimum for a six-register positive ADD transfer. + +Flat-matrix method adapted from research/r439-frame267-seed01/optimality.py, +authored by Ross Richardson with substantial OpenAI Codex assistance (PR925), +Apache-2.0. Current frame-272 adaptation: @woklerx with substantial OpenAI +Codex assistance. It applies backward breadth-first enumeration with stricter +input validation and a hard state budget. The augmented reverse-prefix BFS +is new. Neither checker imports search.py or uses the searcher's recurrence, +gate nominations, or stored distances. + +Only gates r[d] += r[s], d != s, on these same six labelled registers are in +scope. Every forward intermediate matrix is entrywise at least the identity. +Removing a possible last gate therefore subtracts one whole row and retains +only matrices entrywise at least the identity. Every valid circuit reverses +to such a path, and every path to identity reverses to a valid circuit. Each +edge decreases the entry sum, so the graph is finite. Breadth-first distance +to identity proves the minimum without a single-write restriction. The claim +does not extend to XOR circuits with another positive transfer or extra wires. +""" + + +def check_minimum(matrix, claimed, *, max_states=1_000_000): + """Return a completed BFS receipt, or reject an incorrect/unproved claim. + + Budget exhaustion raises ValueError; it can never certify a minimum. + The 23-gate ceiling is the selected frame-272 baseline length. + """ + if type(claimed) is not int or not 0 <= claimed <= 23: + raise ValueError("invalid claimed distance") + if type(max_states) is not int or not 1 <= max_states <= 1_000_000: + raise ValueError("invalid state budget") + if not isinstance(matrix, (list, tuple)) or len(matrix) != 6: + raise ValueError("matrix shape") + if any(not isinstance(row, (list, tuple)) or len(row) != 6 for row in matrix): + raise ValueError("matrix shape") + if any(type(x) is not int or not 0 <= x <= 255 for row in matrix for x in row): + raise ValueError("matrix entries") + if any(matrix[i][i] < 1 for i in range(6)): + raise ValueError("matrix is not entrywise at least identity") + target = bytes(x for row in matrix for x in row) + identity = bytes(int(i == j) for i in range(6) for j in range(6)) + frontier, seen, layers = {target}, {target}, [1] + edges = 0 + for depth in range(claimed + 1): + if identity in frontier: + if depth != claimed: + raise ValueError("claimed minimum exceeds independent distance") + return { + "minimum": depth, + "layers": layers, + "visited_states": len(seen), + "edges_from_completed_layers": edges, + "completed_expansion_depths": list(range(depth)), + } + if depth == claimed: + raise ValueError("claimed minimum is below independent distance") + following = set() + for state in frontier: + for destination in range(0, 36, 6): + for source in range(0, 36, 6): + if destination == source: + continue + reduced = [] + for column in range(6): + entry = state[destination + column] - state[source + column] + if entry < int(column == destination // 6): + break + reduced.append(entry) + if len(reduced) != 6: + continue + edges += 1 + previous = state[:destination] + bytes(reduced) + state[destination + 6:] + if previous not in seen: + if len(seen) == max_states: + raise ValueError("independent state budget exceeded; no minimum certified") + seen.add(previous) + following.add(previous) + frontier = following + layers.append(len(frontier)) + if not frontier: + raise ValueError("target has no positive ADD factorization") + raise ValueError("unreachable") + + +def check_reverse_guard_exclusion(matrix, reverse_cap, through=11, *, max_states=1_000_000): + """Prove no factorization of length at most ``through`` meets the cap. + + A state stores both the remaining transfer and the accumulated positive + reverse prefix, as 72 bytes. Removing a last forward gate also appends the + first available reverse gate. The reverse prefix can only grow entrywise, + so any entry above reverse_cap makes every completion impossible. Apart + from this necessary condition, all legal last gates are enumerated. This + checker uses no distances, nominations, or recurrence from search.py. + + Reaching identity is a counterexample and raises ValueError. Exhausting + the budget also raises ValueError and is never reported as exclusion. + """ + if type(through) is not int or not 0 <= through <= 23: + raise ValueError("invalid exclusion depth") + if type(max_states) is not int or not 1 <= max_states <= 1_000_000: + raise ValueError("invalid state budget") + for value in (matrix, reverse_cap): + if not isinstance(value, (list, tuple)) or len(value) != 6: + raise ValueError("matrix shape") + if any(not isinstance(row, (list, tuple)) or len(row) != 6 for row in value): + raise ValueError("matrix shape") + if any(type(x) is not int or not 0 <= x <= 255 for row in value for x in row): + raise ValueError("matrix entries") + if any(value[i][i] < 1 for i in range(6)): + raise ValueError("matrix is not entrywise at least identity") + target = bytes(x for row in matrix for x in row) + cap = bytes(x for row in reverse_cap for x in row) + identity = bytes(int(i == j) for i in range(6) for j in range(6)) + start = target + identity + frontier, seen, layers = {start}, {start}, [1] + subtraction_edges = guard_prunes = 0 + completed = [] + for depth in range(through + 1): + if any(state[:36] == identity for state in frontier): + raise ValueError("reverse-compatible factorization exists at depth " + str(depth)) + if depth == through or not frontier: + return { + "excluded_gate_counts": list(range(through + 1)), + "layers": layers, + "visited_states": len(seen), + "valid_subtraction_edges": subtraction_edges, + "guard_pruned_edges": guard_prunes, + "completed_expansion_depths": completed, + } + following = set() + for state in frontier: + remaining, reverse = state[:36], state[36:] + for destination in range(0, 36, 6): + for source in range(0, 36, 6): + if destination == source: + continue + reduced = [] + for column in range(6): + entry = remaining[destination + column] - remaining[source + column] + if entry < int(column == destination // 6): + break + reduced.append(entry) + if len(reduced) != 6: + continue + subtraction_edges += 1 + extended = [reverse[destination + col] + reverse[source + col] + for col in range(6)] + if any(entry > cap[destination + col] for col, entry in enumerate(extended)): + guard_prunes += 1 + continue + next_remaining = remaining[:destination] + bytes(reduced) + remaining[destination + 6:] + next_reverse = reverse[:destination] + bytes(extended) + reverse[destination + 6:] + previous = next_remaining + next_reverse + if previous not in seen: + if len(seen) == max_states: + raise ValueError("independent state budget exceeded; no exclusion certified") + seen.add(previous) + following.add(previous) + completed.append(depth) + frontier = following + layers.append(len(frontier)) + raise ValueError("unreachable") diff --git a/research/r439-frame272-seed06/search.py b/research/r439-frame272-seed06/search.py new file mode 100644 index 0000000000..26f504bb20 --- /dev/null +++ b/research/r439-frame272-seed06/search.py @@ -0,0 +1,211 @@ +"""Exact nonnegative row-subtraction DAG for the one claimed frame272 transfer. + +This adaptation: GitHub @woklerx, substantial OpenAI Codex assistance. +Adapted from Ross Richardson's PR925 research/r439-frame267-seed01/search.py; +the predecessor also credits substantial OpenAI Codex assistance. Apache-2.0. +No search across frames, wires, integer transfers or general F2 circuits. +""" +import argparse +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path +import time + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = ROOT / 'research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz' +REGS = [242, 294, 296, 302, 316, 501] +IDENTITY = tuple(tuple(int(i == j) for j in range(6)) for i in range(6)) +STATE_LIMIT = 1_000_000 +PR936_WORD = ROOT / 'research/r439-five-wire-prefix/candidate.json.gz' +PR936_SHA256 = '3a11fc4675cd708316f9b0d398e0c3b73d626de0f824c5ed9b9c96279cfef091' +PR936_OPS = [[0, 2], [0, 3], [0, 1], [0, 4], [5, 3], [3, 1], + [1, 4], [2, 1], [5, 2], [4, 0], [4, 5], [4, 2], + [4, 3], [1, 0], [1, 5], [2, 5], [2, 0], [3, 2]] + + +def transfer(ops): + rows = list(IDENTITY) + for dst, src in ops: + rows[dst] = tuple(x + y for x, y in zip(rows[dst], rows[src])) + return tuple(rows) + + +def overlap_reverse_bound(target): + """Bind the stricter tie-break cap to Ross Richardson's exact PR936 word.""" + raw = PR936_WORD.read_bytes() + if hashlib.sha256(raw).hexdigest() != PR936_SHA256: + raise ValueError('PR936 comparison word changed') + word = json.loads(gzip.decompress(raw)) + segment = word['A'][695:713] + if len(segment) != 18 or any(f != 272 or len(ss) != 1 for f, _, ss in segment): + raise ValueError('PR936 comparison slice changed') + actual = [[REGS.index(dst), REGS.index(ss[0])] for _, dst, ss in segment] + if actual != PR936_OPS or transfer(actual) != target: + raise ValueError('PR936 comparison transfer changed') + return transfer(list(reversed(actual))) + + +def nominate(original): + target = transfer(original) + distances, choices = {}, {} + edges = 0 + states = 0 + infinity = 999 + started = time.monotonic() + + def distance(rows): + nonlocal edges, states + if rows in distances: + return distances[rows] + states += 1 + if states > STATE_LIMIT: + raise ValueError('state budget exceeded; no optimum established') + if states % 100000 == 0: + print(f'SEARCH_PROGRESS states={states} edges={edges} elapsed={time.monotonic()-started:.1f}s', flush=True) + if rows == IDENTITY: + distances[rows] = 0 + return 0 + best = infinity + for dst in range(6): + for src in range(6): + if dst == src or rows[dst][dst] - rows[src][dst] < 1: + continue + difference = tuple(x - y for x, y in zip(rows[dst], rows[src])) + if min(difference) < 0: + continue + previous = list(rows) + previous[dst] = difference + previous = tuple(previous) + edges += 1 + length = 1 + distance(previous) + if length < best: + best = length + choices[rows] = (dst, src, previous) + distances[rows] = best + return best + + minimum = distance(target) + if minimum >= infinity: + raise ValueError('no positive-addition factorization found') + backward, current = [], target + while current != IDENTITY: + dst, src, current = choices[current] + backward.append([dst, src]) + unconstrained_replacement = list(reversed(backward)) + reverse_bound = transfer(list(reversed(original))) + guard_states = 0 + guard_prunes = 0 + failures = set() + + def guarded(rows, reverse_rows, remaining): + nonlocal guard_states, guard_prunes + key = (rows, reverse_rows, remaining) + if key in failures: + return None + guard_states += 1 + if guard_states > STATE_LIMIT: + raise ValueError('reverse guard state budget exceeded; no guarded optimum established') + if rows == IDENTITY: + return [] if remaining == 0 else None + for dst in range(6): + for src in range(6): + if dst == src or rows[dst][dst] - rows[src][dst] < 1: + continue + difference = tuple(x - y for x, y in zip(rows[dst], rows[src])) + if min(difference) < 0: + continue + previous = list(rows) + previous[dst] = difference + previous = tuple(previous) + if distances[previous] > remaining - 1: + continue + next_reverse = tuple(x + y for x, y in zip(reverse_rows[dst], reverse_rows[src])) + if any(x > y for x, y in zip(next_reverse, reverse_bound[dst])): + guard_prunes += 1 + continue + next_reverse_rows = list(reverse_rows) + next_reverse_rows[dst] = next_reverse + suffix = guarded(previous, tuple(next_reverse_rows), remaining - 1) + if suffix is not None: + return [[dst, src]] + suffix + failures.add(key) + return None + + attempts = [] + guarded_backward = None + for length in range(minimum, len(original) + 1): + before = guard_states + before_prunes = guard_prunes + guarded_backward = guarded(target, IDENTITY, length) + attempts.append({'length': length, 'states': guard_states - before, + 'prunes': guard_prunes - before_prunes, + 'found': guarded_backward is not None}) + print(f'REVERSE_LENGTH {attempts[-1]}', flush=True) + if guarded_backward is not None: + break + if guarded_backward is not None: + backward = guarded_backward + print(f'REVERSE_GUARD states={guard_states} prunes={guard_prunes} found={guarded_backward is not None}', flush=True) + baseline_guard = {'states': guard_states, 'prunes': guard_prunes, + 'found': guarded_backward is not None, + 'minimum': len(backward) if guarded_backward is not None else None, + 'attempts': attempts} + # Baseline guarded minimality was proved above. Among words at that same + # length, choose one satisfying the stricter existing PR936 reverse cap. + # Reset the failed-state cache because its meaning depends on this cap. + stricter_bound = overlap_reverse_bound(target) + if any(a > b for row_a, row_b in zip(stricter_bound, reverse_bound) + for a, b in zip(row_a, row_b)): + raise ValueError('PR936 cap is not dominated by the baseline cap') + reverse_bound = stricter_bound + guard_states = guard_prunes = 0 + failures.clear() + stronger_backward = guarded(target, IDENTITY, len(backward)) + if stronger_backward is None: + raise ValueError('no PR936-dominated nominee at the baseline guarded minimum') + backward = stronger_backward + overlap_selection = {'pr': 936, 'word_sha256': PR936_SHA256, + 'length': len(backward), 'states': guard_states, + 'prunes': guard_prunes, 'found': True} + print(f'OVERLAP_SELECTION {overlap_selection}', flush=True) + return {'replacement': list(reversed(backward)), + 'unconstrained_replacement': unconstrained_replacement, 'minimum': minimum, + 'states': len(distances), 'edges': edges, + 'distance_histogram': {str(k): v for k, v in sorted(Counter(distances.values()).items())}, + 'dead_end_distance': infinity, + 'reverse_guard': baseline_guard, + 'overlap_selection': overlap_selection} + + +def original_ops(): + word = json.loads(gzip.decompress(WORD.read_bytes())) + segment = word['A'][725:748] + if len(segment) != 23 or any(f != 272 or len(ss) != 1 for f, _, ss in segment): + raise ValueError('source slice changed') + if (word['A'][724][0] == 272 or word['A'][748][0] == 272): + raise ValueError('source slice is not the complete frame') + return [[REGS.index(dst), REGS.index(ss[0])] for _, dst, ss in segment] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-witness', action='store_true') + args = parser.parse_args() + old = original_ops() + result = {'phase': 'A', 'start': 725, 'stop': 748, 'frame': 272, + 'registers': REGS, 'assignment_seed': 6, 'original': old, **nominate(old)} + path = HERE / 'WITNESS.json' + if args.write_witness: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + elif result != json.loads(path.read_text()): + raise ValueError('search witness mismatch') + print(f"PASS_FRAME272_SEARCH states={result['states']} edges={result['edges']} minimum={result['minimum']}") + for label, ops in [('original', old), ('replacement', result['replacement'])]: + print(label, 'forward', transfer(ops), 'reverse', transfer(list(reversed(ops)))) + + +if __name__ == '__main__': + main() diff --git a/research/r439-frame272-seed06/test_package.py b/research/r439-frame272-seed06/test_package.py new file mode 100644 index 0000000000..295b4d3423 --- /dev/null +++ b/research/r439-frame272-seed06/test_package.py @@ -0,0 +1,150 @@ +"""Defect-sensitive package checks; no theorem claim from unit tests. + +Adapted from research/r439-frame267-seed01/test_package.py. +Predecessor: Ross Richardson, substantial OpenAI Codex assistance. +This adaptation: @woklerx, substantial OpenAI Codex assistance; Apache-2.0. +""" +import copy +import gzip +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def load(name): + spec = importlib.util.spec_from_file_location(name, HERE / (name + '.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +class Package(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.verify = load('verify') + cls.optimality = load('optimality') + cls.recipe = json.loads((HERE / 'WITNESS.json').read_text()) + cls.word = json.loads(gzip.decompress((ROOT / cls.verify.WORD).read_bytes())) + + def test_boolean_gate_index_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['replacement'][0][0] = True + with self.assertRaisesRegex(self.verify.Reject, 'invalid circuit gate'): + self.verify.build(self.word, recipe) + + def test_self_add_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['replacement'][0] = [0, 0] + with self.assertRaisesRegex(self.verify.Reject, 'invalid circuit gate'): + self.verify.build(self.word, recipe) + + def test_negative_original_gate_index_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['original'][0][0] = -1 + with self.assertRaisesRegex(self.verify.Reject, 'invalid circuit gate'): + self.verify.build(self.word, recipe) + + def test_unconstrained_minimum_fails_reverse_guard(self): + recipe = copy.deepcopy(self.recipe) + recipe['replacement'] = recipe['unconstrained_replacement'] + self.assertEqual(self.verify.matrix(recipe['replacement'], True), + self.verify.matrix(recipe['original'], True)) + with self.assertRaisesRegex(self.verify.Reject, 'reverse positive matrix increased'): + self.verify.build(self.word, recipe) + + def test_overlap_window_corruption_rejected(self): + overlap = json.loads((HERE / 'OVERLAP.json').read_text()) + overlap['versions'][1]['selected_frame272_windows'][0]['old'][0].reverse() + with self.assertRaisesRegex(self.verify.Reject, 'overlap source window mismatch'): + self.verify.check_overlap(self.recipe, overlap) + + def test_wrong_wire_binding_rejected(self): + recipe = copy.deepcopy(self.recipe) + recipe['registers'][0] += 1 + with self.assertRaisesRegex(self.verify.Reject, 'unexpected circuit registers'): + self.verify.build(self.word, recipe) + + def test_missing_literal_cleanup_fails_h4(self): + new = self.verify.build(self.word, self.recipe) + spec = importlib.util.spec_from_file_location('owning_checker', ROOT / self.verify.AUDITOR) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + new['C'] = copy.deepcopy(self.word['C']) + checker = module.Word(new) + checker.full() # Identical scalar map: the stale inverse still restores. + hypotheses, _, _ = checker.interface() + self.assertFalse(hypotheses['H4_C_literal_reverse_at_full']) + + def test_independent_minimum_controls(self): + identity = [[int(i == j) for j in range(6)] for i in range(6)] + one = copy.deepcopy(identity) + one[0][1] = 1 + self.assertEqual(self.optimality.check_minimum(identity, 0)['minimum'], 0) + self.assertEqual(self.optimality.check_minimum(one, 1)['minimum'], 1) + with self.assertRaisesRegex(ValueError, 'below independent distance'): + self.optimality.check_minimum(one, 0) + with self.assertRaisesRegex(ValueError, 'exceeds independent distance'): + self.optimality.check_minimum(one, 2) + with self.assertRaisesRegex(ValueError, 'budget'): + self.optimality.check_minimum(one, 1, max_states=1) + + def test_independent_reverse_guard_controls(self): + identity = [[int(i == j) for j in range(6)] for i in range(6)] + one = copy.deepcopy(identity) + one[0][1] = 1 + with self.assertRaisesRegex(ValueError, 'factorization exists at depth 0'): + self.optimality.check_reverse_guard_exclusion(identity, identity, through=0) + with self.assertRaisesRegex(ValueError, 'factorization exists at depth 1'): + self.optimality.check_reverse_guard_exclusion(one, one, through=1) + receipt = self.optimality.check_reverse_guard_exclusion(one, identity, through=1) + self.assertEqual(receipt['excluded_gate_counts'], [0, 1]) + self.assertEqual(receipt['guard_pruned_edges'], 1) + with self.assertRaisesRegex(ValueError, 'budget'): + self.optimality.check_reverse_guard_exclusion(one, one, through=1, max_states=1) + + def test_existing_output_is_preserved(self): + with tempfile.TemporaryDirectory() as folder: + mark = Path(folder) / 'marker' + mark.write_text('keep') + run = subprocess.run([sys.executable, '-I', '-B', str(HERE / 'verify.py'), '--output', folder], + text=True, capture_output=True) + self.assertNotEqual(run.returncode, 0) + self.assertEqual(mark.read_text(), 'keep') + + def test_minimal_relocation_and_tampering(self): + with tempfile.TemporaryDirectory(prefix='frame272 path with spaces ') as folder: + root = Path(folder) + package = root / HERE.relative_to(ROOT) + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for relative in pins['execution_inputs']: + path = root / relative + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / relative, path) + command = [sys.executable, '-I', '-O', '-B', str(package / 'verify.py')] + passed = subprocess.run(command, text=True, capture_output=True) + self.assertEqual(passed.returncode, 0, passed.stdout + passed.stderr) + expected = package / 'CERTIFICATE.json' + data = json.loads(expected.read_text()) + data['independent_optimality']['layers'][1] -= 1 + expected.write_text(json.dumps(data)) + failed = subprocess.run(command, text=True, capture_output=True) + self.assertNotEqual(failed.returncode, 0) + self.assertIn('certificate mismatch', failed.stderr) + path = root / pins['execution_inputs'][0] + path.write_bytes(path.read_bytes() + b'corruption') + failed = subprocess.run(command, text=True, capture_output=True) + self.assertNotEqual(failed.returncode, 0) + self.assertIn('source hash mismatch', failed.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/r439-frame272-seed06/verify.py b/research/r439-frame272-seed06/verify.py new file mode 100644 index 0000000000..33bf6e8d7a --- /dev/null +++ b/research/r439-frame272-seed06/verify.py @@ -0,0 +1,429 @@ +"""Exact finite frame-272 replacement, minimum and native-word checks; no new rate claim. + +Adapted from research/r439-frame267-seed01/verify.py by Ross Richardson, +which credits mtpsl PR691; supplier auditor by eumemic and exporter by Dylan Crow. +This adaptation: @woklerx with substantial OpenAI Codex assistance. Apache-2.0. +Python 3.10+, standard library only. No assertions are used for acceptance. +""" +import argparse +from collections import Counter +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import struct +import subprocess +import sys +import tempfile + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +AUDITOR = "research/e8-bit-p111-tuned/code/xcheck_p.py" +EXPORTER = "research/e8-bit-carrier-skeleton/code/bit/export_records.py" +COMPARISON_WORD = "research/r439-five-wire-prefix/candidate.json.gz" + + +class Reject(Exception): + pass + + +def need(condition, reason): + if not condition: + raise Reject(reason) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def matrix(ops, positive=False): + need(isinstance(ops, list) and all(isinstance(g, list) and len(g) == 2 for g in ops), "invalid gate list") + # Each column is evolved separately; search.py evolves whole rows. + cols = [] + for j in range(6): + values = [int(i == j) for i in range(6)] + for d, s in ops: + need(type(d) is int and type(s) is int and 0 <= d < 6 and + 0 <= s < 6 and d != s, "invalid circuit gate") + values[d] = values[d] + values[s] if positive else values[d] ^ values[s] + cols.append(values) + return [list(r) for r in zip(*cols)] + + +def circuit_check(old, new): + need(matrix(old) == matrix(new), "circuit F2 map changed") + positive = {} + for direction, a, b in (("forward", old, new), ("reverse", old[::-1], new[::-1])): + before, after = matrix(a, True), matrix(b, True) + need(all(y <= x for rr, ss in zip(before, after) for x, y in zip(rr, ss)), + direction + " positive matrix increased") + positive[direction] = {"original": before, "replacement": after} + return positive + + +def cleanup(w): + return [[1, d, list(ss)] for _, d, ss in reversed(w["A"] + w["B"]) + if not 111 <= d < 222] + + +def build(base, recipe): + need((recipe["phase"], recipe["start"], recipe["stop"], recipe["frame"]) + == ("A", 725, 748, 272), "unexpected circuit location") + regs = recipe["registers"] + need(regs == [242, 294, 296, 302, 316, 501], "unexpected circuit registers") + matrix(recipe["original"]) # Reject malformed indices before binding physical wires. + original = [[272, regs[d], [regs[s]]] for d, s in recipe["original"]] + need(base["A"][725:748] == original, "original gate slice mismatch") + pos = circuit_check(recipe["original"], recipe["replacement"]) + need(pos["forward"]["original"] == pos["forward"]["replacement"], "integer forward map changed") + need(0 < len(recipe["replacement"]) < 23, "no strict circuit improvement") + out = copy.deepcopy(base) + out["A"][725:748] = [[272, regs[d], [regs[s]]] for d, s in recipe["replacement"]] + out["C"] = cleanup(out) + return out + + +def check_overlap(recipe, overlap=None): + """Replay the transcribed prior local windows, not their complete search packages. + + Archive/certificate hashes in OVERLAP.json identify the comparison sources; + this routine checks the algebra and composition of their displayed windows. + """ + if overlap is None: + overlap = json.loads((HERE / "OVERLAP.json").read_text()) + regs = recipe["registers"] + need(overlap["format"] == "r439-frame272-overlap-v1" and overlap["comparison_only"] is True + and overlap["frame"] == 272 and overlap["registers"] == regs, "overlap identity mismatch") + positive = matrix(recipe["original"], True) + need(overlap["positive_transfer"] == positive, "overlap positive transfer mismatch") + versions = overlap["versions"] + need([v["pr"] for v in versions] == [589, 904, 936, 952], "overlap source order changed") + need([v["adds"] for v in versions] == [23, 20, 18, 18], "overlap gate counts changed") + previous = copy.deepcopy(recipe["original"]) + reverse_comparisons = [] + replacement_reverse = matrix(recipe["replacement"][::-1], True) + baseline_reverse = matrix(recipe["original"][::-1], True) + for index, version in enumerate(versions): + need(version["stop"] - version["start"] == version["adds"] == len(version["ops"]), + "overlap slice length mismatch") + if index in (1, 2): + origin = version["parent_frame_start"] + need(origin == versions[index - 1]["start"], "overlap parent coordinates mismatch") + upper = len(previous) + for window in sorted(version["selected_frame272_windows"], + key=lambda x: x["start"], reverse=True): + lo, hi = window["start"] - origin, window["stop"] - origin + need(window["frame"] == 272 and window["section"] == "A" + and 0 <= lo < hi <= upper, "invalid overlap window") + upper = lo + wires = window["registers"] + need(len(set(wires)) == len(wires) and set(wires) <= set(regs), + "invalid overlap wire binding") + mapped = {} + for name in ("old", "new"): + ops = window[name] + need(all(isinstance(g, list) and len(g) == 2 and + all(type(r) is int and 0 <= r < len(wires) for r in g) + and g[0] != g[1] for g in ops), "invalid overlap gate") + mapped[name] = [[regs.index(wires[d]), regs.index(wires[s])] for d, s in ops] + need(previous[lo:hi] == mapped["old"] + and len(mapped["old"]) - len(mapped["new"]) == window["saving"], + "overlap source window mismatch") + previous[lo:hi] = mapped["new"] + need(previous == version["ops"], "overlap composed circuit mismatch") + need(matrix(previous, True) == positive, "overlap integer map mismatch") + previous_reverse = matrix(previous[::-1], True) + if "reverse_positive_transfer" in version: + need(version["reverse_positive_transfer"] == previous_reverse, + "overlap reverse transfer mismatch") + increases = [{"row": i, "column": j, "prior": previous_reverse[i][j], + "replacement": replacement_reverse[i][j]} + for i in range(6) for j in range(6) + if replacement_reverse[i][j] > previous_reverse[i][j]] + reverse_comparisons.append({"pr": version["pr"], "dominated": not increases, + "increased_entries": increases, + "prior_cap_dominated_by_pr589": + all(previous_reverse[i][j] <= baseline_reverse[i][j] + for i in range(6) for j in range(6))}) + record = versions[-1]["frame272_search_record"] + need(record["old"] == previous and record["frame"] == 272 and record["wires"] == regs + and record["new"] is None and record["nomination"] is None + and record["saved_A"] == record["guarded_programs"] == 0, + "PR952 overlap scope mismatch") + if "candidate_comparison" in overlap: + candidate = overlap["candidate_comparison"] + expected = [{"pr": version["pr"], + "forward_add_saving": len(version["ops"]) - len(recipe["replacement"]), + "paired_cleanup_add_saving": 2 * (len(version["ops"]) - len(recipe["replacement"])), + "reverse_entrywise_dominated": comparison["dominated"], + "prior_cap_dominated_by_pr589": comparison["prior_cap_dominated_by_pr589"]} + for version, comparison in zip(versions, reverse_comparisons)] + need(candidate["adds"] == len(recipe["replacement"]) + and candidate["reverse_positive_transfer"] == replacement_reverse + and candidate["by_prior"] == expected, "overlap candidate comparison mismatch") + need(all(row["dominated"] and row["prior_cap_dominated_by_pr589"] + for row in reverse_comparisons), "prior reverse cap comparison failed") + return {"sources": overlap, "this_frame272_adds": len(recipe["replacement"]), + "frame_local_gate_count_difference_vs_pr936_with_cleanup": + 2 * (len(previous) - len(recipe["replacement"])), + "reverse_comparisons": reverse_comparisons, + "composition_claim": "No complete shortened prior word composed; full-word replay uses PR589 only"} + + +def paths(w): + result = [[f] for f in w["start"]] + for sec in ("D", "A", "B", "C"): + for f, d, ss in w[sec]: + for r in [d] + ss: + if result[r][-1] != f: + result[r].append(f) + for r, f in enumerate(w["final"]): + if result[r][-1] != f: + result[r].append(f) + return result + + +def audit(w, module, geometry): + # Geometry is unchanged; reuse the baseline's already checked exact spaces. + obj = copy.copy(geometry) + obj.w = w + result = obj.full() + h, c, _ = obj.interface() + need(all(h.values()) and all(c.values()), "interface H1-H5 or decomposition failed") + need(result["columns"] == 661, "incomplete dirty-column replay") + result["interface_hypotheses"] = h + result["interface_conclusions"] = c + return result + + +def records_check(directory, word): + """Independent set-valued interpreter of the actual exported instructions. + + This checks the scalar projection and literal MOVE/COPY/ERASE lifecycle, + not the multistage formal-column or hosted-recursion contracts. + """ + raw = (directory / "249-records.bin").read_bytes() + need(len(raw) % 24 == 0, "truncated record") + records = list(struct.iter_unpack("<6i", raw)) + dim = {int(k): v["dim"] for k, v in + json.loads((directory / "frames.json").read_text())["frames"].items()} + frames = list(word["start"]) + [None] + values = [{i} for i in range(661)] + [set()] + pths = [[f] for f in frames[:661]] + hist, counts, adds_by_phase = Counter(), Counter(), Counter() + for op, a, b, c, d, e in records: + counts[op] += 1 + if op == 0: + need(0 <= a < 661 and b in dim and c in dim and frames[a] == b + and dim[c] - dim[b] == d and d > 0 and e == 0, + "bad MOVE") + need(set(word["frames"][b]) <= set(word["frames"][c]), "MOVE not nested") + frames[a] = c + pths[a].append(c) + hist[d] += 1 + elif op == 1: + need(0 <= a < 661 and 0 <= b <= 661 and a != b and c == 1 + and d in dim and frames[a] == frames[b] == d and e in (1, 2, 3, 4, 5), + "bad ADD frame") + adds_by_phase[e] += 1 + values[a] = values[a].symmetric_difference(values[b]) + elif op == 2: + need(0 <= a < 661 and b == 661 and not values[b] and frames[b] is None + and c in dim and frames[a] == c, + "COPY lifecycle") + need(d == 0 and e == dim[c], "COPY rank") + values[b] = set(values[a]) + frames[b] = d + hist[e] += 1 + elif op == 3: + need(0 <= a < 661 and b == 661 and frames[a] == c and frames[b] == d == 0 + and e == 0 and values[b] == values[a], "ERASE lifecycle") + values[b] = set() + frames[b] = None + else: + raise Reject("unknown record opcode") + expected = [{i} if not 111 <= i < 222 else {i, i - 111} for i in range(661)] + need(values[:661] == expected and not values[661], "record dirty-column endpoint") + need(frames[:661] == word["final"] and frames[661] is None, "record frame endpoint") + need(pths == paths(word), "record frame paths differ") + return {"records": len(records), "adds": counts[1], "moves": counts[0], + "adds_by_phase": dict(sorted(adds_by_phase.items())), + "copies": counts[2], "erasures": counts[3], + "paid_histogram": dict(sorted(hist.items())), + "rank_mass": sum(k * v for k, v in hist.items()), + "records_sha256": sha(raw)} + + +def rejected(label, fn, exceptions): + try: + fn() + except exceptions: + return label + raise Reject("negative control accepted: " + label) + + +def run(output, write_certificate): + pins = json.loads((HERE / "SOURCES.json").read_text()) + need(set(pins["execution_inputs"]) == {WORD, AUDITOR, EXPORTER, COMPARISON_WORD}, + "incomplete execution source pins") + for path in pins["execution_inputs"]: + pin = pins["files"][path] + need(sha((ROOT / path).read_bytes()) == pin["sha256"], "source hash mismatch: " + path) + base = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + need(base["v"] == 111 and base["R"] == 439 and len(base["start"]) == 661, "word dimensions") + recipe = json.loads((HERE / "WITNESS.json").read_text()) + spec_search = importlib.util.spec_from_file_location("nomination", HERE / "search.py") + search = importlib.util.module_from_spec(spec_search) + spec_search.loader.exec_module(search) + found = search.nominate(search.original_ops()) + expected_recipe = {"phase": "A", "start": 725, "stop": 748, "frame": 272, + "registers": search.REGS, "assignment_seed": 6, + "original": search.original_ops(), **found} + need(recipe == expected_recipe, "nomination metadata or witness mismatch") + # BFS checker evolves flat matrices and does not import nomination code. + spec_opt = importlib.util.spec_from_file_location("independent_minimum", HERE / "optimality.py") + opt = importlib.util.module_from_spec(spec_opt) + spec_opt.loader.exec_module(opt) + optimum = opt.check_minimum(matrix(recipe["original"], True), recipe["minimum"]) + need(recipe["minimum"] == len(recipe["unconstrained_replacement"]) == 11, + "wrong unconstrained witness length") + need(matrix(recipe["unconstrained_replacement"], True) == matrix(recipe["original"], True), + "unconstrained witness integer map mismatch") + need(recipe["reverse_guard"]["minimum"] == len(recipe["replacement"]) == 12, + "wrong guarded witness length") + guarded = opt.check_reverse_guard_exclusion(matrix(recipe["original"], True), + matrix(recipe["original"][::-1], True), through=11) + revised = build(base, recipe) + overlap = check_overlap(recipe) + positive = circuit_check(recipe["original"], recipe["replacement"]) + need(positive["forward"]["original"] == positive["forward"]["replacement"], + "integer forward map changed") + need(paths(base) == paths(revised), "physical frame path changed") + + spec = importlib.util.spec_from_file_location("predecessor_xcheck", ROOT / AUDITOR) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + geometry, labels, baseline, h, c, _ = module.check(base) + need(all(h.values()) and all(c.values()), "baseline interface failed") + revised_audit = audit(revised, module, geometry) + + # Independent exhaustive evaluation of the six-register Boolean map. + for bits in range(64): + endings = [] + for gates in (recipe["original"], recipe["replacement"]): + value = bits + for d, s in gates: + value ^= ((value >> s) & 1) << d + endings.append(value) + need(endings[0] == endings[1], "exhaustive six-bit map differs") + + evidence = {} + for name, word in (("original", base), ("replacement", revised)): + path = output / (name + ".json.gz") + path.write_bytes(gzip.compress(canonical(word), mtime=0)) + directory = output / name / "records" + subprocess.run([sys.executable, "-B", str(ROOT / EXPORTER), str(path), str(directory)], + check=True, capture_output=True, text=True) + evidence[name] = records_check(directory, word) + a, b = evidence["original"], evidence["replacement"] + saving = 2 * (23 - len(recipe["replacement"])) + need(a["adds"] == 24305 and b["adds"] == 24305 - saving, "unexpected native ADD count") + for key in ("moves", "copies", "erasures", "paid_histogram", "rank_mass"): + need(a[key] == b[key], "native cost changed: " + key) + need(b["rank_mass"] == 5129 and b["copies"] == 9, "incorrect native cost") + + controls = [] + fail = (Reject, module.Reject) + controls.append(rejected("drop circuit gate", lambda: circuit_check( + recipe["original"], recipe["replacement"][1:]), fail)) + wrong = copy.deepcopy(recipe["replacement"]) + wrong[0].reverse() + controls.append(rejected("reverse circuit operand", lambda: circuit_check( + recipe["original"], wrong), fail)) + inflated = recipe["replacement"] + [[0, 1], [0, 1]] + need(matrix(inflated) == matrix(recipe["replacement"]), "inflation control is not F2-neutral") + controls.append(rejected("F2-neutral positive-cost inflation", lambda: circuit_check( + recipe["original"], inflated), fail)) + bad = copy.deepcopy(revised) + bad["C"].pop() + controls.append(rejected("dropped cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["C"] = copy.deepcopy(base["C"]) + # Same endpoint but not the literal reverse required by H4. + obj = copy.copy(geometry) + obj.w = bad + obj.full() + controls.append(rejected("nonliteral original cleanup", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["A"][725][0] = 0 + controls.append(rejected("illegal lower frame", lambda: audit(bad, module, geometry), fail)) + bad = copy.deepcopy(revised) + bad["D"][0][2].pop() + controls.append(rejected("missing dirty compensation", lambda: audit(bad, module, geometry), fail)) + + # The record endpoint checker must see literal instruction corruption too. + directory = output / "replacement" / "records" + rawpath = directory / "249-records.bin" + raw = rawpath.read_bytes() + recs = list(struct.iter_unpack("<6i", raw)) + for i, rec in enumerate(recs): + if rec[0] == 1 and rec[5] == 2 and rec[4] == 272: + rawpath.write_bytes(raw[:24*i] + raw[24*(i+1):]) + break + else: + raise Reject("no exported frame272 ADD found for control") + try: + controls.append(rejected("dropped exported frame272 ADD", lambda: records_check(directory, revised), fail)) + finally: + rawpath.write_bytes(raw) + erased = next(i for i, rec in enumerate(recs) if rec[0] == 3) + rawpath.write_bytes(raw[:24*erased] + raw[24*(erased+1):]) + try: + controls.append(rejected("dropped exported ERASE", lambda: records_check(directory, revised), fail)) + finally: + rawpath.write_bytes(raw) + + cert = {"status": "PASS_R439_FRAME272", "frame": 272, "old_gates": 23, "new_gates": len(recipe["replacement"]), + "saved_with_cleanup": saving, "labels": labels, "columns": revised_audit["columns"], + "old_phase_gates": baseline["gates"], "new_phase_gates": revised_audit["gates"], + "interface_hypotheses": revised_audit["interface_hypotheses"], + "interface_conclusions": revised_audit["interface_conclusions"], + "boolean_inputs": 64, "F2_matrix": matrix(recipe["replacement"]), + "positive_matrices": positive, "native_records": evidence, + "physical_frame_paths_sha256": sha(canonical(paths(revised))), + "reconstructed_word_sha256": sha(canonical(revised)), "controls_rejected": controls, + "independent_optimality": optimum, "independent_guard_exclusion": guarded, + "guarded_minimum": 12, "overlap_comparison": overlap, + "kappa_claim": "none; unchanged paid rank profile, no hosted replay"} + path = HERE / "CERTIFICATE.json" + if write_certificate: + path.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n") + else: + need(canonical(cert) == canonical(json.loads(path.read_text())), "certificate mismatch") + print(f"PASS_R439_FRAME272 gates=23->{len(recipe['replacement'])} " + f"native_adds=24305->{b['adds']} columns=661 rank_mass=5129 controls={len(controls)}") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="new directory for reconstructed word and records") + parser.add_argument("--write-certificate", action="store_true", help="regenerate this package's certificate") + args = parser.parse_args() + if args.output: + args.output.mkdir(parents=True, exist_ok=False) + run(args.output.resolve(), args.write_certificate) + else: + with tempfile.TemporaryDirectory(prefix="r439-frame272-") as temporary: + run(Path(temporary), args.write_certificate) + + +if __name__ == "__main__": + main()