From 4fa24646a038b788a62771356305fd6fb8f9ddd5 Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 00:51:55 +1100 Subject: [PATCH 1/2] Add exact joint Horner circuits for PR799 backward frames --- research/x4-joint-horner-seed29/CLAIM.json | 37 + research/x4-joint-horner-seed29/EXPECTED.json | 1689 +++++++++++++++++ research/x4-joint-horner-seed29/OVERLAP.json | 658 +++++++ research/x4-joint-horner-seed29/PROOF.md | 160 ++ research/x4-joint-horner-seed29/README.md | 164 ++ research/x4-joint-horner-seed29/SOURCES.json | 26 + research/x4-joint-horner-seed29/VALIDATION.md | 99 + .../x4-joint-horner-seed29/independent.py | 200 ++ research/x4-joint-horner-seed29/joint.py | 105 + .../x4-joint-horner-seed29/test_package.py | 152 ++ research/x4-joint-horner-seed29/verify.py | 348 ++++ 11 files changed, 3638 insertions(+) create mode 100644 research/x4-joint-horner-seed29/CLAIM.json create mode 100644 research/x4-joint-horner-seed29/EXPECTED.json create mode 100644 research/x4-joint-horner-seed29/OVERLAP.json create mode 100644 research/x4-joint-horner-seed29/PROOF.md create mode 100644 research/x4-joint-horner-seed29/README.md create mode 100644 research/x4-joint-horner-seed29/SOURCES.json create mode 100644 research/x4-joint-horner-seed29/VALIDATION.md create mode 100644 research/x4-joint-horner-seed29/independent.py create mode 100644 research/x4-joint-horner-seed29/joint.py create mode 100644 research/x4-joint-horner-seed29/test_package.py create mode 100644 research/x4-joint-horner-seed29/verify.py diff --git a/research/x4-joint-horner-seed29/CLAIM.json b/research/x4-joint-horner-seed29/CLAIM.json new file mode 100644 index 0000000000..72fd5c7c8b --- /dev/null +++ b/research/x4-joint-horner-seed29/CLAIM.json @@ -0,0 +1,37 @@ +{ + "assignment_seed": 29, + "randomness": "secrets.randbelow(100), operating-system randomness", + "track": "complex supplier", + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "started_utc": "2026-10-13T13:21:25Z", + "expected_finish_utc": "2026-10-13T14:01:25Z", + "verification_reserved_from_utc": "2026-10-13T13:51:25Z", + "candidates": [ + { + "task": "SW4 read exchange / frame rescheduling", + "decision": "Not selected: #775, #815, #864, #876, #910 already cover nearby classes." + }, + { + "task": "Eight-register raw factory resynthesis", + "decision": "Not selected: #681, #922, #924 and #931 cover direct, fused, scale-gauge and butterfly classes." + }, + { + "task": "Joint two-source Horner preparation for adjacent same-target additions in nonzero frames of X4 backward", + "decision": "Selected: differs from within-macro signed/Horner searches and frame-zero source/target grouping." + } + ], + "object": "native/local/LOCAL-PROGRAMS.json.gz:backward in research/community-frontier799-audit/integrated799-replay.tar.gz", + "method": "Enumerate adjacent same-target, different-source ADD pairs with equal nonzero frame; build one two-source binary Horner word; choose disjoint profitable pairs by exact path dynamic programming. Seed 29 selects backward orientation and deterministic tie-breaking. Retain arbitrary private input, source restoration, final work clear and every source read. Check exact full scalar projection and prefix/grid bounds.", + "deliverable": "One finite circuit research package with exact source pins, deterministic receipt, complete bounded candidate census, proof, adverse controls and full backward scalar replay; no new kappa.", + "coordination": { + "pinned_issues": [], + "open_issues": [ + 650, + 913 + ], + "mode": "local claim; no pinned coordination issue available", + "open_pr_count": 722, + "latest_observed_pr": 932 + }, + "status": "claimed" +} diff --git a/research/x4-joint-horner-seed29/EXPECTED.json b/research/x4-joint-horner-seed29/EXPECTED.json new file mode 100644 index 0000000000..1e3ae64c16 --- /dev/null +++ b/research/x4-joint-horner-seed29/EXPECTED.json @@ -0,0 +1,1689 @@ +{ + "baseline": { + "all_formal_columns": 737, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_envelope_peak": "48299247699832632898063/16", + "primitive_stream_sha256": "9678c323b5ce7879e71d71445491067ac9b386103847696f5597756eba5f7dc7", + "real_nonwork_source_reads": 39446, + "real_operand_reads": 146392, + "real_primitive_tags": { + "add": 20516, + "clear": 36728, + "copy": 23856, + "double": 13892, + "halve": 28456, + "negate": 1296, + "subtract": 18930 + }, + "real_primitives": 143674, + "retained_horner_real_primitives": 193210, + "retained_payload_bits": 192, + "scalar_fractional_depth": 19, + "scalar_macros_charged": 19197, + "scalar_prefix_row_l1": "5338828" + }, + "candidate": { + "all_formal_columns": 737, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_envelope_peak": "48299247699832632898063/16", + "primitive_stream_sha256": "94bfbdca745148705eaa3009bb4e362fe8b41e1243a549124a2a4b926acfa1ce", + "real_nonwork_source_reads": 39446, + "real_operand_reads": 136492, + "real_primitive_tags": { + "add": 19888, + "clear": 33556, + "copy": 20684, + "double": 9348, + "halve": 26272, + "negate": 1296, + "subtract": 19558 + }, + "real_primitives": 130602, + "retained_horner_real_primitives": 193210, + "retained_payload_bits": 192, + "scalar_fractional_depth": 19, + "scalar_macros_charged": 19197, + "scalar_prefix_row_l1": "5338828" + }, + "candidates": 6112, + "census_sha256": "1ad06bdc7b48f86ce6c4ad95a37685957344f70b3c4c816c9b38b7ea73862ce8", + "conservative_local_recount": { + "adapters_retained": 380784, + "after": 9875380343082, + "before": 9875380343098, + "compiler": 25934336, + "saving": 16, + "scope": "arithmetic recount only; no global invoice admission" + }, + "controls": { + "event": 11045, + "rejected": [ + "delete_primitive_0", + "delete_primitive_1", + "delete_primitive_2", + "delete_primitive_3", + "delete_primitive_4", + "wrong_source_sign", + "wrong_frame", + "cross_non_scalar", + "nondyadic", + "zero", + "aliased_sources", + "endpoint_neutral_cost_inflation" + ] + }, + "dp_sha256": "07a1cd64b3c39338f2d55b3af24a922dbae2fc4283c6e39a90ee0a396566bc0b", + "non_scalar_events_sha256": "a802da12c169920c03a2625d8c50015c09c91d2fafeb14ec5c4a6213f3cd358e", + "orientation": "backward", + "orientation_maximum_after": 143658, + "orientation_maximum_before": 143674, + "profitable_candidates": 2764, + "saving_real_primitives": 13072, + "scope": "finite scalar construction; no new kappa", + "selected_events": [ + 7281, + 9519, + 9521, + 9526, + 9528, + 9737, + 9739, + 9744, + 9746, + 9955, + 9957, + 9962, + 9964, + 10173, + 10175, + 10180, + 10182, + 10391, + 10393, + 10398, + 10400, + 10609, + 10611, + 10616, + 10618, + 10827, + 10829, + 10834, + 10836, + 11045, + 11047, + 11052, + 11054, + 11263, + 11265, + 11270, + 11272, + 11481, + 11483, + 11488, + 11490, + 11699, + 11701, + 11706, + 11708, + 11917, + 11919, + 11924, + 11926, + 12135, + 12137, + 12142, + 12144, + 12353, + 12355, + 12360, + 12362, + 12814, + 12816, + 12851, + 12862, + 12864, + 12872, + 12874, + 12915, + 12917, + 12919, + 12921, + 12923, + 12925, + 12927, + 12929, + 12932, + 12935, + 12937, + 12939, + 12941, + 12943, + 12945, + 12947, + 12949, + 12951, + 12953, + 12955, + 12957, + 12959, + 12961, + 12963, + 12969, + 12971, + 12973, + 12975, + 12977, + 12979, + 12981, + 12986, + 12988, + 12990, + 12992, + 12994, + 13000, + 13006, + 13008, + 13010, + 13012, + 13014, + 13020, + 13025, + 13031, + 13033, + 13035, + 13037, + 13039, + 13043, + 13047, + 13049, + 13051, + 13053, + 13055, + 13057, + 13060, + 13064, + 13066, + 13068, + 13070, + 13072, + 13074, + 13078, + 13082, + 13084, + 13086, + 13088, + 13090, + 13092, + 13095, + 13099, + 13101, + 13103, + 13105, + 13111, + 13121, + 13123, + 13125, + 13127, + 13129, + 13131, + 13135, + 13139, + 13141, + 13143, + 13145, + 13147, + 13149, + 13151, + 13153, + 13155, + 13157, + 13159, + 13161, + 13163, + 13165, + 13233, + 13275, + 13279, + 13282, + 13291, + 13295, + 13298, + 13307, + 13311, + 13314, + 13387, + 13391, + 13394, + 18164, + 18171, + 18174, + 18206, + 18209, + 18211, + 18214, + 18217, + 18221, + 18229, + 18233, + 18235, + 18245, + 18259, + 18288, + 18351, + 18355, + 18359, + 18368, + 18372, + 18376, + 18385, + 18389, + 18393, + 18402, + 18406, + 18410, + 18519, + 18527, + 18542, + 18546, + 18548, + 18550, + 18556, + 18558, + 18564, + 18566, + 18573, + 18595, + 18625, + 18627, + 18629, + 18653, + 18655, + 18663, + 18667, + 18672, + 18679, + 18700, + 18703, + 18705, + 18724, + 18726, + 18729, + 18737, + 18739, + 18745, + 18751, + 18761, + 18763, + 18766, + 18771, + 18776, + 18778, + 18780, + 18788, + 18792, + 18794, + 18809, + 18819, + 18821, + 18824, + 18836, + 18839, + 18843, + 18845, + 18847, + 18852, + 18856, + 18861, + 18868, + 18872, + 18894, + 18902, + 18909, + 18922, + 18925, + 18927, + 18930, + 18935, + 18937, + 18940, + 18945, + 18952, + 18954, + 18959, + 18964, + 18966, + 18970, + 18975, + 18978, + 18988, + 18990, + 18994, + 18996, + 18998, + 19001, + 19018, + 19020, + 19022, + 19024, + 19036, + 19039, + 19042, + 19044, + 19046, + 19049, + 19060, + 19065, + 19067, + 19071, + 19073, + 19075, + 19083, + 19111, + 19113, + 19119, + 19125, + 19128, + 19130, + 19142, + 19144, + 19147, + 19149, + 19156, + 19163, + 19167, + 19173, + 19176, + 19189, + 19193, + 19195, + 19197, + 19199, + 19209, + 19231, + 19235, + 19241, + 19250, + 19252, + 19254, + 19256, + 19259, + 19261, + 19263, + 19265, + 19267, + 19269, + 19278, + 19280, + 19282, + 19284, + 19286, + 19288, + 19290, + 19292, + 19295, + 19297, + 19299, + 19301, + 19303, + 19305, + 19307, + 19314, + 19316, + 19318, + 19320, + 19324, + 19328, + 19330, + 19332, + 19361, + 19369, + 19373, + 19376, + 19378, + 19382, + 19389, + 19393, + 19400, + 19403, + 19414, + 19427, + 19429, + 19441, + 19443, + 19447, + 19456, + 19458, + 19464, + 19466, + 19468, + 19470, + 19472, + 19480, + 19482, + 19485, + 19491, + 19494, + 19502, + 19513, + 19515, + 19520, + 19524, + 19531, + 19536, + 19538, + 19540, + 19542, + 19544, + 19547, + 19560, + 19563, + 19573, + 19575, + 19577, + 19583, + 19588, + 19593, + 19596, + 19598, + 19602, + 19606, + 19610, + 19613, + 19615, + 19617, + 19619, + 19623, + 19646, + 19648, + 19650, + 19652, + 19654, + 19659, + 19662, + 19664, + 19666, + 19668, + 19672, + 19674, + 19676, + 19678, + 19680, + 19684, + 19686, + 19706, + 19708, + 19711, + 19713, + 19715, + 19734, + 19738, + 19742, + 19746, + 19750, + 19752, + 19755, + 19757, + 19760, + 19762, + 19765, + 19767, + 19769, + 19771, + 19773, + 19775, + 19780, + 19831, + 19833, + 19837, + 19839, + 19841, + 19843, + 19845, + 19852, + 19854, + 19856, + 19858, + 19861, + 19863, + 19867, + 19880, + 19889, + 19891, + 19893, + 19896, + 19898, + 19900, + 19905, + 19907, + 19910, + 19912, + 19915, + 19917, + 19919, + 19921, + 19923, + 19925, + 19927, + 19931, + 19933, + 19936, + 19938, + 19942, + 19944, + 19946, + 19949, + 19951, + 19953, + 19955, + 19957, + 19962, + 19983, + 19988, + 19990, + 19993, + 20001, + 20003, + 20019, + 20021, + 20023, + 20042, + 20044, + 20046, + 20049, + 20052, + 20054, + 20061, + 20063, + 20065, + 20072, + 20080, + 20087, + 20089, + 20091, + 20093, + 20095, + 20097, + 20111, + 20113, + 20115, + 20121, + 20128, + 20135, + 20137, + 20139, + 20141, + 20143, + 20146, + 20148, + 20153, + 20158, + 20160, + 20162, + 20164, + 20167, + 20169, + 20173, + 20203, + 20207, + 20209, + 20211, + 20213, + 20215, + 20217, + 20219, + 20225, + 20227, + 20229, + 20234, + 20236, + 20242, + 20244, + 20246, + 20248, + 20250, + 20252, + 20254, + 20256, + 20258, + 20261, + 20263, + 20306, + 20309, + 20316, + 20325, + 20327, + 20331, + 20333, + 20335, + 20337, + 20339, + 20360, + 20366, + 20368, + 20370, + 20372, + 20374, + 20376, + 20378, + 20380, + 20382, + 20385, + 20387, + 20389, + 20391, + 20395, + 20402, + 20404, + 20409, + 20411, + 20413, + 20415, + 20417, + 20419, + 20441, + 20443, + 20445, + 20447, + 20452, + 20454, + 20456, + 20459, + 20461, + 20464, + 20466, + 20489, + 20491, + 20493, + 20495, + 20497, + 20499, + 20501, + 20503, + 20505, + 20507, + 20509, + 20511, + 20516, + 20572, + 20575, + 20577, + 20579, + 20581, + 20583, + 20585, + 20589, + 20607, + 20613, + 20615, + 20617, + 20620, + 20622, + 20625, + 20627, + 20629, + 20631, + 20633, + 20641, + 20664, + 20668, + 20671, + 20673, + 20675, + 20677, + 20679, + 20681, + 20683, + 20685, + 20688, + 20690, + 20692, + 20694, + 20706, + 20708, + 20710, + 20712, + 20717, + 20730, + 20732, + 20734, + 20737, + 20740, + 20742, + 20746, + 20755, + 20763, + 20765, + 20768, + 20770, + 20781, + 20786, + 20791, + 20793, + 20798, + 20802, + 20805, + 20807, + 20809, + 20812, + 20814, + 20819, + 20821, + 20823, + 20825, + 20827, + 20829, + 20831, + 20837, + 20839, + 20841, + 20843, + 20846, + 20848, + 20863, + 20866, + 20872, + 20874, + 20876, + 20883, + 20891, + 20893, + 20896, + 20898, + 20906, + 20908, + 20910, + 20912, + 20914, + 20918, + 20922, + 20931, + 20943, + 20945, + 20947, + 20950, + 20957, + 20967, + 20970, + 20972, + 20974, + 20981, + 20983, + 20985, + 20988, + 20990, + 20992, + 20994, + 21004, + 21006, + 21008, + 21010, + 21012, + 21014, + 21017, + 21019, + 21021, + 21024, + 21026, + 21029, + 21041, + 21044, + 21056, + 21068, + 21070, + 21075, + 21078, + 21080, + 21082, + 21088, + 21090, + 21092, + 21100, + 21102, + 21104, + 21106, + 21108, + 21110, + 21112, + 21114, + 21116, + 21118, + 21120, + 21122, + 21124, + 21134, + 21136, + 21163, + 21169, + 21171, + 21174, + 21176, + 21178, + 21180, + 21183, + 21201, + 21208, + 21210, + 21212, + 21214, + 21216, + 21218, + 21220, + 21222, + 21224, + 21226, + 21228, + 21230, + 21267, + 21269, + 21280, + 21284, + 21286, + 21288, + 21290, + 21296, + 21300, + 21306, + 21308, + 21310, + 21312, + 21314, + 21316, + 21318, + 21320, + 21322, + 21329, + 21331, + 21339, + 21341, + 21344, + 21346, + 21351, + 21359, + 21361, + 21365, + 21374, + 21376, + 21378, + 21380, + 21382, + 21384, + 21391, + 21393, + 21395, + 21398, + 21406, + 21408, + 21410, + 21412, + 21414, + 21416, + 21418, + 21420, + 21424, + 21427, + 21430, + 21432, + 21434, + 21436, + 21438, + 21440, + 21442, + 21444, + 21446, + 21448, + 21450, + 21484, + 21486, + 21488, + 21490, + 21498, + 21500, + 21505, + 21539, + 21544, + 21547, + 21570, + 21574, + 21576, + 21578, + 21581, + 21586, + 21588, + 21590, + 21592, + 21594, + 21596, + 21599, + 21611, + 21621, + 21634, + 21638, + 21644, + 21648, + 21650, + 21657, + 21661, + 21663, + 21665, + 21667, + 21669, + 21671, + 21674, + 21676, + 21678, + 21684, + 21692, + 21699, + 21701, + 21703, + 21706, + 21708, + 21715, + 21735, + 21737, + 21755, + 21759, + 21761, + 21763, + 21767, + 21772, + 21776, + 21781, + 21787, + 21789, + 21792, + 21795, + 21799, + 21801, + 21803, + 21805, + 21807, + 21812, + 21819, + 21826, + 21828, + 21837, + 21839, + 21841, + 21843, + 21845, + 21847, + 21849, + 21851, + 21853, + 21855, + 21857, + 21859, + 21861, + 21864, + 21867, + 21869, + 21873, + 21883, + 21887, + 21889, + 21915, + 21922, + 21925, + 21928, + 21931, + 21934, + 21936, + 21947, + 21951, + 21953, + 21956, + 21958, + 21960, + 21962, + 21964, + 21971, + 21973, + 21976, + 21978, + 21981, + 21989, + 21991, + 21999, + 22001, + 22004, + 22006, + 22016, + 22018, + 22020, + 22025, + 22032, + 22045, + 22047, + 22052, + 22057, + 22065, + 22067, + 22069, + 22071, + 22077, + 22079, + 22082, + 22086, + 22092, + 22094, + 22098, + 22100, + 22102, + 22109, + 22111, + 22116, + 22120, + 22122, + 22126, + 22135, + 22144, + 22147, + 22149, + 22160, + 22162, + 22164, + 22170, + 22181, + 22187, + 22196, + 22198, + 22200, + 22209, + 22211, + 22215, + 22224, + 22226, + 22228, + 22245, + 22279, + 22282, + 22304, + 22307, + 22309, + 22311, + 22313, + 22315, + 22317, + 22319, + 22321, + 22324, + 22327, + 22329, + 22331, + 22359, + 22361, + 22364, + 22370, + 22372, + 22374, + 22376, + 22386, + 22460, + 22463, + 22465, + 22470, + 22472, + 22474, + 22476, + 22480, + 22482, + 22485, + 22487, + 22489, + 22494, + 22498, + 22500, + 22503, + 22506, + 22508, + 22511, + 22513, + 22516, + 22518, + 22520, + 22522, + 22532, + 22534, + 22536, + 22543, + 22548, + 22552, + 22557, + 22559, + 22561, + 22564, + 22567, + 22569, + 22571, + 22573, + 22578, + 22580, + 22584, + 22589, + 22591, + 22595, + 22598, + 22600, + 22605, + 22607, + 22609, + 22613, + 22615, + 22617, + 22619, + 22621, + 22627, + 22630, + 22638, + 22640, + 22646, + 22669, + 22673, + 22675, + 22701, + 22703, + 22705, + 22711, + 22716, + 22732, + 22738, + 22741, + 22743, + 22745, + 22747, + 22749, + 22751, + 22755, + 22758, + 22760, + 22762, + 22766, + 22774, + 22776, + 22778, + 22795, + 22799, + 22802, + 22805, + 22807, + 22810, + 22818, + 22826, + 22831, + 22833, + 22835, + 22839, + 22841, + 22844, + 22847, + 22849, + 22851, + 22853, + 22855, + 22859, + 22862, + 22864, + 22866, + 22868, + 22870, + 22874, + 22876, + 22879, + 22881, + 22883, + 22885, + 22887, + 22890, + 22892, + 22896, + 22898, + 22900, + 22902, + 22905, + 22907, + 22909, + 22911, + 22915, + 22918, + 22920, + 22922, + 22924, + 22926, + 22928, + 22930, + 22932, + 22934, + 22936, + 22938, + 22940, + 22942, + 22944, + 22946, + 22948, + 22950, + 22952, + 22954, + 22958, + 22976, + 22983, + 22989, + 22999, + 23007, + 23015, + 23019, + 23024, + 23035, + 23061, + 23068, + 23070, + 23072, + 23077, + 23080, + 23082, + 23085, + 23088, + 23093, + 23095, + 23097, + 23099, + 23101, + 23104, + 23107, + 23116, + 23125, + 23127, + 23134, + 23136, + 23138, + 23140, + 23145, + 23147, + 23150, + 23152, + 23159, + 23161, + 23163, + 23170, + 23172, + 23177, + 23180, + 23182, + 23184, + 23186, + 23188, + 23190, + 23192, + 23194, + 23203, + 23205, + 23209, + 23220, + 23222, + 23224, + 23226, + 23228, + 23245, + 23249, + 23251, + 23253, + 23255, + 23257, + 23261, + 23263, + 23267, + 23271, + 23273, + 23276, + 23280, + 23283, + 23287, + 23289, + 23292, + 23294, + 23297, + 23299, + 23301, + 23303, + 23305, + 23322, + 23326, + 23328, + 23330, + 23332, + 23334, + 23336, + 23338, + 23340, + 23342, + 23344, + 23346, + 23365, + 23378, + 23381, + 23387, + 23389, + 23391, + 23394, + 23397, + 23399, + 23401, + 23406, + 23408, + 23410, + 23412, + 23414, + 23416, + 23418, + 23420, + 23422, + 23424, + 23426, + 23428, + 23430, + 23432, + 23435, + 23437, + 23440, + 23443, + 23445, + 23447, + 23450, + 23452, + 23454, + 23456, + 23458, + 23460, + 23462, + 23464, + 23466, + 23468, + 23470, + 23473, + 23475, + 23479, + 23481, + 23483, + 23486, + 23488, + 23490, + 23492, + 23494, + 23496, + 23500, + 23517, + 23523, + 23525, + 23527, + 23529, + 23531, + 23534, + 23538, + 23541, + 23543, + 23545, + 23548, + 23550, + 23553, + 23557, + 23559, + 23561, + 23563, + 23565, + 23568, + 23570, + 23572, + 23574, + 23576, + 23578, + 23580, + 23582, + 23584, + 23586, + 23588, + 23590, + 23593, + 23597, + 23599, + 23601, + 23604, + 23606, + 23609, + 23611, + 23613, + 23616, + 23619, + 23622, + 23624, + 23626, + 23628, + 23630, + 23632, + 23637, + 23639, + 23641, + 23643, + 23645, + 23649, + 23654, + 23657, + 23660, + 23662, + 23665, + 23667, + 23670, + 23672, + 23675, + 23678, + 23680, + 23685, + 23688, + 23690, + 23692, + 23694, + 23696, + 23699, + 23701, + 23704, + 23706, + 23709, + 23713, + 23717, + 23719, + 23721, + 23723, + 23725, + 23727, + 23729, + 23731, + 23733, + 23735, + 23737, + 23743, + 23745, + 23747, + 23749, + 23751, + 23753, + 23755, + 23757, + 23759, + 23766, + 23768, + 23770, + 23772, + 23774, + 23776, + 23779, + 23781, + 23783, + 23785, + 23787, + 23790, + 23793, + 23795, + 23798, + 23801, + 23803, + 23806, + 23808, + 23810, + 23812, + 23814, + 23816, + 23818, + 23820, + 23822, + 23824, + 23827, + 23829, + 23831, + 23833, + 23836, + 23839, + 23841, + 23843, + 23845, + 23847, + 23849, + 23851, + 23853, + 23855, + 23857, + 23859, + 23861, + 23863, + 23865, + 23867, + 23869, + 23871, + 23873, + 23876, + 23878, + 23880, + 23882, + 23884, + 23889, + 23891, + 23894, + 23896, + 23898, + 23900, + 23902, + 23904, + 23906, + 23908, + 23910, + 23912, + 23914, + 23917, + 23919, + 23921, + 23923, + 23925, + 23927, + 23929, + 23931, + 23933, + 23937, + 23940, + 23942, + 23944, + 23946, + 23948, + 23953, + 23955, + 23957, + 23959, + 23961, + 23964, + 23966, + 23968, + 23970, + 23972, + 23975, + 23977, + 23980, + 23982, + 23984, + 23986, + 23988, + 23990, + 23992, + 23994, + 23996, + 23998, + 24000, + 24002, + 24004, + 24006, + 24008, + 24010, + 24013, + 24015, + 24017, + 24019, + 24021, + 24023, + 24025, + 24027, + 24029, + 24031, + 24033, + 24035, + 24037, + 24039, + 24041, + 24043, + 24045, + 24048, + 24050, + 24052, + 24054, + 24056, + 24059, + 24061, + 24063, + 24065, + 24067, + 24069, + 24071, + 24073, + 24075, + 24077, + 24079, + 24081, + 24083, + 24085, + 24088, + 24090, + 24092, + 24094, + 24096, + 24098, + 24100, + 24102, + 24104, + 24106, + 24108 + ], + "selected_pairs": 1586, + "status": "PASS_X4_JOINT_HORNER", + "unchanged_forward_pr696_primitives": 143658, + "unchanged_non_scalar_events": 5202 +} diff --git a/research/x4-joint-horner-seed29/OVERLAP.json b/research/x4-joint-horner-seed29/OVERLAP.json new file mode 100644 index 0000000000..984f67d528 --- /dev/null +++ b/research/x4-joint-horner-seed29/OVERLAP.json @@ -0,0 +1,658 @@ +{ + "selection": { + "phase": "selection", + "observed_utc": "2026-10-13T13:28:00Z", + "open_pr_count": 722, + "prs": [ + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "c7e1c7b7ad0a6b9ef872b4a89a39e43e3905e1b7", + "number": 932, + "title": "Finite construction: selected X4 target forests save 47,690 primitives with an exact class floor (no new kappa)", + "updatedAt": "2026-10-13T13:21:37Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/932" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "4e2925b076050f8035b054f95416029a63af64fa", + "number": 931, + "title": "Scoped negative result: bounded butterfly search misses the PR681 factory cost", + "updatedAt": "2026-10-13T13:13:07Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/931" + }, + { + "author": { + "id": "MDQ6VXNlcjgwMjk5Njgz", + "is_bot": false, + "login": "CubeJerry", + "name": "" + }, + "headRefOid": "d02d83332581f6a23616c1366c6b3901d42f4b06", + "number": 924, + "title": "Research: certify coupled factory scales and exact gauge floor", + "updatedAt": "2026-10-13T13:21:08Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/924" + }, + { + "author": { + "id": "MDQ6VXNlcjgwMjk5Njgz", + "is_bot": false, + "login": "CubeJerry", + "name": "" + }, + "headRefOid": "efd5643c0016b6c6dac26e9ed7dee8a75295ff2a", + "number": 922, + "title": "Research: fuse complex factory to 32 operations (no new kappa)", + "updatedAt": "2026-10-13T12:44:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/922" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "79ee104a90c3c7c244362cce74997fce37923ce9", + "number": 919, + "title": "Finite construction: CK helper-run sign normalization saves 224 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T12:34:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/919" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "085c32a25e2a09b029fa816195b97fa93d6f0788", + "number": 917, + "title": "Finite construction: two-sided CK compensation saves 8,798 beyond target forests (no new kappa)", + "updatedAt": "2026-10-13T12:23:50Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/917" + }, + { + "author": { + "id": "U_kgDOETsF7g", + "is_bot": false, + "login": "nightangelflowerwin-ops", + "name": "Stephen Shore" + }, + "headRefOid": "1f0cd934f83ddf2f14f20275ecca072c5b85a7b9", + "number": 916, + "title": "Integration: admit PR883 X4 primitive lowering through selected invoice and assembly (no new kappa)", + "updatedAt": "2026-10-13T12:22:59Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/916" + }, + { + "author": { + "id": "MDQ6VXNlcjI3NTY4NjE3", + "is_bot": false, + "login": "ToikY", + "name": "" + }, + "headRefOid": "5896f6fce48ee1d507722cc91eb1dcccc878670d", + "number": 909, + "title": "Scoped negative result: nonunit dyadic target pairs cannot improve X4 (no new kappa)", + "updatedAt": "2026-10-13T11:53:08Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/909" + }, + { + "author": { + "id": "MDQ6VXNlcjI3NTY4NjE3", + "is_bot": false, + "login": "ToikY", + "name": "" + }, + "headRefOid": "dbe8dc01f8306bd7dab8d861a953b23e5cda6a70", + "number": 901, + "title": "Research construction: restored X4 target pairs save 33,800 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T11:16:04Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/901" + }, + { + "author": { + "id": "MDQ6VXNlcjgyODk5MzMx", + "is_bot": false, + "login": "mightyOil", + "name": "" + }, + "headRefOid": "b31a870a3842b37f6ab97767c506ce91783632a2", + "number": 883, + "title": "Research construction: four-primitive X4 preconditions save 784 per orientation (no new kappa)", + "updatedAt": "2026-10-13T09:40:02Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/883" + }, + { + "author": { + "id": "MDQ6VXNlcjgyODk5MzMx", + "is_bot": false, + "login": "mightyOil", + "name": "" + }, + "headRefOid": "e698981e0ffa680b6c5896dace1609025b97ad70", + "number": 882, + "title": "Research construction: seven grid-preserving JP8 circuits save 104 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T10:40:17Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/882" + }, + { + "author": { + "id": "MDQ6VXNlcjUwMzY2Njc2", + "is_bot": false, + "login": "navinor", + "name": "Aaron Wang" + }, + "headRefOid": "0d8d4be2b8093e809c4c422849c486532f6ee1c1", + "number": 876, + "title": "Scoped negative result: simultaneous full pair/triple exchanges do not beat SW4 (seed 29)", + "updatedAt": "2026-10-13T09:11:25Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/876" + }, + { + "author": { + "id": "U_kgDOBlXDXA", + "is_bot": false, + "login": "amazedbot", + "name": "Amazed" + }, + "headRefOid": "72899c888af7e171f8aba4d5c66f4b31a5719eba", + "number": 860, + "title": "Research construction: signed CK reuse saves 926 primitives", + "updatedAt": "2026-10-13T09:18:43Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/860" + }, + { + "author": { + "id": "U_kgDOBhtdKA", + "is_bot": false, + "login": "faw01", + "name": "faw" + }, + "headRefOid": "6e9c76b2b9e31350a10ceb5b98e94df1438e3a1f", + "number": 839, + "title": "Research construction: remove known-zero JP8 clears (9,228 primitives per orientation; no new kappa)", + "updatedAt": "2026-10-13T06:56:21Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/839" + }, + { + "author": { + "id": "MDQ6VXNlcjI3MzA1OQ==", + "is_bot": false, + "login": "bitplane", + "name": "Gareth Davidson" + }, + "headRefOid": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "number": 837, + "title": "Research: bidirectional Horner saves 312 SW4 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T06:57:25Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/837" + }, + { + "author": { + "id": "U_kgDOD9_NhQ", + "is_bot": false, + "login": "dd-hemant", + "name": "" + }, + "headRefOid": "133735a2cc2319c12ba5d786214b2217e083e7da", + "number": 816, + "title": "Research: signed CK target forests save 66,520 primitives with an exact class floor (no new kappa)", + "updatedAt": "2026-10-13T06:21:41Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/816" + }, + { + "author": { + "id": "MDQ6VXNlcjQwMTkwNTQ=", + "is_bot": false, + "login": "davidawad", + "name": "David Awad" + }, + "headRefOid": "b1a5c533a22c2665600102d872f6a84e0664a70d", + "number": 807, + "title": "Research: restored CK helper pairs save 35,872 primitives per orientation (no new \u03ba)", + "updatedAt": "2026-10-13T06:02:09Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/807" + }, + { + "author": { + "id": "U_kgDODSjO3g", + "is_bot": false, + "login": "Varun-Mittal-1001", + "name": "Varun" + }, + "headRefOid": "f9383f324ee86793c5ae7b73f8e39d5827a8aa52", + "number": 793, + "title": "Research: batch JP8 compensation, saving 80,150 / 81,464 primitives (no new kappa)", + "updatedAt": "2026-10-13T05:52:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/793" + }, + { + "author": { + "id": "MDQ6VXNlcjI3MzA1OQ==", + "is_bot": false, + "login": "bitplane", + "name": "Gareth Davidson" + }, + "headRefOid": "93ceb65cfbf339d7ca743614d4756a3af1440cd4", + "number": 787, + "title": "Research: compose complex coefficient lowering and cleanup sharing", + "updatedAt": "2026-10-13T05:34:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/787" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "b6d6934092c063ab2575ebee00f48bbc7b1c9d82", + "number": 750, + "title": "Research: save 62 CK primitives per orientation by relocating one scale (no new kappa)", + "updatedAt": "2026-10-13T05:06:33Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/750" + }, + { + "author": { + "id": "MDQ6VXNlcjUzNjcwMzYz", + "is_bot": false, + "login": "AllStars101-sudo", + "name": "Chris" + }, + "headRefOid": "ba76ba3321d000c8996b0b254bcf0d7260e1bbb6", + "number": 734, + "title": "Research: prefix-bounded signed-Horner circuits for CK and JP8 (no new kappa)", + "updatedAt": "2026-10-13T05:00:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/734" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "a3d9c0aa0a16b68b1f4dd064671ad018013e6dd4", + "number": 719, + "title": "Scoped negative result: rank-two obstruction for 78 CK cleanup pairs", + "updatedAt": "2026-10-13T04:45:00Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/719" + } + ] + }, + "pre_submission": { + "observed_utc": "2026-10-13T13:45:00Z", + "open_pr_count": 710, + "latest_observed_pr": 939, + "refreshed_main": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "selected_pr": 890, + "selected_kappa": "0.001661957774647029", + "pinned_coordination_issues": [], + "overlap_conclusion": "No adjacent two-source nonzero-frame joint Horner contribution found. PR937 changes a historical central factor, PR932 a frame-zero target basis; both are distinct. Fixed X4 data are unchanged; no U8 transport is claimed.", + "prs": [ + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "3a8ec54d62fb8824c658dc7ed356f99423cac8cf", + "number": 939, + "title": "Scoped negative result: E8 star-copy ratio cannot improve through 55 punctures (no new kappa)", + "updatedAt": "2026-10-13T13:43:55Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/939" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "df645942469e6a739ec94010a6068c398f4a6c86", + "number": 938, + "title": "Independent verification: complete minimum-word census for dirty fanout stars (no new kappa)", + "updatedAt": "2026-10-13T13:43:36Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/938" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "b303fed6dfe2066dcd78c0d8ed74d2a3b153ba72", + "number": 937, + "title": "Finite complex construction: two center shears save 5,562 primitives per invocation (no new kappa)", + "updatedAt": "2026-10-13T13:41:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/937" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "0679fb6e1e4c91f573ae07ab1d0ea273b13c74e3", + "number": 936, + "title": "Finite bit construction: five-wire prefixes save 340 further ADDs beyond PR904 (no new kappa)", + "updatedAt": "2026-10-13T13:40:34Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/936" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "f3100aec6ce6a7b061987875d5e9a8b93801ac0b", + "number": 934, + "title": "Research: optimal 3x3 binary connector queries (no new kappa)", + "updatedAt": "2026-10-13T13:24:27Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/934" + }, + { + "author": { + "id": "MDQ6VXNlcjM4Mjk3MjY5", + "is_bot": false, + "login": "ianlibanio", + "name": "Ian Lib\u00e2nio" + }, + "headRefOid": "b9348c6907516e55dc07e135ad4d7a480d4f9840", + "number": 933, + "title": "Scoped negative result: no relocation or Steinberg rewrite with exact reframing raises PR589's bit c (no new kappa)", + "updatedAt": "2026-10-13T13:22:15Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/933" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "c5b5b30279bdda513e97017587806a0b9f0ca850", + "number": 932, + "title": "Finite construction: selected X4 target forests save 47,690 primitives with an exact class floor (no new kappa)", + "updatedAt": "2026-10-13T13:22:08Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/932" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "4e2925b076050f8035b054f95416029a63af64fa", + "number": 931, + "title": "Scoped negative result: bounded butterfly search misses the PR681 factory cost", + "updatedAt": "2026-10-13T13:13:07Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/931" + }, + { + "author": { + "id": "MDQ6VXNlcjgwMjk5Njgz", + "is_bot": false, + "login": "CubeJerry", + "name": "" + }, + "headRefOid": "d02d83332581f6a23616c1366c6b3901d42f4b06", + "number": 924, + "title": "Research: compose PR922 factory fusions with PR924 rescaling", + "updatedAt": "2026-10-13T13:29:56Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/924" + }, + { + "author": { + "id": "MDQ6VXNlcjgwMjk5Njgz", + "is_bot": false, + "login": "CubeJerry", + "name": "" + }, + "headRefOid": "efd5643c0016b6c6dac26e9ed7dee8a75295ff2a", + "number": 922, + "title": "Research: fuse complex factory to 32 operations (no new kappa)", + "updatedAt": "2026-10-13T12:44:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/922" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "79ee104a90c3c7c244362cce74997fce37923ce9", + "number": 919, + "title": "Finite construction: CK helper-run sign normalization saves 224 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T12:34:13Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/919" + }, + { + "author": { + "id": "MDQ6VXNlcjU2NTI3MTY=", + "is_bot": false, + "login": "RossRichardson", + "name": "Ross Richardson" + }, + "headRefOid": "085c32a25e2a09b029fa816195b97fa93d6f0788", + "number": 917, + "title": "Finite construction: two-sided CK compensation saves 8,798 beyond target forests (no new kappa)", + "updatedAt": "2026-10-13T12:23:50Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/917" + }, + { + "author": { + "id": "U_kgDOETsF7g", + "is_bot": false, + "login": "nightangelflowerwin-ops", + "name": "Stephen Shore" + }, + "headRefOid": "1f0cd934f83ddf2f14f20275ecca072c5b85a7b9", + "number": 916, + "title": "Integration: admit PR883 X4 primitive lowering through selected invoice and assembly (no new kappa)", + "updatedAt": "2026-10-13T12:22:59Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/916" + }, + { + "author": { + "id": "MDQ6VXNlcjI3NTY4NjE3", + "is_bot": false, + "login": "ToikY", + "name": "" + }, + "headRefOid": "dbe8dc01f8306bd7dab8d861a953b23e5cda6a70", + "number": 901, + "title": "Research construction: restored X4 target pairs save 33,800 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T11:16:04Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/901" + }, + { + "author": { + "id": "MDQ6VXNlcjgyODk5MzMx", + "is_bot": false, + "login": "mightyOil", + "name": "" + }, + "headRefOid": "b31a870a3842b37f6ab97767c506ce91783632a2", + "number": 883, + "title": "Research construction: four-primitive X4 preconditions save 784 per orientation (no new kappa)", + "updatedAt": "2026-10-13T09:40:02Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/883" + }, + { + "author": { + "id": "MDQ6VXNlcjgyODk5MzMx", + "is_bot": false, + "login": "mightyOil", + "name": "" + }, + "headRefOid": "e698981e0ffa680b6c5896dace1609025b97ad70", + "number": 882, + "title": "Research construction: seven grid-preserving JP8 circuits save 104 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T10:40:17Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/882" + }, + { + "author": { + "id": "MDQ6VXNlcjUwMzY2Njc2", + "is_bot": false, + "login": "navinor", + "name": "Aaron Wang" + }, + "headRefOid": "0d8d4be2b8093e809c4c422849c486532f6ee1c1", + "number": 876, + "title": "Scoped negative result: simultaneous full pair/triple exchanges do not beat SW4 (seed 29)", + "updatedAt": "2026-10-13T09:11:25Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/876" + }, + { + "author": { + "id": "U_kgDOBlXDXA", + "is_bot": false, + "login": "amazedbot", + "name": "Amazed" + }, + "headRefOid": "72899c888af7e171f8aba4d5c66f4b31a5719eba", + "number": 860, + "title": "Research construction: signed CK reuse saves 926 primitives", + "updatedAt": "2026-10-13T09:18:43Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/860" + }, + { + "author": { + "id": "U_kgDOBhtdKA", + "is_bot": false, + "login": "faw01", + "name": "faw" + }, + "headRefOid": "6e9c76b2b9e31350a10ceb5b98e94df1438e3a1f", + "number": 839, + "title": "Research construction: remove known-zero JP8 clears (9,228 primitives per orientation; no new kappa)", + "updatedAt": "2026-10-13T06:56:21Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/839" + }, + { + "author": { + "id": "MDQ6VXNlcjI3MzA1OQ==", + "is_bot": false, + "login": "bitplane", + "name": "Gareth Davidson" + }, + "headRefOid": "0a2977195efc8fb2a918fbfb694ec8d294387f08", + "number": 837, + "title": "Research: bidirectional Horner saves 312 SW4 primitives per orientation (no new kappa)", + "updatedAt": "2026-10-13T06:57:25Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/837" + }, + { + "author": { + "id": "U_kgDOD9_NhQ", + "is_bot": false, + "login": "dd-hemant", + "name": "" + }, + "headRefOid": "133735a2cc2319c12ba5d786214b2217e083e7da", + "number": 816, + "title": "Research: signed CK target forests save 66,520 primitives with an exact class floor (no new kappa)", + "updatedAt": "2026-10-13T06:21:41Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/816" + }, + { + "author": { + "id": "MDQ6VXNlcjQwMTkwNTQ=", + "is_bot": false, + "login": "davidawad", + "name": "David Awad" + }, + "headRefOid": "b1a5c533a22c2665600102d872f6a84e0664a70d", + "number": 807, + "title": "Research: restored CK helper pairs save 35,872 primitives per orientation (no new \u03ba)", + "updatedAt": "2026-10-13T06:02:09Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/807" + }, + { + "author": { + "id": "U_kgDODSjO3g", + "is_bot": false, + "login": "Varun-Mittal-1001", + "name": "Varun" + }, + "headRefOid": "f9383f324ee86793c5ae7b73f8e39d5827a8aa52", + "number": 793, + "title": "Research: batch JP8 compensation, saving 80,150 / 81,464 primitives (no new kappa)", + "updatedAt": "2026-10-13T05:52:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/793" + }, + { + "author": { + "id": "MDQ6VXNlcjI3MzA1OQ==", + "is_bot": false, + "login": "bitplane", + "name": "Gareth Davidson" + }, + "headRefOid": "93ceb65cfbf339d7ca743614d4756a3af1440cd4", + "number": 787, + "title": "Research: compose complex coefficient lowering and cleanup sharing", + "updatedAt": "2026-10-13T05:34:22Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/787" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "b6d6934092c063ab2575ebee00f48bbc7b1c9d82", + "number": 750, + "title": "Research: save 62 CK primitives per orientation by relocating one scale (no new kappa)", + "updatedAt": "2026-10-13T05:06:33Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/750" + }, + { + "author": { + "id": "MDQ6VXNlcjUzNjcwMzYz", + "is_bot": false, + "login": "AllStars101-sudo", + "name": "Chris" + }, + "headRefOid": "ba76ba3321d000c8996b0b254bcf0d7260e1bbb6", + "number": 734, + "title": "Research: prefix-bounded signed-Horner circuits for CK and JP8 (no new kappa)", + "updatedAt": "2026-10-13T05:00:52Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/734" + }, + { + "author": { + "id": "MDQ6VXNlcjE4NjIyMjg4", + "is_bot": false, + "login": "thakrarsagar", + "name": "" + }, + "headRefOid": "a3d9c0aa0a16b68b1f4dd064671ad018013e6dd4", + "number": 719, + "title": "Scoped negative result: rank-two obstruction for 78 CK cleanup pairs", + "updatedAt": "2026-10-13T04:45:00Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/719" + } + ] + } +} diff --git a/research/x4-joint-horner-seed29/PROOF.md b/research/x4-joint-horner-seed29/PROOF.md new file mode 100644 index 0000000000..4bec3e0405 --- /dev/null +++ b/research/x4-joint-horner-seed29/PROOF.md @@ -0,0 +1,160 @@ +# Joint two-source Horner preparation in fixed X4 frames + +This is a finite scalar circuit construction. The selected conditional exponent +is unchanged. The independently checked claim is the exact linear map and cost +of the declared replacement class, not the full integer multiplication theorem. + +## Circuit identity and full bill + +Consider two adjacent scalar additions at the same frame: + +``` +T <- T + a S1 +T <- T + b S2 +``` + +The three registers are distinct and neither source is modified. Let +`a=A/2^K`, `b=B/2^K`, with the least common dyadic denominator, and nonzero +signed integers A and B. Set `L=max(bitlength(|A|),bitlength(|B|))`. + +Choose sigma as the sign of the first occupied leading digit, breaking a +leading-digit tie in favor of S1. Copy that source into the existing coefficient +work register W. For the remaining leading source digit, if present, add or +subtract its source according to its sign relative to sigma. For each lower +position, double W once and add/subtract each occupied source digit. After all +positions, `W=sigma*(A*S1+B*S2)`. Halve W K times, then add or subtract W into T +according to sigma, and clear W. + +Induction over digit positions proves the displayed value of W. Therefore the +complete arbitrary-input boundary map is + +``` +(T,S1,S2,W) -> (T+a*S1+b*S2,S1,S2,0). +``` + +The initial copy erases arbitrary prior W, rather than assuming it is clean. +The sources are unchanged throughout, so there is no restoration debt. The +target is updated once after both sources have been consumed; its earlier +update cannot affect S2 because target/source aliasing is excluded. + +Every primitive is charged. Per real component the count is + +``` +1 copy + (L-1) doubles + (popcount(|A|)+popcount(|B|)-1) signed source reads + + K halves + 1 target accumulation + 1 clear += L + popcount(|A|)+popcount(|B|) + K + 1. +``` + +Complex values execute the same real-coefficient map separately on real and +imaginary components, doubling this count. There is one existing coefficient +work register per component, no new helper, source cache, persistent copy, +frame transition or recursive child. All instructions are at the common frame. +The source-read count is the total popcount and equals the two separately +lowered reads, including unit coefficients. Doublings, halvings, target +accumulations and clears account for the savings. + +For example, `a=b=1/2` becomes `copy S1 to W; add S2 to W; halve W; +add W to T; clear W`: five primitives, compared with eight under PR696's +separate copy/Horner/accumulate/clear circuits. Removing only one redundant +clear would cost seven. This is a shared preparation across two *different* +sources, not just a changed clearing boundary. + +## Finite domain and optimal disjoint selection + +The input is the PR799 X4 backward event list, selected at the starting base and source-bound to its +SPEC and the committed integrated replay. Exactly 6,112 adjacent event pairs +have scalar ADDs, equal nonzero frame IDs, a common target, distinct sources, +and no register alias. No commutation, frame-zero compensation, reordering, +larger block or new parameter value is searched. + +For each pair i, compute the above circuit and its exact saving d_i over +separately applying the accepted PR696 lowering. Retain only `d_i>1`, ensuring +that each candidate beats deletion of one work clear. There are 2,764 such +candidates. Selecting pair i consumes events i and i+1. + +With `D[N]=D[N+1]=0`, the suffix recurrence is + +``` +D[i] = max(D[i+1], d_i+D[i+2]) if pair i is retained, +D[i] = D[i+1] otherwise. +``` + +Every admissible matching either omits i or consumes i and i+1, proving the +recurrence by induction. The witness attains `D[0]=6536` per component using +1,586 pairs. Ties skip the earlier pair. The code-disjoint verifier instead +uses a forward longest-path recurrence and checks the submitted nonoverlapping +witness attains its bound. This certifies only the stated disjoint pairing +class with this binary circuit and the `d_i>1` restriction. It is not general +circuit optimality, nor optimality over all coefficient-work schedules. + +All 6,112 candidate four-register matrices are checked, including unselected +and losing ones. The Fraction and separate integer-grid implementations agree; +the latter checks all 97,792 matrix entries. Neither uses floating point. + +## Composition, frames and private work + +Each accepted pair has exactly the original two-macro boundary map. Every +surrounding event therefore receives the same logical inputs. Induction over +the event list proves scalar composition. The main checker evaluates every +primitive and checks each single-macro or pair boundary, followed by the full +backward endpoint `L_i <- L_i-L_(112+i)` for `0<=i<112`, with all other logical +registers restored. Its 737 independent formal columns cover 728 logical +registers (including 504 arbitrary helpers), eight arbitrary center inputs, +and arbitrary coefficient work. All private outputs clear. + +A pair cannot cross a non-scalar event or frame change. Every source and target +already participates in an addition at the common frame. The primitive model +uses the existing private coefficient stream at that frame. The scalar +interpreters preserve, but do not execute, the physical phase/Clifford, frame, +wrapper or recursive operations. Production admission must still represent +the fused block's larger clearing boundary explicitly and rebind its receipts. + +## Prefixes and complete conservative accounting + +Joint W can have a larger *local* intermediate than either original W. There +is no general per-macro prefix-domination claim. For the particular full X4 +backward word, exact replay checks every updated row after every primitive: + +- maximum scalar row-l1: 5,338,828 before and after; +- maximum dyadic fractional depth: 19 before and after; +- propagated nonnegative envelope: `48299247699832632898063/16` before and after, + still within the inherited 192-bit local magnitude allocation. + +These finite scalar quantities do not certify the complete recursive physical +precision/tape interface. In particular, a magnitude allowance alone is not +a proof of a rounding or recovery contract. + +The full backward primitive bill changes from 143,674 to 130,602 under PR696, +saving 13,072. Non-work source reads remain 39,446; total arithmetic operand +reads change from 146,392 to 136,492. These counts include both real components; +they are not hardware traffic or runtime measurements. + +The forward PR696 count is retained at 143,658. The existing conservative local +invoice uses the maximum of the two orientations, so that maximum changes +only from 143,674 to 143,658. Retaining all 19,197 original macro charges, +3,574 recursive children, 728 logical registers and eight centers gives + +``` +adapters = 16*(19197+3574+728+8)+64*73 = 380784, +compiler = 64*74^3 = 25934336, +local bound = max(forward,backward) + adapters*compiler. +``` + +It changes from **9,875,380,343,098** to **9,875,380,343,082**, a reduction of +**16** under that conservative arithmetic recount. No adapter credit is taken +for fusion. This is not a run of the global invoice or outer assembly. The paid +profile, width/owner construction and analytic supplier exponents are unchanged; +no new kappa follows from a primitive-count improvement. + +## Attribution and inherited obligations + +The X4 checkpoint source is Jeremy Kothe's PR799, extending Chafik Boukhalfa's +PR741 frames and icekylinx's scalar/factory architecture. Sagar Thakrar's +accepted PR696 supplies the baseline lowering. See README for related searches +and the retained DreamingOfClouds, Rohan Arun, eumemic and predecessor credits. + +All-size compilation, common-label/mutable-source realization, whole-call +hosting, recursive precision/tape, exact recovery, analytic transfer and the +bit-supplier assumptions remain inherited. Nothing here formalizes or improves +the complete multiplication theorem. Written for Ross Richardson with +substantial OpenAI Codex assistance, under Apache-2.0. diff --git a/research/x4-joint-horner-seed29/README.md b/research/x4-joint-horner-seed29/README.md new file mode 100644 index 0000000000..8b9a1f0802 --- /dev/null +++ b/research/x4-joint-horner-seed29/README.md @@ -0,0 +1,164 @@ +# Joint Horner preparation in X4 checkpoint nonzero frames + +**Finite complex-supplier circuit construction; no new kappa.** Fusing two +adjacent same-target additions with different sources shares their coefficient +preparation. An exact disjoint-pair selection saves **13,072 real-component +primitives** in the complete PR799 X4 backward scalar program, selected at the +starting base. + +| Quantity | Accepted PR696 lowering | Joint preparation | +| --- | ---: | ---: | +| Backward real primitives | 143,674 | 130,602 | +| Forward real primitives, retained | 143,658 | 143,658 | +| Maximum over orientations | 143,674 | 143,658 | +| Backward non-work source reads | 39,446 | 39,446 | +| Backward total arithmetic operand reads | 146,392 | 136,492 | +| Scalar prefix row-l1 maximum | 5,338,828 | 5,338,828 | +| Scalar fractional depth | 19 | 19 | + +The unchanged forward orientation becomes binding in the conservative local +maximum. Keeping the full inherited adapter allowance, that local arithmetic +recount improves by only **16**, from 9,875,380,343,098 to 9,875,380,343,082. +The separate 13,072 saving is a complete *backward* circuit count. Neither is +a measured runtime benefit or a new exponent. During this sprint, main advanced +to the reviewed **PR890, kappa 0.001661957774647029**. This remains a contribution +to the historical #799 checkpoint (kappa 0.001661634653669567); transport to the +new U8 supplier is not claimed. +The forward row is a complete primitive recount under PR696; only the backward +orientation receives a new full scalar replay in this package. + +## Reproduce + +From the repository root, Python 3.11+ and the standard library suffice: + +```sh +python3 -I -B research/x4-joint-horner-seed29/verify.py +``` + +Expected final line: + +```text +PASS_X4_JOINT_HORNER candidates=6112 pairs=1586 saved=13072 columns=737 no_new_kappa +``` + +The command reads pinned committed inputs without network access, evaluates all +6,112 local matrices, recomputes the complete finite selection, replays baseline +and candidate scalar primitives, checks adverse controls, and compares every +receipt field with [EXPECTED.json](EXPECTED.json). It writes nothing normally. +`--write PATH` creates a new development receipt and refuses an existing path. + +Additional checks: + +```sh +python3 -I -O -B research/x4-joint-horner-seed29/independent.py +python3 -I -O -B research/x4-joint-horner-seed29/test_package.py +``` + +The first imports neither the compiler, Fraction, nor predecessor code. Integer +four-column matrices, an independently emitted complete primitive-stream hash, +and a forward longest-path calculation corroborate the main implementation's +Fraction replay and suffix dynamic program. Both implementations were written +by the same AI agent; no independent human review is implied. + +## Construction and completed coverage + +For a common denominator `a=A/2^K`, `b=B/2^K`, build the signed sum +`A*S1+B*S2` in the existing work register using shared binary doublings, halve +K times, accumulate once into the target, and clear. The initial copy handles +arbitrary dirty work. Every copy, read, doubling, halving, signed addition and +clear is charged. No helper, source mutation/restoration, physical frame change +or recursive child is introduced. [PROOF.md](PROOF.md) gives the identity, +exact cost and substitution argument. + +The domain is every adjacent scalar ADD pair in the frozen backward event list +with equal **nonzero** frame, identical target and two distinct nonaliasing +sources: **6,112** pairs. Of these, **2,764** save more than deleting a single +work clear. Exact path dynamic programming selects **1,586** disjoint pairs +with total saving 6,536 per real component. Enumeration ends at the last event; +there is no timeout, sampling or uncompleted region. The optimum is certified +only for this restricted binary-Horner disjoint-pair class. No unrestricted +circuit optimum or coefficient synthesis novelty is claimed. + +The main full projection checks all **737 arbitrary input columns**: 728 +logical, eight center and one coefficient-work input. It verifies each group +boundary, the final shear, helper restoration and private clearing. The +independent local check covers 97,792 exact matrix entries and reproduces the +complete candidate stream hash. The nonnegative full-program envelope remains +`48299247699832632898063/16`, within the retained 192-bit magnitude allowance. +This does not imply general per-macro prefix domination or a full compiler +precision certificate. + +The seed-selected pair's primitive deletion, wrong-sign, source-alias, +non-dyadic, dirty-work, event/frame-boundary and endpoint-neutral cost controls +are rejected. Four separate integer adverse circuits are rejected. Tests also +compare the DP with exhaustive small matchings and check minimal relocation, +source corruption, overlapping recipes and a suboptimal matching. + +## Source pins and overlap + +Exact base: **91a2094f2e022930069e8cfdc810a3ea1b81cd09**. The OS-random seed +**29** assigns the complex track and, by parity, backward orientation; it also +fixes tie handling and a mutation-control example. [CLAIM.json](CLAIM.json) +records the three considered tasks and timing. No pinned coordination issue +existed; the claim is local. [SOURCES.json](SOURCES.json) pins every consumed +input, including decompressed member payloads of the immutable integrated +replay archive. The event hashes are checked against the pinned X4 SPEC. +The #799 selection bytes are accepted at their original path or the official +`certificates/checkpoints/frontier799.json` path, with the same exact hash. +The newer active selection is not repinned or represented as an X4 witness. + +Source heads: PR799 `80e6463157cfc80b85af09e7e2f14748fe2dac60`, PR741 +`e516b1463606840a15f80aac1995d64ce0092e89`, PR696 +`5a3f983715027c4fd83f50bc9001d4b18463bed1`. + +This scope was chosen after inspecting the review ledger, accepted source and +review, open PRs, and prior negative results. The starting construction's actual +word/profile is used, not a number inferred from an open PR title. Related work: + +- [#734](https://github.com/CrocSwap/integer-mult-bounds/pull/734), + [#837](https://github.com/CrocSwap/integer-mult-bounds/pull/837) and + [#882](https://github.com/CrocSwap/integer-mult-bounds/pull/882) optimize + individual coefficient macros. This crosses two different-source macros. +- [#793](https://github.com/CrocSwap/integer-mult-bounds/pull/793), + [#901](https://github.com/CrocSwap/integer-mult-bounds/pull/901) and + [#932](https://github.com/CrocSwap/integer-mult-bounds/pull/932) change + frame-zero compensation ordering or bases. That region is excluded here. +- [#719](https://github.com/CrocSwap/integer-mult-bounds/pull/719) excludes + single rank-one replacements for historical CK repeated-source pairs with + fixed middle gates. Here sources differ, gates are adjacent, and the output + is a paid primitive circuit, so its obstruction is not reopened. +- [#839](https://github.com/CrocSwap/integer-mult-bounds/pull/839) removes known + zero clears; every retained pair here saves strictly more than that one-clear + comparison. [#919](https://github.com/CrocSwap/integer-mult-bounds/pull/919) + normalizes CK signs; this does not relocate live-register signs or scales. +- [#922](https://github.com/CrocSwap/integer-mult-bounds/pull/922), + [#924](https://github.com/CrocSwap/integer-mult-bounds/pull/924) and + [#931](https://github.com/CrocSwap/integer-mult-bounds/pull/931) investigate + historical factory macro topologies. Those words are not consumed here. + +No pending implementation is imported and savings from different submissions +are not assumed additive. [OVERLAP.json](OVERLAP.json) retains inspected heads; +[VALIDATION.md](VALIDATION.md) records final refresh and executed checks. + +## Scope and credit + +Only this research directory is added. The selected frontier, production +generators and `upstream/` remain unchanged. Physical Clifford/frame/phase +operations are preserved as opaque events, not executed by these scalar +interpreters. Typed primitive integration, fresh physical admission and receipt +bindings, global owner/hosting/invoice/assembly remain separate work. The +inherited all-size/compiler, common-label/mutable-source realization, +precision/tape/recovery, bit-supplier and analytic assumptions remain. + +Prepared by **Ross Richardson (@RossRichardson)** with substantial **OpenAI +Codex assistance** in selection, implementation, mathematics, tests and writing. +No delegated agent or independent human review is claimed. Apache-2.0 under +the repository [LICENSE](../../LICENSE). + +Credit **Jeremy Kothe** for PR799 and the supplier lineage; **Chafik Boukhalfa** +for PR741; **icekylinx** for the scalar/factory and Horner architecture; +**Sagar Thakrar** for PR696; **DreamingOfClouds, Rohan Arun, eumemic, Dugongue** +and the contributors retained in the source notices and +[maintainer review](../../docs/research/community-frontier799-review.md). +Related coefficient-work contributions above are credited without a priority +claim for joint Horner arithmetic. diff --git a/research/x4-joint-horner-seed29/SOURCES.json b/research/x4-joint-horner-seed29/SOURCES.json new file mode 100644 index 0000000000..1a2515a40a --- /dev/null +++ b/research/x4-joint-horner-seed29/SOURCES.json @@ -0,0 +1,26 @@ +{ + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "source_heads": { + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60", + "741": "e516b1463606840a15f80aac1995d64ce0092e89", + "696": "5a3f983715027c4fd83f50bc9001d4b18463bed1" + }, + "files": { + "certificates/selected-result.json": "9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036", + "research/gauge44-frames-x/data/SPEC.json": "64817c60a4a2c1839bf12239cb1b7515a40bf8988229d81d4c9faa17b488c7d5", + "research/gauge44-frames-x/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/complex-dyadic-lowering/lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753", + "research/community-frontier799-audit/integrated799-replay.tar.gz": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb" + }, + "archive": "research/community-frontier799-audit/integrated799-replay.tar.gz", + "member_hash_semantics": "SHA256 of decompressed payload for .gz members, exact bytes otherwise. Archive is an immutable committed input, pinned separately.", + "members": { + "native/local/LOCAL-PROGRAMS.json.gz": "223c2bb27ad68a4e9468c3ddaece1899d577b661190922fdd25f5976052c4cab", + "native/local/LOCAL-CHECKS.json": "bbde5cea7bfd5df3d3ee7dfada0ff9d165af43a4d1dec6a9597cbfd8f87cc3b2", + "native/local/INDEPENDENT-LOCAL-REPLAY.json": "355e2ae57b8eadc957bed567ba7c5caf33202ace690560c94b008f10cf906364" + }, + "integration_base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "selection_alias": "certificates/selected-result.json may resolve to certificates/checkpoints/frontier799.json only with its unchanged exact SHA256; active PR890 is not a data dependency." +} diff --git a/research/x4-joint-horner-seed29/VALIDATION.md b/research/x4-joint-horner-seed29/VALIDATION.md new file mode 100644 index 0000000000..b7f1a1374b --- /dev/null +++ b/research/x4-joint-horner-seed29/VALIDATION.md @@ -0,0 +1,99 @@ +# Validation and handoff + +Executed on 2026-10-13 UTC (2026-10-14 in Melbourne), macOS arm64 +Darwin 25.5.0, CPython 3.14.6. No additional Python packages are required. + +## Verified result + +- Full normal and isolated optimized replay: 6,112 eligible pairs, 2,764 + arithmetic-saving candidates, 1,586 selected pairs, 13,072 real primitives + saved backward, all 737 formal input columns, every group boundary, complete + endpoint, arbitrary helper restoration and private erasure. +- Both full scalar executions agree on prefix row-l1 5,338,828, fractional + depth 19, the inherited positive envelope, and all 5,202 non-scalar events. +- The separate integer implementation checks all 6,112 local matrices (97,792 + entries), obtains the same optimum by forward path DP, and independently + rebuilds the complete 130,602-primitive stream and its SHA256. +- Twelve main adverse controls and four independent integer circuit controls + pass. Identity and pricing are separate checks: an endpoint-equivalent + inflated circuit is rejected by its cost check. +- Seven focused tests pass normally and under isolated optimized execution. + They cover 144 varied signed/denominator microcircuits, alias/type/dyadic + rejection, physical event boundaries, exhaustive small matching comparisons, + independent full certificate reconstruction and package controls. +- The minimal relocated tree has spaces in its path, no Git metadata and only + declared source inputs. Its optimized full replay passes from another working + directory. Source corruption, overlapping pairs, a suboptimal matching and a + corrupted #799 checkpoint fail. A different active selection with an intact + #799 checkpoint is accepted. +- `make selected-record-check` passes at the original base and after rebase; + the latter verifies the newly selected PR890 kappa, not the older X4 value. + +Reproduce the contribution with: + +```sh +python3 -I -B research/x4-joint-horner-seed29/verify.py +python3 -I -O -B research/x4-joint-horner-seed29/independent.py +python3 -I -O -B research/x4-joint-horner-seed29/test_package.py +``` + +The first command prints: + +``` +PASS_X4_JOINT_HORNER candidates=6112 pairs=1586 saved=13072 columns=737 no_new_kappa +``` + +The complete deterministic receipt is EXPECTED.json. Search code, certificate +checks and full scalar replay use exact arithmetic. The all-candidate census +and complete primitive stream have independent reconstruction, not just a check +of a nominated winner. Two implementations by the same AI agent are not +independent human review. + +## Current-main reconciliation + +Starting base: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +Submission integration base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. + +The branch was rebased onto that refreshed main. Six non-context source files, +including the original committed replay archive, remained byte-identical. +The prior selected-record bytes moved unchanged to +`certificates/checkpoints/frontier799.json`, SHA256 +`9873519224e2db72d6a8c926f51e3e75129671e467948c6f6b03744f8bcfc699`. +Both readers require this exact hash at the original or official checkpoint +path. They do not silently repin the older witness to the active PR890 record. + +The current accepted record and its maintainer review were read after refresh: +PR890/U8/T21, conditional kappa **0.001661957774647029**. This package retains +the completed X4 contribution and makes no U8 compatibility or transfer claim. +The accepted frontier and `upstream/` have no changes from this contribution. + +The overlap refresh covered 710 open PRs through #939. No pinned sprint issue +existed, so the claim stayed local. New #937 changes a historical central +factor; #932 changes a frame-zero target basis. No same-scope joint two-source +nonzero-frame Horner construction was found. Their work is neither imported +nor silently included in these savings. Exact inspected heads are in +OVERLAP.json. CLAIM.json records the submission result and link. + +## Remaining work and limits + +The exact class optimum is only for disjoint adjacent eligible pairs, the +specific binary circuit, and strictly more than one saved primitive per pair. +It does not exclude signed-digit circuits, longer accumulations, changed order, +or new frames. No new kappa, runtime gain or general circuit optimum is claimed. + +The primitive work register clears at pair boundaries rather than at both old +macro boundaries. A production emitter must represent and admit that interface, +rebind the evidence and rerun the relevant physical and global checks. Scalar +interpreters do not execute physical frame/phase/Clifford events. A local +192-bit magnitude check is not a complete recursive precision/tape proof. + +All original macro adapter charges remain: 380,784 adapters at compiler factor +25,934,336. Because the unchanged forward orientation binds, the complete +conservative local arithmetic recount improves by only **16**, despite the +13,072 backward primitive saving. No global invoice is represented as run. + +Not run: full `make verify`, any selected-supplier cold rebuild, fresh global +owner/hosting/invoice/outer assembly, Lean, another Python version or hosted CI. +The change is an isolated research package and leaves existing generators and +artifacts unchanged. All-size/compiler, realization, hosting, bit-supplier, +precision/tape/recovery and analytic assumptions remain inherited. diff --git a/research/x4-joint-horner-seed29/independent.py b/research/x4-joint-horner-seed29/independent.py new file mode 100644 index 0000000000..bd2d13c458 --- /dev/null +++ b/research/x4-joint-horner-seed29/independent.py @@ -0,0 +1,200 @@ +"""Code-disjoint integer matrix, price and path-certificate crosscheck. + +Does not import Fraction, joint.py, verify.py or predecessor code. +Written by the same Codex agent for Ross Richardson; not a human peer review. +Apache-2.0. Baseline semantics are the credited PR696 copy/unit lowering. +""" +import gzip +import hashlib +import json +from math import gcd +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +W = ("W", 0) + + +def demand(condition, message): + if not condition: + raise ValueError(message) + + +def encode(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def rational(p, d): + demand(type(p) is int and type(d) is int and d != 0 and p != 0, "invalid dyadic") + if d < 0: + p, d = -p, -d + g = gcd(abs(p), d) + p, d = p//g, d//g + demand(d & (d-1) == 0, "non-dyadic") + return p, d + + +def single(op): + tag, dest = op[0], tuple(op[1]) + if tag == "clear": + return [("clear", dest)] + if tag == "copy": + return [("copy", dest, tuple(op[2]))] + if tag == "scale": + n, d = rational(*op[2:]) + demand(abs(n) & (abs(n)-1) == 0, "non-binary scale") + power = abs(n).bit_length()-d.bit_length() + return [("double" if power > 0 else "halve", dest)]*abs(power) + ([("negate", dest)] if n < 0 else []) + demand(tag == "add", "unknown macro") + n, d = rational(*op[3:]) + src = tuple(op[2]) + sign = "add" if n > 0 else "subtract" + if abs(n) == d: + return [(sign, dest, src), ("clear", W)] + word = [("copy", W, src)] + for bit in format(abs(n), "b")[1:]: + word += [("double", W)] + if bit == "1": + word += [("add", W, src)] + return word + [("halve", W)]*(d.bit_length()-1) + [(sign, dest, W), ("clear", W)] + + +def pair(a, b): + ns = [rational(*op[3:]) for op in (a,b)] + common = max(d for _, d in ns) + values = [p*(common//d) for p,d in ns] + degree = max(abs(v).bit_length() for v in values)-1 + terms = [(place, col, 1 if value > 0 else -1) + for place in range(degree, -1, -1) + for col, value in enumerate(values) if abs(value) & (1 << place)] + leading_place, first_col, orientation = terms[0] + sources = [tuple(a[2]), tuple(b[2])] + word = [("copy", W, sources[first_col])] + for place, col, sign in terms[1:]: + word += [("double", W)]*(leading_place-place) + word += [("add" if sign == orientation else "subtract", W, sources[col])] + leading_place = place + word += [("double", W)]*leading_place + word += [("halve", W)]*(common.bit_length()-1) + return word + [("add" if orientation == 1 else "subtract", tuple(a[1]), W), ("clear", W)] + + +def matrix_check(a, b, word): + registers = [tuple(a[1]), tuple(a[2]), tuple(b[2]), W] + demand(len(set(registers)) == 4, "aliased local circuit") + matrix = [[int(i == j) for j in range(4)] for i in range(4)] + denominator = 1 + for op in word: + tag, dest = op[:2] + r = registers.index(dest) + if tag == "clear": + matrix[r] = [0]*4 + elif tag == "copy": + matrix[r] = matrix[registers.index(op[2])].copy() + elif tag == "double": + matrix[r] = [2*v for v in matrix[r]] + elif tag == "halve": + for k in range(4): + if k != r: + matrix[k] = [2*v for v in matrix[k]] + denominator *= 2 + elif tag in ("add", "subtract"): + source = matrix[registers.index(op[2])] + matrix[r] = [x + (y if tag == "add" else -y) for x,y in zip(matrix[r], source)] + else: + raise ValueError("unknown paired primitive") + pa, da = rational(*a[3:]) + pb, db = rational(*b[3:]) + common = max(da, db) + expected = [[common, pa*(common//da), pb*(common//db), 0], + [0,common,0,0], [0,0,common,0], [0,0,0,0]] + demand(all(matrix[i][j]*common == expected[i][j]*denominator for i in range(4) for j in range(4)), + "integer four-column endpoint") + + +def eligible(a,b): + if a[0] != "scalar" or b[0] != "scalar" or a[2] == 0 or a[2] != b[2]: + return False + x,y = a[1],b[1] + return x[0] == y[0] == "add" and x[1] == y[1] and len({tuple(x[1]),tuple(x[2]),tuple(y[2]),W}) == 4 + + +def run(): + pins = json.loads((HERE/"SOURCES.json").read_text()) + for path, digest in pins["files"].items(): + possibilities = [path] + if path == "certificates/selected-result.json": + possibilities += ["certificates/checkpoints/frontier799.json"] + demand(any((ROOT/p).is_file() and hashlib.sha256((ROOT/p).read_bytes()).hexdigest() == digest + for p in possibilities), "independent source pin") + with tarfile.open(ROOT/pins["archive"]) as t: + raw = gzip.decompress(t.extractfile("native/local/LOCAL-PROGRAMS.json.gz").read()) + demand(hashlib.sha256(raw).hexdigest() == pins["members"]["native/local/LOCAL-PROGRAMS.json.gz"], "independent payload pin") + events = json.loads(raw)["backward"] + expected = json.loads((HERE/"EXPECTED.json").read_text()) + starts = expected["selected_events"] + demand(all(type(i) is int and 0 <= i < len(events)-1 for i in starts), "bad selected index") + demand(starts == sorted(set(starts)) and all(b-a > 1 for a,b in zip(starts,starts[1:])), "overlapping pairs") + census, weights = [], {} + for i in range(len(events)-1): + if not eligible(events[i],events[i+1]): + continue + a,b = events[i][1],events[i+1][1] + word = pair(a,b) + matrix_check(a,b,word) + old = len(single(a))+len(single(b)) + saving = old-len(word) + qs = [] + for op in (a,b): + n,d = rational(*op[3:]) + qs.append(str(n) if d == 1 else str(n)+"/"+str(d)) + census.append(dict(event=i,frame=events[i][2],coefficients=qs,before=old,after=len(word),saving=saving)) + if saving > 1: + weights[i] = saving + # Forward longest path, independent of the nomination's backward recurrence. + prefix = [0]*(len(events)+1) + for end in range(1,len(prefix)): + prefix[end] = prefix[end-1] + if end-2 in weights: + prefix[end] = max(prefix[end], prefix[end-2]+weights[end-2]) + demand(all(i in weights for i in starts), "unprofitable/ineligible recipe") + score = sum(weights[i] for i in starts) + demand(score == prefix[-1] and 2*score == expected["saving_real_primitives"], "path optimality") + demand(hashlib.sha256(encode(census)).hexdigest() == expected["census_sha256"], "independent census") + stream = hashlib.sha256() + chosen = set(starts) + count, i = 0,0 + while i < len(events): + e = events[i] + if e[0] != "scalar": + stream.update(encode(e)+b"\n") + i += 1 + continue + size = 2 if i in chosen else 1 + word = pair(e[1],events[i+1][1]) if size == 2 else single(e[1]) + for op in word: + stream.update(encode(["primitive",e[2],op])+b"\n") + count += len(word) + i += size + demand(stream.hexdigest() == expected["candidate"]["primitive_stream_sha256"], "independent complete stream") + demand(2*count == expected["candidate"]["real_primitives"], "independent complete count") + # These are genuine adverse endpoint controls, not just receipt mutations. + a,b = [events[starts[29]][1],events[starts[29]+1][1]] + word = pair(a,b) + rejected = 0 + for bad in (word[1:],word[:-1],word[:-2]+word[-1:],word[:1]+word[2:]): + try: + matrix_check(a,b,bad) + except ValueError: + rejected += 1 + else: + raise ValueError("integer control accepted") + return dict(status="PASS_INDEPENDENT_JOINT_HORNER", integer_pair_matrices=len(census), + matrix_entries_checked=16*len(census), optimal_single_component_saving=score, + complete_real_primitives=2*count, complete_stream_sha256=stream.hexdigest(), + selected_pairs=len(starts), controls=rejected) + + +if __name__ == "__main__": + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/x4-joint-horner-seed29/joint.py b/research/x4-joint-horner-seed29/joint.py new file mode 100644 index 0000000000..4623688552 --- /dev/null +++ b/research/x4-joint-horner-seed29/joint.py @@ -0,0 +1,105 @@ +"""Two-source binary Horner circuits; Ross Richardson / OpenAI Codex. + +Apache-2.0. Baseline primitive vocabulary follows icekylinx and PR696. +No repository state, stored witness, or search result is imported here. +""" +from fractions import Fraction + +WORK = ("W", 0) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def coefficient(op): + require(len(op) == 5 and op[0] == "add", "expected ADD") + require(type(op[3]) is int and type(op[4]) is int and op[4] > 0, + "invalid rational encoding") + q = Fraction(op[3], op[4]) + require(q != 0 and q.denominator & (q.denominator - 1) == 0, + "nonzero dyadic required") + return q + + +def compatible(first, second): + if first[0] != "scalar" or second[0] != "scalar": + return False + if first[2] != second[2] or first[2] == 0: + return False + a, b = first[1], second[1] + if a[0] != "add" or b[0] != "add" or a[1] != b[1]: + return False + regs = (tuple(a[1]), tuple(a[2]), tuple(b[2])) + return len(set(regs)) == 3 and WORK not in regs + + +def lower_pair(a, b): + """(T,S1,S2,W) -> (T+a*S1+b*S2,S1,S2,0), arbitrary input W. + + All returned operations must be hosted at the two original common frames. + Frame compatibility is checked by the caller on the complete events. + """ + qs = [coefficient(a), coefficient(b)] + target, sources = tuple(a[1]), [tuple(a[2]), tuple(b[2])] + require(a[1] == b[1] and len({target, *sources, WORK}) == 4, + "pair register alias") + k = max(q.denominator.bit_length() - 1 for q in qs) + nums = [q.numerator * ((1 << k) // q.denominator) for q in qs] + bits = max(abs(x).bit_length() for x in nums) + word = [] + sign = None + for bit in range(bits - 1, -1, -1): + if sign is not None: + word.append(("double", WORK)) + for n, source in zip(nums, sources): + if (abs(n) >> bit) & 1: + direction = 1 if n > 0 else -1 + if sign is None: + sign = direction + word.append(("copy", WORK, source)) + else: + word.append(("add" if sign == direction else "subtract", WORK, source)) + word.extend([("halve", WORK)] * k) + word.extend([("add" if sign == 1 else "subtract", target, WORK), ("clear", WORK)]) + expected = bits + sum(abs(x).bit_count() for x in nums) + k + 1 + require(len(word) == expected, "joint cost formula") + return word + + +def plan(events, baseline_lower): + """Maximum total saving among disjoint strictly arithmetic-saving pairs. + + Delta must exceed one, so every retained pair improves on deleting only + one redundant coefficient-work clear. Ties skip the earlier pair (seed 29). + """ + census, options = [], {} + for i in range(len(events) - 1): + a, b = events[i:i + 2] + if not compatible(a, b): + continue + word = lower_pair(a[1], b[1]) + before = len(baseline_lower(a[1])) + len(baseline_lower(b[1])) + delta = before - len(word) + row = {"event": i, "frame": a[2], "coefficients": [str(coefficient(a[1])), str(coefficient(b[1]))], + "before": before, "after": len(word), "saving": delta} + census.append(row) + if delta > 1: + options[i] = row + scores = [0] * (len(events) + 2) + take = set() + for i in range(len(events) - 1, -1, -1): + scores[i] = scores[i + 1] + if i in options and options[i]["saving"] + scores[i + 2] > scores[i]: + scores[i] = options[i]["saving"] + scores[i + 2] + take.add(i) + selected, i = [], 0 + while i < len(events): + if i in take: + selected.append(i) + i += 2 + else: + i += 1 + require(sum(options[i]["saving"] for i in selected) == scores[0], "path optimum") + return census, selected, scores diff --git a/research/x4-joint-horner-seed29/test_package.py b/research/x4-joint-horner-seed29/test_package.py new file mode 100644 index 0000000000..3a79dbc567 --- /dev/null +++ b/research/x4-joint-horner-seed29/test_package.py @@ -0,0 +1,152 @@ +"""Focused mathematical and packaging controls for the joint Horner package.""" +import importlib.util +import hashlib +import itertools +import json +import os +from pathlib import Path +import random +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("joint_verify_tests", HERE / "verify.py") +V = importlib.util.module_from_spec(spec) +spec.loader.exec_module(V) +I = V.module("joint_integer_tests", HERE / "independent.py") + + +def add(target, source, numerator, denominator=1, frame=3): + return ["scalar", ["add", ["L", target], ["L", source], numerator, denominator], frame] + + +class Circuits(unittest.TestCase): + def test_integer_and_fraction_identities(self): + # Different denominator alignments and signs, including large odd digits. + for p,q,d,e in itertools.product((-31,-3,1,7),(-15,-1,3,17),(1,2,8),(1,4,16)): + a,b = add(0,1,p,d)[1],add(0,2,q,e)[1] + word = V.J.lower_pair(a,b) + V.check_pair(a,b,word) + V.check_pair_cost(a,b,word) + self.assertEqual(word,I.pair(a,b)) + I.matrix_check(a,b,word) + + def test_aliases_and_non_dyadics(self): + a,b = add(0,1,3,4)[1],add(0,2,-1,2)[1] + for source in (["L",0],["L",1],["W",0]): + bad = [*b[:2],source,*b[3:]] + with self.assertRaisesRegex(ValueError,"alias"): + V.J.lower_pair(a,bad) + for numerator,denominator in ((0,1),(1,3),(True,2),(1,0),(1,-2),(1,2.0)): + bad = [*a[:3],numerator,denominator] + with self.assertRaises(ValueError): + V.J.lower_pair(bad,b) + + def test_physical_event_boundaries(self): + a,b = add(0,1,1,2),add(0,2,1,2) + self.assertTrue(V.J.compatible(a,b)) + for changed in (add(0,2,1,2,4),add(0,2,1,2,0),["phase",0,0]): + self.assertFalse(V.J.compatible(a,changed)) + _,_,lower = V.inputs() + census,chosen,_ = V.J.plan([a,["phase",0,0],b],lower) + self.assertEqual((census,chosen),([],[])) + + def test_endpoint_and_cost_are_distinct(self): + a,b = add(0,1,1,2)[1],add(0,2,1,2)[1] + word = V.J.lower_pair(a,b) + for mutated in (word[1:],word[:-1],word[:-2]+word[-1:]): + with self.assertRaisesRegex(ValueError,"endpoint"): + V.check_pair(a,b,mutated) + expensive = word + [("clear",V.WORK)] + V.check_pair(a,b,expensive) + with self.assertRaisesRegex(ValueError,"cost"): + V.check_pair_cost(a,b,expensive) + + def test_path_dp_by_exhaustive_small_matchings(self): + _,_,lower = V.inputs() + rng = random.Random(29) + for _ in range(30): + events = [add(0,1+i%2,rng.choice((-3,-1,1,5)),rng.choice((1,2,4))) for i in range(9)] + census,chosen,scores = V.J.plan(events,lower) + weights = {r["event"]:r["saving"] for r in census if r["saving"]>1} + optimum = 0 + positions = list(weights) + for mask in range(1<>j&1] + if all(b-a>1 for a,b in zip(selected,selected[1:])): + optimum = max(optimum,sum(weights[i] for i in selected)) + self.assertEqual(scores[0],optimum) + self.assertEqual(sum(weights[i] for i in chosen),optimum) + + def test_independent_complete_certificate(self): + self.assertEqual(I.run()["complete_real_primitives"],130602) + + +class Packaging(unittest.TestCase): + def test_minimal_relocation_and_corruption(self): + pins = json.loads((HERE/"SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="joint Horner controls ") as directory: + root = Path(directory)/"minimal tree with spaces" + package = root/"research"/HERE.name + package.mkdir(parents=True) + for file in HERE.iterdir(): + if file.is_file(): + shutil.copy2(file,package/file.name) + for relative in pins["files"]: + actual = relative + if relative == "certificates/selected-result.json" and hashlib.sha256((ROOT/relative).read_bytes()).hexdigest() != pins["files"][relative]: + actual = "certificates/checkpoints/frontier799.json" + dest = root/actual + dest.parent.mkdir(parents=True,exist_ok=True) + shutil.copy2(ROOT/actual,dest) + environment = dict(os.environ, PYTHONDONTWRITEBYTECODE="1") + command = [sys.executable,"-I","-O","-B",str(package/"verify.py")] + def run(command=command): + return subprocess.run(command,cwd=directory,env=environment,capture_output=True,text=True,timeout=120) + result = run() + self.assertEqual(result.returncode,0,result.stderr) + self.assertIn("saved=13072",result.stdout) + source = root/"research/complex-dyadic-lowering/lower.py" + original = source.read_bytes() + source.write_bytes(original+b"\n# corrupt pinned source\n") + result = run() + self.assertNotEqual(result.returncode,0) + self.assertIn("source pin",result.stderr) + source.write_bytes(original) + receipt = package/"EXPECTED.json" + original = receipt.read_bytes() + data = json.loads(original) + data["selected_events"][1] = data["selected_events"][0]+1 + receipt.write_text(json.dumps(data)) + result = run([sys.executable,"-I","-O","-B",str(package/"independent.py")]) + self.assertNotEqual(result.returncode,0) + self.assertIn("overlapping pairs",result.stderr) + data = json.loads(original) + data["selected_events"] = data["selected_events"][1:] + receipt.write_text(json.dumps(data)) + result = run([sys.executable,"-I","-O","-B",str(package/"independent.py")]) + self.assertNotEqual(result.returncode,0) + self.assertIn("path optimality",result.stderr) + receipt.write_bytes(original) + # Checkpoint lookup must tolerate a new active selection, but must + # still reject corruption of the exact historical checkpoint. + contextual = root/"certificates/selected-result.json" + checkpoint = root/"certificates/checkpoints/frontier799.json" + if not checkpoint.exists(): + checkpoint.parent.mkdir(parents=True,exist_ok=True) + shutil.copy2(contextual,checkpoint) + contextual.write_text('{"kappa":"unrelated new frontier"}\n') + result = run([sys.executable,"-I","-O","-B",str(package/"independent.py")]) + self.assertEqual(result.returncode,0,result.stderr) + checkpoint.write_text('{}\n') + result = run() + self.assertNotEqual(result.returncode,0) + self.assertIn("source pin: certificates/selected-result.json",result.stderr) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/x4-joint-horner-seed29/verify.py b/research/x4-joint-horner-seed29/verify.py new file mode 100644 index 0000000000..557fdb0ba9 --- /dev/null +++ b/research/x4-joint-horner-seed29/verify.py @@ -0,0 +1,348 @@ +"""Exact finite X4 backward scalar circuit replay. Standard library, offline. + +Ross Richardson, with substantial OpenAI Codex assistance. Apache-2.0. +Run normally to compare the complete deterministic receipt; --write creates it. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + result = importlib.util.module_from_spec(spec) + spec.loader.exec_module(result) + return result + + +J = module("joint_horner", HERE / "joint.py") +require, WORK = J.require, J.WORK + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def sha(value): + return hashlib.sha256(value).hexdigest() + + +def inputs(): + pins = json.loads((HERE / "SOURCES.json").read_text()) + require(pins["base_commit"] == "91a2094f2e022930069e8cfdc810a3ea1b81cd09", "starting base metadata") + selected = None + for name, expected in pins["files"].items(): + locations = [name] + if name == "certificates/selected-result.json": + locations.append("certificates/checkpoints/frontier799.json") + matches = [ROOT / path for path in locations + if (ROOT / path).is_file() and sha((ROOT / path).read_bytes()) == expected] + require(matches, "source pin: " + name) + if name == "certificates/selected-result.json": + selected = json.loads(matches[0].read_text()) + members = {} + with tarfile.open(ROOT / pins["archive"]) as archive: + for name, expected in pins["members"].items(): + matches = [m for m in archive.getmembers() if m.name == name] + require(len(matches) == 1 and matches[0].isfile(), "archive member identity") + raw = archive.extractfile(matches[0]).read() + if name.endswith(".gz"): + raw = gzip.decompress(raw) + require(sha(raw) == expected, "member payload pin: " + name) + members[name] = json.loads(raw) + events = members["native/local/LOCAL-PROGRAMS.json.gz"] + checks = members["native/local/LOCAL-CHECKS.json"] + for orientation in ("forward", "backward"): + require(sha(canonical(events[orientation])) == checks[orientation]["sha256"], "source event binding") + spec = json.loads((ROOT / "research/gauge44-frames-x/data/SPEC.json").read_text())["providers"]["gauge44"] + require(spec["program_hashes"] == {o: checks[o]["sha256"] for o in checks}, "selected SPEC binding") + require(spec["expected_profile"] == checks["backward"]["paid_profile"], "selected recursive profile") + require(selected["kappa"] == "1661634653669567/1000000000000000000", "selected witness context") + require(pins["source_heads"]["799"] == selected["audited_source_head"], "PR799 source head") + require(pins["source_heads"]["741"] == selected["reviewed_dependency_heads"]["741"], "PR741 source head") + baseline = module("retained_pr696_lowering", ROOT / "research/complex-dyadic-lowering/lower.py") + return events, checks, baseline.lower + + +def step(rows, op): + tag, dst = op[:2] + if tag == "clear": + rows[dst] = {} + elif tag == "copy": + rows[dst] = rows[op[2]].copy() + elif tag in ("double", "halve", "negate"): + q = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[dst] = {i: q * x for i, x in rows[dst].items()} + elif tag in ("add", "subtract"): + require(dst != op[2], "primitive self ADD") + for i, x in rows[op[2]].items(): + value = rows[dst].get(i, Q(0)) + (x if tag == "add" else -x) + if value: + rows[dst][i] = value + else: + rows[dst].pop(i, None) + else: + raise ValueError("unknown primitive") + + +def direct(rows, op): + tag, dst = op[0], tuple(op[1]) + if tag in ("clear", "copy"): + step(rows, (tag, dst, tuple(op[2])) if tag == "copy" else (tag, dst)) + elif tag == "scale": + q = Q(op[2], op[3]) + rows[dst] = {i: q*x for i, x in rows[dst].items()} + elif tag == "add": + q = J.coefficient(op) + for i, x in rows[tuple(op[2])].items(): + value = rows[dst].get(i, Q(0)) + q*x + if value: + rows[dst][i] = value + else: + rows[dst].pop(i, None) + rows[WORK] = {} + else: + raise ValueError("unknown macro") + + +def check_pair(a, b, word): + regs = [tuple(a[1]), tuple(a[2]), tuple(b[2]), WORK] + require(len(set(regs)) == 4, "local register aliases") + actual = {r: {i: Q(1)} for i, r in enumerate(regs)} + expected = {r: row.copy() for r, row in actual.items()} + direct(expected, a) + direct(expected, b) + for op in word: + step(actual, op) + require(actual == expected, "four-column pair endpoint") + + +def check_pair_cost(a, b, word): + # Recount from the coefficients, independently of lower_pair's loop. + qa, qb = J.coefficient(a), J.coefficient(b) + denominator = max(qa.denominator, qb.denominator) + numerators = [abs(q.numerator) * (denominator // q.denominator) for q in (qa, qb)] + cost = max(x.bit_length() for x in numerators) + sum(x.bit_count() for x in numerators) + denominator.bit_length() + require(len(word) == cost, "joint primitive cost") + + +def retained_count(op): + if op[0] in ("copy", "clear"): + return 1 + q = Q(*op[3:]) if op[0] == "add" else Q(*op[2:]) + a, d = abs(q.numerator), q.denominator + if op[0] == "scale": + return abs(a.bit_length() - d.bit_length()) + int(q < 0) + return a.bit_length() + a.bit_count() + d.bit_length() + 1 + + +def replay(events, lower, chosen=()): + chosen = set(chosen) + # Arbitrary logical, center and coefficient-work columns, including dirt. + regs = [("L", i) for i in range(728)] + [("C", i) for i in range(8)] + [WORK] + rows = {r: {i: Q(1)} for i, r in enumerate(regs)} + envelope = {r: Q(1) for r in regs} + peak = envelope_peak = Q(1) + depth = 0 + tags, paid = Counter(), Counter() + operand_reads = source_reads = scalar_macros = original_count = 0 + stream = hashlib.sha256() + i = 0 + while i < len(events): + event = events[i] + if event[0] != "scalar": + require(event[0] in ("climb", "center", "phase", "adapter", "residual_adapter"), "unknown event") + if event[0] == "climb": + paid[event[5]] += 1 + if event[0] == "center": + paid[event[4]] += 1 + stream.update(canonical(event) + b"\n") + i += 1 + continue + count = 2 if i in chosen else 1 + group = events[i:i + count] + require(len(group) == count and all(e[0] == "scalar" and e[2] == event[2] for e in group), "pair frame boundary") + if count == 2: + require(J.compatible(*group), "ineligible selected pair") + word = J.lower_pair(group[0][1], group[1][1]) + else: + word = lower(event[1]) + touched = {WORK} + for e in group: + op = e[1] + touched.add(tuple(op[1])) + if op[0] in ("add", "copy"): + touched.add(tuple(op[2])) + before = {r: rows[r].copy() for r in touched} + expected = {r: row.copy() for r, row in before.items()} + for e in group: + direct(expected, e[1]) + scalar_macros += 1 + original_count += retained_count(e[1]) + for op in word: + tag, dst = op[:2] + require(dst in touched and (len(op) < 3 or op[2] in touched), "undeclared register") + step(rows, op) + if tag == "clear": + envelope[dst] = Q(0) + elif tag == "copy": + envelope[dst] = envelope[op[2]] + elif tag in ("double", "halve", "negate"): + envelope[dst] *= {"double": Q(2), "halve": Q(1, 2), "negate": Q(1)}[tag] + else: + envelope[dst] += envelope[op[2]] + tags[tag] += 1 + operand_reads += 0 if tag == "clear" else 2 if tag in ("add", "subtract") else 1 + source_reads += int(len(op) == 3 and op[2] != WORK) + peak = max(peak, sum(map(abs, rows[dst].values()), Q(0))) + if rows[dst]: + depth = max(depth, max(x.denominator.bit_length() - 1 for x in rows[dst].values())) + envelope_peak = max(envelope_peak, envelope[dst]) + stream.update(canonical(["primitive", event[2], op]) + b"\n") + require(all(rows[r] == expected[r] for r in touched), "group boundary exact map") + i += count + for r in range(728): + expected = {r: Q(1)} + if r < 112: + expected[r + 112] = Q(-1) + require(rows[("L", r)] == expected, "full backward scalar map") + require(all(not rows[r] for r in regs if r[0] != "L"), "dirty private input not erased") + require(envelope_peak < 2**192, "retained local magnitude allowance") + return {"real_primitives": 2*sum(tags.values()), "real_primitive_tags": {k: 2*v for k,v in sorted(tags.items())}, + "real_operand_reads": 2*operand_reads, "real_nonwork_source_reads": 2*source_reads, + "primitive_stream_sha256": stream.hexdigest(), "all_formal_columns": len(regs), + "scalar_macros_charged": scalar_macros, "retained_horner_real_primitives": 2*original_count, + "paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "scalar_prefix_row_l1": str(peak), "scalar_fractional_depth": depth, + "positive_envelope_peak": str(envelope_peak), "retained_payload_bits": 192} + + +def controls(events, selected): + index = selected[29 % len(selected)] + a, b = (e[1] for e in events[index:index + 2]) + word = J.lower_pair(a, b) + rejected = [] + for k in range(len(word)): + try: + check_pair(a, b, word[:k] + word[k+1:]) + except ValueError: + rejected.append("delete_primitive_" + str(k)) + else: + raise ValueError("accepted missing primitive") + sign_index = next(i for i, x in enumerate(word) if x[0] in ("add", "subtract")) + bad = word.copy() + old = bad[sign_index] + bad[sign_index] = ("subtract" if old[0] == "add" else "add", *old[1:]) + try: + check_pair(a, b, bad) + except ValueError: + rejected.append("wrong_source_sign") + else: + raise ValueError("accepted sign mutation") + for label, edit in (("wrong_frame", lambda x: x.__setitem__(2, x[2]+1)), + ("cross_non_scalar", lambda x: x.__setitem__(0, "phase"))): + ev = json.loads(json.dumps(events[index:index+2])) + edit(ev[1]) + require(not J.compatible(*ev), "accepted frame/boundary mutation") + rejected.append(label) + for label, q in (("nondyadic", [1, 3]), ("zero", [0, 1])): + invalid = list(a) + invalid[3:] = q + try: + J.lower_pair(invalid, b) + except ValueError: + rejected.append(label) + else: + raise ValueError("accepted invalid coefficient") + bad = list(b) + bad[2] = a[2] + try: + J.lower_pair(a, bad) + except ValueError: + rejected.append("aliased_sources") + else: + raise ValueError("accepted source alias") + # An endpoint-equivalent overpriced word must be caught by the cost gate. + inflated = word + [("clear", WORK)] * 10 + check_pair(a, b, inflated) + try: + check_pair_cost(a, b, inflated) + except ValueError as error: + require(str(error) == "joint primitive cost", "wrong cost rejection") + rejected.append("endpoint_neutral_cost_inflation") + else: + raise ValueError("accepted cost inflation") + return {"event": index, "rejected": rejected} + + +def verify(): + programs, checks, lower = inputs() + events = programs["backward"] + census, selected, scores = J.plan(events, lower) + require(selected, "no useful candidate") + for row in census: + i = row["event"] + a, b = events[i][1], events[i+1][1] + word = J.lower_pair(a, b) + check_pair(a, b, word) + check_pair_cost(a, b, word) + baseline = replay(events, lower) + candidate = replay(events, lower, selected) + require(baseline["retained_horner_real_primitives"] == checks["backward"]["real_component_primitive_bound"], "retained bill") + for receipt in (baseline, candidate): + require(receipt["scalar_macros_charged"] == checks["backward"]["scalar_macros"], "macro accounting") + require(receipt["paid_profile"] == checks["backward"]["paid_profile"], "recursive profile") + require(baseline["real_primitives"]-candidate["real_primitives"] == 2*scores[0], "complete primitive saving") + require(candidate["scalar_prefix_row_l1"] == baseline["scalar_prefix_row_l1"], "scalar prefix maximum changed") + require(candidate["scalar_fractional_depth"] == baseline["scalar_fractional_depth"], "scalar grid changed") + require(candidate["positive_envelope_peak"] == baseline["positive_envelope_peak"], "positive envelope changed") + require(candidate["real_nonwork_source_reads"] == baseline["real_nonwork_source_reads"], "source-read bill changed") + fcount = 2*sum(len(lower(e[1])) for e in programs["forward"] if e[0] == "scalar") + contract = json.loads((ROOT / "research/gauge44-frames-x/data/SPEC.json").read_text())["providers"]["gauge44"]["complete_contract"] + children = sum(map(int, checks["backward"]["paid_profile"].values())) + adapters = 16*(checks["backward"]["scalar_macros"]+children+728+8)+64*73 + compiler = 64*74**3 + require(adapters == contract["local_adapters"] and compiler == contract["compiler"], "inherited adapter formula") + before = max(fcount,baseline["real_primitives"]) + after = max(fcount,candidate["real_primitives"]) + non_scalar = [e for e in events if e[0] != "scalar"] + return {"status": "PASS_X4_JOINT_HORNER", "orientation": "backward", "candidates": len(census), + "profitable_candidates": sum(x["saving"] > 1 for x in census), + "census_sha256": sha(canonical(census)), "selected_events": selected, + "selected_pairs": len(selected), "dp_sha256": sha(canonical(scores)), + "saving_real_primitives": 2*scores[0], "baseline": baseline, "candidate": candidate, + "unchanged_forward_pr696_primitives": fcount, + "orientation_maximum_before": before, "orientation_maximum_after": after, + "conservative_local_recount": {"adapters_retained": adapters,"compiler": compiler, + "before":before+adapters*compiler,"after":after+adapters*compiler, + "saving":before-after,"scope":"arithmetic recount only; no global invoice admission"}, + "unchanged_non_scalar_events":len(non_scalar),"non_scalar_events_sha256":sha(canonical(non_scalar)), + "controls": controls(events, selected), "scope": "finite scalar construction; no new kappa"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a new receipt exclusively") + args = parser.parse_args() + result = verify() + if args.write: + with args.write.open("x") as out: + out.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((HERE / "EXPECTED.json").read_text()) + require(canonical(result) == canonical(expected), "frozen receipt mismatch") + print(f"PASS_X4_JOINT_HORNER candidates={result['candidates']} pairs={result['selected_pairs']} " + f"saved={result['saving_real_primitives']} columns=737 no_new_kappa") + + +if __name__ == "__main__": + main() From a3245bf22fa2a2eb778b11128cbc605b130d737f Mon Sep 17 00:00:00 2001 From: ross Date: Wed, 14 Oct 2026 00:54:55 +1100 Subject: [PATCH 2/2] Record joint Horner sprint submission and final overlap check --- research/x4-joint-horner-seed29/CLAIM.json | 17 +++++- research/x4-joint-horner-seed29/OVERLAP.json | 55 ++++++++++++++++++++ 2 files changed, 71 insertions(+), 1 deletion(-) diff --git a/research/x4-joint-horner-seed29/CLAIM.json b/research/x4-joint-horner-seed29/CLAIM.json index 72fd5c7c8b..087a74cd67 100644 --- a/research/x4-joint-horner-seed29/CLAIM.json +++ b/research/x4-joint-horner-seed29/CLAIM.json @@ -33,5 +33,20 @@ "open_pr_count": 722, "latest_observed_pr": 932 }, - "status": "claimed" + "status": "submitted", + "completed_utc": "2026-10-13T13:54:10Z", + "integration_base_commit": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "result": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/945", + "classification": "finite complex-supplier circuit construction; no new kappa", + "candidate_pairs_checked": 6112, + "selected_pairs": 1586, + "backward_real_primitives_saved": 13072, + "conservative_local_bound_saved": 16, + "formal_input_columns": 737, + "current_selected_pr": 890, + "current_selected_kappa": "0.001661957774647029", + "scope_change": "Starting X4 selection became the official PR799 historical checkpoint during the sprint. Its exact inputs remain unchanged; no U8 transport is claimed.", + "verification": "Full backward Fraction replay, separate integer circuit/stream/path checker, 12+4 adverse controls, 7 tests including optimized minimal relocation, and refreshed selected-record integrity passed. No hosted CI pass claimed." + } } diff --git a/research/x4-joint-horner-seed29/OVERLAP.json b/research/x4-joint-horner-seed29/OVERLAP.json index 984f67d528..d23e963a28 100644 --- a/research/x4-joint-horner-seed29/OVERLAP.json +++ b/research/x4-joint-horner-seed29/OVERLAP.json @@ -654,5 +654,60 @@ "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/719" } ] + }, + "publication_refresh": { + "observed_utc": "2026-10-13T13:54:10Z", + "main": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "immediately_before_submission_latest_pr": 943, + "recent_prs": [ + { + "headRefOid": "4fa24646a038b788a62771356305fd6fb8f9ddd5", + "number": 945, + "title": "Finite construction: joint Horner saves 13,072 PR799 backward primitives (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/945" + }, + { + "headRefOid": "3830be96a7d4e9dea4a12a1ef65b71ef1765a759", + "number": 944, + "title": "Research: classify signed 3x3 connector obstructions and a 14-query repair (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/944" + }, + { + "headRefOid": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "number": 943, + "title": "Research: sharp four/five-source dirty-connector boundary (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943" + }, + { + "headRefOid": "1960cfa919a0945d0ca4cb14ea96237000037903", + "number": 942, + "title": "Conditional \u03ba = 0.001661960547713947: T37 whole-owner packing and all-T bound", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/942" + }, + { + "headRefOid": "8af78333709a2eafd84463a7dc91467be5618b49", + "number": 941, + "title": "Finite bit construction: certify R439 matching floor and save 31 further ADDs", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/941" + }, + { + "headRefOid": "fccac36fa9bcc063c4fda733299a22349ce10e56", + "number": 940, + "title": "Research audit: exact scope of retained Fourier layout cancellation (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/940" + }, + { + "headRefOid": "3a8ec54d62fb8824c658dc7ed356f99423cac8cf", + "number": 939, + "title": "Scoped negative result: E8 star-copy ratio cannot improve through 55 punctures (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/939" + }, + { + "headRefOid": "df645942469e6a739ec94010a6068c398f4a6c86", + "number": 938, + "title": "Independent verification: complete minimum-word census for dirty fanout stars (no new kappa)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/938" + } + ] } }