diff --git a/research/dirty-fanout-star-census/CERTIFICATE.json b/research/dirty-fanout-star-census/CERTIFICATE.json new file mode 100644 index 0000000000..a853cb9a6c --- /dev/null +++ b/research/dirty-fanout-star-census/CERTIFICATE.json @@ -0,0 +1,949 @@ +{ + "assignment_seed": 79, + "census": [ + { + "accepted_by_length": [ + 0, + 0, + 0, + 0, + 4 + ], + "alphabet_size": 4, + "maximum_length": 4, + "minimum_word_count": 4, + "outputs": 1, + "raw_words_through_horizon": 341, + "retained_states_by_length": [ + 1, + 4, + 11, + 8, + 1 + ] + }, + { + "accepted_by_length": [ + 0, + 0, + 0, + 0, + 0, + 0, + 24 + ], + "alphabet_size": 6, + "maximum_length": 6, + "minimum_word_count": 24, + "outputs": 2, + "raw_words_through_horizon": 55987, + "retained_states_by_length": [ + 1, + 4, + 14, + 32, + 26, + 8, + 1 + ] + }, + { + "accepted_by_length": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 288 + ], + "alphabet_size": 8, + "maximum_length": 8, + "minimum_word_count": 288, + "outputs": 3, + "raw_words_through_horizon": 19173961, + "retained_states_by_length": [ + 1, + 4, + 14, + 36, + 72, + 64, + 26, + 8, + 1 + ] + }, + { + "accepted_by_length": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 5760 + ], + "alphabet_size": 10, + "maximum_length": 10, + "minimum_word_count": 5760, + "outputs": 4, + "raw_words_through_horizon": 11111111111, + "retained_states_by_length": [ + 1, + 4, + 14, + 36, + 77, + 142, + 131, + 64, + 26, + 8, + 1 + ] + }, + { + "accepted_by_length": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 172800 + ], + "alphabet_size": 12, + "maximum_length": 12, + "minimum_word_count": 172800, + "outputs": 5, + "raw_words_through_horizon": 9726655034461, + "retained_states_by_length": [ + 1, + 4, + 14, + 36, + 77, + 148, + 253, + 240, + 131, + 64, + 26, + 8, + 1 + ] + } + ], + "emitter_cases": [ + { + "branch_factors": [ + 2 + ], + "common_factors": 1, + "dirty_roles": 2, + "leaf_calls": 10, + "mode": "batch", + "outputs": 1, + "word_sha256": "7a9204716945606310cbada39faa7070dce667ec02394420e9204c7a1b3380d5" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 1, + "dirty_roles": 2, + "leaf_calls": 10, + "mode": "separate", + "outputs": 1, + "word_sha256": "7a9204716945606310cbada39faa7070dce667ec02394420e9204c7a1b3380d5" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 1, + "dirty_roles": 2, + "leaf_calls": 10, + "mode": "grouped", + "outputs": 1, + "word_sha256": "7a9204716945606310cbada39faa7070dce667ec02394420e9204c7a1b3380d5" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 2, + "dirty_roles": 2, + "leaf_calls": 16, + "mode": "batch", + "outputs": 1, + "word_sha256": "1c906eb140c64325d675c038c884a3bdba4f33ecc4cabac52182dbe3a2971381" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 2, + "dirty_roles": 2, + "leaf_calls": 16, + "mode": "separate", + "outputs": 1, + "word_sha256": "1c906eb140c64325d675c038c884a3bdba4f33ecc4cabac52182dbe3a2971381" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 2, + "dirty_roles": 2, + "leaf_calls": 16, + "mode": "grouped", + "outputs": 1, + "word_sha256": "1c906eb140c64325d675c038c884a3bdba4f33ecc4cabac52182dbe3a2971381" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 28, + "mode": "batch", + "outputs": 1, + "word_sha256": "8bdb0ee5dec35c74d07024b66dd38a4bdb73ccdabf14549d62bf2bc66535b5e2" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 28, + "mode": "separate", + "outputs": 1, + "word_sha256": "c458c260ae312c7cb06534c7cdcf3834cc9ec71996f9db494df3019afd2f1463" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 28, + "mode": "grouped", + "outputs": 1, + "word_sha256": "8bdb0ee5dec35c74d07024b66dd38a4bdb73ccdabf14549d62bf2bc66535b5e2" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 40, + "mode": "batch", + "outputs": 1, + "word_sha256": "b919d690fb0a9d93c2aa6c0d047224bbb619445fec5c6fb2e586770aaf352b42" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 40, + "mode": "separate", + "outputs": 1, + "word_sha256": "e50f5f825ab774f8c3a51dfceabc1ccca770bbf58f140b63731dd8ad57223424" + }, + { + "branch_factors": [ + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 40, + "mode": "grouped", + "outputs": 1, + "word_sha256": "b919d690fb0a9d93c2aa6c0d047224bbb619445fec5c6fb2e586770aaf352b42" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 30, + "mode": "batch", + "outputs": 2, + "word_sha256": "7df5f6eef82e35f995f7d023e4242fc95e033f65af5d81b34d923e6b635ec594" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 26, + "mode": "separate", + "outputs": 2, + "word_sha256": "42915de54752e2e14e0bf25260389fcc4b98d14b8de3cd26d82d354c11c8762e" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 32, + "mode": "grouped", + "outputs": 2, + "word_sha256": "2c50891974d179163080a94cd2e95a4d91daf8c00f9e5ce1d0f5e97676acd3ef" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 36, + "mode": "batch", + "outputs": 2, + "word_sha256": "6781eb02246d07547d5ed655940ef637132086a02c53c13471d9826cff9d07a4" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 44, + "mode": "separate", + "outputs": 2, + "word_sha256": "e4a30cf8822b2a092ba03335bfaed5677e416fd7e8af6d46dbe160f127c0c25b" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 44, + "mode": "grouped", + "outputs": 2, + "word_sha256": "e4a30cf8822b2a092ba03335bfaed5677e416fd7e8af6d46dbe160f127c0c25b" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 48, + "mode": "batch", + "outputs": 2, + "word_sha256": "0e062efeb255cf2f95192978cbe7e81c5bb935bad613cecc907b51937bb5be3b" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 68, + "mode": "separate", + "outputs": 2, + "word_sha256": "31f4eb180ce49917bbad956f136f36875d5294d1545a593bc0734d730f563c56" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 68, + "mode": "grouped", + "outputs": 2, + "word_sha256": "a9f5a3758d9ae4c8fd31fc35d58ed1db7a74098e69b510bd7b32bc4c692b89a2" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 60, + "mode": "batch", + "outputs": 2, + "word_sha256": "1788422bd282912121b505605e4ef8a66b7a4c85919c4482575d2510bdbaf206" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 92, + "mode": "separate", + "outputs": 2, + "word_sha256": "02de37243496445333b685d387d8c7c6c71f1983b587db664af1c9380a1c7ec5" + }, + { + "branch_factors": [ + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 92, + "mode": "grouped", + "outputs": 2, + "word_sha256": "a45150970450330efde9f5799fcf0010f406d6928caf99f1541f0fb24d9e7d51" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 32, + "mode": "batch", + "outputs": 3, + "word_sha256": "34c7b764487a2b52e5cdf1a1547f04c267609c45014a9ee73d1eb290743bd6e8" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 30, + "mode": "separate", + "outputs": 3, + "word_sha256": "c8fdfe78602b55272b52817f75370594bd5cf2ce2c2c0eacd538eaee8ae9ca18" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 36, + "mode": "grouped", + "outputs": 3, + "word_sha256": "74e1606cda84660f03b8bc459e089158069b4c4f85d43328b7d79cbed3566948" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 38, + "mode": "batch", + "outputs": 3, + "word_sha256": "991d7ada32dd38deb85ffba3890104a0ccee2c5e653b22661624fcf2107edef7" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 54, + "mode": "separate", + "outputs": 3, + "word_sha256": "7b5c316837ecca06af94e797cc0cb709ca83d1017513519a55d955155cb101b4" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 54, + "mode": "grouped", + "outputs": 3, + "word_sha256": "8c66486fad4c9390fd9fbf5f09313a5fae22c5cf5e86f500293af57cb4e52ef6" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 50, + "mode": "batch", + "outputs": 3, + "word_sha256": "68409f5a070b55d98bb03dea2d3ac5de5b8826bebdf9277e389abbe3437f25da" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 84, + "mode": "separate", + "outputs": 3, + "word_sha256": "9a39915c9ac4d15c7e20dd54ffee2a152f1439147b7deca6977bd3fe406cf557" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 90, + "mode": "grouped", + "outputs": 3, + "word_sha256": "55b2b0f60fe2c03e24444b3a1e337bb167a40ae7a96d2a7ce88bf4bde4eea33d" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 62, + "mode": "batch", + "outputs": 3, + "word_sha256": "87c50b9f04de7669026796c2f480a6a3222bbc707f59170d760f1979dedc4039" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 120, + "mode": "separate", + "outputs": 3, + "word_sha256": "39c09b53d7c1881d4b4598497b0b4215e266b422cc5e54a8e018c6b6f02c04f2" + }, + { + "branch_factors": [ + 2, + 3, + 1 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 126, + "mode": "grouped", + "outputs": 3, + "word_sha256": "46e76eef808024a2298a9655cb5182e5243b23441833aa4cb6d5a6e6fe67da5f" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 40, + "mode": "batch", + "outputs": 4, + "word_sha256": "3d71cd242aea01be79b8f38b48ff375b1e699a7b93e5892a6192319accd483d2" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 40, + "mode": "separate", + "outputs": 4, + "word_sha256": "002e32c8f0722c7341f2015344d371d26735f6b21fcee2f6e695b49bb32b9e66" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 46, + "mode": "grouped", + "outputs": 4, + "word_sha256": "9379d7cadd2689234a651b38338d5a7c92fc527f3119ddeabdfd6b905cdd3f1a" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 46, + "mode": "batch", + "outputs": 4, + "word_sha256": "eb4fc53a7f4e6ecffa0290443c7727f7a52c66b65e88cfb8e1fd516777be6514" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 70, + "mode": "separate", + "outputs": 4, + "word_sha256": "d6fc9d480247872ef4b64a789f2d908cf4092b76d5fbbbc1b867f3efb94075b2" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 70, + "mode": "grouped", + "outputs": 4, + "word_sha256": "32c1bb5594b9e3155b3ec2fe2241509d74614dae7d54a014e8a32d71be83774b" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 58, + "mode": "batch", + "outputs": 4, + "word_sha256": "8179aaed50d42ed888216e3f541f4e9c46de01a64fed7d183dc79846a02ff955" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 112, + "mode": "separate", + "outputs": 4, + "word_sha256": "fd3fb3d926c0a58af782e59348b297082f92e9582bc05784353172493f3c81f3" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 118, + "mode": "grouped", + "outputs": 4, + "word_sha256": "567e662ae1683f14a79a1ee0a57a52638bdd91c92b898b68f7c8b57662724f86" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 70, + "mode": "batch", + "outputs": 4, + "word_sha256": "68df78c20f87f7d20095e092d377cadda439fd7e02da0b0a9fe1794ea031a0a6" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 160, + "mode": "separate", + "outputs": 4, + "word_sha256": "839fd271d170e88f10f9a7c20ecb00b0e760a3a20b4ff7e97e19d1916d648a00" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 166, + "mode": "grouped", + "outputs": 4, + "word_sha256": "807304dcbe974751dc965ed81853abc0cabb0f0e1e3b82e5d0fb2b7750d81756" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 60, + "mode": "batch", + "outputs": 5, + "word_sha256": "c3c205d83c3cf8b78204d18ac3863c98c91a242a82371f7d0197593a5114bb5d" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 56, + "mode": "separate", + "outputs": 5, + "word_sha256": "8038ab4c09ac3f7ec826c4f5c0c1efb0cbb5eb3dd63261f29c71ddb8f3470e82" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 1, + "dirty_roles": 3, + "leaf_calls": 68, + "mode": "grouped", + "outputs": 5, + "word_sha256": "c29d0024a1ca0a64f2bbd3a42149fcd888946b18bda5b28a3449fd34f1050086" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 66, + "mode": "batch", + "outputs": 5, + "word_sha256": "ddb5b8c76d2136d00ac132895535ca74dea806e0f64e5ac494e9a9e9d5a8da0f" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 98, + "mode": "separate", + "outputs": 5, + "word_sha256": "d2ac77beb96b7f82c143df4a5255a3d33529b84a4da923fda6f49dd98ad7f104" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 2, + "dirty_roles": 3, + "leaf_calls": 98, + "mode": "grouped", + "outputs": 5, + "word_sha256": "697677117c9d5721dc11a9a2465f2e57c46ded438da15bf93f9b4f5c29ab8029" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 78, + "mode": "batch", + "outputs": 5, + "word_sha256": "9aeef0acd0e737a7cb775ef94ecb8850a1f63a62a5a7b08e5b743b7a810a8219" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 152, + "mode": "separate", + "outputs": 5, + "word_sha256": "c095520d6f8725cbc9f7996ad9adf61c5703bf0b1729e5e4c2c0414e1e0af246" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 3, + "dirty_roles": 3, + "leaf_calls": 158, + "mode": "grouped", + "outputs": 5, + "word_sha256": "60e202d793480db3d1d9cfd65a59c1988020e26284f4c27bb3f32859f365c7a3" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 90, + "mode": "batch", + "outputs": 5, + "word_sha256": "d351603e29f897d1fd2779c23f1d844e7827c725aa5178ae2a0428b7dbcf9005" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 212, + "mode": "separate", + "outputs": 5, + "word_sha256": "f16a71f5ea217058f68925cbe5cbbc0008e5c531aab874cffd10df416f0681c1" + }, + { + "branch_factors": [ + 2, + 3, + 1, + 2, + 3 + ], + "common_factors": 4, + "dirty_roles": 3, + "leaf_calls": 218, + "mode": "grouped", + "outputs": 5, + "word_sha256": "05cc19d830c96134509d780c4e9f7ae30726c2149da9a975f8b29829d624982c" + } + ], + "rejected_controls": [ + "omit_B_restoration", + "wrong_output_sign", + "change_common_factor_on_return", + "omit_output_dirty_cancellation", + "aliased_source_target", + "commuted_factor_product" + ], + "schema": "dirty-fanout-star-census-v1", + "scope": "Exact finite star-query census and free-algebra emitter endpoints; no new kappa", + "source_manifest_sha256": "a6d8db12fb580f67917af4cf79ecb741faff44d7dbdea5cdf0e6014c2a221155", + "source_star_minimum_cases": 5, + "subject_head": "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "unquotiented_unpruned_crosschecks": [ + 1, + 2 + ] +} diff --git a/research/dirty-fanout-star-census/CLAIM.json b/research/dirty-fanout-star-census/CLAIM.json new file mode 100644 index 0000000000..96ad4c83d7 --- /dev/null +++ b/research/dirty-fanout-star-census/CLAIM.json @@ -0,0 +1,45 @@ +{ + "track": "Independent verification", + "assignment_seed": 79, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "subject_pr": 889, + "subject_head": "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "object": "Sharp 2k+2 signed star-query minimum and complete equality census; literal one-factor batch emitter", + "method": "Exact integer coefficient-state automaton, symmetry quotient retaining labelled-word multiplicities; k=1..5 selected by 1+(79 mod 5). Independent free-algebra emitter replay and meaningful mutations.", + "deliverable": "Standalone standard-library checker, deterministic certificate, proof of equality census, source pins and scoped handoff", + "started_utc": "2026-10-13T13:25:57Z", + "expected_finish_utc": "2026-10-13T14:05:57Z", + "verification_starts_by_utc": "2026-10-13T13:55:57Z", + "coordination": "GitHub pinnedIssues returned empty; no reservation issue opened.", + "candidates": [ + { + "pr": 901, + "task": "Independent restored X4 pair compensation replay", + "decision": "Not selected: already includes independent integer replay; newer forest work overlaps." + }, + { + "pr": 816, + "task": "Independent exact CK signed forest cost-floor check", + "decision": "Not selected: already includes a separate Prim solver and scalar checker." + }, + { + "pr": 889, + "task": "Independent integer-state shortest-word census", + "decision": "Selected: predecessor exhausts only k=2 through length five; new census covers every minimum and excludes all shorter words through k=5. PR896 formalizes binary nonlinear recursion, not this star-query census." + } + ], + "stopping_rule": "Finish fixed k=1..5 census; no supplier search, no expanded circuit alphabet, no kappa claim.", + "result": { + "status": "completed", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/938", + "completed_at_utc": "2026-10-13T13:43:03.141512+00:00", + "refreshed_submission_base": "47481c89fd30a43f8f882eb4b391e89c29273fd0", + "latest_overlap_refresh_pr": 937, + "subject_head_unchanged": true, + "coverage": "All signed star words of lengths 0..2k+2 for k=1..5, with exact orbit counts and safe pruning; unpruned labelled cross-check k=1,2; 60 recursive emitter cases; 5 strict star cases; 6 algebraic controls; 10 package tests.", + "finding": "Minimum 2k+2; complete minimizer counts 4,24,288,5760,172800. Written proof gives 2(k+1)(k!)^2 for k>=1 within the stated alphabet.", + "verification": "Normal and optimized replay/package tests, standalone relocation, selected-record checks and five selected-result tests passed. No full regeneration, cold supplier replay or hosted-CI claim.", + "frontier": "Upstream independently selected PR890 during verification; refreshed conditional kappa 1661957774647029/10^18 unchanged by this package." + } +} diff --git a/research/dirty-fanout-star-census/LICENSE b/research/dirty-fanout-star-census/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/dirty-fanout-star-census/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/dirty-fanout-star-census/NOTICE.md b/research/dirty-fanout-star-census/NOTICE.md new file mode 100644 index 0000000000..c5f338fc90 --- /dev/null +++ b/research/dirty-fanout-star-census/NOTICE.md @@ -0,0 +1,26 @@ +# Attribution and license + +Prepared for Ross Richardson (@RossRichardson), with substantial OpenAI Codex +assistance in the mathematics, code, tests and writing. A delegated Codex agent +independently derived the equality count and reviewed the checker within this +scope. This is AI-assisted independent implementation, not independent human +review. New files use Apache-2.0; the repository license is included. + +CubeJerry's PR889, commit `e2021d1c9e06948528cbc0a8fd7079b671da981d`, supplies +the batched dirty-fanout construction, sharp restricted-query minimum and +literal emitter. Three original files are retained without edits under +`vendor/pr889/`; their original attribution and substantial-AI notice remain. +The original README's relative links describe its source package; only the +three files listed in SOURCES.json are vendored here. + +Chafik Boukhalfa (chafreaky), PR628, supplies the dirty product commutator +lineage and restoration contract. Its implementation is not imported here. +The commutator identity and the predecessor's minimum bound are not claimed +as new. This package adds a complete equality characterization/count and an +independently implemented exact census and emitter check. + +The accepted selected frontier and its authors retain all attribution. No +current invoice or exponent is changed. PR896 formalizes a different nonlinear +binary evaluator obligation; its code is not imported. PR934 studies another +multi-source query alphabet; this package counts all shortest labelled words +in the one-source signed star alphabet. diff --git a/research/dirty-fanout-star-census/PROOF.md b/research/dirty-fanout-star-census/PROOF.md new file mode 100644 index 0000000000..8cc737780c --- /dev/null +++ b/research/dirty-fanout-star-census/PROOF.md @@ -0,0 +1,176 @@ +# Exact signed star-query census + +This note independently checks the sharp star-query argument in +[PR889](https://github.com/CrocSwap/integer-mult-bounds/pull/889), at commit +`e2021d1c9e06948528cbc0a8fd7079b671da981d`, and characterizes every equality +case. The predecessor supplies the construction and its query lower bound; +the contribution here is the complete equality census and an independently +justified coefficient-state checker. The repository base for this contribution +is `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. + +## Statement and scope + +Fix an integer `k >= 1`. The only allowed letters are + +``` +B_s: z <- z + s Bx +A_i,s: y_i <- y_i + s A_i z (1 <= i <= k; s in {-1,+1}). +``` + +Source `x`, connector `z`, and outputs `y_i` occupy distinct storage. Each +letter preserves its source and restores any private scratch before returning. +The maps are exact additive linear maps, remain unchanged, and are available +only through these letters. A valid word must implement, for every allowed +choice of maps and arbitrary initial data, + +``` +z <- z; y_i <- y_i + A_i Bx; x <- x. +``` + +There are no combined-output letters, direct product letters, extra +connectors, or other data operations. We count literal words: output labels, +signs, and ordering distinguish words even when two adjacent operations +commute. + +**Result.** No valid word has length below `2k+2`. The exact number of valid +words of length `2k+2` is + +``` +C_k = 2(k+1)(k!)^2. +``` + +This is a mathematical proof for the stated query alphabet, accompanied by +finite executable checks. It is not a machine-checked formal proof, a lower +bound for general circuits, or a proof of the full multiplication theorem. +The universal-map condition matters: a fixed zero map, torsion in a fixed +characteristic, or other special identities can change the valid-word set. +`k=0` is excluded because its shortest valid word is the empty word. + +## Exact integer state + +At every prefix there are integers `t`, `a_i`, and `b_i` such that + +``` +z = z_0 + t Bx, +y_i = y_i,0 + a_i A_i z_0 + b_i A_i Bx. +``` + +All coefficients start at zero. A letter `B_s` updates only `t <- t+s`. +A letter `A_i,s` uses the current `t` and updates only + +``` +(a_i,b_i) <- (a_i+s, b_i+s*t). +``` + +Induction proves these identities using additivity alone; no commutation or +invertibility of the maps is needed. Consequently a word is universally valid +if and only if its final state has + +``` +t = 0; a_i = 0 and b_i = 1 for every i. +``` + +Sufficiency follows directly from the displayed identities. For necessity, +one may already specialize to integer scalars with identity maps: independently +varying `z_0` and `x` separates the two output coefficients, and varying `x` +tests connector restoration. Thus these integer conditions do not merely test +a sample of free-map instances; they characterize universal validity in this +alphabet. A finite matrix replay is a separate implementation check. + +## Minimum length and equality characterization + +Each output must have at least one `A_i` letter to obtain `b_i=1`. Since its +signed count must finish at `a_i=0`, it needs at least two. At least one `B` +letter is necessary to make any observed `t` nonzero, and `t=0` at the end +requires at least two. This proves the lower bound `2k+2`. + +At equality there are exactly two `B` letters of opposite signs, and exactly +two letters of each output, also of opposite signs. Write the first `B` sign +as `s`. The value of `t` is zero before the first `B`, `s` between the two +`B` letters, and zero after the second. Call the middle interval the plateau. + +For output `i`, both letters outside the plateau give `b_i=0`; both inside +give `b_i=s(+1-1)=0`. Hence exactly one must lie inside. To produce `b_i=1`, +its sign must be `s`; the outside letter then has sign `-s`. Conversely, any +word satisfying these conditions has the required final coefficient state. +This characterizes every equality case, with no further ordering condition +among letters from different outputs. + +For a fixed number `j` of outputs whose outside letter is before the first +`B`, choose their labels in `binom(k,j)` ways. Order those `j` letters in +`j!` ways, all `k` plateau letters in `k!` ways, and the remaining `k-j` +outside letters after the second `B` in `(k-j)!` ways. Either first `B` sign +is possible. Therefore the number for this `j` is + +``` +2 binom(k,j) j! k! (k-j)! = 2(k!)^2. +``` + +The `k+1` possible values of `j` are disjoint and exhaustive. This proves +the stated formula. For `k=1,...,5` it gives `4, 24, 288, 5760, 172800`. + +## Why the symmetry quotient preserves exact word counts + +Permuting output labels permutes the pairs `(a_i,b_i)` and commutes with all +state transitions, up to the same permutation of letter labels. A canonical +state can therefore retain `t` and the sorted multiset of these pairs. + +Suppose a pair `(a,b)` has multiplicity `m`. For either sign `s`, there are +exactly `m` distinct labelled next letters whose chosen output has this pair. +Each produces the same canonical successor: replace one copy by +`(a+s,b+s*t)` and sort. Assign that transition weight `m`. Each of the two +`B` transitions has weight one. Distinct transitions reaching the same +canonical successor must have their weights added; they must not be +deduplicated as unlabelled words. + +Starting with count one at the all-zero state, propagate nonnegative integer +counts by multiplication by transition weights and addition at successors. +Induction on word length shows that each state's count equals the number of +literal labelled words whose coefficient state has that canonical form. +Every labelled state in an orbit has the same outgoing multiplicities, so +aggregating incoming counts introduces neither an orbit-size factor nor a +division by `k!`. The desired terminal orbit consists of `t=0` with `k` +copies of `(0,1)`. + +## Safe remaining-length pruning + +For any intermediate state define + +``` +h = |t| + sum_i f(a_i,b_i), +f(a,b) = |a| if a != 0, + 0 if a == 0 and b == 1, + 2 if a == 0 and b != 1. +``` + +Any successful continuation must use at least `|t|` additional `B` letters +to restore the connector, because only those letters change `t` and each +changes it by one. If `a_i != 0`, at least `|a_i|` additional `A_i` letters +are needed to cancel its signed dirt coefficient. If `a_i=0` but `b_i!=1`, +zero further `A_i` letters cannot correct `b_i`, and one cannot leave +`a_i=0`; at least two are necessary. These are disjoint letter families, +so their lower bounds add. This proves `h` is a lower bound on every +successful continuation's length. Pruning only when `h` exceeds the remaining +length cannot remove a successful word. + +The bound need not be attainable. For example, at the initial state it equals +`2k`, although two additional `B` letters are necessary to create a signal. +Such underestimation affects speed, not completeness. Also `h=0` holds exactly +at the desired terminal coefficient state, so an exhausted horizon does not +accept an unresolved output. + +## Attribution and remaining obligations + +PR889 supplies the batched interface and sharp restricted-query minimum; +its cited predecessor, Chafik Boukhalfa's +[PR628](https://github.com/CrocSwap/integer-mult-bounds/pull/628), supplies +the dirty product commutator lineage. No priority claim is made for the +commutator identity. This proof and its companion verifier were prepared for +the requesting contributor with substantial OpenAI Codex assistance and are +provided under the repository's Apache-2.0 license. + +The abstract query contract is inherited. This result does not supply native +source access, coefficient preparation, physical layout, precision guarantees +for approximate maps, supplier integration, or a new exponent `kappa`. +Finite census results should be reported with their completed `k` and length +domain; they do not independently establish obligations outside this alphabet. diff --git a/research/dirty-fanout-star-census/README.md b/research/dirty-fanout-star-census/README.md new file mode 100644 index 0000000000..ca49889905 --- /dev/null +++ b/research/dirty-fanout-star-census/README.md @@ -0,0 +1,111 @@ +# Independent census of dirty fanout star queries + +**Independent verification and a scoped equality-count result; no new κ.** + +[PR889](https://github.com/CrocSwap/integer-mult-bounds/pull/889) proves a +`2k+2` query minimum for its one-connector, `k`-output dirty fanout model. +This package independently reconstructs its exact integer state, exhausts the +shortest-word domain through five outputs, and characterizes **all** minimizers: + +| Outputs `k` | Minimum queries | Number of minimum-length labelled words | +|---:|---:|---:| +| 1 | 4 | 4 | +| 2 | 6 | 24 | +| 3 | 8 | 288 | +| 4 | 10 | 5,760 | +| 5 | 12 | 172,800 | + +The [written proof](PROOF.md) gives `2(k+1)(k!)²` for every `k>=1` in this +alphabet. Each output has one query between the connector's two updates and +one outside, with signs fixed by the connector excursion. The finite census +checks that count independently; it does not use the classification +to generate words or decide state transitions. This is not a formal proof in +a proof assistant or a lower bound for unrestricted circuits. + +## Reproduce + +Python 3.10+ and the standard library suffice, offline and outside a Git checkout: + +```sh +python3 -I -B research/dirty-fanout-star-census/verify.py +``` + +Expected: + +```text +PASS_STAR_CENSUS k=1..5 minima=4,6,8,10,12 counts=4,24,288,5760,172800 emitter_cases=60 star_cases=5 controls=6 no_new_kappa +``` + +The default command compares every byte of the deterministic recomputed +[certificate](CERTIFICATE.json), including its source-manifest digest, and +does not write files. `--write` explicitly regenerates that certificate. +`python3 -I -O -B research/dirty-fanout-star-census/test_package.py` runs ten +additional failure-sensitivity and relocation tests. See [validation](VALIDATION.md). + +## What is checked independently + +Only signed `z += Bx` and `y_i += A_i z` queries are allowed. The source, +connector and outputs are distinct; each query preserves its source and +restores private scratch. Correctness is universal over exact additive linear +maps and arbitrary dirt. The state records the connector coefficient `t` and, +for each output, its coefficients `(a_i,b_i)` on `A_i z_initial` and `A_i Bx`. +Acceptance requires `t=0` and every pair equal to `(0,1)`. + +For each `k=1..5`, the horizon is exactly `0..2k+2`, with all `2(k+1)` signed +letters admitted at every step. The checker quotients states by output-label +permutations but retains **labelled-word multiplicities** as arbitrary-precision +integers. It prunes only with a proved lower bound on the number of remaining +queries; it does not assume the optimum or equality classification to prune. +An unquotiented, unpruned implementation agrees at every length for `k=1,2`. +This is complete compressed enumeration of the stated finite domain, not a +random sample or a replay of only the predecessor's chosen words. + +The only executed predecessor routine is its literal instruction **emitter**. +A new sparse free-associative-algebra interpreter checks all initial source, +target and scratch columns simultaneously, retaining factor order over the +integers. It checks 60 complete recursive words (fanouts 1..5, common lengths +1..4, asymmetric branch lengths 1..3, and all three predecessor schedules) +and their literal inverses. Five one-factor batches separately pass strict +star-alphabet, one-connector, endpoint and minimum-length admission. +No predecessor interpreter, census, invoice, leaf-count function or receipt is +imported. These checks do not audit PR889's physical invoice or rounded maps. + +Six built-in controls expose missing connector restoration, a wrong output +sign, a changed common factor on return, omitted dirty cancellation, aliased +ports, and an incorrectly commuted factor product. The package tests also +detect lost quotient multiplicities and an endpoint-preserving extension that +uses forbidden ports. A signal-only or commuting scalar fixture would miss +some of these failures. + +## Pins, attribution and scope + +Original base: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +Refreshed submission base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +Subject: PR889 at `e2021d1c9e06948528cbc0a8fd7079b671da981d`. +[SOURCES.json](SOURCES.json) pins all three verbatim source/reference files by +SHA256 and Git blob identity; their original paths and notice are retained. +The subject may be reviewed without merging PR889 first. The source snapshot +is a reference/emitter dependency, not an assertion that the entire PR is +approved. [CLAIM.json](CLAIM.json) records OS seed **79**, task selection, +overlap review and the stopping rule. + +Credit **CubeJerry / PR889** for the batched interface and sharp query minimum, +and **Chafik Boukhalfa / PR628** for its dirty-commutator lineage. The new +contribution is the independently checked complete minimizer census and bounded +literal-emitter correspondence. PR896's nonlinear binary evaluator proof and +PR934's binary multi-source query model have different scope. PR934 extends +PR889's one-source construction; it does not count all shortest labelled words +in this one-source model, which is the additional evidence supplied here. +Prepared for **Ross Richardson (@RossRichardson)** with substantial OpenAI Codex +assistance, including a separate delegated proof derivation and code review. +No independent human review is claimed. See [NOTICE.md](NOTICE.md) and [LICENSE](LICENSE). + +The original base selected conditional κ=`1661634653669567/10^18`. During +verification, upstream selected PR890 at `1661957774647029/10^18`; refreshed +main was incorporated and its selected-record checks passed. This package +changes no selected certificate or upstream source. The abstract query contract, +all-size address/compiler correspondence, native source access and hosting, +precision/tape realization and analytic transfer remain separate obligations. +There is no new supplier, cost saving, unrestricted optimum, or multiplication +theorem claim. The finite emitter checks do not establish all-size compiler +correctness, and the census does not apply to rounded nonlinear leaves. diff --git a/research/dirty-fanout-star-census/SOURCES.json b/research/dirty-fanout-star-census/SOURCES.json new file mode 100644 index 0000000000..2a5f25998c --- /dev/null +++ b/research/dirty-fanout-star-census/SOURCES.json @@ -0,0 +1,25 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pull_request": 889, + "commit": "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "files": [ + { + "path": "vendor/pr889/batch.py", + "source_path": "research/dirty-fanout-batch/batch.py", + "sha256": "faf0d547c18eb0d8af6f69b6a0dab22ff97fd72c5d0fa4235f092cc4fac6ea74", + "git_blob": "499db25870245720900266a7373778d05945ca4a" + }, + { + "path": "vendor/pr889/README.md", + "source_path": "research/dirty-fanout-batch/README.md", + "sha256": "0ef1c0a7dd98c0270822e6f78d222a3888083794502b132543038827c783c706", + "git_blob": "400761138ddd10fb77b836be7c59590545be70e0" + }, + { + "path": "vendor/pr889/NOTICE.md", + "source_path": "research/dirty-fanout-batch/NOTICE.md", + "sha256": "e0ea74eed5957ed62f6c3eb5dadd6f51fd61d6c5ba546d29fb96adf4dda50e4b", + "git_blob": "7c5788e0766d4d01d2710828d6972ad53a54b513" + } + ] +} diff --git a/research/dirty-fanout-star-census/VALIDATION.md b/research/dirty-fanout-star-census/VALIDATION.md new file mode 100644 index 0000000000..fad53fb45b --- /dev/null +++ b/research/dirty-fanout-star-census/VALIDATION.md @@ -0,0 +1,79 @@ +# Validation and handoff + +Validation date: 2026-10-14, Australia/Melbourne (2026-10-13 UTC). +Environment: macOS arm64, CPython 3.14.6; standard library only. +Original base: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +Refreshed submission base: `47481c89fd30a43f8f882eb4b391e89c29273fd0`. +Subject PR889: `e2021d1c9e06948528cbc0a8fd7079b671da981d`. + +## Completed checks + +```sh +python3 -I -B research/dirty-fanout-star-census/verify.py +python3 -I -O -B research/dirty-fanout-star-census/verify.py +python3 -I -B research/dirty-fanout-star-census/test_package.py +python3 -I -O -B research/dirty-fanout-star-census/test_package.py +make selected-record-check +python3 -m unittest discover -s tests -p 'test_selected_result.py' +git diff --check +``` + +Normal and optimized verifier output and the deterministic certificate agree: +five complete shortest-word censuses, 60 free-algebra emitter cases with +literal inverse checks, five strict star-admission cases, six built-in controls. +Both package-test modes pass all ten tests. The selected-record check and all +five existing selected-result tests pass, both on the original base and after +incorporating refreshed main. The package is the only changed path relative +to refreshed main; `upstream/` and the selected record match that base. + +The ten package tests cover loss of labelled-word multiplicities, a positive +output relabelling, dirty-connector leakage, a wrong integer sign invisible +modulo two, a valid endpoint outside the claimed query alphabet, standalone +relocation to a path with spaces, source drift, omitted source inventory, +wrong source commit, and certificate drift. The relocated default verifier +does not alter any package bytes. Rejected-source tests fail before executing +the emitter. The six algebraic controls are described in README.md. + +The independent review checked the proof/state correspondence, weighted +quotient, pruning completeness and all-dirt noncommutative endpoints. It led +to explicit source-inventory completeness and one-connector/port admission +checks. The reviewer reran the final verifier and ten package tests. This +was a delegated AI review; no human-review or hosted-CI pass is claimed. + +## Reproduction boundaries + +The census covers all signed words of lengths `0..2k+2` for each `k=1..5` +using proved state compression and pruning, not literal enumeration of each +raw word. Certificate rows give the raw domain cardinalities and retained +state counts. The unpruned, unquotiented cross-check covers `k=1,2`. +The chosen finite domain follows seed `79`: `k_max=1+(79 mod 5)=5`. +The experiment stopped after completing this domain and its fixed controls. + +No original construction code, selected certificate or shared verifier was +changed. Full repository artifact regeneration (`make verify`) and the +expensive selected-supplier cold replay were not run: neither validates an +additional obligation changed by this standalone research package. The +focused package checks and existing selected-record integrity checks above +are the relevant validation performed; no full-suite success is implied. + +No full PR889 invoice, physical layout, rounding analysis, all-size compiler, +supplier integration or complete multiplication theorem was revalidated. +The original-base accepted conditional κ was `1661634653669567/10^18`. +Upstream advanced during verification and selected PR890 at +`1661957774647029/10^18`; this contribution does not change either result. + +## Concurrency review + +No pinned coordination issue existed at claim or prepublication checks. The +local claim records three candidate tasks and their selection. An initial +inventory inspected all 724 open PRs, including pending independent checks +and negative results. The review ledger and selected PR799 construction/review +were read before choosing this non-frontier subject. + +PR889 was refreshed at the same pinned head. PR896 formalizes nonlinear binary +recursion, whereas this package counts exact linear one-source star words. +Concurrent PR934 extends PR889 to a binary multi-source alphabet and supplies +optimal witnesses; this package adds the complete minimizer count for the +one-source alphabet. PR901/PR816 already carry independent scalar/MST evidence +and were not duplicated. No borrowed pending result is promoted to the +selected frontier, and no savings from distinct submissions are combined. diff --git a/research/dirty-fanout-star-census/test_package.py b/research/dirty-fanout-star-census/test_package.py new file mode 100644 index 0000000000..b706f919a8 --- /dev/null +++ b/research/dirty-fanout-star-census/test_package.py @@ -0,0 +1,121 @@ +"""Failure sensitivity and independent package relocation checks; stdlib only.""" +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +ROOT = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("census_verifier", ROOT / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class CensusTests(unittest.TestCase): + def test_lost_label_multiplicity_is_detected(self): + original = v.transitions + + def unweighted(state): + return ((target, 1) for target, _ in original(state)) + + with patch.object(v, "transitions", unweighted): + with self.assertRaisesRegex(ValueError, "minimum-word census"): + v.census(2) + + def test_permuted_output_labels_preserve_free_endpoint(self): + compiler = v.source_emitter() + common, branches = [0, 1], [[2], [3, 4], [5, 6, 7]] + word, dirt = compiler(common, branches) + # Reorder whole output/branch contracts, not the factors inside them. + remap = {1: 3, 2: 1, 3: 2} + renamed = [(f, remap.get(x, x), remap.get(y, y), s) + for f, x, y, s in word] + v.check_word(renamed, 4 + dirt, common, [branches[1], branches[2], branches[0]]) + + def test_dirty_connector_cannot_be_treated_as_clean(self): + # This word implements the desired signal only if the initial connector + # is zero: it omits the output cancellation at the restored dirty value. + word = [(0, 0, 2, 1), (1, 2, 1, 1), (0, 0, 2, -1)] + with self.assertRaisesRegex(ValueError, "endpoint mismatch"): + v.check_word(word, 3, [0], [[1]]) + + def test_negative_coefficient_cannot_be_erased_as_mod_two(self): + word = [(0, 0, 2, 1), (1, 2, 1, -1), + (0, 0, 2, -1), (1, 2, 1, 1)] + with self.assertRaisesRegex(ValueError, "endpoint mismatch"): + v.check_word(word, 3, [0], [[1]]) + + def test_endpoint_preserving_extra_ports_are_outside_star_model(self): + compiler = v.source_emitter() + word, _ = compiler([0], [[1], [2]]) + # An inverse pair is algebraically neutral but uses a forbidden source. + extended = word + [(1, 0, 1, 1), (1, 0, 1, -1)] + v.check_word(extended, 4, [0], [[1], [2]]) + with self.assertRaisesRegex(ValueError, "outside star-query alphabet"): + v.check_star_word(extended, 2, 3) + + +class PackageTests(unittest.TestCase): + def setUp(self): + self.temp = tempfile.TemporaryDirectory(prefix="star census ") + self.package = Path(self.temp.name) / "standalone package" + shutil.copytree(ROOT, self.package, ignore=shutil.ignore_patterns("__pycache__")) + + def tearDown(self): + self.temp.cleanup() + + def run_package(self): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py")], + cwd=self.temp.name, capture_output=True, text=True, timeout=60) + + def test_standalone_relocation_and_read_only_default(self): + before = {p.relative_to(self.package): p.read_bytes() + for p in self.package.rglob("*") if p.is_file()} + run = self.run_package() + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn("PASS_STAR_CENSUS", run.stdout) + after = {p.relative_to(self.package): p.read_bytes() + for p in self.package.rglob("*") if p.is_file()} + self.assertEqual(before, after) + + def test_changed_source_rejected(self): + source = self.package / "vendor/pr889/batch.py" + source.write_text(source.read_text() + "\n# source drift\n") + run = self.run_package() + self.assertNotEqual(run.returncode, 0) + self.assertIn("source SHA256", run.stderr) + + def test_missing_source_pin_rejected(self): + path = self.package / "SOURCES.json" + manifest = json.loads(path.read_text()) + manifest["files"].pop() + path.write_text(json.dumps(manifest)) + run = self.run_package() + self.assertNotEqual(run.returncode, 0) + self.assertIn("source inventory", run.stderr) + + def test_wrong_subject_commit_rejected(self): + path = self.package / "SOURCES.json" + manifest = json.loads(path.read_text()) + manifest["commit"] = "0" * 40 + path.write_text(json.dumps(manifest)) + run = self.run_package() + self.assertNotEqual(run.returncode, 0) + self.assertIn("subject commit", run.stderr) + + def test_changed_receipt_rejected(self): + path = self.package / "CERTIFICATE.json" + receipt = json.loads(path.read_text()) + receipt["census"][4]["minimum_word_count"] += 1 + path.write_text(json.dumps(receipt)) + run = self.run_package() + self.assertNotEqual(run.returncode, 0) + self.assertIn("certificate mismatch", run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/dirty-fanout-star-census/vendor/pr889/NOTICE.md b/research/dirty-fanout-star-census/vendor/pr889/NOTICE.md new file mode 100644 index 0000000000..7c5788e076 --- /dev/null +++ b/research/dirty-fanout-star-census/vendor/pr889/NOTICE.md @@ -0,0 +1,31 @@ +# Attribution and scope + +Prepared for the requesting contributor with substantial OpenAI Codex assistance +in the mathematical argument, implementation, tests and prose. The user's human +identity is not asserted. This package uses the repository's Apache-2.0 license. + +Chafik Boukhalfa / chafreaky's PR628 supplies the dirty product commutator, +literal-inverse convention, exact restoration contract and rounded-error +analysis. Its reference source, proof and notice are retained byte for byte. +Ali Romman's PR621 and OpenAI's exact-DFT/Newton framework are inherited context; +we do not use their analytic kernel claims to certify the abstract matrices here. +The commutator and batching algebra are classical; no literature-priority claim +is made. + +Relevant concurrent work inspected: androolloyd's PR673 (multiway dirty echo), +commdata2338's PR677 (native DATA-query contract), Dillon Amburgey's PR689 +(ternary placement), FanPUYen's PR714 (clean root checkpoint), Sagar Thakrar's +PR730 (fixed scratch optimization), nightangelflowerwin-ops's PR788 (reusable +clean checkpoint), PR822 (dirty sibling connector reuse), and Wentao Li's PR840 +(dyadic ADDRESS-query pair). These concern different contracts or one-output +schedules. Their code is not consumed; no relative optimality against their +broader classes is claimed. Varun Mittal's PR793 batches scalar coefficient +preparation in historical JP8 compensation and preserves its recursive profile; +this package instead batches full product-query calls under a different abstract +multi-output contract. No PR793 code or claimed savings are consumed. PR663's nonlinear-restoration distinction is +acknowledged and explicitly respected by the rounded controls. + +The accepted frontier's authors and source lineage retain all attribution. +This local multi-output result supplies neither a new κ nor an instantiated +current supplier, physical tape compiler, full theorem formalization, human +peer review or measured performance result. diff --git a/research/dirty-fanout-star-census/vendor/pr889/README.md b/research/dirty-fanout-star-census/vendor/pr889/README.md new file mode 100644 index 0000000000..400761138d --- /dev/null +++ b/research/dirty-fanout-star-census/vendor/pr889/README.md @@ -0,0 +1,227 @@ +# Batch product shears with a common right factor + +**Recursive-interface construction; no new κ.** This package supplies an exact +multi-output version of the dirty product commutator from Chafik Boukhalfa's +[PR628](https://github.com/CrocSwap/integer-mult-bounds/pull/628), with a literal +instruction generator, complete local cost recurrence, a restricted-query +optimality argument, and independent exact checks. + +For the seed-58 fixture, five outputs share eight rightmost factors. Batching +uses **246 primitive factor-shear calls**, versus **680** for five separate +balanced binary products, with **four borrowed dirty arrays in either case**. +The comparison is between these explicit binary schedules. Multiway echoes and +arbitrary circuits are outside the comparison. The 434-call reduction (about +63.82%) is not a measured runtime or an integer-multiplication exponent gain. + +From the repository root, Python 3.9+ and the standard library suffice: + +```sh +python3 -I -O -B research/dirty-fanout-batch/verify.py +``` + +Expected: `PASS_DIRTY_FANOUT_BATCH`, 128 free-word cases, 795 dense cases, +`680 -> 246 leaves`, four dirty arrays. The default command checks the complete +committed [certificate](CERTIFICATE.json); `--write` regenerates it instead. +`python3 -I -O -B research/dirty-fanout-batch/test_package.py` checks relocation +and rejects deliberately broken packages. + +## Contract and exact identity + +Let x, y_1,...,y_k and every borrowed array be independent arbitrary elements +of R^L, with distinct storage and unchanged read-only coefficients. R may be a +noncommutative ring; A_i and B are additive linear operators, in the indicated +order. The goal is simultaneously + +``` +x -> x, y_i -> y_i + A_i B x, all borrowed arrays restored. +``` + +A child `target += F(source)` preserves its source and all its own scratch. +It is independent of the target's previous value. Its negative call is the +literal reverse instruction word with signs reversed. Every source/target and +coefficient array is excluded from borrowed storage. All outputs are reserved +throughout the batch. No concurrent observer may use the temporary output +values. Common B and its input x must stay identical across the two calls. + +With one arbitrary dirty connector z, execute: + +1. `z += B x`. +2. For every i, `y_i += A_i z`. +3. `z -= B x`. +4. For every i in reverse order, `y_i -= A_i z`. + +The two observed values of z are z_0+B x and z_0. Thus the increment is +A_i(z_0+B x)-A_i z_0=A_i B x. All dirt cancels, and z returns to z_0. No +commutation of A_i with B, or of individual factors, is used. Neither A_i +nor B needs to be invertible; their additive shears are invertible. Distinct output +ports make the A_i calls commute with one another after their private scratch +has been restored. The emitted negative block nevertheless uses the literal +inverse, so no extra commutation assumption is needed for its implementation. + +This is the familiar commutator identity applied to a direct-sum output map; +we make no algebraic or literature-priority claim. The contribution is the +explicit batched interface, executable factor lowering, pricing, and controls. +It changes the demanded output family; it is not a new single-output echo tree. + +### A sharp bound in the specified star-query model + +Allow only signed queries `z += ±B x` and `y_i += ±A_i z`, with one connector, +read-only x, private query scratch restored before return, and no other data +operations. Treat the maps as free formal operators. At an A_i query, write +z=z_0+t Bx. Final dirt independence forces the signed coefficient sum on A_i z_0 +to vanish, while correctness requires the signed sum of the corresponding t's +to be one. Therefore there must be at least two A_i queries for every output. +At least one B query is needed for a nonzero signal; restoration of z requires +at least one opposite B query. Hence every admissible word uses at least +`2k+2` queries. The construction attains it, including under arbitrary positive +per-operator query prices. This does not bound models admitting combined-output +queries, extra connectors, direct A_i B queries, or other linear operations. + +The finite regression exhausts all 9,331 signed star words of lengths zero +through five for k=2. Their failure supports the implementation of the universal +argument above; enumeration is not the proof of that argument. + +## Recursive lowering and exact cost + +Factor lists are in **application order**: `[B0,B1,A0]` means A0 B1 B0. +Each product is lowered with PR628's balanced binary dirty commutator, using +one distinct array per active recursion level. All child calls operate on +**full length-L rows**. Batching never divides their charged volume by k. +Let C(F;L,w) be the complete cost of an additive product child, with both signs +bounded by the same price and with its heads returned to the documented entry +positions. For a leaf j let c_j include arithmetic, source and coefficient +access, target update, phase/descriptor work, routing and head returns. Then + +``` +C([j]) = c_j + dispatch_leaf +C(F_right followed by F_left) + = 2 C(F_right) + 2 C(F_left) + dispatch_node +C_batch = 2 C(B) + 2 sum_i C(A_i) + dispatch_batch. +``` + +No child or inverse is free. The unbatched *same-root-split* comparator costs +`2k C(B) + 2 sum C(A_i) + dispatch_separate`, so the recursive saving is +`2(k-1) C(B)` before comparing dispatch and layout overhead. If source access, +layout or external frames differ, use their actual c_j; the operation count +alone does not imply a bit-cost improvement. + +For an unweighted balanced product of n factors, L(1)=1 and +L(n)=2L(floor(n/2))+2L(ceil(n/2)). Writing p=2^floor(log2 n), induction gives +L(n)=p(3n-2p). Scratch is ceil(log2 n). The batch's dirty requirement is +`1 + max(ceil(log2 |B|), max_i ceil(log2 |A_i|))`, in addition to its source +and k output arrays. Child scratch is reused only after return; all sibling +outputs remain excluded. There is no clean length-L array. + +For seed 58, k=2+(58 mod 5)=5, |B|=1+(58 mod 17)=8, and |A_i|=i: + +| Schedule | Complete leaf calls | Dirty arrays | +|---|---:|---:| +| Separate products, each split into the common B and its A_i | 758 | 4 | +| Separate balanced products of lengths 9,10,11,12,13 | 680 | 4 | +| Shared B batch | 246 | 4 | + +A separate integer DP checks the minimum over all ordered **binary** splits +for n=1,...,64 and agrees with the balanced counts. No all-arity optimum is +asserted; PR673, PR730 and PR822 investigate different tree/allocation classes. +The certificate lists exact per-factor multiplicities and three positive +nonuniform price assignments for every sampled batch, rather than crediting +only the convenient common-factor calls. + +### Fully charged dense reference realization + +There is also a simple, deliberately slow implementation of each matrix leaf. +For every target entry, form the dot product in one scalar accumulator, then +add/subtract it to the target. All matrix coefficients are read-only. The +source and target rows are distinct. The certificate records, for each schedule +on identical 3-by-3 inputs and the same role layout: + +- N L² coefficient reads and N L² source reads; +- N L target read/write updates; +- N L² multiplications, N L(L+1) additions (including zero-initialized sums), + and one sign negation per negative target update; +- literal one-tape head travel, measured in word slots, including returning + to slot zero after **every** primitive call; +- coefficient storage, data storage and every emitted instruction record; +- array-length/role-alias checks and the explicit preflight matrix-row and + coefficient-alias checks (N L and N R L respectively, for R live roles). + +The tape layout puts all mutable rows first and the coefficient matrices +second. Within a dot product it visits coefficient then source for each term, +then the destination, and returns home at leaf end. The head-travel sum is +`sum |next_position-current_position|` for that literal trace. Coefficients and +source entries must be loaded into a constant number of scalar arithmetic +ports. This reference makes no locality or free-gather assumption. + +For word size w, multiply this travel by w, add O(w) per load/store, the listed +counts times integer multiplication/addition costs M(w), A(w), and charge +O(N(log(number of roles)+log(number of factors))) instruction/control bits +and O(N) generator records. Also charge the listed descriptor/alias preflight +comparisons at the required index/pointer bit width; they are not arithmetic +leaf calls. This invoice describes the reference algorithm, not CPython +interpreter wall time. Input coefficient preparation is additional and +paid once for each distinct factor, equally available to both comparators. +The seed matrices are already supplied exact integers; a cyclic-inverse or +phase oracle would need its own preparation and validation bill. + +For integer matrices of row norm at most K=L H, input magnitude at most D, +and N leaf calls, exact states are bounded by D(1+K)^N. Thus signed word length +`2 + ceil(log2(max(1,D))) + N ceil(log2(1+K))` suffices. The same conservative +word length from the larger comparator can be used for all schedules. This +is a finite dense-matrix realization, not an efficient common-label/tape +compiler for the selected supplier. + +## Rounded leaves: restoration and accuracy are different + +A deterministic grid leaf `target += F(source)` can be inverted exactly by +subtracting the same computed increment. Literal inverse words then restore +all source/borrowed arrays even when F is nonlinear from rounding, provided +read-only data and all excluded arrays are respected. B's paired calls see +the same source and deeper dirt: intervening A_i calls restore their source +z and private scratch. The final A_i calls use the restored connector. + +The target increment need not be the exact, dirt-independent A_i Bx in this +case. For example floor((z+1)/2)-floor(z/2) depends on dirty z. We include this +negative control and make no substitution of approximate linearity for exact +linearity in the identity or query minimum above. + +For a separate accuracy bound, suppose the ideal primitive operators have +infinity norm at most K and each rounded primitive's increment error is at +most u, uniformly on the actual trajectory. A full ideal shear has norm at +most 1+K. Telescoping the N perturbed shears gives + +``` +error <= u sum_(j=0)^(N-1) (1+K)^j <= N u (1+K)^(N-1). +``` + +For u=2^-w, `w >= p + ceil(log2 N) + (N-1)ceil(log2(1+K))` suffices for error +at most 2^-p. Actual state magnitudes are bounded by (D+1)(2+K)^N for u<=1, +which must also be included in integer-word storage. Coefficient perturbation +and preparation errors must be added separately; source-dependent error +bounds require checking the resulting magnitude bound, not silently using +this uniform-u premise. Twenty-seven exact grid experiments compare a floor +rounding interpreter with independent dense ideal products and check the full +error bound and exact all-role reversal. + +## Verification scope, provenance and stopping rule + +[CLAIM.md](CLAIM.md) records the OS seed, three candidates, overlap review and +local claim. Exact base: `f567884aeb8851b6e794af1184119a3bfbe1e631`. +[Source pins](SOURCES.json) retain the original proof, implementation reference +and notice from PR628 at `0768f97d06c623b8211e651543c66135796b62bf`, with Git +blob and SHA256 hashes. Those source files are references; their cyclic-scan +implementation is not imported or asserted to have been revalidated here. + +The test domain is fixed: common lengths 1..16, fanout 1..8 with left lengths +1..k; dense domains/fixtures listed in verify.py; and the seed-selected example. +Random dense inputs use Python Random(58); the track draw used OS randomness. +This is a bounded constructive check, not a search for a new multiplication +bound or an impossibility claim outside the stated star-query model. + +The selected #799/#589 result at this base is κ=1661634653669567/10^18. Its +native calls are not assumed to have the shared source, coefficient, frame, +volume and exclusivity contract used here. No current invoice term is removed. +Existing owner obligations, ordinary child widths, read-only source access, +common-label realization, precision, layout and all-size analytic transfer +remain unresolved for any supplier application. This package changes no +selected certificate or upstream manuscript. See [NOTICE.md](NOTICE.md) for +attribution and substantial AI assistance. diff --git a/research/dirty-fanout-star-census/vendor/pr889/batch.py b/research/dirty-fanout-star-census/vendor/pr889/batch.py new file mode 100644 index 0000000000..499db25870 --- /dev/null +++ b/research/dirty-fanout-star-census/vendor/pr889/batch.py @@ -0,0 +1,105 @@ +"""Exact common-right-factor batching. Apache-2.0; see NOTICE.md.""" +from collections import Counter + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def inverse(word): + return [(f, x, y, -s) for f, x, y, s in reversed(word)] + + +def product(factors, source, target, scratch): + """Factors are in application order, so [B, A] means A B.""" + need(bool(factors), 'empty factor list') + need(len(scratch) >= (len(factors)-1).bit_length(), 'insufficient scratch') + need(len(set([source, target] + list(scratch))) == 2+len(scratch), 'aliased roles') + if len(factors) == 1: + return [(factors[0], source, target, 1)] + mid = len(factors)//2 + z, *rest = scratch + right = product(factors[:mid], source, z, rest) + left = product(factors[mid:], z, target, rest) + return right + left + inverse(right) + inverse(left) + + +def compile_batch(common, branches, mode='batch'): + """Return (literal leaf word, dirty role count), reserving all output roles.""" + need(bool(common) and bool(branches) and all(branches), 'nonempty factors and outputs required') + need(mode in ('batch', 'separate', 'grouped'), 'unknown comparator') + k = len(branches) + depth = max((len(common)-1).bit_length(), *((len(a)-1).bit_length() for a in branches)) + dirt = max(1+depth, max((len(common)+len(a)-1).bit_length() for a in branches)) + scratch = list(range(k+1, k+1+dirt)) + if mode == 'separate': + return [op for i, a in enumerate(branches, 1) + for op in product(common+a, 0, i, scratch)], dirt + right = product(common, 0, scratch[0], scratch[1:]) + lefts = [product(a, scratch[0], i, scratch[1:]) for i, a in enumerate(branches, 1)] + if mode == 'grouped': + return [op for left in lefts for op in right+left+inverse(right)+inverse(left)], dirt + # Distinct targets and read-only shared source make these left words commute. + left = [op for word in lefts for op in word] + return right + left + inverse(right) + inverse(left), dirt + + +def run(word, matrices, arrays, modulus=None): + """Literal exact leaf interpreter; validate every alias before any mutation.""" + need(len({id(v) for v in arrays}) == len(arrays), 'aliased arrays') + n = len(arrays[0]) + need(n > 0 and all(len(v) == n for v in arrays), 'array lengths') + need(modulus is None or type(modulus) is int and modulus > 1, 'modulus') + for f, x, y, sign in word: + need(type(f) is int and f in matrices, 'unknown factor') + need(type(x) is int and type(y) is int and 0 <= x < len(arrays) and 0 <= y < len(arrays) and x != y, 'leaf ports') + need(type(sign) is int and sign in (-1, 1), 'leaf sign') + a = matrices[f] + need(len(a) == n and all(len(row) == n for row in a), 'matrix dimensions') + need(all(a is not v and row is not v for v in arrays for row in a), 'mutable coefficient alias') + for f, x, y, sign in word: + for i, row in enumerate(matrices[f]): + increment = sum(a*b for a, b in zip(row, arrays[x])) + arrays[y][i] += sign*increment + if modulus is not None: + arrays[y][i] %= modulus + + +def leaf_count(n): + need(type(n) is int and n > 0, 'positive factor count') + p = 1 << (n.bit_length()-1) + return p*(3*n-2*p) + + +def invoice(word, dimension, roles, factors): + """Dense reference leaf invoice, including literal head travel in word slots. + + Data rows precede the read-only coefficient matrices on one tape. Each leaf + starts and ends at word slot 0; the scalar accumulator is an arithmetic port. + This deliberately slow layout makes source access and head returns explicit. + """ + n = dimension + counts = Counter(f for f, _, _, _ in word) + moves = 0 + for f, x, y, _ in word: + head = 0 + for i in range(n): + for j in range(n): + for pos in (roles*n + f*n*n + i*n+j, x*n+j): + moves += abs(pos-head) + head = pos + pos = y*n+i + moves += abs(pos-head) + head = pos + moves += head + return dict(leaf_calls=len(word), calls_by_factor={str(f): counts[f] for f in range(factors)}, + coefficient_reads=len(word)*n*n, source_reads=len(word)*n*n, + target_read_writes=len(word)*n, multiplications=len(word)*n*n, + additions=len(word)*n*(n+1), negations=sum(s < 0 for _,_,_,s in word)*n, + head_travel_word_slots=moves, + preflight_array_length_checks=roles, preflight_role_alias_entries=roles, + preflight_matrix_row_length_checks=len(word)*n, + preflight_coefficient_alias_pairs=len(word)*roles*n, + coefficient_storage_words=factors*n*n, data_storage_words=roles*n, + instruction_records=len(word)) diff --git a/research/dirty-fanout-star-census/verify.py b/research/dirty-fanout-star-census/verify.py new file mode 100644 index 0000000000..47a3954f6b --- /dev/null +++ b/research/dirty-fanout-star-census/verify.py @@ -0,0 +1,257 @@ +"""Independent exact census of PR889's signed star queries (Apache-2.0). + +The only imported subject routine is its instruction emitter. No predecessor +state interpreter, word census, price function, or expected receipt is used. +""" +from __future__ import annotations + +import argparse +from collections import Counter +import hashlib +import importlib.util +import json +from math import factorial +from pathlib import Path + +ROOT = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def remaining_lower_bound(t, pairs): + # Each nonzero dirt coefficient needs at least |a| unit queries. If a=0 + # but b!=1, at least two opposite queries are needed to change the signal + # and return the dirt coefficient to zero. B restoration is separate. + return abs(t) + sum(abs(a) if a else (0 if b == 1 else 2) + for a, b in pairs) + + +def transitions(state): + t, pairs = state + yield (t + 1, pairs), 1 + yield (t - 1, pairs), 1 + for (a, b), multiplicity in Counter(pairs).items(): + rest = list(pairs) + rest.remove((a, b)) + for sign in (-1, 1): + changed = tuple(sorted(rest + [(a + sign, b + sign * t)])) + yield (t, changed), multiplicity + + +def census(k): + """Count labelled signed words through 2k+2 via exact orbit multiplicities.""" + limit = 2 * k + 2 + goal = (0, ((0, 1),) * k) + layer = {(0, ((0, 0),) * k): 1} + counts = [0] + sizes = [1] + for depth in range(1, limit + 1): + following = Counter() + for state, ways in layer.items(): + for target, multiplicity in transitions(state): + if remaining_lower_bound(*target) <= limit - depth: + following[target] += ways * multiplicity + layer = following + counts.append(layer.get(goal, 0)) + sizes.append(len(layer)) + require(not any(counts[:-1]), f"shorter valid word at k={k}") + expected = 2 * (k + 1) * factorial(k) ** 2 + require(counts[-1] == expected, f"minimum-word census at k={k}") + return dict(outputs=k, maximum_length=limit, alphabet_size=2*(k+1), + raw_words_through_horizon=sum((2*(k+1))**n for n in range(limit+1)), + accepted_by_length=counts, + retained_states_by_length=sizes, minimum_word_count=expected) + + +def labelled_census(k): + """Unquotiented and unpruned cross-check; only used for k=1,2.""" + limit = 2 * k + 2 + layer = {(0, (0,) * k, (0,) * k): 1} + counts = [0] + for _ in range(limit): + following = Counter() + for (t, a, b), ways in layer.items(): + following[t + 1, a, b] += ways + following[t - 1, a, b] += ways + for i in range(k): + for sign in (-1, 1): + aa, bb = list(a), list(b) + aa[i] += sign + bb[i] += sign * t + following[t, tuple(aa), tuple(bb)] += ways + layer = following + counts.append(layer.get((0, (0,) * k, (1,) * k), 0)) + return counts + + +def source_emitter(): + manifest = json.loads((ROOT / "SOURCES.json").read_text()) + require(manifest["commit"] == "e2021d1c9e06948528cbc0a8fd7079b671da981d", + "unexpected subject commit") + require(sorted(record["path"] for record in manifest["files"]) == + ["vendor/pr889/NOTICE.md", "vendor/pr889/README.md", "vendor/pr889/batch.py"], + "incomplete or duplicate source inventory") + for record in manifest["files"]: + data = (ROOT / record["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == record["sha256"], + "source SHA256: " + record["path"]) + blob = b"blob " + str(len(data)).encode() + b"\0" + data + require(hashlib.sha1(blob).hexdigest() == record["git_blob"], + "source Git blob: " + record["path"]) + spec = importlib.util.spec_from_file_location("subject_batch", ROOT / "vendor/pr889/batch.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.compile_batch + + +def polynomial_replay(word, roles): + """Free associative algebra over Z, retaining every initial dirty input. + + A monomial (r, fs) means the initial contents of role r with factors fs + applied from left to right. Distinct fs never commute or cancel by chance. + """ + values = [{(r, ()): 1} for r in range(roles)] + for f, source, target, sign in word: + require(type(f) is int and f >= 0, "bad factor") + require(type(source) is int and type(target) is int and + 0 <= source < roles and 0 <= target < roles and source != target, + "aliased or invalid ports") + require(type(sign) is int and sign in (-1, 1), "bad sign") + for (r, factors), coefficient in list(values[source].items()): + key = r, factors + (f,) + value = values[target].get(key, 0) + sign * coefficient + if value: + values[target][key] = value + else: + values[target].pop(key, None) + return values + + +def check_word(word, roles, common, branches): + actual = polynomial_replay(word, roles) + expected = [{(r, ()): 1} for r in range(roles)] + for i, branch in enumerate(branches, 1): + expected[i][0, tuple(common + branch)] = 1 + require(actual == expected, "free-polynomial endpoint mismatch") + + +def check_star_word(word, k, connector): + """Admit only the claimed one-connector star alphabet, then check its state.""" + t, a, b = 0, [0] * k, [0] * k + for f, x, y, sign in word: + require(sign in (-1, 1), "nonunit star sign") + if (f, x, y) == (0, 0, connector): + t += sign + else: + require(1 <= f <= k and (x, y) == (connector, f), + "outside star-query alphabet") + a[f-1] += sign + b[f-1] += sign*t + require(t == 0 and a == [0]*k and b == [1]*k, "star endpoint mismatch") + + +def emitter_checks(compile_batch): + records = [] + for k in range(1, 6): + for common_length in range(1, 5): + common = list(range(common_length)) + branches = [] + next_factor = common_length + for i in range(k): + # Seed 79 diversifies asymmetric branch lengths (1..3). + length = 1 + (79 + i) % 3 + branches.append(list(range(next_factor, next_factor + length))) + next_factor += length + for mode in ("batch", "separate", "grouped"): + word, dirt = compile_batch(common, branches, mode) + roles = k + 1 + dirt + check_word(word, roles, common, branches) + reverse = [(f, x, y, -s) for f, x, y, s in reversed(word)] + identity = [{(r, ()): 1} for r in range(roles)] + require(polynomial_replay(word + reverse, roles) == identity, + "literal inverse mismatch") + encoded = json.dumps(word, separators=(",", ":")).encode() + records.append(dict(outputs=k, common_factors=common_length, + branch_factors=list(map(len, branches)), mode=mode, + leaf_calls=len(word), dirty_roles=dirt, + word_sha256=hashlib.sha256(encoded).hexdigest())) + common, branches = [0], [[i] for i in range(1, k + 1)] + word, dirt = compile_batch(common, branches) + require(dirt == 1, "emitter uses extra connector storage") + require(len(word) == 2 * k + 2, "emitter misses query minimum") + check_star_word(word, k, k + 1) + check_word(word, k + 1 + dirt, common, branches) + return records + + +def mutation_controls(compile_batch): + common, branches = [0], [[1], [2]] + word, dirt = compile_batch(common, branches) + roles = 3 + dirt + mutants = {} + mutants["omit_B_restoration"] = word[:3] + word[4:] + wrong = list(word) + f, x, y, s = wrong[1] + wrong[1] = (f, x, y, -s) + mutants["wrong_output_sign"] = wrong + wrong = list(word) + f, x, y, s = wrong[3] + wrong[3] = (79, x, y, s) + mutants["change_common_factor_on_return"] = wrong + mutants["omit_output_dirty_cancellation"] = word[:-1] + wrong = list(word) + f, x, y, s = wrong[1] + wrong[1] = (f, x, x, s) + mutants["aliased_source_target"] = wrong + results = [] + for name, mutant in mutants.items(): + try: + check_word(mutant, roles, common, branches) + except ValueError: + results.append(name) + else: + raise ValueError("accepted mutation: " + name) + # Reversed application order would agree for commuting scalar fixtures. + actual = polynomial_replay(word, roles) + require(actual[1].get((0, (1, 0)), 0) != 1, + "factor-order control was invisible") + results.append("commuted_factor_product") + return results + + +def certificate(): + compiler = source_emitter() + rows = [census(k) for k in range(1, 6)] + for k in (1, 2): + require(labelled_census(k) == rows[k - 1]["accepted_by_length"], + "labelled/unpruned census mismatch") + return dict(schema="dirty-fanout-star-census-v1", assignment_seed=79, + subject_head="e2021d1c9e06948528cbc0a8fd7079b671da981d", + source_manifest_sha256=hashlib.sha256((ROOT / "SOURCES.json").read_bytes()).hexdigest(), + census=rows, unquotiented_unpruned_crosschecks=[1, 2], + source_star_minimum_cases=5, + emitter_cases=emitter_checks(compiler), + rejected_controls=mutation_controls(compiler), + scope="Exact finite star-query census and free-algebra emitter endpoints; no new kappa") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate CERTIFICATE.json") + args = parser.parse_args() + result = certificate() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + path = ROOT / "CERTIFICATE.json" + if args.write: + path.write_text(encoded) + else: + require(path.read_text() == encoded, "certificate mismatch") + print("PASS_STAR_CENSUS k=1..5 minima=4,6,8,10,12 counts=4,24,288,5760,172800 " + "emitter_cases=60 star_cases=5 controls=6 no_new_kappa") + + +if __name__ == "__main__": + main()