diff --git a/research/ut4-noncentral-shared-middle/CERTIFICATE.json b/research/ut4-noncentral-shared-middle/CERTIFICATE.json new file mode 100644 index 0000000000..c689734e5d --- /dev/null +++ b/research/ut4-noncentral-shared-middle/CERTIFICATE.json @@ -0,0 +1,1019 @@ +{ + "bounded_coefficient_checks": { + "coefficient_digest": "b94b89bf4f84879a0dd3c7b55a553b7eeaf553855dcba33d702db719832783f8", + "expanded_factors": 27, + "length_counts": [ + 1, + 27, + 729, + 19683 + ], + "registers": 2, + "scope": "all words through length three; not an optimality census" + }, + "group_structure": { + "contragredient_products": 4096, + "group_products": 4096, + "noncentral_root_controls": 2, + "transpose_antihomomorphism_control": 1 + }, + "rank_one_calls": { + "faithful_columns": 204672, + "formal_involutions": 852, + "idempotents": 155, + "nilpotents": 129 + }, + "result": "sharp-formal-tariff-no-new-kappa", + "schema_version": 1, + "semantic_controls": [ + "omitted-call-0", + "omitted-call-1", + "omitted-call-2", + "omitted-call-3", + "omitted-call-4", + "omitted-call-5", + "omitted-call-6", + "omitted-call-7", + "wrong-paid-label", + "dirty-workspace-not-restored", + "rank-two-coupling-rejected", + "root-label-rejected", + "boolean-coupling-rejected", + "boolean-role-count-rejected", + "rank-two-four-call-two-root-counterexample", + "dual-natural-common-kernel-rejected-by-formal-and-dirty-columns", + "overlapping-targets-invalidate-added-middle-bills", + "degree-two-match-with-wrong-central-term" + ], + "source_inputs_checked": [ + "research/bit-three-register-lower-bound/README.md" + ], + "summary": { + "coefficient_words": 20440, + "controls": 18, + "witness_regular_columns": 8896, + "witnesses": 34 + }, + "theorem": { + "prior_four_register_pair_minimum": 8, + "unit_minimum": "4(p+q)", + "universal_evidence": "written proof in README.md, not finite extrapolation", + "x": "2p", + "y": "2(p+q)", + "z": "2q" + }, + "witnesses": [ + { + "conjugated": false, + "formal_sha256": "ea269139eda49fccfbf70eb7f4b9196c20959252b247f0ba29d6168d6afafd20", + "label_counts": { + "x": 0, + "y": 2, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 1, + 1 + ], + "z": [ + 1, + 1 + ] + }, + "p": 0, + "q": 1, + "registers": 1, + "regular_columns": 64, + "regular_sha256": "65c25d65ad40d82c875005d7ebdc16fef7587b666fc01c7fd6314ffd9d5fc6ab" + }, + { + "conjugated": false, + "formal_sha256": "edbc5ecf9d42526f647dcea63c9bebbfda5fe88a41ea6692cc6206c33c0f1b86", + "label_counts": { + "x": 0, + "y": 2, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 1, + 1 + ], + "z": [ + 1, + 1 + ] + }, + "p": 0, + "q": 1, + "registers": 2, + "regular_columns": 128, + "regular_sha256": "61b4c25e87d4a9d3ab578066696a8e96bf3f762fa87e6ff3a7148560feffb170" + }, + { + "conjugated": false, + "formal_sha256": "1e1213af0517967458c6adc1c55101ec376344d2dc41aefa082b9b91dfb2ec73", + "label_counts": { + "x": 0, + "y": 4, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 2, + 2 + ], + "z": [ + 2, + 2 + ] + }, + "p": 0, + "q": 2, + "registers": 2, + "regular_columns": 128, + "regular_sha256": "da9373f81de7b47e535a362b40cb4915b11593d78bda4d93166ac82766e1853d" + }, + { + "conjugated": false, + "formal_sha256": "64337c66722b9555abcbddab282e6eda804d61e5b10560eda7ba530bbcea4cac", + "label_counts": { + "x": 0, + "y": 4, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 2, + 2 + ], + "z": [ + 2, + 2 + ] + }, + "p": 0, + "q": 2, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "a0e4132a2284b6987d67b60ba2f279cd69b50fad9a272f6f5588f178310403a1" + }, + { + "conjugated": false, + "formal_sha256": "5920f3055e90e235e54b76cb27a0a09c82c59e663e4ee6f8b2934f34879c1950", + "label_counts": { + "x": 0, + "y": 6, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 3, + 3 + ], + "z": [ + 3, + 3 + ] + }, + "p": 0, + "q": 3, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "a1dd7de21a16a3ad4da2ee8b7d84b51a90990617c165a148cc873c6b0cae306b" + }, + { + "conjugated": false, + "formal_sha256": "ede0e3a6e086218078a44f6f1da507eefa26572a8db2a564107eed868b6ae46f", + "label_counts": { + "x": 0, + "y": 6, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 0, + 0 + ], + "y": [ + 3, + 3 + ], + "z": [ + 3, + 3 + ] + }, + "p": 0, + "q": 3, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "89d77fac98bc6ec7d70c05ed02c54bbf226f980de00ac81aac9d6020b96a948d" + }, + { + "conjugated": false, + "formal_sha256": "119b714d831408db2dfd9a9ccdade9ed156f595018f81525bcfe504b51097278", + "label_counts": { + "x": 2, + "y": 2, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 1, + 1 + ], + "z": [ + 0, + 0 + ] + }, + "p": 1, + "q": 0, + "registers": 1, + "regular_columns": 64, + "regular_sha256": "10b6c37becba47fcf6620215653a06ae4743e3b0c3c559c84a9de1a690a30a94" + }, + { + "conjugated": false, + "formal_sha256": "a61642be207bdd86bb6b72cb0e50934f7cc0213ffefa552ea4994e6d9a628aa8", + "label_counts": { + "x": 2, + "y": 2, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 1, + 1 + ], + "z": [ + 0, + 0 + ] + }, + "p": 1, + "q": 0, + "registers": 2, + "regular_columns": 128, + "regular_sha256": "4d0e94fd49bd51ecbcf22133862ccf0c83ced9cd7bb1d0779b69152c2621cb69" + }, + { + "conjugated": false, + "formal_sha256": "5831d40f006154ed8546a52600bb648e8953b9865d2a85ea81eed06268775a05", + "label_counts": { + "x": 2, + "y": 4, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 2, + 2 + ], + "z": [ + 1, + 1 + ] + }, + "p": 1, + "q": 1, + "registers": 2, + "regular_columns": 128, + "regular_sha256": "b5422ccd1fb34eaa939f81807d65c25f44f8c8a2c6e2cf5ba754f9ed84c76c90" + }, + { + "conjugated": false, + "formal_sha256": "7d6d4eb1bc114b71b51acea16029d9f81725389663283c42b59da49097de340d", + "label_counts": { + "x": 2, + "y": 4, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 2, + 2 + ], + "z": [ + 1, + 1 + ] + }, + "p": 1, + "q": 1, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "e49f57d2bea5bebf52f401924bfb3af2c1e9b0f363e6b11ebf8315e6d31ac750" + }, + { + "conjugated": false, + "formal_sha256": "f27fd2d15cd1f26aef7234519b71f692aa68f4f91d15a8ea83bd7bd0240450d6", + "label_counts": { + "x": 2, + "y": 6, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 3, + 3 + ], + "z": [ + 2, + 2 + ] + }, + "p": 1, + "q": 2, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "cba5584e1dc21381242fe1501c77621c6d56752b90628dfb3a5e2c1f02557b07" + }, + { + "conjugated": false, + "formal_sha256": "4fe8a66786e7d684d8e0f16f66665d1a734f6c7c0e3e556f5b6bf4d1c071dc14", + "label_counts": { + "x": 2, + "y": 6, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 3, + 3 + ], + "z": [ + 2, + 2 + ] + }, + "p": 1, + "q": 2, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "365b4d11095c75954b4c481709a863c669efce6c5f7065b17a47eb47780a7115" + }, + { + "conjugated": false, + "formal_sha256": "e99cb26e930e28a3f973dab4edbe98324edcfe092fcb1ff853a24393066f807a", + "label_counts": { + "x": 2, + "y": 8, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 4, + 4 + ], + "z": [ + 3, + 3 + ] + }, + "p": 1, + "q": 3, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "0f5450cfa153ebe44dad04b61994f849d97cca4b860e2ed409d542b02999e37f" + }, + { + "conjugated": false, + "formal_sha256": "aedde4fb303088e107bd481474b22384b960ea7aa75c6f8633787f114361feb2", + "label_counts": { + "x": 2, + "y": 8, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 4, + 4 + ], + "z": [ + 3, + 3 + ] + }, + "p": 1, + "q": 3, + "registers": 5, + "regular_columns": 320, + "regular_sha256": "1e3fd737252bcb63c844bb197fee6e278961b1164bbcf933f4bdc4957456430c" + }, + { + "conjugated": false, + "formal_sha256": "bda2ed7e6687c896e47b1980089ae38f593f877164f5b608f5dc829043ab3400", + "label_counts": { + "x": 4, + "y": 4, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 2, + 2 + ], + "z": [ + 0, + 0 + ] + }, + "p": 2, + "q": 0, + "registers": 2, + "regular_columns": 128, + "regular_sha256": "3cb0a5a715ee801ab846ce347d04b653730d5f00fe4a6567563c1c88a71cf515" + }, + { + "conjugated": false, + "formal_sha256": "030d86560e1d9d724b1b7ca25af4eefdaf233c23749dbc7641c4ee01acaacbfb", + "label_counts": { + "x": 4, + "y": 4, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 2, + 2 + ], + "z": [ + 0, + 0 + ] + }, + "p": 2, + "q": 0, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "2ae7d5b426429e802322ed557581ff394075cdee48a6437a3c5a25c0b5904c3f" + }, + { + "conjugated": false, + "formal_sha256": "fe6eb0e8afa67372115407becd316f0c7d505c901c0be53e134825564cf0faec", + "label_counts": { + "x": 4, + "y": 6, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 3, + 3 + ], + "z": [ + 1, + 1 + ] + }, + "p": 2, + "q": 1, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "ad2ae1e66eba289ce7402f6931f943ba75274dccdf3a2355c2f0bdd17da51292" + }, + { + "conjugated": false, + "formal_sha256": "e5343fc84a725ef0781f3c8f65b98e88e5a794b22a4614c1e621249c156562bc", + "label_counts": { + "x": 4, + "y": 6, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 3, + 3 + ], + "z": [ + 1, + 1 + ] + }, + "p": 2, + "q": 1, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "b1f7a83eb2b4fd742addd67309814e4912b85109d22989dfee40a06349977460" + }, + { + "conjugated": false, + "formal_sha256": "14050343d53ce2fe871887fc4b2b9c3b0a4b7d3bd8ea378c5f89187a33fda0ae", + "label_counts": { + "x": 4, + "y": 8, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 4, + 4 + ], + "z": [ + 2, + 2 + ] + }, + "p": 2, + "q": 2, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "c563c06d3e47b19d54664731ca9db1ccbeb820a93b95ca2102bcd7f7e4cca577" + }, + { + "conjugated": false, + "formal_sha256": "5ea586a9bcf257d17223c618e50da6d3078409a3c97f3cbffbf1ba6b6d4dcfd0", + "label_counts": { + "x": 4, + "y": 8, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 4, + 4 + ], + "z": [ + 2, + 2 + ] + }, + "p": 2, + "q": 2, + "registers": 5, + "regular_columns": 320, + "regular_sha256": "f066b1e0a818040db2d6407de8f541c3997741d58d543cbea036f60e94b62a3f" + }, + { + "conjugated": false, + "formal_sha256": "77f9f2f7d702339a5d0225cdd0e22558b0d1405b114a082f4b20b60c367ad250", + "label_counts": { + "x": 4, + "y": 10, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 5, + 5 + ], + "z": [ + 3, + 3 + ] + }, + "p": 2, + "q": 3, + "registers": 5, + "regular_columns": 320, + "regular_sha256": "2a2d0bb3060e4317684079d7f6c843b3cb3ebe1997bec43db4e13b50b525967c" + }, + { + "conjugated": false, + "formal_sha256": "c824970243fe18aa0aa61bd424caac337005caa803a28bb4843b30a0cd8d2fed", + "label_counts": { + "x": 4, + "y": 10, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 5, + 5 + ], + "z": [ + 3, + 3 + ] + }, + "p": 2, + "q": 3, + "registers": 6, + "regular_columns": 384, + "regular_sha256": "9d6f0be5159f99512da68d77dcfa4c4e71f31af78ddfb0034fb4292c7740a54d" + }, + { + "conjugated": false, + "formal_sha256": "d9dfb26298addf1210cbd2293c08e4379ad1d9942fcdf5984ad0dd66047cc3c8", + "label_counts": { + "x": 6, + "y": 6, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 3, + 3 + ], + "z": [ + 0, + 0 + ] + }, + "p": 3, + "q": 0, + "registers": 3, + "regular_columns": 192, + "regular_sha256": "a3ca11ba00ee86592480e346c058557df2fffc1ed6d641746857fdef0735b0d2" + }, + { + "conjugated": false, + "formal_sha256": "28245ae8fe19e31c54119dcd63cd313a819369451019785fb00299f14e320773", + "label_counts": { + "x": 6, + "y": 6, + "z": 0 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 3, + 3 + ], + "z": [ + 0, + 0 + ] + }, + "p": 3, + "q": 0, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "448d2d5a8ee05af5bafea3f0984be75d7ff81d8cef9607ec7877d0fbe482246f" + }, + { + "conjugated": false, + "formal_sha256": "3fa92096ab9bbd96cb86482c0770962e4bfb8abca46f5025c816e8635d099792", + "label_counts": { + "x": 6, + "y": 8, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 4, + 4 + ], + "z": [ + 1, + 1 + ] + }, + "p": 3, + "q": 1, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "c7dc9a9907a8b1625fa643db9274920d836ea71e2935a1838e8d47336c11435b" + }, + { + "conjugated": false, + "formal_sha256": "a4f05c62bfbce5e9ecd052d0c396a1d8e6528aada893953a9a75900042c5057b", + "label_counts": { + "x": 6, + "y": 8, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 4, + 4 + ], + "z": [ + 1, + 1 + ] + }, + "p": 3, + "q": 1, + "registers": 5, + "regular_columns": 320, + "regular_sha256": "592cc11a0af215c1bbfcec39c0a26fe7b0587f264079bdd32f21594ae4c701a1" + }, + { + "conjugated": false, + "formal_sha256": "8c0bbeb2667e6e7c41ace81bf76fb38e143f7898e93558e7e193c7b910337024", + "label_counts": { + "x": 6, + "y": 10, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 5, + 5 + ], + "z": [ + 2, + 2 + ] + }, + "p": 3, + "q": 2, + "registers": 5, + "regular_columns": 320, + "regular_sha256": "ccec4283e025c61461ab22a0b7c63049e47287cb240b8529dd78ee298c8f6a6c" + }, + { + "conjugated": false, + "formal_sha256": "64a979e6265a3efbe383e5b8dfea257ed12e97aa54c9ca40bcbfc10cad48e2f4", + "label_counts": { + "x": 6, + "y": 10, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 5, + 5 + ], + "z": [ + 2, + 2 + ] + }, + "p": 3, + "q": 2, + "registers": 6, + "regular_columns": 384, + "regular_sha256": "86b38eb7fd36d9367ccdaf8891f1e41951102257707a3a8540566dc972b65990" + }, + { + "conjugated": false, + "formal_sha256": "1489e809f3130fdb010f6559c7a4976a9fa7ebbb5b94fc09000f71952cd5b0ca", + "label_counts": { + "x": 6, + "y": 12, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 6, + 6 + ], + "z": [ + 3, + 3 + ] + }, + "p": 3, + "q": 3, + "registers": 6, + "regular_columns": 384, + "regular_sha256": "355f9cf69e037659045ad87b3e5fbb9568a158f1c08e05106c387ff826fa2cf0" + }, + { + "conjugated": false, + "formal_sha256": "0f544a3d0675c24774278be37c7dfd2e864789973a761682ea48fd32eea320c5", + "label_counts": { + "x": 6, + "y": 12, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 6, + 6 + ], + "z": [ + 3, + 3 + ] + }, + "p": 3, + "q": 3, + "registers": 7, + "regular_columns": 448, + "regular_sha256": "7d0a82b87842d4a17ed7e94df44f0056bb96b7a19d262639d698ea7926f72b46" + }, + { + "conjugated": false, + "formal_sha256": "01e216c4d42446dee1895208741ef79eb7c8b19002230cda1ffb792492fde5c3", + "label_counts": { + "x": 2, + "y": 4, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 2, + 2 + ], + "z": [ + 1, + 1 + ] + }, + "p": 1, + "q": 1, + "registers": 8, + "regular_columns": 512, + "regular_sha256": "d612a00f0e2650fd2668a095614e41e4561ba8c79f24e4a62719ed3597a95838" + }, + { + "conjugated": false, + "formal_sha256": "2dcb472a2c352d58f2289c4f452b03bbb2f54beb60881002650cb59ffd4fa935", + "label_counts": { + "x": 6, + "y": 12, + "z": 6 + }, + "label_span_ranks": { + "x": [ + 3, + 3 + ], + "y": [ + 6, + 6 + ], + "z": [ + 3, + 3 + ] + }, + "p": 3, + "q": 3, + "registers": 8, + "regular_columns": 512, + "regular_sha256": "9d4300f2eae550f087d399011410c29da615c88aaff78e649d1787bb2a402fb0" + }, + { + "conjugated": true, + "formal_sha256": "5d3f5dd1de78892c3d3877a7d04a1de824ef1721dc495175f72516094da989bb", + "label_counts": { + "x": 2, + "y": 4, + "z": 2 + }, + "label_span_ranks": { + "x": [ + 1, + 1 + ], + "y": [ + 2, + 2 + ], + "z": [ + 1, + 1 + ] + }, + "p": 1, + "q": 1, + "registers": 4, + "regular_columns": 256, + "regular_sha256": "e912ae0892008ef9bf11cecc2547cc8613aecafa683545d873cf7ce657d189f2" + }, + { + "conjugated": true, + "formal_sha256": "acfb8deecf9389c3e5ce72f972c777382541f617756f7827b5cadb0bfc5e4414", + "label_counts": { + "x": 4, + "y": 8, + "z": 4 + }, + "label_span_ranks": { + "x": [ + 2, + 2 + ], + "y": [ + 4, + 4 + ], + "z": [ + 2, + 2 + ] + }, + "p": 2, + "q": 2, + "registers": 8, + "regular_columns": 512, + "regular_sha256": "414690b3a4cd186b6c65f68b2c83a3a984ca4a5e63d7721ceef9c6c7388aceb9" + } + ] +} diff --git a/research/ut4-noncentral-shared-middle/README.md b/research/ut4-noncentral-shared-middle/README.md new file mode 100644 index 0000000000..8a082d7a85 --- /dev/null +++ b/research/ut4-noncentral-shared-middle/README.md @@ -0,0 +1,260 @@ +# Disjoint UT4 root targets cannot share the middle-generator bill + +**Sharp formal-algebra theorem; no new supplier or kappa.** For `p` target +roles carrying `u=I+E13` and `q` different roles carrying `v=I+E24`, in the +restricted `UT4(F2)` alphabet below, every word pays + +``` +n_x >= 2p, n_y >= 2(p+q), n_z >= 2q. +``` + +The direct `4(p+q)`-call word attains all three bounds simultaneously, for +every finite `r>=p+q>0`. All extra roles may contain arbitrary dirty inputs +and must be restored. The result includes every nonzero binary rank-one +scalar coupling, both idempotent and nilpotent, and arbitrary free scalar +mixing. Thus nonnegative uniform label prices `alpha,beta,gamma` give the +exact tariff `2p alpha + 2(p+q) beta + 2q gamma` in this model. + +In particular, **the minimum in Cinna Davis's [PR1761](https://github.com/CrocSwap/integer-mult-bounds/pull/1761) +is eight**, not five, six or seven. That predecessor proves a four-register +length-at-most-four exclusion and gives the eight-call upper witness. This +successor closes its explicit gap by a written all-register argument, not a +larger finite search. It does not claim the predecessor's construction or +bounded exclusion as new. + +## Model and complete formal bill + +Use one-based address indices and let + +``` +G = UT4(F2), R = F2[G], +x = I+E12, y = I+E23, z = I+E34, +u = xyxy = I+E13, v = yzyz = I+E24. +``` + +The roots `u,v` are noncentral: `[u,z]=[x,v]=I+E14`. The group has 64 +elements. Equality below is equality in the **full formal group algebra**, +not equality only in a natural representation or on one small address set. +For scalar register count `r`, an allowed paid factor is + +``` +D_N(g) = I_r + ([g]+1)N, +g in {x,y,z}, N=a b^T != 0, a,b in F2^r. +``` + +There is no restriction on `b^T a`. Since `g` is an involution, +`([g]+1)^2=0`, so every paid factor squares to identity even when `N` is +nilpotent. All inverses are charged occurrences, not free undo. All scalar +register inputs are arbitrary; the target is + +``` +T = diag([u] repeated p, [v] repeated q, [1] repeated r-p-q). +``` + +Free operations are scalar `GL_r(F2)` maps only. Move them to one end by +conjugating the `N`s; rank one is preserved. Augmentation `[g] -> 1` sends +every paid factor and `T` to identity, forcing that final scalar map to +identity. The displayed alphabet therefore includes every normalized word. +This standard normalization is credited to the preceding register-model work. +No free address map, clean allocation, COPY, ERASE or higher-rank paid call +is permitted. + +The upper word applies `x,y,x,y` on each `u` coordinate and `y,z,y,z` on each +`v` coordinate, with coordinate-projector couplings. Each four-call product +is exactly its formal group monomial; different scalar roles do not interact. +It uses `p+q` data roles, no additional workspace or scalar preparation, and +exactly `2p,2(p+q),2q` calls; appended dirty roles stay identity. No restoration +outside this word is omitted. + +This is a **complete abstract paid-call bill**, not a physical supplier +invoice. Frames, common labels, hosting, precision/tape and recursive +interfaces have not been realized. Their costs are not declared zero. No +selected paid profile, moment or multiplication exponent is improved. + +## Proof: the simultaneous middle span, not two added bounds + +All ranks and scalar spans are over `F2`. Let +`P=diag(I_p,0,0)` and `Q=diag(0,I_q,0)` in `M_r(F2)`. Their column spaces +are disjoint of dimensions `p,q`; their row spaces are likewise disjoint. +Write products in **left-to-right matrix order**. For labels `a,b` define + +``` +S_a = sum_{i: g_i=a} N_i, +C_ab = sum_{i= p+p, n_y >= (p+q)+(p+q), n_z >= q+q. +``` + +The explicit upper word attains every bound. This proves the theorem for +all finite register counts and word lengths, including arbitrary dirty +workspace, without an exhaustive search or an unquantified extrapolation. +Scalar conjugation preserves the direct-sum dimensions, so the same proof +also applies to a simultaneous scalar conjugate of the target. + +### Why the disjoint-role hypothesis matters + +Putting both root actions on **one** role is a different endpoint: +`[uv]`, not `diag([u],[v])`. In fact the full formal identity + +``` +xyzxyz = uv +``` + +costs only six calls and two middle calls. Its two root coefficients occupy +the same scalar subspace, of dimension one rather than two. This is a +positive countercontrol to dropping disjointness, not an improvement on the +stated two-role target. In contrast, `xzyxzy` also has the desired degree-two +coefficients but acquires the nontrivial `E14` term. The verifier distinguishes +these endpoints in the full algebra. + +## Executable evidence and reproduction + +The package's standard-library checker uses exact binary arithmetic. Its +primary representation is a scalar matrix of 64-bit formal coefficient +vectors. A second engine uses literal binary 4-by-4 address matrices and +replays the faithful left-regular action on **every** address/register basis +column, including dirty workspace. It imports no primary arithmetic. + +Finite controls corroborate the proof and implementation; they do not prove +the unbounded theorem. `CERTIFICATE.json` records the complete deterministic +finite coverage. `VALIDATION.json` records only commands actually exercised. + +The deterministic evidence contains: + +| Check | Exact exercised domain | +| --- | --- | +| Group law and contragredient homomorphism | All 4,096 ordered group pairs each | +| Expanded rank-one alphabet | 284 matrices at `r=1,2,3,4`: 155 idempotents, 129 nilpotents | +| Involutions and faithful single-call action | 852 calls; 204,672 regular basis columns | +| Coefficient recurrence and span inclusions | All 20,440 two-register words of length `0..3` over 27 factors | +| Attaining formal/faithful witnesses | 34 fixtures through eight roles; 8,896 dirty basis columns, including two non-coordinate scalar conjugates | +| Semantic controls | 18: eight omitted calls, wrong label, dirty restoration, rank/label/type violations, a genuine rank-two shortcut, common representation kernel, overlapping targets, and wrong class-three term | + +The coefficient census has lengths `1,27,729,19683`; its canonical coefficient +digest is `b94b89bf4f84879a0dd3c7b55a553b7eeaf553855dcba33d702db719832783f8`. +It is not a search excluding lengths five through seven: the written span +proof excludes those lengths and all other short words uniformly. +The verifier recomputes and compares the complete certificate, read-only by +default; `--emit` prints it without modifying files. All semantic guards +remain active under `-O`. + +From the repository root: + +```sh +uv run --python 3.12 --no-project python -I -O -B research/ut4-noncentral-shared-middle/verify.py +uv run --python 3.12 --no-project python -I -B scripts/research_package.py --package research/ut4-noncentral-shared-middle +``` + +The card's working example `scripts/research_baseline.py` returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`, with the complex primitive binding. +That checks selected source bindings and arithmetic, **not** the selected +cold replay. No native supplier, all-size realization, Lean, independent +human proof review or hosted CI pass is claimed. + +## Provenance, novelty and attribution + +Exact base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. One unforced chooser +invocation sampled OS nonce `5080ba3917adb12fda1e688c38733a49`, selecting +`bit-mechanisms`; [SELECTION.json](SELECTION.json) preserves the entire emitted +record. [TASK.json](TASK.json) records the two proposed cards, actual refined +scope, cost screen, stopping rule, overlap coverage and claim. The public +[successor claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1759#discussioncomment-18925851) +links the [round coordination thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929). + +- **Cinna Davis (@1337isnot1337), PR1761**, head + `0f4f6d79b14573116e47d31d012f8e3f7a49cd87`: exact noncentral pair, + four-register `q<=4` exclusion, eight-call upper word and explicit gap. +- **steph4n-gh, PR1573**, head `0b8c5a69297c794f2de22c04494c83e41300ae36`: + UT3 all-register theorem using two representations and zero-sum scalar + rank-nullity. Those tools, rather than their reinvention, are used here. +- **Arham Tahir, PR1589**, head `010ec8c01c0edbbb08b541be236ab78d096f2ca1`: + UT3 nilpotent rank-one extension and mixed-coefficient proof. +- PR1662/1680/1690/1816 treat the **central E14 target**, a different + class-three constraint. This proof neither replays nor settles their claims. +- Credit @woklerx's PR1443, @juper997's PR1478, Gareth Davidson/@bitplane's + PR1333, and the eumemic/Ali Romman/David Govea register-model lineage. + +[SOURCES.json](SOURCES.json) pins source provenance and contextual predecessor +heads. No predecessor code is imported, frozen evidence is unchanged, and +no selected-frontier file is edited. Cached overlap covers 579 open PRs and +547 discussion records with complete pagination, plus local notes; exact +relevant heads were read live. This is not a claim of literature priority or +a novelty guarantee from search absence. The new result is the simultaneous +shared-middle obstruction and exact resolution of the existing noncentral +pair gap, not a second presentation of the UT3 theorem. + +## Open next questions + +Can an actual bit-supplier implementation realize this restricted nonabelian +alphabet at a favorable **complete** tariff and with the needed target +interface? The first useful step is one explicit realized `x,y,z` call family, +with every frame transition, dirty-state restoration and recursive/precision +charge counted. The absence of such a realization blocks a supplier claim; +more dirty registers or a longer search in the current disjoint-root model +cannot lower the proved abstract bill. A formally cheaper enlarged primitive +must be priced rather than simply assigned unit cost. + +Prepared for **Adam Gall** with substantial **OpenAI Codex GPT-6 Astra** +assistance in research, proof, implementation and writing. The two executable +representations are AI-assisted work from the same session, not independent +human review. New work is Apache-2.0; predecessor notices remain unchanged. diff --git a/research/ut4-noncentral-shared-middle/SELECTION.json b/research/ut4-noncentral-shared-middle/SELECTION.json new file mode 100644 index 0000000000..4085e8f785 --- /dev/null +++ b/research/ut4-noncentral-shared-middle/SELECTION.json @@ -0,0 +1,60 @@ +{ + "seed": "5080ba3917adb12fda1e688c38733a49", + "track": "bit-mechanisms", + "suggestions": [ + { + "task_id": "bit-new-register-model", + "scope_key": "7f5f4426ef796683c485", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "method": "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "starting_points": ["research/bit-three-register-lower-bound/README.md", "certificates/selected-result.json"], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": ["python3", "-B", "scripts/research_baseline.py"], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": ["Choose a fixed larger register count or a specified nonabelian operation family."], + "scope_change_triggers": ["Remaining inside the already-excluded three-register abelian model."], + "overlap_terms": ["three-register", "nonabelian", "group algebra"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "bit-helper-contract", + "scope_key": "3475f46c8358c6a9211b", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "method": "Derive a replacement interface lemma and price its implementation.", + "starting_points": ["research/r439-bsection-stars-seed01/README.md", "research/r439-copy-path-sharing-barrier/README.md"], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": ["python3", "-B", "research/r439-bsection-stars-seed01/verify.py"], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": ["Choose one helper-star or quartet instance; narrow to one boundary implication."], + "scope_change_triggers": ["Changing only source count or scalar addition count without an interface argument."], + "overlap_terms": ["H2_D_frame0_targets_from_helpers", "K_equals_D", "helper-star"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/ut4-noncentral-shared-middle/SOURCES.json b/research/ut4-noncentral-shared-middle/SOURCES.json new file mode 100644 index 0000000000..c2b6a5683e --- /dev/null +++ b/research/ut4-noncentral-shared-middle/SOURCES.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ], + "remote_context": [ + { + "pr": 1761, + "commit": "0f4f6d79b14573116e47d31d012f8e3f7a49cd87", + "path": "research/ut4-noncentral-commutator-seedbfe59/README.md", + "author": "Cinna Davis (@1337isnot1337)", + "git_blob": "a3de0db4b4e8ed4be897f64ec4d55917fc240539", + "sha256": "d78bcf3d757587b69b486b191747f0f9590cddb0136c272edd479b3ce885ed32", + "usage": "Context and open gap; no executable dependency or imported proof premise." + }, + { + "pr": 1573, + "commit": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "path": "research/ut3-commutator-all-registers/README.md", + "author": "steph4n-gh", + "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d", + "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b", + "usage": "Credited zero-sum rank-nullity and representation method; proof restated for the new target." + }, + { + "pr": 1589, + "commit": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "path": "research/ut3-two-targets-any-registers/README.md", + "author": "Arham Tahir", + "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f", + "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399", + "usage": "Credited nilpotent rank-one extension; no imported implementation." + } + ] +} diff --git a/research/ut4-noncentral-shared-middle/TASK.json b/research/ut4-noncentral-shared-middle/TASK.json new file mode 100644 index 0000000000..0562ba47ce --- /dev/null +++ b/research/ut4-noncentral-shared-middle/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Sharp separate x/y/z paid-call tariffs for disjoint E13/E24 target roles in F2[UT4(F2)], with arbitrary finite restored dirty workspace and every nonzero binary rank-one coupling.", + "scope_change_reason": "Choose the card's specified nonabelian alphabet variation. PR1761 leaves the exact noncentral pair minimum between five and eight after a four-register length-four search. Replace that bounded search by a simultaneous shared-middle column/row-span proof, closing its stated gap rather than changing a seed or enlarging a search cutoff. Nilpotent couplings are included as an optimistic strengthening, following PR1589.", + "bottleneck_link": "A negative screen for a concrete pending bit mechanism: the shared y generator cannot amortize its call bill across disjoint root targets even with restored dirty workspace. This is a formal-algebra side result, not a physical supplier or kappa improvement; the selected complex primitive remains binding.", + "budget_minutes": 120, + "stop_rule": "Prove or falsify the simultaneous middle-label span implication before synthesis. Stop after a complete written all-register argument, exact full-formal attaining witnesses and bounded independent representation/control checks; do not launch a larger word census or lower the target.", + "outcome": "negative-result", + "evidence": "README.md proves nx>=2p, ny>=2(p+q), nz>=2q for every r>=p+q>0, attained by explicit formal coordinate words. verify.py and regular.py provide finite exact corroboration, complete dirty-column fixtures and semantic controls; CERTIFICATE.json is their deterministic receipt. No finite extrapolation or physical supplier claim.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex GPT-6 Astra assistance in research, proof, implementation and writing. No worker subagents; no independent human or proof-assistant verification claimed.", + "seed": "5080ba3917adb12fda1e688c38733a49", + "track": "bit-mechanisms", + "scope_key": "7f5f4426ef796683c485/UT4-disjoint-height-two-roots/all-rank-one-dirty-workspace/sharp-label-tariff", + "selection_file": "SELECTION.json", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1759#discussioncomment-18925851", + "round_coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929", + "changed_hypothesis": "Replace the three-register rational abelian frame model by the explicitly priced nonabelian UT4 alphabet x=I+E12,y=I+E23,z=I+E34, and prove a target-specific theorem with arbitrary finite dirty workspace.", + "method_domain": "Natural and inverse-transpose group representations, all four second-order coefficient identities, shared span unions, and rank-nullity for zero first-order sums. Full formal coefficient and independent regular-operator fixtures through eight scalar registers, plus exhaustive group-law and bounded rank-inequality controls.", + "optimistic_complete_budget": { + "paid_labels": ["x", "y", "z"], + "couplings": "Every nonzero binary rank-one N; trace zero or one", + "uniform_tariff": "2p*alpha + 2(p+q)*beta + 2q*gamma for nonnegative uniform per-label prices", + "data_roles": "p+q disjoint target roles", + "dirty_workspace": "r-p-q arbitrary input roles, all restored", + "free_operations": "Scalar GL_r(F2) mixing only, removed by augmentation normalization", + "forbidden_free_operations": "No free address maps, clean allocation, COPY, ERASE, higher-rank calls or uncharged inverse", + "attaining_word": "xyxy on each E13 role; yzyz on each E24 role; all other roles identity", + "physical_limits": "No supplier implementation or compiler/hosting/precision bill is provided; those costs are not declared zero." + }, + "success_falsification": { + "success": "Separate universal label bounds and exact formal upper witness meet; PR1761's p=q=1,r=4 gap closes at eight.", + "falsification": "Any legal shorter formal endpoint, or a failure of a second-order representation/zero-sum span implication, invalidates the proposed theorem. Overlapping target subspaces must fail the disjoint-union claim.", + "first_example": "uv run --python 3.12 --no-project python -B scripts/research_baseline.py returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY; complex binding; no full cold replay." + }, + "nearest_work": [ + {"pr": 1761, "head": "0f4f6d79b14573116e47d31d012f8e3f7a49cd87", "author": "Cinna Davis (@1337isnot1337)", "delta": "Same E13/E24 pair; predecessor excludes length<=4 in r=4 and leaves5..7 open."}, + {"pr": 1573, "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", "author": "steph4n-gh", "delta": "Credits the zero-projector-sum rank proof for one UT3 root family; does not sum the two overlapping y obligations here."}, + {"pr": 1589, "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", "author": "Arham Tahir", "delta": "Credits nilpotent rank-one extension and mixed-coefficient method in UT3."}, + {"pr": 1662, "head": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390", "delta": "Different height-three central E14 targets, not the disjoint noncentral roots."} + ], + "overlap": { + "open_prs": {"records": 579, "complete_pagination": true, "fetched_at": "2026-10-14T14:10:13.054433+00:00"}, + "discussion_records": {"records": 547, "complete_pagination": true, "fetched_at": "2026-10-14T14:11:43.639832+00:00"}, + "queries": ["--task bit-new-register-model --offline", "--task bit-helper-contract --offline", "noncentral UT4 shared middle --offline"], + "final_live_head_check": { + "checked_on": "2026-10-14", + "method": "Targeted GitHub GraphQL query for PR1761,1573,1589,1662 and the last three comments in discussion1759", + "heads_unchanged": { + "1761": "0f4f6d79b14573116e47d31d012f8e3f7a49cd87", + "1573": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "1589": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "1662": "01cc02b164ecc4f9d84df3f56a1fe65b88daf390" + }, + "discussion": "Only the predecessor FINDING/HANDOFF and this successor CLAIM appeared; the predecessor still explicitly leaves5..7 open.", + "limits": "Targeted live refresh, not a second global novelty scan." + }, + "limits": "Cached open PR bodies, discussions and local notes; no claim of novelty from absence. Targeted live PR1761/1573/1589 reads and thread1759 checked before claiming." + }, + "open_questions": [ + { + "question": "Can an actual bit supplier realize this restricted nonabelian alphabet with a favorable complete tariff and the required target interface?", + "why_it_matters": "The abstract direct bill is now sharp; more restored dirty roles cannot help. A supplier claim requires actual address-call realization and paid recursive/interface costs.", + "first_step": "Specify one implemented x/y/z call family and count every frame transition, dirty restoration, recursive and precision charge before synthesis.", + "blocked_by": "No physical realization or supplier interface for this formal group-algebra alphabet is supplied. Assigning an enlarged primitive unit cost is not an implementation." + } + ] +} diff --git a/research/ut4-noncentral-shared-middle/VALIDATION.json b/research/ut4-noncentral-shared-middle/VALIDATION.json new file mode 100644 index 0000000000..e162f76add --- /dev/null +++ b/research/ut4-noncentral-shared-middle/VALIDATION.json @@ -0,0 +1,76 @@ +{ + "recorded_at_utc": "2026-10-14T14:25:55.296602+00:00", + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "phase": "focused final verification after implementation and certificate generation", + "commands": [ + { + "argv": [ + "uv", + "run", + "--python", + "3.12", + "--no-project", + "python", + "-c", + "import sys,platform; print(sys.version); print(platform.platform())" + ], + "exit_code": 0, + "elapsed_seconds": 0.033, + "stdout": "3.12.12 (main, Jan 14 2026, 23:36:32) [Clang 21.1.4 ]\nmacOS-27.0.1-arm64-arm-64bit\n", + "stderr": "" + }, + { + "argv": [ + "uv", + "run", + "--python", + "3.12", + "--no-project", + "python", + "-I", + "-O", + "-B", + "research/ut4-noncentral-shared-middle/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 1.354, + "stdout": "PASS_UT4_SHARED_MIDDLE pair_minimum=8 witnesses=34 dirty_columns=8896 coefficient_words=20440 controls=18 no_new_kappa\n", + "stderr": "" + }, + { + "argv": [ + "uv", + "run", + "--python", + "3.12", + "--no-project", + "python", + "-I", + "-B", + "scripts/research_package.py", + "--package", + "research/ut4-noncentral-shared-middle" + ], + "exit_code": 0, + "elapsed_seconds": 1.426, + "stdout": "CHECK Exact formal and independent faithful dirty-column witnesses; natural/contragredient coefficient identities; all expanded rank-one calls r<=4; bounded coefficient census; omission, dirty restoration, quotient-kernel, rank/label and overlapping-target controls; complete certificate and runtime source pins.\nPASS_UT4_SHARED_MIDDLE pair_minimum=8 witnesses=34 dirty_columns=8896 coefficient_words=20440 controls=18 no_new_kappa\nPASS_REGISTERED_RESEARCH_PACKAGE research/ut4-noncentral-shared-middle outcome=negative-result\n", + "stderr": "" + } + ], + "orientation": { + "command": "uv run --python 3.12 --no-project python -B scripts/research_baseline.py", + "observed_status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "binding_primitive": "complex", + "scope": "selected source bindings and arithmetic only; not full cold replay" + }, + "not_run": [ + "selected frontier cold replay", + "native supplier", + "physical compiler and hosting", + "precision/tape realization", + "outer analytic transfer", + "Lean proof", + "hosted CI", + "independent human proof review" + ] +} diff --git a/research/ut4-noncentral-shared-middle/VERIFY.json b/research/ut4-noncentral-shared-middle/VERIFY.json new file mode 100644 index 0000000000..7f9e4ed4f2 --- /dev/null +++ b/research/ut4-noncentral-shared-middle/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact formal and independent faithful dirty-column witnesses; natural/contragredient coefficient identities; all expanded rank-one calls r<=4; bounded coefficient census; omission, dirty restoration, quotient-kernel, rank/label and overlapping-target controls; complete certificate and runtime source pins." + } + ] +} diff --git a/research/ut4-noncentral-shared-middle/regular.py b/research/ut4-noncentral-shared-middle/regular.py new file mode 100755 index 0000000000..9d52f70eb9 --- /dev/null +++ b/research/ut4-noncentral-shared-middle/regular.py @@ -0,0 +1,106 @@ +#!/usr/bin/env python3 +"""Literal UT4 matrices and faithful dirty-column replay; Apache-2.0. + +Written with substantial OpenAI Codex assistance. No primary-verifier imports. +""" +from itertools import product + + +def multiply(a, b): + """Multiply binary matrices represented by integer row bitsets.""" + result = [] + for row in a: + value = 0 + for k, right in enumerate(b): + if row & (1 << k): + value ^= right + result.append(value) + return tuple(result) + + +def transpose(a): + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(a)) + for j in range(len(a))) + + +def inverse(a): + n = len(a) + rows = [row | (1 << (n + i)) for i, row in enumerate(a)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i] & (1 << j)), None) + if pivot is None: + raise ValueError("singular matrix") + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(n): + if i != j and rows[i] & (1 << j): + rows[i] ^= rows[j] + return tuple(row >> n for row in rows) + + +IDENTITY = (1, 2, 4, 8) +POSITIONS = ((0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)) +# Build the group from literal entries, not the primary six-bit product formula. +GROUP = [] +for number in range(64): + rows = list(IDENTITY) + for bit, (i, j) in enumerate(POSITIONS): + if number & (1 << bit): + rows[i] ^= 1 << j + GROUP.append(tuple(rows)) +GROUP = tuple(GROUP) +INDEX = {g: i for i, g in enumerate(GROUP)} +LEFT = tuple(tuple(INDEX[multiply(g, h)] for h in GROUP) for g in GROUP) +GENERATORS = {"x": (3, 2, 4, 8), "y": (1, 6, 4, 8), "z": (1, 2, 12, 8)} + + +def left_translate(g, support): + result = 0 + while support: + low = support & -support + result ^= 1 << LEFT[g][low.bit_length() - 1] + support ^= low + return result + + +def replay(word, registers): + """Return every faithful regular column, for all 64*r dirty basis inputs. + + A word is in left-to-right matrix order; apply rightmost factor first. + Each tuple is (label, binary left vector, binary right vector). + """ + columns = [] + for source, address in product(range(registers), range(64)): + state = [0] * registers + state[source] = 1 << address + for label, left, right in reversed(word): + g = INDEX[GENERATORS[label]] + value = 0 + for j in range(registers): + if right & (1 << j): + value ^= state[j] + delta = left_translate(g, value) ^ value + for i in range(registers): + if left & (1 << i): + state[i] ^= delta + columns.append(sum(block << (64 * i) for i, block in enumerate(state))) + return tuple(columns) + + +def represented(formal, dual=False): + """Map a formal matrix to natural/contragredient address blocks.""" + r = len(formal) + result = [0] * (4 * r) + for i in range(r): + for j in range(r): + mask = formal[i][j] + while mask: + low = mask & -mask + address = GROUP[low.bit_length() - 1] + if dual: + address = transpose(inverse(address)) + for a, row in enumerate(address): + for b in range(4): + if row & (1 << b): + result[a * r + i] ^= 1 << (b * r + j) + mask ^= low + return tuple(result) diff --git a/research/ut4-noncentral-shared-middle/verify.py b/research/ut4-noncentral-shared-middle/verify.py new file mode 100755 index 0000000000..aa51985997 --- /dev/null +++ b/research/ut4-noncentral-shared-middle/verify.py @@ -0,0 +1,469 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the written shared-middle theorem. Apache-2.0. + +Substantial OpenAI Codex assistance. Finite checks are not the universal proof. +""" +from __future__ import annotations + +import argparse +import hashlib +import importlib.util +import json +from collections import Counter +from itertools import product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("ut4_regular", HERE / "regular.py") +if SPEC is None or SPEC.loader is None: + raise RuntimeError("cannot load independent regular engine") +regular = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(regular) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def bits(value): + while value: + low = value & -value + yield low.bit_length() - 1 + value ^= low + + +def group_product(g, h): + # Strict-upper entries 12,13,14,23,24,34; no literal matrix multiplication. + a, b, c, d, e, f = ((g >> k) & 1 for k in range(6)) + A, B, C, D, E, F = ((h >> k) & 1 for k in range(6)) + out = (a ^ A, b ^ B ^ (a & D), c ^ C ^ (a & E) ^ (b & F), + d ^ D, e ^ E ^ (d & F), f ^ F) + return sum(value << i for i, value in enumerate(out)) + + +TABLE = tuple(tuple(group_product(g, h) for h in range(64)) for g in range(64)) +LABELS = {"x": 1, "y": 8, "z": 32} +U, V, CENTRAL = 2, 16, 4 +PAIRS = ("xy", "yx", "yz", "zy") + + +def identity(r): + return tuple(1 << i for i in range(r)) + + +def zero(r): + return (0,) * r + + +def matrix_xor(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def matrix_product(a, b): + out = [] + for row in a: + value = 0 + for j in bits(row): + value ^= b[j] + out.append(value) + return tuple(out) + + +def matrix_transpose(a): + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(a)) + for j in range(len(a))) + + +def outer(u, v, r): + return tuple(v if (u >> i) & 1 else 0 for i in range(r)) + + +def rank(vectors): + pivots = {} + for item in vectors: + while item: + pivot = item.bit_length() - 1 + if pivot in pivots: + item ^= pivots[pivot] + else: + pivots[pivot] = item + break + return len(pivots) + + +def rank_one_factors(matrix): + nonzero = [row for row in matrix if row] + require(nonzero and all(row == nonzero[0] for row in nonzero), "coupling must have rank one") + return sum(bool(row) << i for i, row in enumerate(matrix)), nonzero[0] + + +def validate_call(label, matrix, r): + require(label in LABELS, "paid address label outside x/y/z") + require(len(matrix) == r and all(type(row) is int and 0 <= row < 1 << r for row in matrix), + "invalid scalar coupling") + return rank_one_factors(matrix) + + +def formal_identity(r): + return tuple(tuple(int(i == j) for j in range(r)) for i in range(r)) + + +def right_translate(mask, g): + out = 0 + for h in bits(mask): + out ^= 1 << TABLE[h][g] + return out + + +def append_factor(formal, g, coupling): + """Right multiply by I+([g]+1)N, allowing general N for controls.""" + r = len(formal) + result = [list(row) for row in formal] + for i in range(r): + for k in range(r): + changed = formal[i][k] ^ right_translate(formal[i][k], g) + for j in bits(coupling[k]): + result[i][j] ^= changed + return tuple(tuple(row) for row in result) + + +def formal_word(word, r): + result = formal_identity(r) + for label, u, v in word: + coupling = outer(u, v, r) + validate_call(label, coupling, r) + result = append_factor(result, LABELS[label], coupling) + return result + + +def target(p, q, r): + require(type(p) is int and type(q) is int and type(r) is int and p >= 0 and q >= 0 + and 0 < p + q <= r, "invalid target roles") + group = [U] * p + [V] * q + [0] * (r - p - q) + return tuple(tuple((1 << group[i]) if i == j else 0 for j in range(r)) for i in range(r)) + + +def direct_word(p, q): + result = [] + for i in range(p + q): + labels = "xyxy" if i < p else "yzyz" + result.extend((label, 1 << i, 1 << i) for label in labels) + return result + + +def conjugate_formal(formal, scalar, inverse): + r = len(scalar) + out = [[0] * r for _ in range(r)] + for i in range(r): + for a in bits(scalar[i]): + for b in range(r): + for j in bits(inverse[b]): + out[i][j] ^= formal[a][b] + return tuple(tuple(row) for row in out) + + +def conjugate_word(word, scalar, inverse): + r = len(scalar) + out = [] + for label, u, v in word: + left = sum(((row & u).bit_count() & 1) << i for i, row in enumerate(scalar)) + right = 0 + for j in bits(v): + right ^= inverse[j] + out.append((label, left, right)) + return out + + +def formal_regular(formal): + """Faithful embedding computed from the independent formal coefficients.""" + r = len(formal) + columns = [] + for j in range(r): + for h in range(64): + column = 0 + for i in range(r): + for g in bits(formal[i][j]): + column ^= 1 << (64 * i + TABLE[g][h]) + columns.append(column) + return tuple(columns) + + +def update_coefficients(coefficients, label, coupling): + result = dict(coefficients) + for pair in PAIRS: + if pair[1] == label: + result[pair] = matrix_xor(result[pair], matrix_product(coefficients[pair[0]], coupling)) + result[label] = matrix_xor(result[label], coupling) + return result + + +def coefficients_of(word, r): + coefficients = {key: zero(r) for key in (*LABELS, *PAIRS)} + for label, u, v in word: + coefficients = update_coefficients(coefficients, label, outer(u, v, r)) + return coefficients + + +def block(matrix, i, j, r): + return tuple((matrix[i * r + k] >> (j * r)) & ((1 << r) - 1) for k in range(r)) + + +def check_coefficients(formal, coefficients): + r = len(formal) + natural = regular.represented(formal) + dual = regular.represented(formal, dual=True) + for key, i, j in (("x", 0, 1), ("y", 1, 2), ("z", 2, 3), + ("xy", 0, 2), ("yz", 1, 3)): + require(block(natural, i, j, r) == coefficients[key], "natural coefficient mismatch") + for key, i, j in (("x", 1, 0), ("y", 2, 1), ("z", 3, 2), + ("yx", 2, 0), ("zy", 3, 1)): + require(block(dual, i, j, r) == coefficients[key], "dual coefficient mismatch") + + +def span_bounds(word, coefficients, r): + spans = {} + for label in LABELS: + left = [u for g, u, _ in word if g == label] + right = [v for g, _, v in word if g == label] + dl, dr = rank(left), rank(right) + if coefficients[label] == zero(r): + require(dl + dr <= len(left), "zero-sum rank-nullity fails") + spans[label] = (dl, dr) + for pair in PAIRS: + if pair[0] == label: + require(rank(left + list(matrix_transpose(coefficients[pair]))) == dl, + "coefficient column escapes label span") + if pair[1] == label: + require(rank(right + list(coefficients[pair])) == dr, + "coefficient row escapes label span") + return spans + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def group_checks(): + for g, h in product(range(64), repeat=2): + require(TABLE[g][h] == regular.LEFT[g][h], "independent group products differ") + left = regular.transpose(regular.inverse(regular.GROUP[TABLE[g][h]])) + right = regular.multiply(regular.transpose(regular.inverse(regular.GROUP[g])), + regular.transpose(regular.inverse(regular.GROUP[h]))) + require(left == right, "contragredient is not multiplicative") + require(TABLE[U][32] != TABLE[32][U] and TABLE[1][V] != TABLE[V][1], "roots unexpectedly central") + require(regular.transpose(regular.multiply(regular.GENERATORS["x"], regular.GENERATORS["y"])) + != regular.multiply(regular.transpose(regular.GENERATORS["x"]), + regular.transpose(regular.GENERATORS["y"])), "transpose control fails") + return {"group_products": 4096, "contragredient_products": 4096, + "noncentral_root_controls": 2, "transpose_antihomomorphism_control": 1} + + +def call_checks(): + counts = Counter() + for r in (1, 2, 3, 4): + for u, v in product(range(1, 1 << r), repeat=2): + coupling = outer(u, v, r) + validate_call("x", coupling, r) + counts["idempotents" if (u & v).bit_count() & 1 else "nilpotents"] += 1 + for label, g in LABELS.items(): + first = append_factor(formal_identity(r), g, coupling) + second = append_factor(first, g, coupling) + require(second == formal_identity(r), "formal call not involutive") + require(formal_regular(first) == regular.replay([(label, u, v)], r), + "faithful single-call mismatch") + counts["formal_involutions"] += 1 + counts["faithful_columns"] += 64 * r + return dict(sorted(counts.items())) + + +def bounded_coefficients(): + r = 2 + factors = [(label, u, v) for label in LABELS for u, v in product(range(1, 4), repeat=2)] + levels = [0, 0, 0, 0] + h = hashlib.sha256() + + def visit(word, formal, coefficients): + levels[len(word)] += 1 + check_coefficients(formal, coefficients) + span_bounds(word, coefficients, r) + h.update(bytes(value for key in (*LABELS, *PAIRS) for value in coefficients[key])) + if len(word) == 3: + return + for label, u, v in factors: + coupling = outer(u, v, r) + visit(word + [(label, u, v)], append_factor(formal, LABELS[label], coupling), + update_coefficients(coefficients, label, coupling)) + + visit([], formal_identity(r), {key: zero(r) for key in (*LABELS, *PAIRS)}) + return {"registers": r, "expanded_factors": len(factors), "length_counts": levels, + "coefficient_digest": h.hexdigest(), "scope": "all words through length three; not an optimality census"} + + +def witness_checks(): + fixtures = [(p, q, p + q + extra, False) for p, q in product(range(4), repeat=2) + if p + q for extra in (0, 1)] + fixtures += [(1, 1, 8, False), (3, 3, 8, False), (1, 1, 4, True), (2, 2, 8, True)] + receipts = [] + for p, q, r, conjugated in fixtures: + word = direct_word(p, q) + expected = target(p, q, r) + P = tuple((1 << i) if i < p else 0 for i in range(r)) + Q = tuple((1 << i) if p <= i < p + q else 0 for i in range(r)) + if conjugated: + s1, s2 = list(identity(r)), list(identity(r)) + s1[0] ^= 1 << (r - 1) + s2[r - 1] ^= 1 << 1 + scalar = matrix_product(s1, s2) + inverse = matrix_product(s2, s1) + require(matrix_product(scalar, inverse) == identity(r), "conjugator inverse") + word = conjugate_word(word, scalar, inverse) + expected = conjugate_formal(expected, scalar, inverse) + P = matrix_product(matrix_product(scalar, P), inverse) + Q = matrix_product(matrix_product(scalar, Q), inverse) + actual = formal_word(word, r) + require(actual == expected, "full formal witness endpoint differs") + independent = regular.replay(word, r) + require(formal_regular(expected) == independent, "faithful dirty-column witness differs") + coefficients = coefficients_of(word, r) + check_coefficients(actual, coefficients) + for key in LABELS: + require(coefficients[key] == zero(r), "nonzero first coefficient") + require(coefficients["xy"] == coefficients["yx"] == P, "first root coefficient") + require(coefficients["yz"] == coefficients["zy"] == Q, "second root coefficient") + require(rank(list(P) + list(Q)) == p + q, "row target sum not direct") + require(rank(list(matrix_transpose(P)) + list(matrix_transpose(Q))) == p + q, + "column target sum not direct") + spans = span_bounds(word, coefficients, r) + require(spans == {"x": (p, p), "y": (p + q, p + q), "z": (q, q)}, "sharp label spans") + counts = {key: sum(label == key for label, _, _ in word) for key in LABELS} + require(counts == {"x": 2 * p, "y": 2 * (p + q), "z": 2 * q}, "attaining invoice") + receipts.append({"p": p, "q": q, "registers": r, "conjugated": conjugated, + "label_counts": counts, "label_span_ranks": spans, + "regular_columns": 64 * r, "formal_sha256": digest(actual), + "regular_sha256": digest(independent)}) + return receipts + + +def expect_failure(operation, message): + try: + operation() + except ValueError: + return + raise ValueError("negative control accepted: " + message) + + +def semantic_controls(): + controls = [] + word, r = direct_word(1, 1), 3 + expected = target(1, 1, r) + for i in range(len(word)): + require(formal_word(word[:i] + word[i + 1:], r) != expected, "omission invisible") + controls.append("omitted-call-" + str(i)) + wrong = list(word) + wrong[0] = ("z", 1, 1) + require(formal_word(wrong, r) != expected, "wrong label invisible") + controls.append("wrong-paid-label") + require(formal_word(word + [("x", 4, 1)], r) != expected, "dirty workspace unrestored") + controls.append("dirty-workspace-not-restored") + expect_failure(lambda: validate_call("x", (3, 0, 4), 3), "rank two") + controls.append("rank-two-coupling-rejected") + expect_failure(lambda: validate_call("u", (1, 0, 0), 3), "expanded address alphabet") + controls.append("root-label-rejected") + expect_failure(lambda: validate_call("x", (True, 0, 0), 3), "Boolean scalar encoding") + controls.append("boolean-coupling-rejected") + expect_failure(lambda: target(True, 1, 3), "Boolean role count") + controls.append("boolean-role-count-rejected") + # Higher-rank calls really change the bill; this is not a syntactic-only rejection. + rank_two = (1, 2) + four = formal_identity(2) + for label in "xyxy": + four = append_factor(four, LABELS[label], rank_two) + require(four == target(2, 0, 2), "rank-two positive counterexample") + controls.append("rank-two-four-call-two-root-counterexample") + # Nonzero formal kernel invisible to both proof representations. + lam = (1 << 0) ^ (1 << LABELS["x"]) ^ (1 << CENTRAL) ^ (1 << TABLE[CENTRAL][LABELS["x"]]) + require(lam.bit_count() == 4, "kernel perturbation vanished formally") + mutant = [list(row) for row in expected] + mutant[0][2] ^= lam + mutant = tuple(tuple(row) for row in mutant) + require(mutant != expected, "formal kernel mutant accepted") + for dual in (False, True): + require(regular.represented(mutant, dual) == regular.represented(expected, dual), + "kernel control not invisible to proof representation") + baseline_cols, mutant_cols = formal_regular(expected), formal_regular(mutant) + require(baseline_cols[:128] == mutant_cols[:128] and baseline_cols[128:] != mutant_cols[128:], + "dirty-only kernel control does not isolate dirty columns") + controls.append("dual-natural-common-kernel-rejected-by-formal-and-dirty-columns") + # P and Q overlap on one role. The union has rank one and the middle bill is two, not four. + overlap_word = [(label, 1, 1) for label in "xyzxyz"] + uv = TABLE[U][V] + require(formal_word(overlap_word, 1) == ((1 << uv,),), "overlap six-call witness") + coeff = coefficients_of(overlap_word, 1) + require(all(coeff[pair] == (1,) for pair in PAIRS), "overlap second coefficients") + require(span_bounds(overlap_word, coeff, 1)["y"] == (1, 1), "overlap span union") + require(formal_regular(((1 << uv,),)) == regular.replay(overlap_word, 1), "overlap faithful replay") + controls.append("overlapping-targets-invalidate-added-middle-bills") + triple_word = [(label, 1, 1) for label in "xzyxzy"] + triple_endpoint = formal_word(triple_word, 1) + require(coefficients_of(triple_word, 1) == coeff and triple_endpoint != ((1 << uv,),), + "degree-two alone incorrectly accepted full endpoint") + require(triple_endpoint == ((1 << TABLE[uv][CENTRAL],),), "class-three correction") + controls.append("degree-two-match-with-wrong-central-term") + return controls + + +def source_checks(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + root = HERE.parent.parent + checked = [] + for entry in manifest["files"]: + if entry["usage"] == "input": + data = (root / entry["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == entry["sha256"], "runtime source pin mismatch") + checked.append(entry["path"]) + selection = json.loads((HERE / "SELECTION.json").read_text()) + require(selection["seed"] == "5080ba3917adb12fda1e688c38733a49" + and selection["track"] == "bit-mechanisms" + and selection["base_commit"] == manifest["base_commit"], "selection provenance mismatch") + return checked + + +def result(): + sources = source_checks() + structure = group_checks() + calls = call_checks() + bounded = bounded_coefficients() + witnesses = witness_checks() + controls = semantic_controls() + return {"schema_version": 1, "result": "sharp-formal-tariff-no-new-kappa", + "theorem": {"x": "2p", "y": "2(p+q)", "z": "2q", "unit_minimum": "4(p+q)", + "prior_four_register_pair_minimum": 8, + "universal_evidence": "written proof in README.md, not finite extrapolation"}, + "source_inputs_checked": sources, "group_structure": structure, + "rank_one_calls": calls, "bounded_coefficient_checks": bounded, + "witnesses": witnesses, "semantic_controls": controls, + "summary": {"witnesses": len(witnesses), + "witness_regular_columns": sum(w["regular_columns"] for w in witnesses), + "coefficient_words": sum(bounded["length_counts"]), "controls": len(controls)}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print regenerated certificate without writing") + args = parser.parse_args() + actual = result() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + else: + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(json.dumps(actual, sort_keys=True) == json.dumps(expected, sort_keys=True), + "certificate mismatch (including scalar types)") + s = actual["summary"] + print("PASS_UT4_SHARED_MIDDLE pair_minimum=8" + f" witnesses={s['witnesses']} dirty_columns={s['witness_regular_columns']}" + f" coefficient_words={s['coefficient_words']} controls={s['controls']} no_new_kappa") + + +if __name__ == "__main__": + main()