diff --git a/research/common-image-full-guard-family/CASES.json b/research/common-image-full-guard-family/CASES.json new file mode 100644 index 0000000000..e0e93c7279 --- /dev/null +++ b/research/common-image-full-guard-family/CASES.json @@ -0,0 +1,579 @@ +{ + "example": { + "header_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64 + ], + "k": 6, + "m": 7, + "u": 64, + "v_rows": [ + 65, + 66, + 68, + 72, + 80, + 96 + ] + }, + "family_cases": [ + [ + 2, + 1 + ], + [ + 2, + 2 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 3 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 4, + 4 + ], + [ + 5, + 1 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 4 + ], + [ + 5, + 5 + ], + [ + 6, + 1 + ], + [ + 6, + 2 + ], + [ + 6, + 3 + ], + [ + 6, + 4 + ], + [ + 6, + 5 + ], + [ + 6, + 6 + ], + [ + 7, + 1 + ], + [ + 7, + 2 + ], + [ + 7, + 3 + ], + [ + 7, + 4 + ], + [ + 7, + 5 + ], + [ + 7, + 6 + ], + [ + 7, + 7 + ], + [ + 8, + 1 + ], + [ + 8, + 2 + ], + [ + 8, + 3 + ], + [ + 8, + 4 + ], + [ + 8, + 5 + ], + [ + 8, + 6 + ], + [ + 8, + 7 + ], + [ + 8, + 8 + ], + [ + 9, + 1 + ], + [ + 9, + 2 + ], + [ + 9, + 3 + ], + [ + 9, + 4 + ], + [ + 9, + 5 + ], + [ + 9, + 6 + ], + [ + 9, + 7 + ], + [ + 9, + 8 + ], + [ + 9, + 9 + ], + [ + 10, + 1 + ], + [ + 10, + 2 + ], + [ + 10, + 3 + ], + [ + 10, + 4 + ], + [ + 10, + 5 + ], + [ + 10, + 6 + ], + [ + 10, + 7 + ], + [ + 10, + 8 + ], + [ + 10, + 9 + ], + [ + 10, + 10 + ], + [ + 11, + 1 + ], + [ + 11, + 2 + ], + [ + 11, + 3 + ], + [ + 11, + 4 + ], + [ + 11, + 5 + ], + [ + 11, + 6 + ], + [ + 11, + 7 + ], + [ + 11, + 8 + ], + [ + 11, + 9 + ], + [ + 11, + 10 + ], + [ + 11, + 11 + ], + [ + 12, + 1 + ], + [ + 12, + 2 + ], + [ + 12, + 3 + ], + [ + 12, + 4 + ], + [ + 12, + 5 + ], + [ + 12, + 6 + ], + [ + 12, + 7 + ], + [ + 12, + 8 + ], + [ + 12, + 9 + ], + [ + 12, + 10 + ], + [ + 12, + 11 + ], + [ + 12, + 12 + ], + [ + 13, + 1 + ], + [ + 13, + 2 + ], + [ + 13, + 3 + ], + [ + 13, + 4 + ], + [ + 13, + 5 + ], + [ + 13, + 6 + ], + [ + 13, + 7 + ], + [ + 13, + 8 + ], + [ + 13, + 9 + ], + [ + 13, + 10 + ], + [ + 13, + 11 + ], + [ + 13, + 12 + ], + [ + 13, + 13 + ], + [ + 14, + 1 + ], + [ + 14, + 2 + ], + [ + 14, + 3 + ], + [ + 14, + 4 + ], + [ + 14, + 5 + ], + [ + 14, + 6 + ], + [ + 14, + 7 + ], + [ + 14, + 8 + ], + [ + 14, + 9 + ], + [ + 14, + 10 + ], + [ + 14, + 11 + ], + [ + 14, + 12 + ], + [ + 14, + 13 + ], + [ + 14, + 14 + ], + [ + 15, + 1 + ], + [ + 15, + 2 + ], + [ + 15, + 3 + ], + [ + 15, + 4 + ], + [ + 15, + 5 + ], + [ + 15, + 6 + ], + [ + 15, + 7 + ], + [ + 15, + 8 + ], + [ + 15, + 9 + ], + [ + 15, + 10 + ], + [ + 15, + 11 + ], + [ + 15, + 12 + ], + [ + 15, + 13 + ], + [ + 15, + 14 + ], + [ + 15, + 15 + ], + [ + 16, + 1 + ], + [ + 16, + 2 + ], + [ + 16, + 3 + ], + [ + 16, + 4 + ], + [ + 16, + 5 + ], + [ + 16, + 6 + ], + [ + 16, + 7 + ], + [ + 16, + 8 + ], + [ + 16, + 9 + ], + [ + 16, + 10 + ], + [ + 16, + 11 + ], + [ + 16, + 12 + ], + [ + 16, + 13 + ], + [ + 16, + 14 + ], + [ + 16, + 15 + ], + [ + 16, + 16 + ] + ], + "field": "F2", + "matrix_encoding": "Rows are m-bit integers, bit j is column j (zero-based). Header code=sum(row_i<<(m*i)); canonical records sorted ascending header code, each [header_code,passing_mask]. Mask bit i means ALL proper leading minors of G*(I-u*v_i)*G^-1 nonzero.", + "request_kind": "Corank-one complements P_i=I-u*v_i; each guard is ALL proper leading principal minors orders1..m-1. Not the rank-one U_i first-pivot request of4240.", + "schema_version": 1, + "scope": "Exact common-image family only. k1 marginal andk2transpose4807 are prior. Allsixshareline; exactlyonecoupledpair+4otherwiseorthogonal, arbitrarynonorthogonal/oddfields/restrictedheaders/physicalcaller remain open.", + "small_gl_dimensions": [ + 2, + 3, + 4 + ], + "small_gl_tuple": "u=e_m; ordered V=[e_m^T,e_m^T+e_1^T,...,e_m^T+e_(m-1)^T]. Count first k requests of this full independent tuple.", + "support_index": "j is number of ZERO entries of u among first m-1 coordinates; last u=1,Vlast=ones for passing tuples.", + "uniform_measure": "Uniform complete GL_m(F2) headers. Orbit pairs(u,V) with u!=0,rankV=k,Vu=ones_k have equal fibers." +} diff --git a/research/common-image-full-guard-family/NOTICE b/research/common-image-full-guard-family/NOTICE new file mode 100644 index 0000000000..210b6e6762 --- /dev/null +++ b/research/common-image-full-guard-family/NOTICE @@ -0,0 +1,25 @@ +Common-image full-guard family +Prepared for ToikY with substantial OpenAI Codex assistance; Apache-2.0. +Separate AI primary, independent oracle and static reviewer are not independent +human or formal proof-kernel acceptance. + +Eight exact predecessor prose/metadata objects retain their original headers, +credit and disclosures in inputs/; SOURCE-PINS.json records source repository, +head, path, Git blob and SHA256. No predecessor executable is copied or run. + +Nick Petalas: PR6694 released shared-direction question; PR4807 pair law, +PR4275 binary full-guard context, PR4227 marginal, PR4261 partial-sum lineage, +and PR4778 question. The k2 transpose-dual law is prior coverage. +unpaidmoon: PR6515 six-event orthogonal theorem and nonorthogonal motivation; +its substantial Cursor Grok assistance notice remains exact in the source. +Ryanson Jonathan: PR4607 five-event spectrum/theorem. PR4599, PR5146 and their +source attributions remain credited through the exact retained notices. +Cinna Davis BIT context, source527, commdata2338 and Jose Manuel/normalizer/ +recursive compiler lineage retain predecessor credit. No inherited physical +claim is independently admitted by the present probability count. + +Classical methods: rank-one determinant lemma, orbit-stabilizer and binary +finite-rank counting. Gzip payload equality follows the repository convention +credited to Maxime Fleury after Antoine Olivier's independent replay findings. +Douglas Colkitt and other repository contributors retain task/replay-framework +credit. Original upstream and predecessor packages remain unchanged. diff --git a/research/common-image-full-guard-family/ORACLE.json b/research/common-image-full-guard-family/ORACLE.json new file mode 100644 index 0000000000..0c8b70dc61 --- /dev/null +++ b/research/common-image-full-guard-family/ORACLE.json @@ -0,0 +1,3412 @@ +{ + "case_manifest_sha256": "3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273", + "example": { + "header_rows": [ + 1, + 2, + 4, + 8, + 16, + 32, + 64 + ], + "joint_probability": [ + 22, + 2667 + ], + "k": 6, + "m": 7, + "product_probability": [ + 150094635296999121, + 288338191148183248175104 + ], + "proper_minors": [ + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 1, + 1, + 1, + 1, + 1, + 1 + ] + ], + "ratio": [ + 49948348072913633542144, + 3151987341236981541 + ], + "ratio_gt_one": true, + "single_probability": [ + 729, + 8128 + ], + "u": 64, + "v_rows": [ + 65, + 66, + 68, + 72, + 80, + 96 + ] + }, + "family": [ + { + "header_fiber": 1, + "k": 1, + "m": 2, + "orbit_denominator": 6, + "orbit_numerator": 3, + "probability": [ + 1, + 2 + ], + "support_histogram": [ + 1, + 2 + ] + }, + { + "header_fiber": 1, + "k": 2, + "m": 2, + "orbit_denominator": 6, + "orbit_numerator": 2, + "probability": [ + 1, + 3 + ], + "support_histogram": [ + 0, + 2 + ] + }, + { + "header_fiber": 6, + "k": 1, + "m": 3, + "orbit_denominator": 28, + "orbit_numerator": 9, + "probability": [ + 9, + 28 + ], + "support_histogram": [ + 1, + 4, + 4 + ] + }, + { + "header_fiber": 2, + "k": 2, + "m": 3, + "orbit_denominator": 84, + "orbit_numerator": 16, + "probability": [ + 4, + 21 + ], + "support_histogram": [ + 0, + 4, + 12 + ] + }, + { + "header_fiber": 1, + "k": 3, + "m": 3, + "orbit_denominator": 168, + "orbit_numerator": 24, + "probability": [ + 1, + 7 + ], + "support_histogram": [ + 0, + 0, + 24 + ] + }, + { + "header_fiber": 168, + "k": 1, + "m": 4, + "orbit_denominator": 120, + "orbit_numerator": 27, + "probability": [ + 9, + 40 + ], + "support_histogram": [ + 1, + 6, + 12, + 8 + ] + }, + { + "header_fiber": 24, + "k": 2, + "m": 4, + "orbit_denominator": 840, + "orbit_numerator": 98, + "probability": [ + 7, + 60 + ], + "support_histogram": [ + 0, + 6, + 36, + 56 + ] + }, + { + "header_fiber": 4, + "k": 3, + "m": 4, + "orbit_denominator": 5040, + "orbit_numerator": 408, + "probability": [ + 17, + 210 + ], + "support_histogram": [ + 0, + 0, + 72, + 336 + ] + }, + { + "header_fiber": 1, + "k": 4, + "m": 4, + "orbit_denominator": 20160, + "orbit_numerator": 1344, + "probability": [ + 1, + 15 + ], + "support_histogram": [ + 0, + 0, + 0, + 1344 + ] + }, + { + "header_fiber": 20160, + "k": 1, + "m": 5, + "orbit_denominator": 496, + "orbit_numerator": 81, + "probability": [ + 81, + 496 + ], + "support_histogram": [ + 1, + 8, + 24, + 32, + 16 + ] + }, + { + "header_fiber": 1344, + "k": 2, + "m": 5, + "orbit_denominator": 7440, + "orbit_numerator": 544, + "probability": [ + 34, + 465 + ], + "support_histogram": [ + 0, + 8, + 72, + 224, + 240 + ] + }, + { + "header_fiber": 96, + "k": 3, + "m": 5, + "orbit_denominator": 104160, + "orbit_numerator": 4848, + "probability": [ + 101, + 2170 + ], + "support_histogram": [ + 0, + 0, + 144, + 1344, + 3360 + ] + }, + { + "header_fiber": 8, + "k": 4, + "m": 5, + "orbit_denominator": 1249920, + "orbit_numerator": 45696, + "probability": [ + 17, + 465 + ], + "support_histogram": [ + 0, + 0, + 0, + 5376, + 40320 + ] + }, + { + "header_fiber": 1, + "k": 5, + "m": 5, + "orbit_denominator": 9999360, + "orbit_numerator": 322560, + "probability": [ + 1, + 31 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 322560 + ] + }, + { + "header_fiber": 9999360, + "k": 1, + "m": 6, + "orbit_denominator": 2016, + "orbit_numerator": 243, + "probability": [ + 27, + 224 + ], + "support_histogram": [ + 1, + 10, + 40, + 80, + 80, + 32 + ] + }, + { + "header_fiber": 322560, + "k": 2, + "m": 6, + "orbit_denominator": 62496, + "orbit_numerator": 2882, + "probability": [ + 1441, + 31248 + ], + "support_histogram": [ + 0, + 10, + 120, + 560, + 1200, + 992 + ] + }, + { + "header_fiber": 10752, + "k": 3, + "m": 6, + "orbit_denominator": 1874880, + "orbit_numerator": 50160, + "probability": [ + 209, + 7812 + ], + "support_histogram": [ + 0, + 0, + 240, + 3360, + 16800, + 29760 + ] + }, + { + "header_fiber": 384, + "k": 4, + "m": 6, + "orbit_denominator": 52496640, + "orbit_numerator": 1048320, + "probability": [ + 13, + 651 + ], + "support_histogram": [ + 0, + 0, + 0, + 13440, + 201600, + 833280 + ] + }, + { + "header_fiber": 16, + "k": 5, + "m": 6, + "orbit_denominator": 1259919360, + "orbit_numerator": 21611520, + "probability": [ + 67, + 3906 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 1612800, + 19998720 + ] + }, + { + "header_fiber": 1, + "k": 6, + "m": 6, + "orbit_denominator": 20158709760, + "orbit_numerator": 319979520, + "probability": [ + 1, + 63 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 319979520 + ] + }, + { + "header_fiber": 20158709760, + "k": 1, + "m": 7, + "orbit_denominator": 8128, + "orbit_numerator": 729, + "probability": [ + 729, + 8128 + ], + "support_histogram": [ + 1, + 12, + 60, + 160, + 240, + 192, + 64 + ] + }, + { + "header_fiber": 319979520, + "k": 2, + "m": 7, + "orbit_denominator": 512064, + "orbit_numerator": 14896, + "probability": [ + 133, + 4572 + ], + "support_histogram": [ + 0, + 12, + 180, + 1120, + 3600, + 5952, + 4032 + ] + }, + { + "header_fiber": 5160960, + "k": 3, + "m": 7, + "orbit_denominator": 31747968, + "orbit_numerator": 486024, + "probability": [ + 2893, + 188976 + ], + "support_histogram": [ + 0, + 0, + 360, + 6720, + 50400, + 178560, + 249984 + ] + }, + { + "header_fiber": 86016, + "k": 4, + "m": 7, + "orbit_denominator": 1904878080, + "orbit_numerator": 20630400, + "probability": [ + 1535, + 141732 + ], + "support_histogram": [ + 0, + 0, + 0, + 26880, + 604800, + 4999680, + 14999040 + ] + }, + { + "header_fiber": 1536, + "k": 5, + "m": 7, + "orbit_denominator": 106673172480, + "orbit_numerator": 964776960, + "probability": [ + 997, + 110236 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 4838400, + 119992320, + 839946240 + ] + }, + { + "header_fiber": 32, + "k": 6, + "m": 7, + "orbit_denominator": 5120312279040, + "orbit_numerator": 42237296640, + "probability": [ + 22, + 2667 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 1919877120, + 40317419520 + ] + }, + { + "header_fiber": 1, + "k": 7, + "m": 7, + "orbit_denominator": 163849992929280, + "orbit_numerator": 1290157424640, + "probability": [ + 1, + 127 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1290157424640 + ] + }, + { + "header_fiber": 163849992929280, + "k": 1, + "m": 8, + "orbit_denominator": 32640, + "orbit_numerator": 2187, + "probability": [ + 729, + 10880 + ], + "support_histogram": [ + 1, + 14, + 84, + 280, + 560, + 672, + 448, + 128 + ] + }, + { + "header_fiber": 1290157424640, + "k": 2, + "m": 8, + "orbit_denominator": 4145280, + "orbit_numerator": 75938, + "probability": [ + 37969, + 2072640 + ], + "support_histogram": [ + 0, + 14, + 252, + 1960, + 8400, + 20832, + 28224, + 16256 + ] + }, + { + "header_fiber": 10239344640, + "k": 3, + "m": 8, + "orbit_denominator": 522305280, + "orbit_numerator": 4552968, + "probability": [ + 27101, + 3108960 + ], + "support_histogram": [ + 0, + 0, + 504, + 11760, + 117600, + 624960, + 1749888, + 2048256 + ] + }, + { + "header_fiber": 82575360, + "k": 4, + "m": 8, + "orbit_denominator": 64765854720, + "orbit_numerator": 377934144, + "probability": [ + 9071, + 1554480 + ], + "support_histogram": [ + 0, + 0, + 0, + 47040, + 1411200, + 17498880, + 104993280, + 253983744 + ] + }, + { + "header_fiber": 688128, + "k": 5, + "m": 8, + "orbit_denominator": 7771902566400, + "orbit_numerator": 36788935680, + "probability": [ + 6709, + 1417320 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 11289600, + 419973120, + 5879623680, + 30478049280 + ] + }, + { + "header_fiber": 6144, + "k": 6, + "m": 8, + "orbit_denominator": 870453087436800, + "orbit_numerator": 3702483025920, + "probability": [ + 551, + 129540 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 6719569920, + 282221936640, + 3413541519360 + ] + }, + { + "header_fiber": 64, + "k": 7, + "m": 8, + "orbit_denominator": 83563496393932800, + "orbit_numerator": 336731087831040, + "probability": [ + 87, + 21590 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 9031101972480, + 327699985858560 + ] + }, + { + "header_fiber": 1, + "k": 8, + "m": 8, + "orbit_denominator": 5348063769211699200, + "orbit_numerator": 20972799094947840, + "probability": [ + 1, + 255 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 20972799094947840 + ] + }, + { + "header_fiber": 5348063769211699200, + "k": 1, + "m": 9, + "orbit_denominator": 130816, + "orbit_numerator": 6561, + "probability": [ + 6561, + 130816 + ], + "support_histogram": [ + 1, + 16, + 112, + 448, + 1120, + 1792, + 1792, + 1024, + 256 + ] + }, + { + "header_fiber": 20972799094947840, + "k": 2, + "m": 9, + "orbit_denominator": 33358080, + "orbit_numerator": 384064, + "probability": [ + 353, + 30660 + ], + "support_histogram": [ + 0, + 16, + 336, + 3136, + 16800, + 55552, + 112896, + 130048, + 65280 + ] + }, + { + "header_fiber": 82570075176960, + "k": 3, + "m": 9, + "orbit_denominator": 8472952320, + "orbit_numerator": 41887968, + "probability": [ + 436333, + 88259920 + ], + "support_histogram": [ + 0, + 0, + 672, + 18816, + 235200, + 1666560, + 6999552, + 16386048, + 16581120 + ] + }, + { + "header_fiber": 327659028480, + "k": 4, + "m": 9, + "orbit_denominator": 2135183984640, + "orbit_numerator": 6679846656, + "probability": [ + 138059, + 44129960 + ], + "support_histogram": [ + 0, + 0, + 0, + 75264, + 2822400, + 46663680, + 419973120, + 2031869952, + 4178442240 + ] + }, + { + "header_fiber": 1321205760, + "k": 5, + "m": 9, + "orbit_denominator": 529525628190720, + "orbit_numerator": 1304739072000, + "probability": [ + 2275, + 923304 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 22579200, + 1119928320, + 23518494720, + 243824394240, + 1036253675520 + ] + }, + { + "header_fiber": 5505024, + "k": 6, + "m": 9, + "orbit_denominator": 127086150765772800, + "orbit_numerator": 277156020879360, + "probability": [ + 108271, + 49646205 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 17918853120, + 1128887746560, + 27308332154880, + 248700882124800 + ] + }, + { + "header_fiber": 24576, + "k": 7, + "m": 9, + "orbit_denominator": 28467297771533107200, + "orbit_numerator": 58366721890713600, + "probability": [ + 2262, + 1103249 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 36124407889920, + 2621599886868480, + 55708997595955200 + ] + }, + { + "header_fiber": 128, + "k": 8, + "m": 9, + "orbit_denominator": 5465721172134356582400, + "orbit_numerator": 10863909931182981120, + "probability": [ + 37, + 18615 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 167782392759582720, + 10696127538423398400 + ] + }, + { + "header_fiber": 1, + "k": 9, + "m": 9, + "orbit_denominator": 699612310033197642547200, + "orbit_numerator": 1369104324918194995200, + "probability": [ + 1, + 511 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1369104324918194995200 + ] + }, + { + "header_fiber": 699612310033197642547200, + "k": 1, + "m": 10, + "orbit_denominator": 523776, + "orbit_numerator": 19683, + "probability": [ + 6561, + 174592 + ], + "support_histogram": [ + 1, + 18, + 144, + 672, + 2016, + 4032, + 5376, + 4608, + 2304, + 512 + ] + }, + { + "header_fiber": 1369104324918194995200, + "k": 2, + "m": 10, + "orbit_denominator": 267649536, + "orbit_numerator": 1933442, + "probability": [ + 138103, + 19117824 + ], + "support_histogram": [ + 0, + 18, + 432, + 4704, + 30240, + 124992, + 338688, + 585216, + 587520, + 261632 + ] + }, + { + "header_fiber": 2684518284153323520, + "k": 3, + "m": 10, + "orbit_denominator": 136501263360, + "orbit_numerator": 381600480, + "probability": [ + 795001, + 284377632 + ], + "support_histogram": [ + 0, + 0, + 864, + 28224, + 423360, + 3749760, + 20998656, + 73737216, + 149230080, + 133432320 + ] + }, + { + "header_fiber": 5284484811325440, + "k": 4, + "m": 10, + "orbit_denominator": 69342641786880, + "orbit_numerator": 115903119360, + "probability": [ + 269492, + 161231961 + ], + "support_histogram": [ + 0, + 0, + 0, + 112896, + 5080320, + 104993280, + 1259919360, + 9143414784, + 37605980160, + 67783618560 + ] + }, + { + "header_fiber": 10485088911360, + "k": 5, + "m": 10, + "orbit_denominator": 34948691460587520, + "orbit_numerator": 44659552573440, + "probability": [ + 1357387, + 1062234096 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 40642560, + 2519838720, + 70555484160, + 1097209774080, + 9326283079680, + 34162943754240 + ] + }, + { + "header_fiber": 21139292160, + "k": 6, + "m": 10, + "orbit_denominator": 17334550964451409920, + "orbit_numerator": 19309442516582400, + "probability": [ + 10057645, + 9028989816 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 40317419520, + 3386663239680, + 122887494696960, + 2238307939123200, + 16944820102103040 + ] + }, + { + "header_fiber": 44040192, + "k": 7, + "m": 10, + "orbit_denominator": 8320584462936676761600, + "orbit_numerator": 8646800200087633920, + "probability": [ + 837766, + 806159805 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 108373223669760, + 11797199490908160, + 501380978363596800, + 8133513649009459200 + ] + }, + { + "header_fiber": 98304, + "k": 8, + "m": 10, + "orbit_denominator": 3727621839395631189196800, + "orbit_numerator": 3740834283369466429440, + "probability": [ + 89183, + 88868010 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 755020767418122240, + 96265147845810585600, + 3643814114756237721600 + ] + }, + { + "header_fiber": 256, + "k": 9, + "m": 10, + "orbit_denominator": 1431406786327922376651571200, + "orbit_numerator": 1411546558990659040051200, + "probability": [ + 1031, + 1045506 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12321938924263754956800, + 1399224620066395285094400 + ] + }, + { + "header_fiber": 1, + "k": 10, + "m": 10, + "orbit_denominator": 366440137299948128422802227200, + "orbit_numerator": 358201502736997192984166400, + "probability": [ + 1, + 1023 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 358201502736997192984166400 + ] + }, + { + "header_fiber": 366440137299948128422802227200, + "k": 1, + "m": 11, + "orbit_denominator": 2096128, + "orbit_numerator": 59049, + "probability": [ + 59049, + 2096128 + ], + "support_histogram": [ + 1, + 20, + 180, + 960, + 3360, + 8064, + 13440, + 15360, + 11520, + 5120, + 1024 + ] + }, + { + "header_fiber": 358201502736997192984166400, + "k": 2, + "m": 11, + "orbit_denominator": 2144338944, + "orbit_numerator": 9706576, + "probability": [ + 55151, + 12183744 + ], + "support_histogram": [ + 0, + 20, + 540, + 6720, + 50400, + 249984, + 846720, + 1950720, + 2937600, + 2616320, + 1047552 + ] + }, + { + "header_fiber": 350490707179057918771200, + "k": 3, + "m": 11, + "orbit_denominator": 2191514400768, + "orbit_numerator": 3457605624, + "probability": [ + 13096991, + 8301190912 + ], + "support_histogram": [ + 0, + 0, + 1080, + 40320, + 705600, + 7499520, + 52496640, + 245790720, + 746150400, + 1334323200, + 1070598144 + ] + }, + { + "header_fiber": 343618340371625410560, + "k": 4, + "m": 11, + "orbit_denominator": 2235344688783360, + "orbit_numerator": 1991722656000, + "probability": [ + 92275, + 103561824 + ], + "support_histogram": [ + 0, + 0, + 0, + 161280, + 8467200, + 209986560, + 3149798400, + 30478049280, + 188029900800, + 677836185600, + 1092010106880 + ] + }, + { + "header_fiber": 338207027924828160, + "k": 5, + "m": 11, + "orbit_denominator": 2271110203803893760, + "orbit_numerator": 1501581983569920, + "probability": [ + 2327601041, + 3520446124448 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 67737600, + 5039677440, + 176388710400, + 3657365913600, + 46631415398400, + 341629437542400, + 1109482268590080 + ] + }, + { + "header_fiber": 335522845163520, + "k": 6, + "m": 11, + "orbit_denominator": 2289279085434324910080, + "orbit_numerator": 1299416039730708480, + "probability": [ + 84602813, + 149051146398 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 80634839040, + 8466658099200, + 409624982323200, + 11191539695616000, + 169448201021030400, + 1118358126738800640 + ] + }, + { + "header_fiber": 338228674560, + "k": 7, + "m": 11, + "orbit_denominator": 2270964852750850310799360, + "orbit_numerator": 1193292898038165012480, + "probability": [ + 462460191, + 880111531112 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 270933059174400, + 39323998303027200, + 2506904891817984000, + 81335136490094592000, + 1109411261724890234880 + ] + }, + { + "header_fiber": 352321536, + "k": 8, + "m": 11, + "orbit_denominator": 2180126258640816298367385600, + "orbit_numerator": 1101956794878577449369600, + "probability": [ + 5254219, + 10395018084 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2516735891393740800, + 481325739229052928000, + 36438141147562377216000, + 1065034811255894625484800 + ] + }, + { + "header_fiber": 393216, + "k": 9, + "m": 11, + "orbit_denominator": 1953393127742171403337177497600, + "orbit_numerator": 968325046780566856060108800, + "probability": [ + 707269, + 1426767188 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 61609694621318774784000, + 13992246200663952850944000, + 954271190885281584434380800 + ] + }, + { + "header_fiber": 512, + "k": 10, + "m": 11, + "orbit_denominator": 1500205922105987637762952318156800, + "orbit_numerator": 736462289627266228775446118400, + "probability": [ + 1028, + 2094081 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3582015027369971929841664000, + 732880274599896256845604454400 + ] + }, + { + "header_fiber": 1, + "k": 11, + "m": 11, + "orbit_denominator": 768105432118265670534631586896281600, + "orbit_numerator": 375234700595146883504949480652800, + "probability": [ + 1, + 2047 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 375234700595146883504949480652800 + ] + }, + { + "header_fiber": 768105432118265670534631586896281600, + "k": 1, + "m": 12, + "orbit_denominator": 8386560, + "orbit_numerator": 177147, + "probability": [ + 19683, + 931840 + ], + "support_histogram": [ + 1, + 22, + 220, + 1320, + 5280, + 14784, + 29568, + 42240, + 42240, + 28160, + 11264, + 2048 + ] + }, + { + "header_fiber": 375234700595146883504949480652800, + "k": 2, + "m": 12, + "orbit_denominator": 17167288320, + "orbit_numerator": 48650978, + "probability": [ + 24325489, + 8583644160 + ], + "support_histogram": [ + 0, + 22, + 660, + 9240, + 79200, + 458304, + 1862784, + 5364480, + 10771200, + 14389760, + 11523072, + 4192256 + ] + }, + { + "header_fiber": 183399169401342562807893196800, + "k": 3, + "m": 12, + "orbit_denominator": 35124271902720, + "orbit_numerator": 31234929528, + "probability": [ + 118314127, + 133046484480 + ], + "support_histogram": [ + 0, + 0, + 1320, + 55440, + 1108800, + 13749120, + 115492608, + 675924480, + 2735884800, + 7338777600, + 11776579584, + 8577355776 + ] + }, + { + "header_fiber": 89725621037838827205427200, + "k": 4, + "m": 12, + "orbit_denominator": 71794011769159680, + "orbit_numerator": 34052911066944, + "probability": [ + 767787497, + 1618732227840 + ], + "support_histogram": [ + 0, + 0, + 0, + 221760, + 13305600, + 384975360, + 6929556480, + 83814635520, + 689442969600, + 3728099020800, + 12012111175680, + 17532115206144 + ] + }, + { + "header_fiber": 43983147567568052551680, + "k": 5, + "m": 12, + "orbit_denominator": 146459784009085747200, + "orbit_numerator": 50030218895247360, + "probability": [ + 7050163873, + 20638835904960 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 106444800, + 9239408640, + 388055162880, + 10057756262400, + 170981856460800, + 1878961906483200, + 12204304954490880, + 35765515020533760 + ] + }, + { + "header_fiber": 21645249787189002240, + "k": 6, + "m": 12, + "orbit_denominator": 297606281106462238310400, + "orbit_numerator": 85951611910197411840, + "probability": [ + 96140293, + 332884450080 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 147830538240, + 18626647818240, + 1126468701388800, + 41035645550592000, + 931965105615667200, + 12301939394126807040, + 72675526521724600320 + ] + }, + { + "header_fiber": 10736731045232640, + "k": 7, + "m": 12, + "orbit_denominator": 599974262710627872433766400, + "orbit_numerator": 159174029319117503201280, + "probability": [ + 1869328247, + 7046054193360 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 596052730183680, + 108140995333324800, + 9191984603332608000, + 447343250695520256000, + 12203523878973792583680, + 146513861467796794245120 + ] + }, + { + "header_fiber": 5411658792960, + "k": 8, + "m": 12, + "orbit_denominator": 1190348937217885698908592537600, + "orbit_numerator": 302601065634302814930862080, + "probability": [ + 327915073, + 1289927244060 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 6921023701332787200, + 1764861043839860736000, + 200409776311593074688000, + 11715382923814840880332800, + 290683501152108839782318080 + ] + }, + { + "header_fiber": 2818572288, + "k": 9, + "m": 12, + "orbit_denominator": 2285469959458340541904497672192000, + "orbit_numerator": 568686488568104333053683302400, + "probability": [ + 5394431, + 21679449480 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 225902213611502174208000, + 76957354103651740680192000, + 10496983099738097428778188800, + 558112322212048972382050713600 + ] + }, + { + "header_fiber": 1572864, + "k": 10, + "m": 12, + "orbit_denominator": 4095562167349346251092859828568064000, + "orbit_numerator": 1008218665507241152179550656921600, + "probability": [ + 2187, + 8883980 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 19701082650534845614129152000, + 8061683020598858825301648998400, + 1000137281403991758508634878771200 + ] + }, + { + "header_fiber": 1024, + "k": 11, + "m": 12, + "orbit_denominator": 6290783489048595841678632696680546304000, + "orbit_numerator": 1540338445943077956787817618079744000, + "probability": [ + 821, + 3352986 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4127581706546615718554444287180800, + 1536210864236531341069263173792563200 + ] + }, + { + "header_fiber": 1, + "k": 12, + "m": 12, + "orbit_denominator": 6441762292785762141878919881400879415296000, + "orbit_numerator": 1573079924978208093254925489963584716800, + "probability": [ + 1, + 4095 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1573079924978208093254925489963584716800 + ] + }, + { + "header_fiber": 6441762292785762141878919881400879415296000, + "k": 1, + "m": 13, + "orbit_denominator": 33550336, + "orbit_numerator": 531441, + "probability": [ + 531441, + 33550336 + ], + "support_histogram": [ + 1, + 24, + 264, + 1760, + 7920, + 25344, + 59136, + 101376, + 126720, + 112640, + 67584, + 24576, + 4096 + ] + }, + { + "header_fiber": 1573079924978208093254925489963584716800, + "k": 2, + "m": 13, + "orbit_denominator": 137388625920, + "orbit_numerator": 243609184, + "probability": [ + 83657, + 47180160 + ], + "support_histogram": [ + 0, + 24, + 792, + 12320, + 118800, + 785664, + 3725568, + 12874752, + 32313600, + 57559040, + 69138432, + 50307072, + 16773120 + ] + }, + { + "header_fiber": 384240333409430408709068268188467200, + "k": 3, + "m": 13, + "orbit_denominator": 562469034516480, + "orbit_numerator": 281698177488, + "probability": [ + 64491341, + 128770383360 + ], + "support_histogram": [ + 0, + 0, + 1584, + 73920, + 1663200, + 23569920, + 230985216, + 1622218752, + 8207654400, + 29355110400, + 70659477504, + 102928269312, + 68669153280 + ] + }, + { + "header_fiber": 93900374733487392157641316761600, + "k": 4, + "m": 13, + "orbit_denominator": 2301623289241436160, + "orbit_numerator": 580648644191616, + "probability": [ + 48728879, + 193155575040 + ], + "support_histogram": [ + 0, + 0, + 0, + 295680, + 19958400, + 659957760, + 13859112960, + 201155125248, + 2068328908800, + 14912396083200, + 72072667054080, + 210385382473728, + 280994175221760 + ] + }, + { + "header_fiber": 22969758985686739764589363200, + "k": 5, + "m": 13, + "orbit_denominator": 9409036006418991022080, + "orbit_numerator": 1659169922199229440, + "probability": [ + 11990107131, + 67995054760192 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 159667200, + 15838986240, + 776110325760, + 24138615029760, + 512945569382400, + 7515847625932800, + 73225829726945280, + 429186180246405120, + 1148704188306554880 + ] + }, + { + "header_fiber": 5629842888648710726615040, + "k": 6, + "m": 13, + "orbit_denominator": 38388866906189483370086400, + "orbit_numerator": 5636484751306917150720, + "probability": [ + 22241341183, + 151480918366960 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 253423779840, + 37253295636480, + 2703524883333120, + 123106936651776000, + 3727860422462668800, + 73811636364760842240, + 872106318260695203840, + 4686713088290743910400 + ] + }, + { + "header_fiber": 1385295986380096143360, + "k": 7, + "m": 13, + "orbit_denominator": 156012355106754060416031129600, + "orbit_numerator": 20880006681388073877504000, + "probability": [ + 4597749055, + 34353708272507 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 1192105460367360, + 259538388799979520, + 27575953809997824000, + 1789373002782081024000, + 73221143273842755502080, + 1758166337613561530941440, + 19046801990813583251865600 + ] + }, + { + "header_fiber": 343575393447444480, + "k": 8, + "m": 13, + "orbit_denominator": 629041815790432371597437514547200, + "orbit_numerator": 80356006888627397569271562240, + "probability": [ + 174156332263, + 1363328265302640 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 16610456883198689280, + 5294583131519582208000, + 801639105246372298752000, + 70292297542889045281996800, + 3488202013825306077387816960, + 76796705626960367671522099200 + ] + }, + { + "header_fiber": 86586540687360, + "k": 9, + "m": 13, + "orbit_denominator": 2496037925056435650498632057723289600, + "orbit_numerator": 311489966200044810615226210713600, + "probability": [ + 20683062013, + 165737945977968 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 677706640834506522624000, + 307829416414606962720768000, + 62981898598428584572669132800, + 6697347866544587668584608563200, + 304729327927778738920599689625600 + ] + }, + { + "header_fiber": 22548578304, + "k": 10, + "m": 13, + "orbit_denominator": 9584785632216712897914747101657432064000, + "orbit_numerator": 1182210715521972453849540693118156800, + "probability": [ + 37504624, + 304069127895 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 78804330602139382456516608000, + 48370098123593152951809893990400, + 12001647376847901102103618545254400, + 1170160619242670357455102808162304000 + ] + }, + { + "header_fiber": 6291456, + "k": 11, + "m": 13, + "orbit_denominator": 34351871705864699026126453612340236517376000, + "orbit_numerator": 4212314955226808216906230949204931379200, + "probability": [ + 1870969, + 15257949070 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 24765490239279694311326665723084800, + 18434530370838376092831158085510758400, + 4193855659365730561119088464453697536000 + ] + }, + { + "header_fiber": 2048, + "k": 12, + "m": 13, + "orbit_denominator": 105528949880416355408260465497109206581379072000, + "orbit_numerator": 12902401544671262780876898868681321847193600, + "probability": [ + 1367, + 11180715 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 18876959099738497119059105879563016601600, + 12883524585571524283757839762801758830592000 + ] + }, + { + "header_fiber": 1, + "k": 13, + "m": 13, + "orbit_denominator": 216123289355092695876117433338079655078664339456000, + "orbit_numerator": 26385458351250481733136055834218002085052416000, + "probability": [ + 1, + 8191 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 26385458351250481733136055834218002085052416000 + ] + }, + { + "header_fiber": 216123289355092695876117433338079655078664339456000, + "k": 1, + "m": 14, + "orbit_denominator": 134209536, + "orbit_numerator": 1594323, + "probability": [ + 531441, + 44736512 + ], + "support_histogram": [ + 1, + 26, + 312, + 2288, + 11440, + 41184, + 109824, + 219648, + 329472, + 366080, + 292864, + 159744, + 53248, + 8192 + ] + }, + { + "header_fiber": 26385458351250481733136055834218002085052416000, + "k": 2, + "m": 14, + "orbit_denominator": 1099310309376, + "orbit_numerator": 1219108802, + "probability": [ + 609554401, + 549655154688 + ], + "support_histogram": [ + 0, + 26, + 936, + 16016, + 171600, + 1276704, + 6918912, + 27895296, + 84015360, + 187066880, + 299599872, + 326995968, + 218050560, + 67100672 + ] + }, + { + "header_fiber": 3221667686355370174986087403445421500006400, + "k": 3, + "m": 14, + "orbit_denominator": 9003351433789440, + "orbit_numerator": 2538206907600, + "probability": [ + 116218265, + 412241366016 + ], + "support_histogram": [ + 0, + 0, + 1872, + 96096, + 2402400, + 38301120, + 428972544, + 3514807296, + 21339901440, + 95404108800, + 306191069184, + 669033750528, + 892698992640, + 549554503680 + ] + }, + { + "header_fiber": 393462101411256738518085906624990412800, + "k": 4, + "m": 14, + "orbit_denominator": 73719441539867934720, + "orbit_numerator": 9886802049196800, + "probability": [ + 28293275095, + 210964519058688 + ], + "support_histogram": [ + 0, + 0, + 0, + 384384, + 28828800, + 1072431360, + 25738352640, + 435836104704, + 5377655162880, + 48465287270400, + 312314890567680, + 1367504986079232, + 3652924277882880, + 4499752276131840 + ] + }, + { + "header_fiber": 48076991863545544784712354181939200, + "k": 5, + "m": 14, + "orbit_denominator": 603319909562279177748480, + "orbit_numerator": 54891963107180559360, + "probability": [ + 1190041796467, + 13079800181638656 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 230630400, + 25738352640, + 1441347747840, + 52300332564480, + 1333658480394240, + 24426504784281600, + 317311928816762880, + 2789710171601633280, + 14933154447985213440, + 36825972627862978560 + ] + }, + { + "header_fiber": 5880258300335805379734876979200, + "k": 6, + "m": 14, + "orbit_denominator": 4932743580581194557271572480, + "orbit_numerator": 368017405397771250401280, + "probability": [ + 127664335671, + 1711156654587136 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 411813642240, + 69184691896320, + 5857637247221760, + 320078035294617600, + 12115546373003673600, + 319850424247296983040, + 5668691068694518824960, + 60927270147779670835200, + 301089152205407712706560 + ] + }, + { + "header_fiber": 720619889747034973006725120, + "k": 7, + "m": 14, + "orbit_denominator": 40251187617542547587336031436800, + "orbit_numerator": 2716247168416331020149719040, + "probability": [ + 1568926303, + 23249411067760 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 2213910140682240, + 562333175733288960, + 71697479905994342400, + 5815462259041763328000, + 317291620853318607175680, + 11428081194488149951119360, + 247608425880576582274252800, + 2456887481996126935685529600 + ] + }, + { + "header_fiber": 88658943128326153175040, + "k": 8, + "m": 14, + "orbit_denominator": 327161652955385826789867263518310400, + "orbit_numerator": 20990919158989885704255496519680, + "probability": [ + 1166508134369, + 18181039454988320 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 35989323246930493440, + 13765916141950913740800, + 2605327092050709970944000, + 304599956019185862888652800, + 22673313089864489503020810240, + 998357173150484779729787289600, + 19969581453664519733251984588800 + ] + }, + { + "header_fiber": 10994412590318223360, + "k": 9, + "m": 14, + "orbit_denominator": 2638231569432231307233489613011655065600, + "orbit_numerator": 165039992790312584358933093679104000, + "probability": [ + 842978729015, + 13475358654873696 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1762037266169716958822400, + 1000445603347472628842496000, + 272921560593190533148232908800, + 43532761132539819845799955660800, + 3961481263061123605967795965132800, + 161034704842350687128944003724083200 + ] + }, + { + "header_fiber": 1385384650997760, + "k": 10, + "m": 14, + "orbit_denominator": 20937005735014187654204973568860494600601600, + "orbit_numerator": 1293261726246871889086662074407531315200, + "probability": [ + 25247767601, + 408743755676208 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 256114074456952992983678976000, + 209603758535570329457842873958400, + 78010707949511357163673520544153600, + 15212088050154714646916336506109952000, + 1277971417628895053055299613554324275200 + ] + }, + { + "header_fiber": 180388626432, + "k": 11, + "m": 14, + "orbit_denominator": 160796204044908961184294197008848598532620288000, + "orbit_numerator": 9869460542726203324415861267078215788134400, + "probability": [ + 1011619223, + 16481603051460 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 107317124370212008682415551466700800, + 119824447410449444603402527555819929600, + 54520123571754497294548150037898067968000, + 9814820487389914007464701032097210433536000 + ] + }, + { + "header_fiber": 25165824, + "k": 12, + "m": 14, + "orbit_denominator": 1152587190593907433769020804159426754281822224384000, + "orbit_numerator": 70520241773457481721427102799177444411991654400, + "probability": [ + 287368, + 4696760355 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 122700234148300231273884188217159607910400, + 167485819612429815688851916916422864797696000, + 70352633253610903605506976998072804387586048000 + ] + }, + { + "header_fiber": 4096, + "k": 13, + "m": 14, + "orbit_denominator": 7081495699008967273076863820755517978307515746615296000, + "orbit_numerator": 432589589668751648014765635402004144184434360320000, + "probability": [ + 5465, + 89462102 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 343010958566256262530768725844834027105681408000, + 432246578710185391752234866676159310157328678912000 + ] + }, + { + "header_fiber": 1, + "k": 14, + "m": 14, + "orbit_denominator": 29005806383140729950522834209814601639147584498136252416000, + "orbit_numerator": 1770481986396919364617154013905548534404418268823552000, + "probability": [ + 1, + 16383 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1770481986396919364617154013905548534404418268823552000 + ] + }, + { + "header_fiber": 29005806383140729950522834209814601639147584498136252416000, + "k": 1, + "m": 15, + "orbit_denominator": 536854528, + "orbit_numerator": 4782969, + "probability": [ + 4782969, + 536854528 + ], + "support_histogram": [ + 1, + 28, + 364, + 2912, + 16016, + 64064, + 192192, + 439296, + 768768, + 1025024, + 1025024, + 745472, + 372736, + 114688, + 16384 + ] + }, + { + "header_fiber": 1770481986396919364617154013905548534404418268823552000, + "k": 2, + "m": 15, + "orbit_denominator": 8795287732224, + "orbit_numerator": 6098732656, + "probability": [ + 8864437, + 12783848448 + ], + "support_histogram": [ + 0, + 28, + 1092, + 20384, + 240240, + 1985984, + 12108096, + 55790592, + 196035840, + 523787264, + 1048599552, + 1525981184, + 1526353920, + 939409408, + 268419072 + ] + }, + { + "header_fiber": 108074837406721973178925284696956936540374695936000, + "k": 3, + "m": 15, + "orbit_denominator": 144084403629293568, + "orbit_numerator": 22858491474024, + "probability": [ + 952437144751, + 6003516817887232 + ], + "support_histogram": [ + 0, + 0, + 2184, + 122304, + 3363360, + 59579520, + 750701952, + 7029614592, + 49793103360, + 267131504640, + 1071668742144, + 3122157502464, + 6248892948480, + 7693763051520, + 4397241237504 + ] + }, + { + "header_fiber": 6597975421655798118371507002256223232013107200, + "k": 4, + "m": 15, + "orbit_denominator": 2360102531447828643840, + "orbit_numerator": 168217774423171200, + "probability": [ + 320928293695, + 4502637613415424 + ], + "support_histogram": [ + 0, + 0, + 0, + 489216, + 40360320, + 1668226560, + 45042117120, + 871672209408, + 12547862046720, + 135702804357120, + 1093102116986880, + 6381689935036416, + 25570469945180160, + 62996531865845760, + 72026811470315520 + ] + }, + { + "header_fiber": 402905191845126900242519968383990182707200, + "k": 5, + "m": 15, + "orbit_denominator": 38649039054989641871523840, + "orbit_numerator": 1813807615028765690880, + "probability": [ + 61793005374203, + 1316699884951624704 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 322882560, + 40037437440, + 2522358558720, + 104600665128960, + 3111869787586560, + 68394213395988480, + 1110591750858670080, + 13018647467474288640, + 104532081135896494080, + 515563616790081699840, + 1179511064637886955520 + ] + }, + { + "header_fiber": 24615419834135318929772725341152870400, + "k": 6, + "m": 15, + "orbit_denominator": 632607471252070458153102213120, + "orbit_numerator": 23975584178257454390968320, + "probability": [ + 130993874092303, + 3456337197998014848 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 640598999040, + 121073210818560, + 11715274494443520, + 746848749020774400, + 33923529844410286080, + 1119476484865539440640, + 26453891653907754516480, + 426490891034457695846400, + 4215248130875707977891840, + 19306237105992933687951360 + ] + }, + { + "header_fiber": 1505346124885966177212128506675200, + "k": 7, + "m": 15, + "orbit_denominator": 10344397369913856131719527388938240, + "orbit_numerator": 351879730904270515280931717120, + "probability": [ + 272469232039383, + 8009924300122383616 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 3874342746193920, + 1124666351466577920, + 167294119780653465600, + 16283294325316937318400, + 1110520672986615125114880, + 53331045574278033105223680, + 1733258981164036075919769600, + 34396424747945777099597414400, + 315695589157196451665380638720 + ] + }, + { + "header_fiber": 92239345887620476544860815360, + "k": 8, + "m": 15, + "orbit_denominator": 168820565076994132069662686987472076800, + "orbit_numerator": 5438821537830176503057216438272000, + "probability": [ + 60449278254145, + 1876340534871188288 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 71978646493860986880, + 32120470997885465395200, + 7294915857741987918643200, + 1066099846067150520110284800, + 105808794419367617680763781120, + 6988500212053393458108511027200, + 279574140351303276265527784243200, + 5152152015045446091179012023910400 + ] + }, + { + "header_fiber": 5674172360212873803202560, + "k": 9, + "m": 15, + "orbit_denominator": 2744347105891616610924436639668346080460800, + "orbit_numerator": 86035803504129215514906475870185062400, + "probability": [ + 439447136790909, + 14017367525214171328 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4111420287729339570585600, + 2801247689372923360758988800, + 955225462076166866018815180800, + 203152885285185825947066459750400, + 27730368841427865241774571755929600, + 2254485867792909619805216052137164800, + 83753383156578771658206019460687462400 + ] + }, + { + "header_fiber": 351821202890183147520, + "k": 10, + "m": 15, + "orbit_denominator": 44260830123819992700989314124571085585671782400, + "orbit_numerator": 1368773012796758748384825009433170935808000, + "probability": [ + 1113414188335, + 36003512479145988 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 717119408479468380354301132800, + 733613154874496153102450058854400, + 364049970431053000097143095872716800, + 106484616351083002528414355542769664000, + 17891599846804530742774194589760539852800, + 1350774563549302429303546681861967393587200 + ] + }, + { + "header_fiber": 22166154415964160, + "k": 11, + "m": 15, + "orbit_denominator": 702507895725270924150102393785192270415782530252800, + "orbit_numerator": 21577283559899353752884610765613022394187776000, + "probability": [ + 4423341019465, + 144014049916583952 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 375609935295742030388454430133452800, + 559180754582097408149211795260493004800, + 381640865002281481061837050265286475776000, + 137407486823458796104505814449360946069504000, + 21439493872654528157905892934513146471016038400 + ] + }, + { + "header_fiber": 1443109011456, + "k": 12, + "m": 15, + "orbit_denominator": 10790521278340161394945572768540553273586419664683008000, + "orbit_numerator": 330296735722862484856689181060306242363030975283200, + "probability": [ + 8075699399, + 263826422661060 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 572601092692067745944792878346744836915200, + 1172400737287008709821963418414960053583872000, + 984936865550552650477097677973019261426204672000, + 329310625883973552505434515474121929794806349824000 + ] + }, + { + "header_fiber": 100663296, + "k": 13, + "m": 15, + "orbit_denominator": 154692913046284553757939731209797371730134912312895602688000, + "orbit_numerator": 4727050985851297407996278217351559129718736172351488000, + "probability": [ + 179153643, + 5862809392468 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2401076709963793837715381080913838189739769856000, + 6051452101942595484531288133466230342202601504768000, + 4720997132672644848717909213837011985538343831076864000 + ] + }, + { + "header_fiber": 8192, + "k": 14, + "m": 15, + "orbit_denominator": 1900866515512744596577563417105990103819897802500861165830144000, + "orbit_numerator": 58036399514091016772150308575823880957776830852036034560000, + "probability": [ + 16390, + 536821761 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 24786747809556871104640156194677679481661855763529728000, + 58011612766281459901045668419629203278295168996272504832000 + ] + }, + { + "header_fiber": 1, + "k": 15, + "m": 15, + "orbit_denominator": 15571898495080403735163399512932270930492602798087054670480539648000, + "orbit_numerator": 475231131781377719509366115693602433255794024417464359583744000, + "probability": [ + 1, + 32767 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 475231131781377719509366115693602433255794024417464359583744000 + ] + }, + { + "header_fiber": 15571898495080403735163399512932270930492602798087054670480539648000, + "k": 1, + "m": 16, + "orbit_denominator": 2147450880, + "orbit_numerator": 14348907, + "probability": [ + 4782969, + 715816960 + ], + "support_histogram": [ + 1, + 30, + 420, + 3640, + 21840, + 96096, + 320320, + 823680, + 1647360, + 2562560, + 3075072, + 2795520, + 1863680, + 860160, + 245760, + 32768 + ] + }, + { + "header_fiber": 475231131781377719509366115693602433255794024417464359583744000, + "k": 2, + "m": 16, + "orbit_denominator": 70365522984960, + "orbit_numerator": 30503229218, + "probability": [ + 2178802087, + 5026108784640 + ], + "support_histogram": [ + 0, + 30, + 1260, + 25480, + 327600, + 2978976, + 20180160, + 104607360, + 420076800, + 1309468160, + 3145798656, + 5722429440, + 7631769600, + 7045570560, + 4026286080, + 1073709056 + ] + }, + { + "header_fiber": 14503788432563563434943725681914253593840994458202537984000, + "k": 3, + "m": 16, + "orbit_denominator": 2305596726125199360, + "orbit_numerator": 205799608058088, + "probability": [ + 8574983669087, + 96066530255216640 + ], + "support_histogram": [ + 0, + 0, + 2520, + 152880, + 4586400, + 89369280, + 1251169920, + 13180527360, + 106699507200, + 667828761600, + 3215006226432, + 11708090634240, + 31244464742400, + 57703222886400, + 65958618562560, + 35181150928896 + ] + }, + { + "header_fiber": 442674534017933202140877966118735612069374754553856000, + "k": 4, + "m": 16, + "orbit_denominator": 75540571134766031831040, + "orbit_numerator": 2860982240716455744, + "probability": [ + 2128707024342601, + 56205782094319964160 + ], + "support_histogram": [ + 0, + 0, + 0, + 611520, + 55036800, + 2502339840, + 75070195200, + 1634385392640, + 26888275814400, + 339257010892800, + 3279306350960640, + 23931337256386560, + 127852349725900800, + 472473988993843200, + 1080402172054732800, + 1152675229034348544 + ] + }, + { + "header_fiber": 13512653663551074546424846340620745179162843545600, + "k": 5, + "m": 16, + "orbit_denominator": 2474709110374935202784870400, + "orbit_numerator": 59896023561810828887040, + "probability": [ + 4761270696750581, + 196720237330119874560 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 440294400, + 60056156160, + 4203930931200, + 196126247116800, + 6668292401971200, + 170985533489971200, + 3331775252576010240, + 48819928003028582400, + 522660405679482470400, + 3866727125925612748800, + 17692665969568304332800, + 37761640503165258301440 + ] + }, + { + "header_fiber": 412574916449409945848340447625205947092172800, + "k": 6, + "m": 16, + "orbit_denominator": 81051672782999877761610075340800, + "orbit_numerator": 1560212268740843070978293760, + "probability": [ + 125025010313868667, + 6494940738947667471360 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 960898498560, + 201788684697600, + 21966139677081600, + 1600390176473088000, + 84808824611025715200, + 3358429454596618321920, + 99202093702154079436800, + 2132454455172288479232000, + 31614360981567809834188800, + 289593556589894005319270400, + 1236769249759668539888762880 + ] + }, + { + "header_fiber": 12603094955077283292043635374670269644800, + "k": 7, + "m": 16, + "orbit_denominator": 2653307560224283998404067426356428800, + "orbit_numerator": 45489154842057630527344575774720, + "probability": [ + 246563692027932061, + 14381654493384120829440 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 6457237910323200, + 2108749408999833600, + 358487399529971712000, + 40708235813292343296000, + 3331562018959845375344640, + 199991420903542624144588800, + 8666294905820180379598848000, + 257973185609593328246980608000, + 4735433837357946774980709580800, + 40486878160132509321798541639680 + ] + }, + { + "header_fiber": 385368607970807341366304897708851200, + "k": 8, + "m": 16, + "orbit_denominator": 86773770449574983883806621111560647475200, + "orbit_numerator": 1403497292127935182782111450629406720, + "probability": [ + 92906734159963, + 5744127664823054080 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 134959962175989350400, + 68829580709754568704000, + 18237289644354969796608000, + 3198299538201451560330854400, + 396782979072628566302864179200, + 34942501060266967290542555136000, + 2096806052634774571991458381824000, + 77282280225681691367685180358656000, + 1324082863348973584860099505784094720 + ] + }, + { + "header_fiber": 11806636273615420997742184366080, + "k": 9, + "m": 16, + "orbit_denominator": 2832295867474127473967448113081339533590528000, + "orbit_numerator": 44491413467607841481266597210495333171200, + "probability": [ + 75749953173786889, + 4822195174618953900160 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 8810186330848584794112000, + 7003119223432308401897472000, + 2865676386228500598056445542400, + 761823319819446847301499224064000, + 138651844207139326208872858779648000, + 16908644008446822148539120391028736000, + 1256300747348681574873090291910311936000, + 43218064659710497809833647868792851660800 + ] + }, + { + "header_fiber": 363147031053623923404963840, + "k": 10, + "m": 16, + "orbit_denominator": 92083603243318832433629673052500510916095246336000, + "orbit_numerator": 1425502057459070052008041645763868467449036800, + "probability": [ + 9276478723277303, + 599235603891005034560 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1792798521198670950885752832000, + 2200839464623488459307350176563200, + 1365187389116448750364286609522688000, + 532423081755415012642071777713848320000, + 134186998851033980570806459423204048896000, + 20261618453239536439553200227929510903808000, + 1405105718216507704793311559510193193195929600 + ] + }, + { + "header_fiber": 11258278492485860720640, + "k": 11, + "m": 16, + "orbit_denominator": 2970248706216492258979158733981456480109568265814016000, + "orbit_numerator": 45645714921335046060048587667022819965838295040000, + "probability": [ + 207941490991205, + 13531126539474307232 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1126829805887226091165363290400358400, + 2096927829682865280559544232226848768000, + 1908204325011407405309185251326432378880000, + 1030556151175940970783793608370207095521280000, + 321592408089817922368588394017697197065240576000, + 45323090046791672525813057663560791639727905177600 + ] + }, + { + "header_fiber": 354658470655426560, + "k": 12, + "m": 16, + "orbit_denominator": 94287574930136330269034414851507354504598135030000123904000, + "orbit_numerator": 1443683222724257025624508601593880461771505974797926400, + "probability": [ + 253030902849, + 16525557571414640 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2147254097595254047292973293800293138432000, + 5862003686435043549109817092074800267919360000, + 7387026491629144878578232584797644460696535040000, + 4939659388259603287581517732111828946922095247360000, + 1438736170445354852659409702472073769811522621957734400 + ] + }, + { + "header_fiber": 11544872091648, + "k": 13, + "m": 16, + "orbit_denominator": 2896514301853788065864737224238305930381254708121603806330880000, + "orbit_numerator": 44268835510967538865712937871387567789689807572217888768000, + "probability": [ + 1677773981473, + 109776918152968680 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12005383549818969188576905404569190948698849280000, + 45385890764569466133984661000996727566519511285760000, + 70814956990089672730768638207555179783075157466152960000, + 44197975156081301073697066059942106208609974946541600768000 + ] + }, + { + "header_fiber": 402653184, + "k": 14, + "m": 16, + "orbit_denominator": 83048858062751811424473745693360707635891334991262624335118991360000, + "orbit_numerator": 1268114703767265857960091247898125967345035741666103091265536000, + "probability": [ + 716253943, + 46907485476180 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 185900608571676533284801171460082596112463918226472960000, + 870174191494221898515685026294438049174427534944087572480000, + 1267244343675163064385042278070660069213265201667240777220096000 + ] + }, + { + "header_fiber": 16384, + "k": 15, + "m": 16, + "orbit_denominator": 2041008735750188517567866774160032750859665448745270255659884331663360000, + "orbit_numerator": 31150925457137528136119439517599945897484042506540371306354835456000, + "probability": [ + 65549, + 4294770690 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 7128466976720665792640491735404036498836910366261965393756160000, + 31143796990160807470326799025864541860985205596174109340961079296000 + ] + }, + { + "header_fiber": 1, + "k": 16, + "m": 16, + "orbit_denominator": 33439887126531088671831929227837976590084758712242507868731544889972490240000, + "orbit_numerator": 510259969886794669593834275239764653850381608487716607442306323185664000, + "probability": [ + 1, + 65535 + ], + "support_histogram": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 510259969886794669593834275239764653850381608487716607442306323185664000 + ] + } + ], + "schema_version": 1, + "small_gl": [ + { + "gl_count": 6, + "joint_first_k": [ + 3, + 2 + ], + "m": 2, + "mask_histogram": [ + 2, + 1, + 1, + 2 + ], + "record_sha256": "3bba2177840a4fe8a5084ae0152f95ea20d69de19afa28a954878698b3d02010" + }, + { + "gl_count": 168, + "joint_first_k": [ + 54, + 32, + 24 + ], + "m": 3, + "mask_histogram": [ + 78, + 14, + 14, + 8, + 14, + 8, + 8, + 24 + ], + "record_sha256": "6f6f47f8cc6df37c47f34956e3de77e196e72c3e3410fd19bbbf1f3435ab7275" + }, + { + "gl_count": 20160, + "joint_first_k": [ + 4536, + 2352, + 1632, + 1344 + ], + "m": 4, + "mask_histogram": [ + 10944, + 1032, + 1032, + 432, + 1032, + 432, + 432, + 288, + 1032, + 432, + 432, + 288, + 432, + 288, + 288, + 1344 + ], + "record_sha256": "b5afda7d17d3ef6e66d7bde49f5b3042cc202ff47c4925edb8554cc63d28eb62" + } + ], + "source_manifest_sha256": "680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9" +} diff --git a/research/common-image-full-guard-family/PROOF.md b/research/common-image-full-guard-family/PROOF.md new file mode 100644 index 0000000000..87d6fa4854 --- /dev/null +++ b/research/common-image-full-guard-family/PROOF.md @@ -0,0 +1,179 @@ +# Binary common-image full-guard family + +This is a counting theorem for complete, equally weighted headers. The proof +covers all dimensions below; the executable domains are finite corroboration. +The complements guarded here are corank one. They are not rank-one first-pivot +requests. No physical header producer or paid caller is supplied. + +## Statement + +Work over F_2. Fix m >= 2 and 1 <= k <= m. Let u be a nonzero column and +v_1,...,v_k independent ordered covectors, with v_i u = 1. Put +U_i = u v_i and P_i = I - U_i. For G uniform in GL_m(F_2), let E_i mean +that every leading principal minor of G P_i G^{-1} of orders 1,...,m-1 +is nonzero. Define + + A_j = 0 if j < k-1, + A_j = 2^j product_{r=0}^{k-2}(2^j-2^r) otherwise, + +where an empty product is one. Then + + Pr(E_1 and ... and E_k) + = [sum_{j=0}^{m-1} binom(m-1,j) A_j] / [(2^m-1) A_{m-1}]. (1) + +The summand indexed by j counts passing orbit tuples with exactly j zero +coordinates of the transformed u among its first m-1 coordinates. Every +orbit tuple has exactly + + 2^{(k-1)(m-k)} |GL_{m-k}(F_2)| (2) + +complete headers above it, with |GL_0|=1. + +The new larger-family case is k >= 3. The k=1 marginal is predecessor +PR4227. The k=2 specialization is the transpose-dual of Nick Petalas's +PR4807 common-covector pair law; neither specialization is claimed as new. + +## The tuple orbit and constant header fibers + +Write V for the k by m matrix with rows v_i and t for the all-ones column +in F_2^k. Conjugation acts as (u,V) -> (G u,V G^{-1}). It preserves + + u != 0, rank(V)=k, V u=t. (3) + +Conversely this action is transitive. The columns t,e_2,...,e_k form a +basis of F_2^k. Choose preimages b_2,...,b_k under V of e_2,...,e_k; +take b_1=u; then extend these columns by a basis of ker(V). Their images +are independent, so the resulting m by m matrix B is invertible and + + B^{-1}u=e_1, V B=[Q 0], Q=[t e_2 ... e_k]. + +For a second tuple use B' in the same way. G=B' B^{-1} sends the first +tuple to the second. Thus every tuple satisfying (3) is reached and +uniform complete headers give a uniform distribution on these tuples. +This conclusion does not apply to a restricted or weighted header set. + +In these adapted coordinates a stabilizing matrix has block form + + [ I_k 0 ] + [ T H ], + +where H is any element of GL_{m-k} and the first column of T is zero +because the matrix fixes e_1. Its other (k-1)(m-k) entries are free. +This proves (2) and the equality of every header fiber by orbit-stabilizer. +At k=m the empty blocks give the same formula with fiber one. + +For fixed nonzero u, choose coordinates in which u is the last unit +vector. The condition V u=t fixes the final column of V to t. Let B_0 +be its other m-1 columns. Choose an invertible row operation taking t +to the first unit vector. The first row of B_0 is arbitrary, while the +remaining k-1 rows must be independent. There are A_{m-1} possibilities. +Consequently the orbit has size D=(2^m-1)A_{m-1}. Equivalently its +constant fiber is |GL_m|/D, agreeing with (2). Over F_2 a common image +line has a unique nonzero vector u, so no scalar gauge has been counted. + +## From all proper minors to coordinate support + +For a transformed tuple write u'=G u and V'=V G^{-1}. The rank-one +determinant lemma gives, for each proper order l, + + det((I-u'v'_i)_{1:l,1:l}) + = 1 + sum_{a=1}^l u'_a v'_{i,a}. + +In F_2 this determinant is nonzero precisely when the partial sum is +zero. Every proper prefix must vanish. Subtract consecutive prefixes +(the first prefix is already a single product) to obtain + + u'_a v'_{i,a}=0 for every a (729/8128)^6 = s_7^6. + +For a simple exact inequality, 22/2667>1/128, while 729/8128<1/8, +so s_7^6<1/8^6<1/128. Each individual event still has the same +marginal s_7. Sharing changes the joint distribution, not the single +uniform-GL corank-one full-guard marginal. + +This exhibits all six common-image kernels. It does not settle a narrower +reading of PR6515 Q2 involving exactly one coupled pair and four otherwise +orthogonal kernels. Nor does it identify PR4240's rank-one first-pivot +predicate with the complementary full-guard predicate used here. + +## Evidence and scope + +The primary literally conjugates the complements and checks every proper +minor for every GL_2, GL_3 and GL_4 header. Its 20,334 complete actual +header-code/passing-mask records include orbit coverage and constant-fiber +checks for every k in those dimensions. A separate engine uses column-rank +and zero-support dynamic programming for the 135 frozen (m,k) pairs through +m=16, plus literal quotient-span states at (7,6). After both blind firsts, +its separately written literal-matrix census compares every submitted small +header record as data. These finite checks corroborate, and do not replace, +the all-dimension argument above. There is no GL_7 or predecessor spectrum +run. AI static review is recorded separately from execution and from human +or proof-kernel acceptance. + +The direct released request is Nick Petalas's PR6694 README question 3. +The binary prefix criterion and orthogonal-family context are predecessors +PR4275 and PR6515; their orthogonal spectra are not reused or contradicted. +PR4807 explicitly excludes larger families, rather than requesting this law. +Arbitrary nonorthogonal mixtures, odd fields, restricted headers and physical +selection/emission/dispatch/restoration/stock/precision/caller costs remain +outside this theorem. No supplier, recursive invoice, kappa or selected +frontier change follows from a complete-header counting probability. diff --git a/research/common-image-full-guard-family/README.md b/research/common-image-full-guard-family/README.md new file mode 100644 index 0000000000..9e9bd1b5da --- /dev/null +++ b/research/common-image-full-guard-family/README.md @@ -0,0 +1,95 @@ +# Common-image binary full guards, for any family size + +For independent normalized covectors v_i and a nonzero common column u over +F_2, this package counts uniform complete headers that pass every proper +leading principal minor of each corank-one complement I-u v_i. The written +proof covers all m>=2 and 1<=k<=m. With A_j=0 for j=3 family law. The k=1 marginal and k=2 +transpose-dual of Nick Petalas's PR4807 are prior results. At (m,k)=(7,6), +u=e7 and v_i=e7^T+ei^T give six distinct, noncommuting common-image kernels. +Their joint probability is 22/2667, strictly greater than (729/8128)^6; +each individual marginal remains 729/8128. I7 passes all 36 proper minors. + +This takes the shared-direction continuation in [PR6694 question 3](https://github.com/CrocSwap/integer-mult-bounds/pull/6694). +The operator boundary matters: these are full guards on CORANK-ONE complements, +not rank-one first-pivot requests. All six kernels share one line. The narrower +PR6515 interpretation with one coupled pair and four otherwise orthogonal +kernels remains open. This counting result supplies no physical header producer, +paid caller, supplier admission, new kappa or frontier change. + +## Evidence + +[PROOF.md](PROOF.md) gives transitivity, equal fibers, the binary prefix +equivalence, rank/support count and exact m7 example. [RESULT.json](RESULT.json) +and [ORACLE.json](ORACLE.json) agree on every proof-relevant field: 135 pairs +2<=m<=16,1<=k<=m; complete GL2/GL3/GL4 censuses; exact example and ratio. +The primary uses binomial/full-rank products. The oracle independently uses +column-rank/support DP and literal quotient-span states (374 subspaces at7,6). +Both also implement literal conjugation and every proper determinant for all +20,334 small headers. After independent blind first seals, the oracle compares +all submitted [SMALL-GL.json.gz](SMALL-GL.json.gz) records as data, in normal +and optimized Python. Regeneration compares decompressed canonical values; +gzip container equality is not a mathematical acceptance condition. + +Eight authenticated predecessor prose/metadata files stay inert in inputs/. +No predecessor executable or peer code is imported or executed. Neither engine +read the other's results before its first seal. Subsequent data comparison is +explicit. [RUN-RECORDS.json](RUN-RECORDS.json) and [VALIDATION.md](VALIDATION.md) +distinguish direct runs, independent review and later transport checks. + +## Reproduce + +From the repository root, CPython3.12, standard library only: + +```sh +python3.12 -I -W error -B research/common-image-full-guard-family/verify.py +python3.12 -I -W error -B research/common-image-full-guard-family/oracle.py --check-primary research/common-image-full-guard-family/RESULT.json +python3.12 -W error -B scripts/research_package.py --package research/common-image-full-guard-family +``` + +The registered manifest adds both optimized modes. Direct verifiers need no +Git, network, source checkout, compiler, Lean or Docker; provenance/committed-byte +checks separately require Git history. SMALL-GL is a declared runtime input. +Runtime authentication binds source, cases and schema bytes in both engines. +Receipt checks reject duplicate/nonfinite/float/boolean aliases and compare +actual typed values. The proof-relevant artifact is bounded at8MiB decompressed. +Fixed execution domains include at most65,536 candidate matrices of order4, +135 family rows and a fixed 374-span oracle domain. New functions stay below60 +physical lines. Explicit checks remain active under -O. CPython dynamic +allocation, arbitrary-precision integers and bounded recursive JSON-value type +comparison are managed-runtime deviations from fixed allocation/no recursion; +no stronger hard-real-time or formal-verification claim is made. + +## Open next questions + +Structured copies are in [TASK.json](TASK.json). + +1. What is the joint law for exactly one coupled pair plus four orthogonal + kernels? This isolates the narrower reading of PR6515 Q2. First write a + normalized partial-Gram fixture and its precise full-guard predicate. The + current all-six-common-line orbit is different, so its law cannot transfer. +2. Can a named physical caller use this family? Pin its actual header domain + and producer, then charge selection, emission, dispatch, restoration, stock + and precision. Those resources and the full caller invoice are unknown. +3. What changes over odd fields or restricted header sets? First characterize + the new prefix/orbit distribution. Binary vanishing-prefix and uniform-fiber + assumptions are essential here; no broader sign or applicability claim is made. + +## Credit and limits + +Nick Petalas supplies the released6694 question and4807 common-covector pair, +4275 binary full-guard context,4227 marginal and4261 partial sums. unpaidmoon +supplies6515's six-orthogonal theorem and nonorthogonal question, with its +Cursor/Grok disclosure retained. Ryanson Jonathan's4607 and the retained4599, +5146, Cinna Davis/source527/commdata2338/Jose Manuel/normalizer/compiler lineage +remain predecessor credit, not newly rerun evidence. See [NOTICE](NOTICE) and +[SOURCE-PINS.json](SOURCE-PINS.json) for exact immutable sources. Classical +rank-one determinants, orbit-stabilizer and finite-field rank counts are used. +Prepared for ToikY with substantial OpenAI Codex assistance and separate AI +primary/oracle/static review. Apache-2.0. Human acceptance, formal kernel +checking, GL7 enumeration, historical spectra, physical caller admission and +selected replay are unclaimed. diff --git a/research/common-image-full-guard-family/RESULT.json b/research/common-image-full-guard-family/RESULT.json new file mode 100644 index 0000000000..d94c43a058 --- /dev/null +++ b/research/common-image-full-guard-family/RESULT.json @@ -0,0 +1 @@ +{"case_manifest_sha256":"3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273","example":{"header_rows":[1,2,4,8,16,32,64],"joint_probability":[22,2667],"k":6,"m":7,"product_probability":[150094635296999121,288338191148183248175104],"proper_minors":[[1,1,1,1,1,1],[1,1,1,1,1,1],[1,1,1,1,1,1],[1,1,1,1,1,1],[1,1,1,1,1,1],[1,1,1,1,1,1]],"ratio":[49948348072913633542144,3151987341236981541],"ratio_gt_one":true,"single_probability":[729,8128],"u":64,"v_rows":[65,66,68,72,80,96]},"family":[{"header_fiber":1,"k":1,"m":2,"orbit_denominator":6,"orbit_numerator":3,"probability":[1,2],"support_histogram":[1,2]},{"header_fiber":1,"k":2,"m":2,"orbit_denominator":6,"orbit_numerator":2,"probability":[1,3],"support_histogram":[0,2]},{"header_fiber":6,"k":1,"m":3,"orbit_denominator":28,"orbit_numerator":9,"probability":[9,28],"support_histogram":[1,4,4]},{"header_fiber":2,"k":2,"m":3,"orbit_denominator":84,"orbit_numerator":16,"probability":[4,21],"support_histogram":[0,4,12]},{"header_fiber":1,"k":3,"m":3,"orbit_denominator":168,"orbit_numerator":24,"probability":[1,7],"support_histogram":[0,0,24]},{"header_fiber":168,"k":1,"m":4,"orbit_denominator":120,"orbit_numerator":27,"probability":[9,40],"support_histogram":[1,6,12,8]},{"header_fiber":24,"k":2,"m":4,"orbit_denominator":840,"orbit_numerator":98,"probability":[7,60],"support_histogram":[0,6,36,56]},{"header_fiber":4,"k":3,"m":4,"orbit_denominator":5040,"orbit_numerator":408,"probability":[17,210],"support_histogram":[0,0,72,336]},{"header_fiber":1,"k":4,"m":4,"orbit_denominator":20160,"orbit_numerator":1344,"probability":[1,15],"support_histogram":[0,0,0,1344]},{"header_fiber":20160,"k":1,"m":5,"orbit_denominator":496,"orbit_numerator":81,"probability":[81,496],"support_histogram":[1,8,24,32,16]},{"header_fiber":1344,"k":2,"m":5,"orbit_denominator":7440,"orbit_numerator":544,"probability":[34,465],"support_histogram":[0,8,72,224,240]},{"header_fiber":96,"k":3,"m":5,"orbit_denominator":104160,"orbit_numerator":4848,"probability":[101,2170],"support_histogram":[0,0,144,1344,3360]},{"header_fiber":8,"k":4,"m":5,"orbit_denominator":1249920,"orbit_numerator":45696,"probability":[17,465],"support_histogram":[0,0,0,5376,40320]},{"header_fiber":1,"k":5,"m":5,"orbit_denominator":9999360,"orbit_numerator":322560,"probability":[1,31],"support_histogram":[0,0,0,0,322560]},{"header_fiber":9999360,"k":1,"m":6,"orbit_denominator":2016,"orbit_numerator":243,"probability":[27,224],"support_histogram":[1,10,40,80,80,32]},{"header_fiber":322560,"k":2,"m":6,"orbit_denominator":62496,"orbit_numerator":2882,"probability":[1441,31248],"support_histogram":[0,10,120,560,1200,992]},{"header_fiber":10752,"k":3,"m":6,"orbit_denominator":1874880,"orbit_numerator":50160,"probability":[209,7812],"support_histogram":[0,0,240,3360,16800,29760]},{"header_fiber":384,"k":4,"m":6,"orbit_denominator":52496640,"orbit_numerator":1048320,"probability":[13,651],"support_histogram":[0,0,0,13440,201600,833280]},{"header_fiber":16,"k":5,"m":6,"orbit_denominator":1259919360,"orbit_numerator":21611520,"probability":[67,3906],"support_histogram":[0,0,0,0,1612800,19998720]},{"header_fiber":1,"k":6,"m":6,"orbit_denominator":20158709760,"orbit_numerator":319979520,"probability":[1,63],"support_histogram":[0,0,0,0,0,319979520]},{"header_fiber":20158709760,"k":1,"m":7,"orbit_denominator":8128,"orbit_numerator":729,"probability":[729,8128],"support_histogram":[1,12,60,160,240,192,64]},{"header_fiber":319979520,"k":2,"m":7,"orbit_denominator":512064,"orbit_numerator":14896,"probability":[133,4572],"support_histogram":[0,12,180,1120,3600,5952,4032]},{"header_fiber":5160960,"k":3,"m":7,"orbit_denominator":31747968,"orbit_numerator":486024,"probability":[2893,188976],"support_histogram":[0,0,360,6720,50400,178560,249984]},{"header_fiber":86016,"k":4,"m":7,"orbit_denominator":1904878080,"orbit_numerator":20630400,"probability":[1535,141732],"support_histogram":[0,0,0,26880,604800,4999680,14999040]},{"header_fiber":1536,"k":5,"m":7,"orbit_denominator":106673172480,"orbit_numerator":964776960,"probability":[997,110236],"support_histogram":[0,0,0,0,4838400,119992320,839946240]},{"header_fiber":32,"k":6,"m":7,"orbit_denominator":5120312279040,"orbit_numerator":42237296640,"probability":[22,2667],"support_histogram":[0,0,0,0,0,1919877120,40317419520]},{"header_fiber":1,"k":7,"m":7,"orbit_denominator":163849992929280,"orbit_numerator":1290157424640,"probability":[1,127],"support_histogram":[0,0,0,0,0,0,1290157424640]},{"header_fiber":163849992929280,"k":1,"m":8,"orbit_denominator":32640,"orbit_numerator":2187,"probability":[729,10880],"support_histogram":[1,14,84,280,560,672,448,128]},{"header_fiber":1290157424640,"k":2,"m":8,"orbit_denominator":4145280,"orbit_numerator":75938,"probability":[37969,2072640],"support_histogram":[0,14,252,1960,8400,20832,28224,16256]},{"header_fiber":10239344640,"k":3,"m":8,"orbit_denominator":522305280,"orbit_numerator":4552968,"probability":[27101,3108960],"support_histogram":[0,0,504,11760,117600,624960,1749888,2048256]},{"header_fiber":82575360,"k":4,"m":8,"orbit_denominator":64765854720,"orbit_numerator":377934144,"probability":[9071,1554480],"support_histogram":[0,0,0,47040,1411200,17498880,104993280,253983744]},{"header_fiber":688128,"k":5,"m":8,"orbit_denominator":7771902566400,"orbit_numerator":36788935680,"probability":[6709,1417320],"support_histogram":[0,0,0,0,11289600,419973120,5879623680,30478049280]},{"header_fiber":6144,"k":6,"m":8,"orbit_denominator":870453087436800,"orbit_numerator":3702483025920,"probability":[551,129540],"support_histogram":[0,0,0,0,0,6719569920,282221936640,3413541519360]},{"header_fiber":64,"k":7,"m":8,"orbit_denominator":83563496393932800,"orbit_numerator":336731087831040,"probability":[87,21590],"support_histogram":[0,0,0,0,0,0,9031101972480,327699985858560]},{"header_fiber":1,"k":8,"m":8,"orbit_denominator":5348063769211699200,"orbit_numerator":20972799094947840,"probability":[1,255],"support_histogram":[0,0,0,0,0,0,0,20972799094947840]},{"header_fiber":5348063769211699200,"k":1,"m":9,"orbit_denominator":130816,"orbit_numerator":6561,"probability":[6561,130816],"support_histogram":[1,16,112,448,1120,1792,1792,1024,256]},{"header_fiber":20972799094947840,"k":2,"m":9,"orbit_denominator":33358080,"orbit_numerator":384064,"probability":[353,30660],"support_histogram":[0,16,336,3136,16800,55552,112896,130048,65280]},{"header_fiber":82570075176960,"k":3,"m":9,"orbit_denominator":8472952320,"orbit_numerator":41887968,"probability":[436333,88259920],"support_histogram":[0,0,672,18816,235200,1666560,6999552,16386048,16581120]},{"header_fiber":327659028480,"k":4,"m":9,"orbit_denominator":2135183984640,"orbit_numerator":6679846656,"probability":[138059,44129960],"support_histogram":[0,0,0,75264,2822400,46663680,419973120,2031869952,4178442240]},{"header_fiber":1321205760,"k":5,"m":9,"orbit_denominator":529525628190720,"orbit_numerator":1304739072000,"probability":[2275,923304],"support_histogram":[0,0,0,0,22579200,1119928320,23518494720,243824394240,1036253675520]},{"header_fiber":5505024,"k":6,"m":9,"orbit_denominator":127086150765772800,"orbit_numerator":277156020879360,"probability":[108271,49646205],"support_histogram":[0,0,0,0,0,17918853120,1128887746560,27308332154880,248700882124800]},{"header_fiber":24576,"k":7,"m":9,"orbit_denominator":28467297771533107200,"orbit_numerator":58366721890713600,"probability":[2262,1103249],"support_histogram":[0,0,0,0,0,0,36124407889920,2621599886868480,55708997595955200]},{"header_fiber":128,"k":8,"m":9,"orbit_denominator":5465721172134356582400,"orbit_numerator":10863909931182981120,"probability":[37,18615],"support_histogram":[0,0,0,0,0,0,0,167782392759582720,10696127538423398400]},{"header_fiber":1,"k":9,"m":9,"orbit_denominator":699612310033197642547200,"orbit_numerator":1369104324918194995200,"probability":[1,511],"support_histogram":[0,0,0,0,0,0,0,0,1369104324918194995200]},{"header_fiber":699612310033197642547200,"k":1,"m":10,"orbit_denominator":523776,"orbit_numerator":19683,"probability":[6561,174592],"support_histogram":[1,18,144,672,2016,4032,5376,4608,2304,512]},{"header_fiber":1369104324918194995200,"k":2,"m":10,"orbit_denominator":267649536,"orbit_numerator":1933442,"probability":[138103,19117824],"support_histogram":[0,18,432,4704,30240,124992,338688,585216,587520,261632]},{"header_fiber":2684518284153323520,"k":3,"m":10,"orbit_denominator":136501263360,"orbit_numerator":381600480,"probability":[795001,284377632],"support_histogram":[0,0,864,28224,423360,3749760,20998656,73737216,149230080,133432320]},{"header_fiber":5284484811325440,"k":4,"m":10,"orbit_denominator":69342641786880,"orbit_numerator":115903119360,"probability":[269492,161231961],"support_histogram":[0,0,0,112896,5080320,104993280,1259919360,9143414784,37605980160,67783618560]},{"header_fiber":10485088911360,"k":5,"m":10,"orbit_denominator":34948691460587520,"orbit_numerator":44659552573440,"probability":[1357387,1062234096],"support_histogram":[0,0,0,0,40642560,2519838720,70555484160,1097209774080,9326283079680,34162943754240]},{"header_fiber":21139292160,"k":6,"m":10,"orbit_denominator":17334550964451409920,"orbit_numerator":19309442516582400,"probability":[10057645,9028989816],"support_histogram":[0,0,0,0,0,40317419520,3386663239680,122887494696960,2238307939123200,16944820102103040]},{"header_fiber":44040192,"k":7,"m":10,"orbit_denominator":8320584462936676761600,"orbit_numerator":8646800200087633920,"probability":[837766,806159805],"support_histogram":[0,0,0,0,0,0,108373223669760,11797199490908160,501380978363596800,8133513649009459200]},{"header_fiber":98304,"k":8,"m":10,"orbit_denominator":3727621839395631189196800,"orbit_numerator":3740834283369466429440,"probability":[89183,88868010],"support_histogram":[0,0,0,0,0,0,0,755020767418122240,96265147845810585600,3643814114756237721600]},{"header_fiber":256,"k":9,"m":10,"orbit_denominator":1431406786327922376651571200,"orbit_numerator":1411546558990659040051200,"probability":[1031,1045506],"support_histogram":[0,0,0,0,0,0,0,0,12321938924263754956800,1399224620066395285094400]},{"header_fiber":1,"k":10,"m":10,"orbit_denominator":366440137299948128422802227200,"orbit_numerator":358201502736997192984166400,"probability":[1,1023],"support_histogram":[0,0,0,0,0,0,0,0,0,358201502736997192984166400]},{"header_fiber":366440137299948128422802227200,"k":1,"m":11,"orbit_denominator":2096128,"orbit_numerator":59049,"probability":[59049,2096128],"support_histogram":[1,20,180,960,3360,8064,13440,15360,11520,5120,1024]},{"header_fiber":358201502736997192984166400,"k":2,"m":11,"orbit_denominator":2144338944,"orbit_numerator":9706576,"probability":[55151,12183744],"support_histogram":[0,20,540,6720,50400,249984,846720,1950720,2937600,2616320,1047552]},{"header_fiber":350490707179057918771200,"k":3,"m":11,"orbit_denominator":2191514400768,"orbit_numerator":3457605624,"probability":[13096991,8301190912],"support_histogram":[0,0,1080,40320,705600,7499520,52496640,245790720,746150400,1334323200,1070598144]},{"header_fiber":343618340371625410560,"k":4,"m":11,"orbit_denominator":2235344688783360,"orbit_numerator":1991722656000,"probability":[92275,103561824],"support_histogram":[0,0,0,161280,8467200,209986560,3149798400,30478049280,188029900800,677836185600,1092010106880]},{"header_fiber":338207027924828160,"k":5,"m":11,"orbit_denominator":2271110203803893760,"orbit_numerator":1501581983569920,"probability":[2327601041,3520446124448],"support_histogram":[0,0,0,0,67737600,5039677440,176388710400,3657365913600,46631415398400,341629437542400,1109482268590080]},{"header_fiber":335522845163520,"k":6,"m":11,"orbit_denominator":2289279085434324910080,"orbit_numerator":1299416039730708480,"probability":[84602813,149051146398],"support_histogram":[0,0,0,0,0,80634839040,8466658099200,409624982323200,11191539695616000,169448201021030400,1118358126738800640]},{"header_fiber":338228674560,"k":7,"m":11,"orbit_denominator":2270964852750850310799360,"orbit_numerator":1193292898038165012480,"probability":[462460191,880111531112],"support_histogram":[0,0,0,0,0,0,270933059174400,39323998303027200,2506904891817984000,81335136490094592000,1109411261724890234880]},{"header_fiber":352321536,"k":8,"m":11,"orbit_denominator":2180126258640816298367385600,"orbit_numerator":1101956794878577449369600,"probability":[5254219,10395018084],"support_histogram":[0,0,0,0,0,0,0,2516735891393740800,481325739229052928000,36438141147562377216000,1065034811255894625484800]},{"header_fiber":393216,"k":9,"m":11,"orbit_denominator":1953393127742171403337177497600,"orbit_numerator":968325046780566856060108800,"probability":[707269,1426767188],"support_histogram":[0,0,0,0,0,0,0,0,61609694621318774784000,13992246200663952850944000,954271190885281584434380800]},{"header_fiber":512,"k":10,"m":11,"orbit_denominator":1500205922105987637762952318156800,"orbit_numerator":736462289627266228775446118400,"probability":[1028,2094081],"support_histogram":[0,0,0,0,0,0,0,0,0,3582015027369971929841664000,732880274599896256845604454400]},{"header_fiber":1,"k":11,"m":11,"orbit_denominator":768105432118265670534631586896281600,"orbit_numerator":375234700595146883504949480652800,"probability":[1,2047],"support_histogram":[0,0,0,0,0,0,0,0,0,0,375234700595146883504949480652800]},{"header_fiber":768105432118265670534631586896281600,"k":1,"m":12,"orbit_denominator":8386560,"orbit_numerator":177147,"probability":[19683,931840],"support_histogram":[1,22,220,1320,5280,14784,29568,42240,42240,28160,11264,2048]},{"header_fiber":375234700595146883504949480652800,"k":2,"m":12,"orbit_denominator":17167288320,"orbit_numerator":48650978,"probability":[24325489,8583644160],"support_histogram":[0,22,660,9240,79200,458304,1862784,5364480,10771200,14389760,11523072,4192256]},{"header_fiber":183399169401342562807893196800,"k":3,"m":12,"orbit_denominator":35124271902720,"orbit_numerator":31234929528,"probability":[118314127,133046484480],"support_histogram":[0,0,1320,55440,1108800,13749120,115492608,675924480,2735884800,7338777600,11776579584,8577355776]},{"header_fiber":89725621037838827205427200,"k":4,"m":12,"orbit_denominator":71794011769159680,"orbit_numerator":34052911066944,"probability":[767787497,1618732227840],"support_histogram":[0,0,0,221760,13305600,384975360,6929556480,83814635520,689442969600,3728099020800,12012111175680,17532115206144]},{"header_fiber":43983147567568052551680,"k":5,"m":12,"orbit_denominator":146459784009085747200,"orbit_numerator":50030218895247360,"probability":[7050163873,20638835904960],"support_histogram":[0,0,0,0,106444800,9239408640,388055162880,10057756262400,170981856460800,1878961906483200,12204304954490880,35765515020533760]},{"header_fiber":21645249787189002240,"k":6,"m":12,"orbit_denominator":297606281106462238310400,"orbit_numerator":85951611910197411840,"probability":[96140293,332884450080],"support_histogram":[0,0,0,0,0,147830538240,18626647818240,1126468701388800,41035645550592000,931965105615667200,12301939394126807040,72675526521724600320]},{"header_fiber":10736731045232640,"k":7,"m":12,"orbit_denominator":599974262710627872433766400,"orbit_numerator":159174029319117503201280,"probability":[1869328247,7046054193360],"support_histogram":[0,0,0,0,0,0,596052730183680,108140995333324800,9191984603332608000,447343250695520256000,12203523878973792583680,146513861467796794245120]},{"header_fiber":5411658792960,"k":8,"m":12,"orbit_denominator":1190348937217885698908592537600,"orbit_numerator":302601065634302814930862080,"probability":[327915073,1289927244060],"support_histogram":[0,0,0,0,0,0,0,6921023701332787200,1764861043839860736000,200409776311593074688000,11715382923814840880332800,290683501152108839782318080]},{"header_fiber":2818572288,"k":9,"m":12,"orbit_denominator":2285469959458340541904497672192000,"orbit_numerator":568686488568104333053683302400,"probability":[5394431,21679449480],"support_histogram":[0,0,0,0,0,0,0,0,225902213611502174208000,76957354103651740680192000,10496983099738097428778188800,558112322212048972382050713600]},{"header_fiber":1572864,"k":10,"m":12,"orbit_denominator":4095562167349346251092859828568064000,"orbit_numerator":1008218665507241152179550656921600,"probability":[2187,8883980],"support_histogram":[0,0,0,0,0,0,0,0,0,19701082650534845614129152000,8061683020598858825301648998400,1000137281403991758508634878771200]},{"header_fiber":1024,"k":11,"m":12,"orbit_denominator":6290783489048595841678632696680546304000,"orbit_numerator":1540338445943077956787817618079744000,"probability":[821,3352986],"support_histogram":[0,0,0,0,0,0,0,0,0,0,4127581706546615718554444287180800,1536210864236531341069263173792563200]},{"header_fiber":1,"k":12,"m":12,"orbit_denominator":6441762292785762141878919881400879415296000,"orbit_numerator":1573079924978208093254925489963584716800,"probability":[1,4095],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,1573079924978208093254925489963584716800]},{"header_fiber":6441762292785762141878919881400879415296000,"k":1,"m":13,"orbit_denominator":33550336,"orbit_numerator":531441,"probability":[531441,33550336],"support_histogram":[1,24,264,1760,7920,25344,59136,101376,126720,112640,67584,24576,4096]},{"header_fiber":1573079924978208093254925489963584716800,"k":2,"m":13,"orbit_denominator":137388625920,"orbit_numerator":243609184,"probability":[83657,47180160],"support_histogram":[0,24,792,12320,118800,785664,3725568,12874752,32313600,57559040,69138432,50307072,16773120]},{"header_fiber":384240333409430408709068268188467200,"k":3,"m":13,"orbit_denominator":562469034516480,"orbit_numerator":281698177488,"probability":[64491341,128770383360],"support_histogram":[0,0,1584,73920,1663200,23569920,230985216,1622218752,8207654400,29355110400,70659477504,102928269312,68669153280]},{"header_fiber":93900374733487392157641316761600,"k":4,"m":13,"orbit_denominator":2301623289241436160,"orbit_numerator":580648644191616,"probability":[48728879,193155575040],"support_histogram":[0,0,0,295680,19958400,659957760,13859112960,201155125248,2068328908800,14912396083200,72072667054080,210385382473728,280994175221760]},{"header_fiber":22969758985686739764589363200,"k":5,"m":13,"orbit_denominator":9409036006418991022080,"orbit_numerator":1659169922199229440,"probability":[11990107131,67995054760192],"support_histogram":[0,0,0,0,159667200,15838986240,776110325760,24138615029760,512945569382400,7515847625932800,73225829726945280,429186180246405120,1148704188306554880]},{"header_fiber":5629842888648710726615040,"k":6,"m":13,"orbit_denominator":38388866906189483370086400,"orbit_numerator":5636484751306917150720,"probability":[22241341183,151480918366960],"support_histogram":[0,0,0,0,0,253423779840,37253295636480,2703524883333120,123106936651776000,3727860422462668800,73811636364760842240,872106318260695203840,4686713088290743910400]},{"header_fiber":1385295986380096143360,"k":7,"m":13,"orbit_denominator":156012355106754060416031129600,"orbit_numerator":20880006681388073877504000,"probability":[4597749055,34353708272507],"support_histogram":[0,0,0,0,0,0,1192105460367360,259538388799979520,27575953809997824000,1789373002782081024000,73221143273842755502080,1758166337613561530941440,19046801990813583251865600]},{"header_fiber":343575393447444480,"k":8,"m":13,"orbit_denominator":629041815790432371597437514547200,"orbit_numerator":80356006888627397569271562240,"probability":[174156332263,1363328265302640],"support_histogram":[0,0,0,0,0,0,0,16610456883198689280,5294583131519582208000,801639105246372298752000,70292297542889045281996800,3488202013825306077387816960,76796705626960367671522099200]},{"header_fiber":86586540687360,"k":9,"m":13,"orbit_denominator":2496037925056435650498632057723289600,"orbit_numerator":311489966200044810615226210713600,"probability":[20683062013,165737945977968],"support_histogram":[0,0,0,0,0,0,0,0,677706640834506522624000,307829416414606962720768000,62981898598428584572669132800,6697347866544587668584608563200,304729327927778738920599689625600]},{"header_fiber":22548578304,"k":10,"m":13,"orbit_denominator":9584785632216712897914747101657432064000,"orbit_numerator":1182210715521972453849540693118156800,"probability":[37504624,304069127895],"support_histogram":[0,0,0,0,0,0,0,0,0,78804330602139382456516608000,48370098123593152951809893990400,12001647376847901102103618545254400,1170160619242670357455102808162304000]},{"header_fiber":6291456,"k":11,"m":13,"orbit_denominator":34351871705864699026126453612340236517376000,"orbit_numerator":4212314955226808216906230949204931379200,"probability":[1870969,15257949070],"support_histogram":[0,0,0,0,0,0,0,0,0,0,24765490239279694311326665723084800,18434530370838376092831158085510758400,4193855659365730561119088464453697536000]},{"header_fiber":2048,"k":12,"m":13,"orbit_denominator":105528949880416355408260465497109206581379072000,"orbit_numerator":12902401544671262780876898868681321847193600,"probability":[1367,11180715],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,18876959099738497119059105879563016601600,12883524585571524283757839762801758830592000]},{"header_fiber":1,"k":13,"m":13,"orbit_denominator":216123289355092695876117433338079655078664339456000,"orbit_numerator":26385458351250481733136055834218002085052416000,"probability":[1,8191],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,26385458351250481733136055834218002085052416000]},{"header_fiber":216123289355092695876117433338079655078664339456000,"k":1,"m":14,"orbit_denominator":134209536,"orbit_numerator":1594323,"probability":[531441,44736512],"support_histogram":[1,26,312,2288,11440,41184,109824,219648,329472,366080,292864,159744,53248,8192]},{"header_fiber":26385458351250481733136055834218002085052416000,"k":2,"m":14,"orbit_denominator":1099310309376,"orbit_numerator":1219108802,"probability":[609554401,549655154688],"support_histogram":[0,26,936,16016,171600,1276704,6918912,27895296,84015360,187066880,299599872,326995968,218050560,67100672]},{"header_fiber":3221667686355370174986087403445421500006400,"k":3,"m":14,"orbit_denominator":9003351433789440,"orbit_numerator":2538206907600,"probability":[116218265,412241366016],"support_histogram":[0,0,1872,96096,2402400,38301120,428972544,3514807296,21339901440,95404108800,306191069184,669033750528,892698992640,549554503680]},{"header_fiber":393462101411256738518085906624990412800,"k":4,"m":14,"orbit_denominator":73719441539867934720,"orbit_numerator":9886802049196800,"probability":[28293275095,210964519058688],"support_histogram":[0,0,0,384384,28828800,1072431360,25738352640,435836104704,5377655162880,48465287270400,312314890567680,1367504986079232,3652924277882880,4499752276131840]},{"header_fiber":48076991863545544784712354181939200,"k":5,"m":14,"orbit_denominator":603319909562279177748480,"orbit_numerator":54891963107180559360,"probability":[1190041796467,13079800181638656],"support_histogram":[0,0,0,0,230630400,25738352640,1441347747840,52300332564480,1333658480394240,24426504784281600,317311928816762880,2789710171601633280,14933154447985213440,36825972627862978560]},{"header_fiber":5880258300335805379734876979200,"k":6,"m":14,"orbit_denominator":4932743580581194557271572480,"orbit_numerator":368017405397771250401280,"probability":[127664335671,1711156654587136],"support_histogram":[0,0,0,0,0,411813642240,69184691896320,5857637247221760,320078035294617600,12115546373003673600,319850424247296983040,5668691068694518824960,60927270147779670835200,301089152205407712706560]},{"header_fiber":720619889747034973006725120,"k":7,"m":14,"orbit_denominator":40251187617542547587336031436800,"orbit_numerator":2716247168416331020149719040,"probability":[1568926303,23249411067760],"support_histogram":[0,0,0,0,0,0,2213910140682240,562333175733288960,71697479905994342400,5815462259041763328000,317291620853318607175680,11428081194488149951119360,247608425880576582274252800,2456887481996126935685529600]},{"header_fiber":88658943128326153175040,"k":8,"m":14,"orbit_denominator":327161652955385826789867263518310400,"orbit_numerator":20990919158989885704255496519680,"probability":[1166508134369,18181039454988320],"support_histogram":[0,0,0,0,0,0,0,35989323246930493440,13765916141950913740800,2605327092050709970944000,304599956019185862888652800,22673313089864489503020810240,998357173150484779729787289600,19969581453664519733251984588800]},{"header_fiber":10994412590318223360,"k":9,"m":14,"orbit_denominator":2638231569432231307233489613011655065600,"orbit_numerator":165039992790312584358933093679104000,"probability":[842978729015,13475358654873696],"support_histogram":[0,0,0,0,0,0,0,0,1762037266169716958822400,1000445603347472628842496000,272921560593190533148232908800,43532761132539819845799955660800,3961481263061123605967795965132800,161034704842350687128944003724083200]},{"header_fiber":1385384650997760,"k":10,"m":14,"orbit_denominator":20937005735014187654204973568860494600601600,"orbit_numerator":1293261726246871889086662074407531315200,"probability":[25247767601,408743755676208],"support_histogram":[0,0,0,0,0,0,0,0,0,256114074456952992983678976000,209603758535570329457842873958400,78010707949511357163673520544153600,15212088050154714646916336506109952000,1277971417628895053055299613554324275200]},{"header_fiber":180388626432,"k":11,"m":14,"orbit_denominator":160796204044908961184294197008848598532620288000,"orbit_numerator":9869460542726203324415861267078215788134400,"probability":[1011619223,16481603051460],"support_histogram":[0,0,0,0,0,0,0,0,0,0,107317124370212008682415551466700800,119824447410449444603402527555819929600,54520123571754497294548150037898067968000,9814820487389914007464701032097210433536000]},{"header_fiber":25165824,"k":12,"m":14,"orbit_denominator":1152587190593907433769020804159426754281822224384000,"orbit_numerator":70520241773457481721427102799177444411991654400,"probability":[287368,4696760355],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,122700234148300231273884188217159607910400,167485819612429815688851916916422864797696000,70352633253610903605506976998072804387586048000]},{"header_fiber":4096,"k":13,"m":14,"orbit_denominator":7081495699008967273076863820755517978307515746615296000,"orbit_numerator":432589589668751648014765635402004144184434360320000,"probability":[5465,89462102],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,343010958566256262530768725844834027105681408000,432246578710185391752234866676159310157328678912000]},{"header_fiber":1,"k":14,"m":14,"orbit_denominator":29005806383140729950522834209814601639147584498136252416000,"orbit_numerator":1770481986396919364617154013905548534404418268823552000,"probability":[1,16383],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,1770481986396919364617154013905548534404418268823552000]},{"header_fiber":29005806383140729950522834209814601639147584498136252416000,"k":1,"m":15,"orbit_denominator":536854528,"orbit_numerator":4782969,"probability":[4782969,536854528],"support_histogram":[1,28,364,2912,16016,64064,192192,439296,768768,1025024,1025024,745472,372736,114688,16384]},{"header_fiber":1770481986396919364617154013905548534404418268823552000,"k":2,"m":15,"orbit_denominator":8795287732224,"orbit_numerator":6098732656,"probability":[8864437,12783848448],"support_histogram":[0,28,1092,20384,240240,1985984,12108096,55790592,196035840,523787264,1048599552,1525981184,1526353920,939409408,268419072]},{"header_fiber":108074837406721973178925284696956936540374695936000,"k":3,"m":15,"orbit_denominator":144084403629293568,"orbit_numerator":22858491474024,"probability":[952437144751,6003516817887232],"support_histogram":[0,0,2184,122304,3363360,59579520,750701952,7029614592,49793103360,267131504640,1071668742144,3122157502464,6248892948480,7693763051520,4397241237504]},{"header_fiber":6597975421655798118371507002256223232013107200,"k":4,"m":15,"orbit_denominator":2360102531447828643840,"orbit_numerator":168217774423171200,"probability":[320928293695,4502637613415424],"support_histogram":[0,0,0,489216,40360320,1668226560,45042117120,871672209408,12547862046720,135702804357120,1093102116986880,6381689935036416,25570469945180160,62996531865845760,72026811470315520]},{"header_fiber":402905191845126900242519968383990182707200,"k":5,"m":15,"orbit_denominator":38649039054989641871523840,"orbit_numerator":1813807615028765690880,"probability":[61793005374203,1316699884951624704],"support_histogram":[0,0,0,0,322882560,40037437440,2522358558720,104600665128960,3111869787586560,68394213395988480,1110591750858670080,13018647467474288640,104532081135896494080,515563616790081699840,1179511064637886955520]},{"header_fiber":24615419834135318929772725341152870400,"k":6,"m":15,"orbit_denominator":632607471252070458153102213120,"orbit_numerator":23975584178257454390968320,"probability":[130993874092303,3456337197998014848],"support_histogram":[0,0,0,0,0,640598999040,121073210818560,11715274494443520,746848749020774400,33923529844410286080,1119476484865539440640,26453891653907754516480,426490891034457695846400,4215248130875707977891840,19306237105992933687951360]},{"header_fiber":1505346124885966177212128506675200,"k":7,"m":15,"orbit_denominator":10344397369913856131719527388938240,"orbit_numerator":351879730904270515280931717120,"probability":[272469232039383,8009924300122383616],"support_histogram":[0,0,0,0,0,0,3874342746193920,1124666351466577920,167294119780653465600,16283294325316937318400,1110520672986615125114880,53331045574278033105223680,1733258981164036075919769600,34396424747945777099597414400,315695589157196451665380638720]},{"header_fiber":92239345887620476544860815360,"k":8,"m":15,"orbit_denominator":168820565076994132069662686987472076800,"orbit_numerator":5438821537830176503057216438272000,"probability":[60449278254145,1876340534871188288],"support_histogram":[0,0,0,0,0,0,0,71978646493860986880,32120470997885465395200,7294915857741987918643200,1066099846067150520110284800,105808794419367617680763781120,6988500212053393458108511027200,279574140351303276265527784243200,5152152015045446091179012023910400]},{"header_fiber":5674172360212873803202560,"k":9,"m":15,"orbit_denominator":2744347105891616610924436639668346080460800,"orbit_numerator":86035803504129215514906475870185062400,"probability":[439447136790909,14017367525214171328],"support_histogram":[0,0,0,0,0,0,0,0,4111420287729339570585600,2801247689372923360758988800,955225462076166866018815180800,203152885285185825947066459750400,27730368841427865241774571755929600,2254485867792909619805216052137164800,83753383156578771658206019460687462400]},{"header_fiber":351821202890183147520,"k":10,"m":15,"orbit_denominator":44260830123819992700989314124571085585671782400,"orbit_numerator":1368773012796758748384825009433170935808000,"probability":[1113414188335,36003512479145988],"support_histogram":[0,0,0,0,0,0,0,0,0,717119408479468380354301132800,733613154874496153102450058854400,364049970431053000097143095872716800,106484616351083002528414355542769664000,17891599846804530742774194589760539852800,1350774563549302429303546681861967393587200]},{"header_fiber":22166154415964160,"k":11,"m":15,"orbit_denominator":702507895725270924150102393785192270415782530252800,"orbit_numerator":21577283559899353752884610765613022394187776000,"probability":[4423341019465,144014049916583952],"support_histogram":[0,0,0,0,0,0,0,0,0,0,375609935295742030388454430133452800,559180754582097408149211795260493004800,381640865002281481061837050265286475776000,137407486823458796104505814449360946069504000,21439493872654528157905892934513146471016038400]},{"header_fiber":1443109011456,"k":12,"m":15,"orbit_denominator":10790521278340161394945572768540553273586419664683008000,"orbit_numerator":330296735722862484856689181060306242363030975283200,"probability":[8075699399,263826422661060],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,572601092692067745944792878346744836915200,1172400737287008709821963418414960053583872000,984936865550552650477097677973019261426204672000,329310625883973552505434515474121929794806349824000]},{"header_fiber":100663296,"k":13,"m":15,"orbit_denominator":154692913046284553757939731209797371730134912312895602688000,"orbit_numerator":4727050985851297407996278217351559129718736172351488000,"probability":[179153643,5862809392468],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,2401076709963793837715381080913838189739769856000,6051452101942595484531288133466230342202601504768000,4720997132672644848717909213837011985538343831076864000]},{"header_fiber":8192,"k":14,"m":15,"orbit_denominator":1900866515512744596577563417105990103819897802500861165830144000,"orbit_numerator":58036399514091016772150308575823880957776830852036034560000,"probability":[16390,536821761],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,24786747809556871104640156194677679481661855763529728000,58011612766281459901045668419629203278295168996272504832000]},{"header_fiber":1,"k":15,"m":15,"orbit_denominator":15571898495080403735163399512932270930492602798087054670480539648000,"orbit_numerator":475231131781377719509366115693602433255794024417464359583744000,"probability":[1,32767],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,475231131781377719509366115693602433255794024417464359583744000]},{"header_fiber":15571898495080403735163399512932270930492602798087054670480539648000,"k":1,"m":16,"orbit_denominator":2147450880,"orbit_numerator":14348907,"probability":[4782969,715816960],"support_histogram":[1,30,420,3640,21840,96096,320320,823680,1647360,2562560,3075072,2795520,1863680,860160,245760,32768]},{"header_fiber":475231131781377719509366115693602433255794024417464359583744000,"k":2,"m":16,"orbit_denominator":70365522984960,"orbit_numerator":30503229218,"probability":[2178802087,5026108784640],"support_histogram":[0,30,1260,25480,327600,2978976,20180160,104607360,420076800,1309468160,3145798656,5722429440,7631769600,7045570560,4026286080,1073709056]},{"header_fiber":14503788432563563434943725681914253593840994458202537984000,"k":3,"m":16,"orbit_denominator":2305596726125199360,"orbit_numerator":205799608058088,"probability":[8574983669087,96066530255216640],"support_histogram":[0,0,2520,152880,4586400,89369280,1251169920,13180527360,106699507200,667828761600,3215006226432,11708090634240,31244464742400,57703222886400,65958618562560,35181150928896]},{"header_fiber":442674534017933202140877966118735612069374754553856000,"k":4,"m":16,"orbit_denominator":75540571134766031831040,"orbit_numerator":2860982240716455744,"probability":[2128707024342601,56205782094319964160],"support_histogram":[0,0,0,611520,55036800,2502339840,75070195200,1634385392640,26888275814400,339257010892800,3279306350960640,23931337256386560,127852349725900800,472473988993843200,1080402172054732800,1152675229034348544]},{"header_fiber":13512653663551074546424846340620745179162843545600,"k":5,"m":16,"orbit_denominator":2474709110374935202784870400,"orbit_numerator":59896023561810828887040,"probability":[4761270696750581,196720237330119874560],"support_histogram":[0,0,0,0,440294400,60056156160,4203930931200,196126247116800,6668292401971200,170985533489971200,3331775252576010240,48819928003028582400,522660405679482470400,3866727125925612748800,17692665969568304332800,37761640503165258301440]},{"header_fiber":412574916449409945848340447625205947092172800,"k":6,"m":16,"orbit_denominator":81051672782999877761610075340800,"orbit_numerator":1560212268740843070978293760,"probability":[125025010313868667,6494940738947667471360],"support_histogram":[0,0,0,0,0,960898498560,201788684697600,21966139677081600,1600390176473088000,84808824611025715200,3358429454596618321920,99202093702154079436800,2132454455172288479232000,31614360981567809834188800,289593556589894005319270400,1236769249759668539888762880]},{"header_fiber":12603094955077283292043635374670269644800,"k":7,"m":16,"orbit_denominator":2653307560224283998404067426356428800,"orbit_numerator":45489154842057630527344575774720,"probability":[246563692027932061,14381654493384120829440],"support_histogram":[0,0,0,0,0,0,6457237910323200,2108749408999833600,358487399529971712000,40708235813292343296000,3331562018959845375344640,199991420903542624144588800,8666294905820180379598848000,257973185609593328246980608000,4735433837357946774980709580800,40486878160132509321798541639680]},{"header_fiber":385368607970807341366304897708851200,"k":8,"m":16,"orbit_denominator":86773770449574983883806621111560647475200,"orbit_numerator":1403497292127935182782111450629406720,"probability":[92906734159963,5744127664823054080],"support_histogram":[0,0,0,0,0,0,0,134959962175989350400,68829580709754568704000,18237289644354969796608000,3198299538201451560330854400,396782979072628566302864179200,34942501060266967290542555136000,2096806052634774571991458381824000,77282280225681691367685180358656000,1324082863348973584860099505784094720]},{"header_fiber":11806636273615420997742184366080,"k":9,"m":16,"orbit_denominator":2832295867474127473967448113081339533590528000,"orbit_numerator":44491413467607841481266597210495333171200,"probability":[75749953173786889,4822195174618953900160],"support_histogram":[0,0,0,0,0,0,0,0,8810186330848584794112000,7003119223432308401897472000,2865676386228500598056445542400,761823319819446847301499224064000,138651844207139326208872858779648000,16908644008446822148539120391028736000,1256300747348681574873090291910311936000,43218064659710497809833647868792851660800]},{"header_fiber":363147031053623923404963840,"k":10,"m":16,"orbit_denominator":92083603243318832433629673052500510916095246336000,"orbit_numerator":1425502057459070052008041645763868467449036800,"probability":[9276478723277303,599235603891005034560],"support_histogram":[0,0,0,0,0,0,0,0,0,1792798521198670950885752832000,2200839464623488459307350176563200,1365187389116448750364286609522688000,532423081755415012642071777713848320000,134186998851033980570806459423204048896000,20261618453239536439553200227929510903808000,1405105718216507704793311559510193193195929600]},{"header_fiber":11258278492485860720640,"k":11,"m":16,"orbit_denominator":2970248706216492258979158733981456480109568265814016000,"orbit_numerator":45645714921335046060048587667022819965838295040000,"probability":[207941490991205,13531126539474307232],"support_histogram":[0,0,0,0,0,0,0,0,0,0,1126829805887226091165363290400358400,2096927829682865280559544232226848768000,1908204325011407405309185251326432378880000,1030556151175940970783793608370207095521280000,321592408089817922368588394017697197065240576000,45323090046791672525813057663560791639727905177600]},{"header_fiber":354658470655426560,"k":12,"m":16,"orbit_denominator":94287574930136330269034414851507354504598135030000123904000,"orbit_numerator":1443683222724257025624508601593880461771505974797926400,"probability":[253030902849,16525557571414640],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,2147254097595254047292973293800293138432000,5862003686435043549109817092074800267919360000,7387026491629144878578232584797644460696535040000,4939659388259603287581517732111828946922095247360000,1438736170445354852659409702472073769811522621957734400]},{"header_fiber":11544872091648,"k":13,"m":16,"orbit_denominator":2896514301853788065864737224238305930381254708121603806330880000,"orbit_numerator":44268835510967538865712937871387567789689807572217888768000,"probability":[1677773981473,109776918152968680],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,12005383549818969188576905404569190948698849280000,45385890764569466133984661000996727566519511285760000,70814956990089672730768638207555179783075157466152960000,44197975156081301073697066059942106208609974946541600768000]},{"header_fiber":402653184,"k":14,"m":16,"orbit_denominator":83048858062751811424473745693360707635891334991262624335118991360000,"orbit_numerator":1268114703767265857960091247898125967345035741666103091265536000,"probability":[716253943,46907485476180],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,185900608571676533284801171460082596112463918226472960000,870174191494221898515685026294438049174427534944087572480000,1267244343675163064385042278070660069213265201667240777220096000]},{"header_fiber":16384,"k":15,"m":16,"orbit_denominator":2041008735750188517567866774160032750859665448745270255659884331663360000,"orbit_numerator":31150925457137528136119439517599945897484042506540371306354835456000,"probability":[65549,4294770690],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,7128466976720665792640491735404036498836910366261965393756160000,31143796990160807470326799025864541860985205596174109340961079296000]},{"header_fiber":1,"k":16,"m":16,"orbit_denominator":33439887126531088671831929227837976590084758712242507868731544889972490240000,"orbit_numerator":510259969886794669593834275239764653850381608487716607442306323185664000,"probability":[1,65535],"support_histogram":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,510259969886794669593834275239764653850381608487716607442306323185664000]}],"schema_version":1,"small_gl":[{"gl_count":6,"joint_first_k":[3,2],"m":2,"mask_histogram":[2,1,1,2],"record_sha256":"3bba2177840a4fe8a5084ae0152f95ea20d69de19afa28a954878698b3d02010"},{"gl_count":168,"joint_first_k":[54,32,24],"m":3,"mask_histogram":[78,14,14,8,14,8,8,24],"record_sha256":"6f6f47f8cc6df37c47f34956e3de77e196e72c3e3410fd19bbbf1f3435ab7275"},{"gl_count":20160,"joint_first_k":[4536,2352,1632,1344],"m":4,"mask_histogram":[10944,1032,1032,432,1032,432,432,288,1032,432,432,288,432,288,288,1344],"record_sha256":"b5afda7d17d3ef6e66d7bde49f5b3042cc202ff47c4925edb8554cc63d28eb62"}],"source_manifest_sha256":"680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9"} diff --git a/research/common-image-full-guard-family/RUN-RECORDS.json b/research/common-image-full-guard-family/RUN-RECORDS.json new file mode 100644 index 0000000000..f4c5c08eb9 --- /dev/null +++ b/research/common-image-full-guard-family/RUN-RECORDS.json @@ -0,0 +1,467 @@ +{ + "schema_version": 1, + "environment": { + "python_executable": "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "python_version": "3.12.14", + "platform": "macOS arm64", + "dependencies": "stdlib only", + "concurrency": "One scientific child at a time; other agents limited to static review/metadata." + }, + "advance_claim": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19385133", + "status": "rendered before candidate execution" + }, + "primary_first": { + "RESULT.json_bytes": 41343, + "RESULT.json_sha256": "b9e98971c5202d76f34e439b86d634cfcb21bb6b0b3afa5b75599b2c0f914b20", + "SMALL-GL.json.gz_bytes": 51428, + "SMALL-GL.json.gz_sha256": "cb8fb0d740b464caede975d02eb2391a633d8f231db5b305f23a83063f7b19f2", + "child_maxrss_bytes_darwin": 36519936, + "command": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/verify.py", + "--emit", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/RESULT.json", + "--write-small", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/SMALL-GL.json.gz" + ], + "elapsed_seconds": 0.51401, + "returncode": 0, + "utc_after_first": "2026-11-03T22:57:24.349836+00:00" + }, + "primary_strict_modes": [ + { + "command": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/verify.py" + ], + "cumulative_child_maxrss_bytes_darwin": 31604736, + "elapsed_seconds": 0.502857, + "label": "RETAINED", + "returncode": 0, + "utc_finished": "2026-11-03T22:59:20.813547+00:00" + }, + { + "command": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "-O", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/verify.py" + ], + "cumulative_child_maxrss_bytes_darwin": 36798464, + "elapsed_seconds": 0.540966, + "label": "OPTIMIZED-RETAINED", + "returncode": 0, + "utc_finished": "2026-11-03T22:59:21.354855+00:00" + }, + { + "command": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/verify.py", + "--emit", + "/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/PRIMARY-REEMIT.json", + "--write-small", + "/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/PRIMARY-REGENERATED-SMALL-GL.json.gz" + ], + "cumulative_child_maxrss_bytes_darwin": 36798464, + "elapsed_seconds": 0.518827, + "label": "EMIT", + "returncode": 0, + "utc_finished": "2026-11-03T22:59:21.873838+00:00" + }, + { + "command": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "-O", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/verify.py", + "--emit", + "/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/PRIMARY-OPT-REEMIT.json" + ], + "cumulative_child_maxrss_bytes_darwin": 36929536, + "elapsed_seconds": 0.535172, + "label": "OPTIMIZED-EMIT", + "returncode": 0, + "utc_finished": "2026-11-03T22:59:22.409263+00:00" + } + ], + "primary_regeneration": { + "canonical_small_sha256": "9a0f1d17822fcf9c404b9fafe049faed6cc543ffde92c32569014693d4ce8c2d", + "code_unchanged_since_first": true, + "decompressed_bytes": 204314, + "decompressed_canonical_value_equal": true, + "first_artifact_unchanged": true, + "first_receipt_unchanged": true, + "gzip_container_equality_required": false, + "result_sha256": "b9e98971c5202d76f34e439b86d634cfcb21bb6b0b3afa5b75599b2c0f914b20", + "utc": "2026-11-03T22:59:22.414139+00:00" + }, + "oracle_blind_first": { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/oracle.py", + "--emit", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/ORACLE.json" + ], + "canonical_receipt_sha256": "b9e98971c5202d76f34e439b86d634cfcb21bb6b0b3afa5b75599b2c0f914b20", + "code_after_sha256": "11a16a48536271d802d58e0456a2708a559f4ab889b391762ae28ba72018d4a7", + "code_before_sha256": "11a16a48536271d802d58e0456a2708a559f4ab889b391762ae28ba72018d4a7", + "elapsed_seconds": 0.6350185424089432, + "exit_code": 0, + "peak_rss_bytes_macos": 30949376, + "primary_data_read": false, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "receipt_sha256": "c798ba1f88169b34de48d823fc4ed8257c253aaea858fce8d30bb68d2d224806", + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stdout_sha256": "cfc95a26d0d11152a61c978fe32359fec213f81ee45e72d4ab4372be421daeb0", + "utc_finished": "2026-11-03T22:57:50.513346+00:00", + "utc_started": "2026-11-03T22:57:49.878546+00:00" + }, + "oracle_actual_modes": [ + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/oracle.py", + "--check-primary", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/RESULT.json" + ], + "code_sha256": "11a16a48536271d802d58e0456a2708a559f4ab889b391762ae28ba72018d4a7", + "elapsed_seconds": 0.628040624782443, + "exit_code": 0, + "peak_rss_bytes_macos": 38060032, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "source_cases_schema": { + "CASES.json": "3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273", + "SCHEMA.json": "c01cd12853adcce258701b3d8e56bfff7ba9d370223dcecccc62200ef8bd087a", + "SOURCE-PINS.json": "680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9" + }, + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stdout_sha256": "d2ae377633ab28ae8d40b69a7da490a0d10b070186267d12b5693727d7d8d906", + "utc_finished": "2026-11-03T23:01:28.507067+00:00", + "utc_started": "2026-11-03T23:01:27.879394+00:00" + }, + { + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-O", + "-W", + "error", + "-B", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/oracle.py", + "--check-primary", + "/private/tmp/crocswap-b9/research/common-image-full-guard-family/RESULT.json" + ], + "code_sha256": "11a16a48536271d802d58e0456a2708a559f4ab889b391762ae28ba72018d4a7", + "elapsed_seconds": 0.6832929588854313, + "exit_code": 0, + "peak_rss_bytes_macos": 38567936, + "python": "3.12.14 (main, Aug 25 2026, 13:50:33) [Clang 22.1.3 ]", + "source_cases_schema": { + "CASES.json": "3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273", + "SCHEMA.json": "c01cd12853adcce258701b3d8e56bfff7ba9d370223dcecccc62200ef8bd087a", + "SOURCE-PINS.json": "680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9" + }, + "stderr_sha256": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "stdout_sha256": "d2ae377633ab28ae8d40b69a7da490a0d10b070186267d12b5693727d7d8d906", + "utc_finished": "2026-11-03T23:01:29.190721+00:00", + "utc_started": "2026-11-03T23:01:28.507813+00:00" + } + ], + "independence": "Neither engine read peer code or scientific data before its first seal; no predecessor executable or peer code imported/executed. Actual peer data read after both firsts for whole-profile and full small-header comparisons.", + "common_canonical_sha256": "b9e98971c5202d76f34e439b86d634cfcb21bb6b0b3afa5b75599b2c0f914b20", + "small_records_canonical_sha256": "9a0f1d17822fcf9c404b9fafe049faed6cc543ffde92c32569014693d4ce8c2d", + "scientific_failures": [], + "root_external_rejections": { + "pre_execution_seal": { + "utc_before_first": "2026-11-03T23:10:38.591569+00:00", + "code_sha256": "2f0e37601771e20bb9cae4ecdf685717ad967b13b84d6e44e4bf4417faeff480", + "purpose": "Actual CLI/source/schema/receipt and complete GL record binding mutants, including histogram-preserving swaps and duplicates." + }, + "evidence_sha256": "99442f562d1c1d56b1b48a12cac1faba34e360311273d793a429815ff42c9cfa", + "control_count": 21, + "runs": [ + { + "case": "source-primary", + "script": "verify.py", + "exit": 1, + "seconds": 0.1255052089691162, + "intended_reason": "source", + "matched": true, + "stderr": "FAIL: source bytes/SHA256\n" + }, + { + "case": "cases-primary", + "script": "verify.py", + "exit": 1, + "seconds": 0.08966429065912962, + "intended_reason": "CASES.json", + "matched": true, + "stderr": "FAIL: immutable CASES.json\n" + }, + { + "case": "schema-primary", + "script": "verify.py", + "exit": 1, + "seconds": 0.08589283376932144, + "intended_reason": "SCHEMA.json", + "matched": true, + "stderr": "FAIL: immutable SCHEMA.json\n" + }, + { + "case": "source-oracle", + "script": "oracle.py", + "exit": 1, + "seconds": 0.08462495822459459, + "intended_reason": "pinned source", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: pinned source bytes changed\n" + }, + { + "case": "cases-oracle", + "script": "oracle.py", + "exit": 1, + "seconds": 0.08417204208672047, + "intended_reason": "source/cases/schema", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: source/cases/schema digest changed\n" + }, + { + "case": "schema-oracle", + "script": "oracle.py", + "exit": 1, + "seconds": 0.0825509587302804, + "intended_reason": "source/cases/schema", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: source/cases/schema digest changed\n" + }, + { + "case": "missing-primary", + "script": "verify.py", + "exit": 1, + "seconds": 0.82148745842278, + "intended_reason": "No such file", + "matched": true, + "stderr": "FAIL: [Errno 2] No such file or directory: '/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/MUTANT/RESULT.json'\n" + }, + { + "case": "missing-oracle", + "script": "oracle.py", + "exit": 1, + "seconds": 0.10960070788860321, + "intended_reason": "No such file", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: [Errno 2] No such file or directory: '/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/MUTANT/ORACLE.json'\n" + }, + { + "case": "missing-records", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6815422503277659, + "intended_reason": "No such file", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: [Errno 2] No such file or directory: '/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/MUTANT/SMALL-GL.json.gz'\n" + }, + { + "case": "version-bool-primary", + "script": "verify.py", + "exit": 1, + "seconds": 0.5368874175474048, + "intended_reason": "version", + "matched": true, + "stderr": "FAIL: receipt version\n" + }, + { + "case": "version-bool-peer", + "script": "oracle.py", + "exit": 1, + "seconds": 0.673986959271133, + "intended_reason": "version", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: receipt schema_version must be integer1\n" + }, + { + "case": "duplicate-peer", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6837103748694062, + "intended_reason": "duplicate", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: duplicate JSON key: schema_version\n" + }, + { + "case": "nonfinite-peer", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6973036667332053, + "intended_reason": "noninteger", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: noninteger JSON number: NaN\n" + }, + { + "case": "support-preserved-total", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6938527505844831, + "intended_reason": "primary receipt differs", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual complete primary receipt differs\n" + }, + { + "case": "example-header", + "script": "oracle.py", + "exit": 1, + "seconds": 0.7072057500481606, + "intended_reason": "primary receipt differs", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual complete primary receipt differs\n" + }, + { + "case": "example-minor", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6934897918254137, + "intended_reason": "primary receipt differs", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual complete primary receipt differs\n" + }, + { + "case": "ratio-flag-int", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6887553753331304, + "intended_reason": "bool", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: example comparison must be bool\n" + }, + { + "case": "mask-histogram-preserved", + "script": "oracle.py", + "exit": 1, + "seconds": 0.677071874961257, + "intended_reason": "actual complete primary GL records differ", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual complete primary GL records differ\n" + }, + { + "case": "duplicate-header-same-mask", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6993903340771794, + "intended_reason": "actual complete primary GL records differ", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual complete primary GL records differ\n" + }, + { + "case": "record-mask-bool", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6837545419111848, + "intended_reason": "two integers", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual GL record needs two integers\n" + }, + { + "case": "artifact-version-bool", + "script": "oracle.py", + "exit": 1, + "seconds": 0.6965714581310749, + "intended_reason": "version", + "matched": true, + "stderr": "FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: actual GL artifact version invalid\n" + } + ], + "all_intended": true, + "mutant_restored": true, + "scope": "Root-owned external controls in a temporary mutant copy. Original scientific code, immutable inputs, receipts and submitted certificate unchanged." + }, + "registered_committed_export_cold": "pending root evidence", + "publication_ci": "pending", + "static_review": { + "reviewer": "separate AI static reviewer", + "scope": "complete scientific code and final proof/metadata; no independent execution or human/formal-kernel acceptance", + "outcome": "No material objection; one terminology clarification only.", + "final_proof_sha256": "51fbfb9ea8f4f5bcb5023abab0824d448f960676757b0d23c3f5c646e6f895d8" + }, + "root_registered_commit_export": [ + { + "name": "REGISTERED", + "exit": 0, + "seconds": 2.7850987501442432, + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "scripts/research_package.py", + "--package", + "research/common-image-full-guard-family" + ] + }, + { + "name": "COMMIT-CHECK", + "exit": 0, + "seconds": 0.20010424964129925, + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "scripts/check_research_commit.py", + "--package", + "research/common-image-full-guard-family", + "--check-source-history", + "--check-modes" + ] + }, + { + "name": "INITIAL-EXPORT", + "exit": 0, + "seconds": 0.09082883317023516, + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "scripts/export_research_package.py", + "export", + "--package", + "research/common-image-full-guard-family", + "--ref", + "HEAD", + "--output", + "/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/INITIAL-PACKAGE.tar" + ] + }, + { + "name": "INITIAL-EXPORT-CHECK", + "exit": 0, + "seconds": 0.0443576667457819, + "argv": [ + "/Users/evaayala/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "scripts/export_research_package.py", + "check", + "/private/tmp/contribution-batch-b10-20261103T1814Z/session-07/INITIAL-PACKAGE.tar", + "--check-inputs" + ] + } + ], + "science_freeze_utc": "2026-11-03T23:17:28.551866+00:00" +} diff --git a/research/common-image-full-guard-family/SCHEMA.json b/research/common-image-full-guard-family/SCHEMA.json new file mode 100644 index 0000000000..5eaeb05502 --- /dev/null +++ b/research/common-image-full-guard-family/SCHEMA.json @@ -0,0 +1,18 @@ +{ + "actual_span_oracle": "At m7k6 independently enumerate literalpropercolumnchoices and full quotient spans inF2^6/, aggregatebyj. This validates DP count, notGL7enumeration. No 6515/6694 spectrum/predecessorchecker execution.", + "admission": "Exacttypedkeys,duplicate/nonfinite/float/boolasint guards. Auth8sourceobjects/source manifest+CASES prior math. FreezeSCHEMAbytes inpreseals; runtimeSCHEMAauthenticationifimplementedmustbespecifiedwithoutassumingbothenginesreadunusedmetadata. Source docs inert only. Retainedwholeprofile compares actualcounts/histograms/witness, notpassflags.", + "artifact": "Optional SMALL-GL.json.gz exactkeys schema_version,domains; domains in2,3,4order each exactkeys m,records. Allactualrecords asdefinedabove, bounded<=8MiBdecompressed. If retained, both engines compare complete canonical record values/types; metadata input declaration required.", + "canonical": "Compactjsonsort_keys=True,separators=(comma,colon),UTF8+LF. Rational pair [num,den] reduced with den>0; allcount/bit/header values strictint excludingbool.", + "common_keys": [ + "schema_version", + "source_manifest_sha256", + "case_manifest_sha256", + "family", + "small_gl", + "example" + ], + "example": "Exactkeys m,k,u,v_rows,header_rows,proper_minors,joint_probability,single_probability,product_probability,ratio,ratio_gt_one. Tuple/header bindCASESexample, proper_minors6lists of6GF2integerdets; ratio_gt_one strictbool. Structural distinct/rank/idempotent/noncommuting/commonimage controls must be actualchecks. Probability/ratio exactreducedpairs; source marginal s_m=3^(m-1)/[(2^m-1)2^(m-1)].", + "family": "List inCASESfamilyorder. Exactkeys m,k,support_histogram,orbit_numerator,orbit_denominator,probability,header_fiber. Hist lengthm indexedj; all nonnegativeintegers; numerator=sumhist; denominatorpositive; probabilityreducednum/den; header_fiber=|GL_m(F2)|/orbit_denominator integer. Primarybinomial/fullrankproduct, oracleindependentbivariatecolumn-rankDP; no primarycodeimport.", + "schema_version": 1, + "small_gl": "List inCASESdimensionorder. Exactkeys m,gl_count,mask_histogram,joint_first_k,record_sha256. Hist length2^m full passingmask counts, joint_first_k listm countfirstkpassed, digestcompactJSON+LF actualsorted [[header_code,mask],...] for everyinvertibleheader. Literal conjugation and EVERYproperleadingdeterminant, notpartialproduct-only orfirstpivotproxy." +} diff --git a/research/common-image-full-guard-family/SMALL-GL.json.gz b/research/common-image-full-guard-family/SMALL-GL.json.gz new file mode 100644 index 0000000000..1d782b5a97 Binary files /dev/null and b/research/common-image-full-guard-family/SMALL-GL.json.gz differ diff --git a/research/common-image-full-guard-family/SOURCE-PINS.json b/research/common-image-full-guard-family/SOURCE-PINS.json new file mode 100644 index 0000000000..838ef1a91f --- /dev/null +++ b/research/common-image-full-guard-family/SOURCE-PINS.json @@ -0,0 +1,86 @@ +{ + "files": [ + { + "bytes": 2808, + "commit": "f6cf478e2550e747074a746a4038a74b321ceb6f", + "git_blob": "83ec7c9f997320b2889c9f8feb9a9378349ff331", + "local_path": "inputs/6515-README.md", + "pr": 6515, + "repository": "unpaidmoon/integer-mult-bounds", + "sha256": "0dcbb3cdac1d5c6252489f2fd7767b90ab532ecb359f11d027415f5697d9e860", + "source_path": "research/six-event-guard-correlation/README.md" + }, + { + "bytes": 6613, + "commit": "f6cf478e2550e747074a746a4038a74b321ceb6f", + "git_blob": "fcc1b102176ca84ef68c0b1d13345c4d840ce315", + "local_path": "inputs/6515-PROOF.md", + "pr": 6515, + "repository": "unpaidmoon/integer-mult-bounds", + "sha256": "e8be89172bbc2dffd6296f845502ab3d4c25e26dc751e61a844f9546e4093204", + "source_path": "research/six-event-guard-correlation/PROOF.md" + }, + { + "bytes": 7835, + "commit": "f6cf478e2550e747074a746a4038a74b321ceb6f", + "git_blob": "9e139624812d0346177f342f81aad090096f56ab", + "local_path": "inputs/6515-TASK.json", + "pr": 6515, + "repository": "unpaidmoon/integer-mult-bounds", + "sha256": "e5f627ce18fcbcab0935e897e8a4e757f8cb743a276d0862701bab9c2a263ec1", + "source_path": "research/six-event-guard-correlation/TASK.json" + }, + { + "bytes": 5970, + "commit": "bd8ea82bb0a7e40427d6d4fc1477fda0ab40388b", + "git_blob": "08535a3694325873810a42d7022a85fb714e0555", + "local_path": "inputs/4807-README.md", + "pr": 4807, + "repository": "petalas/integer-mult-bounds", + "sha256": "53607e82913b1f0124aa46719f97f782c0e8db7f29de4c23fb9833776f6996e7", + "source_path": "research/common-covector-header-law/README.md" + }, + { + "bytes": 5856, + "commit": "bd8ea82bb0a7e40427d6d4fc1477fda0ab40388b", + "git_blob": "8c0baf75700a470a009dbd67cdb6b4a33efbd9d7", + "local_path": "inputs/4807-PROOF.md", + "pr": 4807, + "repository": "petalas/integer-mult-bounds", + "sha256": "9c9bfc2cab96c5451f819292de156ae36b04447db7ca1a0fd33cd71682f24044", + "source_path": "research/common-covector-header-law/PROOF.md" + }, + { + "bytes": 6898, + "commit": "a3ba3670815329ac69c84c0ea0fefcfa16d7cbff", + "git_blob": "830650a2a4f954d0170e138c17eed5967d21a824", + "local_path": "inputs/4275-README.md", + "pr": 4275, + "repository": "petalas/integer-mult-bounds", + "sha256": "b7a6cf666e30a4ef135aa7190fe545dd7203cd1ffcc175138bd3dda7484155f2", + "source_path": "research/corankone-triple-header-law/README.md" + }, + { + "bytes": 7205, + "commit": "a3ba3670815329ac69c84c0ea0fefcfa16d7cbff", + "git_blob": "c36c3137027fe71f52ccf7c94add1758c39123a8", + "local_path": "inputs/4275-PROOF.md", + "pr": 4275, + "repository": "petalas/integer-mult-bounds", + "sha256": "1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f", + "source_path": "research/corankone-triple-header-law/PROOF.md" + }, + { + "bytes": 6316, + "commit": "66d43a6c84bd13a93a9c2050de8b90eb75aa98ea", + "git_blob": "58bbe1ff1d019c9c8d6bb61423ba9cad0244bada", + "local_path": "inputs/6694-README.md", + "pr": 6694, + "repository": "petalas/integer-mult-bounds", + "sha256": "7f05555b8294399246cc09fb93846b077edf37a9703016c453de81a703fb1526", + "source_path": "research/seven-event-guard-correlation/README.md" + } + ], + "schema_version": 1, + "scope": "Eight immutable inert source prose/metadata files; no source executable imported or run. Direct released request6694Q3;6515Q2 broad motivation only;4807largerfamilies excluded, not an explicit request." +} diff --git a/research/common-image-full-guard-family/SOURCES.json b/research/common-image-full-guard-family/SOURCES.json new file mode 100644 index 0000000000..75ea7c3d55 --- /dev/null +++ b/research/common-image-full-guard-family/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } + ] +} diff --git a/research/common-image-full-guard-family/SOURCES.md b/research/common-image-full-guard-family/SOURCES.md new file mode 100644 index 0000000000..e92081c221 --- /dev/null +++ b/research/common-image-full-guard-family/SOURCES.md @@ -0,0 +1,22 @@ +# Source contract + +Canonical catalogue and selected record are historical provenance in SOURCES.json. They do not transfer supplier admission. The eight external objects below are vendored exact and authenticated by both direct engines before computation. They are inert prose/metadata, not source executables. No pending external Git-object dependency is needed for direct replay. + +- PR6515: `unpaidmoon/integer-mult-bounds@f6cf478e2550e747074a746a4038a74b321ceb6f` / `research/six-event-guard-correlation/README.md`; local `inputs/6515-README.md`; Git blob `83ec7c9f997320b2889c9f8feb9a9378349ff331`, SHA256 `0dcbb3cdac1d5c6252489f2fd7767b90ab532ecb359f11d027415f5697d9e860`. + +- PR6515: `unpaidmoon/integer-mult-bounds@f6cf478e2550e747074a746a4038a74b321ceb6f` / `research/six-event-guard-correlation/PROOF.md`; local `inputs/6515-PROOF.md`; Git blob `fcc1b102176ca84ef68c0b1d13345c4d840ce315`, SHA256 `e8be89172bbc2dffd6296f845502ab3d4c25e26dc751e61a844f9546e4093204`. + +- PR6515: `unpaidmoon/integer-mult-bounds@f6cf478e2550e747074a746a4038a74b321ceb6f` / `research/six-event-guard-correlation/TASK.json`; local `inputs/6515-TASK.json`; Git blob `9e139624812d0346177f342f81aad090096f56ab`, SHA256 `e5f627ce18fcbcab0935e897e8a4e757f8cb743a276d0862701bab9c2a263ec1`. + +- PR4807: `petalas/integer-mult-bounds@bd8ea82bb0a7e40427d6d4fc1477fda0ab40388b` / `research/common-covector-header-law/README.md`; local `inputs/4807-README.md`; Git blob `08535a3694325873810a42d7022a85fb714e0555`, SHA256 `53607e82913b1f0124aa46719f97f782c0e8db7f29de4c23fb9833776f6996e7`. + +- PR4807: `petalas/integer-mult-bounds@bd8ea82bb0a7e40427d6d4fc1477fda0ab40388b` / `research/common-covector-header-law/PROOF.md`; local `inputs/4807-PROOF.md`; Git blob `8c0baf75700a470a009dbd67cdb6b4a33efbd9d7`, SHA256 `9c9bfc2cab96c5451f819292de156ae36b04447db7ca1a0fd33cd71682f24044`. + +- PR4275: `petalas/integer-mult-bounds@a3ba3670815329ac69c84c0ea0fefcfa16d7cbff` / `research/corankone-triple-header-law/README.md`; local `inputs/4275-README.md`; Git blob `830650a2a4f954d0170e138c17eed5967d21a824`, SHA256 `b7a6cf666e30a4ef135aa7190fe545dd7203cd1ffcc175138bd3dda7484155f2`. + +- PR4275: `petalas/integer-mult-bounds@a3ba3670815329ac69c84c0ea0fefcfa16d7cbff` / `research/corankone-triple-header-law/PROOF.md`; local `inputs/4275-PROOF.md`; Git blob `c36c3137027fe71f52ccf7c94add1758c39123a8`, SHA256 `1490daed4867cd92539f85538b81d8e3469bace39a16b7d4b6582745d5bc1e4f`. + +- PR6694: `petalas/integer-mult-bounds@66d43a6c84bd13a93a9c2050de8b90eb75aa98ea` / `research/seven-event-guard-correlation/README.md`; local `inputs/6694-README.md`; Git blob `58bbe1ff1d019c9c8d6bb61423ba9cad0244bada`, SHA256 `7f05555b8294399246cc09fb93846b077edf37a9703016c453de81a703fb1526`. + + +6694Q3 is the direct released shared-direction question.6515Q2 is broad motivation; its possible one-pair/four-orthogonal reading remains open.4807 proves the k2 transpose-dual and excludes larger families, rather than explicitly requesting them.4275 supplies binary full-guard context.4227/4261 and further lineage retain credit via the exact source notices. The current predicate is every proper leading minor of corank-one complements;4240 rank-one first-pivot requests are separate. diff --git a/research/common-image-full-guard-family/TASK.json b/research/common-image-full-guard-family/TASK.json new file mode 100644 index 0000000000..095961be05 --- /dev/null +++ b/research/common-image-full-guard-family/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the complete binary uniform-header full-guard count for all m>=2,1<=k<=m with independent normalized covectors and one common image, and independently validate bounded finite domains.", + "scope_change_reason": "Take6694READMEQ3 shared-direction continuation; k>=3 is new scope, k1/k2 retain prior credit. This is a mathematical header-count side result, not the original changed paid/target-invoice acceptance gate.", + "bottleneck_link": "Quantifies dependence of a precise nonorthogonal complement full-guard family before any producer/caller applicability or pricing can be asserted.", + "budget_minutes": 60, + "stop_rule": "One common-image binary full-guard family only; preserve frozen inputs/first failures; science cutoff23:27:03UTC, final15minutes verification/handoff; stop if orbit/fiber proof or complete small census disagrees.", + "outcome": "completed", + "evidence": "Scoped all-dimension proof;135 rows,20334 complete small headers, actual retained record comparisons,374-span oracle and exact22/2667 m7k6 example. Original paid/target invoice gate remains unmet. Transport/publication tracked separately.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance with separate AI primary, independent oracle and static review; no independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "What is the full-guard law for one coupled pair plus four otherwise orthogonal kernels?", + "why_it_matters": "That narrower reading of6515Q2 is a different partial-Gram orbit from all six sharing one image.", + "first_step": "Write one normalized binary partial-Gram tuple and prove its precise complement/full-minor predicate.", + "blocked_by": "The present common-image orbit does not cover this mixed family." + }, + { + "question": "Can a named physical caller supply and use these complete headers?", + "why_it_matters": "A counting probability does not price selection or produce a compatible supplier.", + "first_step": "Pin one producer/header domain and complete selection, emission, dispatch, restoration, stock and precision costs.", + "blocked_by": "No physical producer, actual caller or complete paid/target invoice is supplied." + }, + { + "question": "What remains true for odd fields or restricted header distributions?", + "why_it_matters": "The binary prefix equivalence and complete uniform orbit are essential assumptions.", + "first_step": "Derive the changed prefix constraints and actual orbit weights before transferring the count.", + "blocked_by": "No nonbinary or restricted-header law/sign theorem is proved." + } + ] +} diff --git a/research/common-image-full-guard-family/VALIDATION.md b/research/common-image-full-guard-family/VALIDATION.md new file mode 100644 index 0000000000..9427e90d55 --- /dev/null +++ b/research/common-image-full-guard-family/VALIDATION.md @@ -0,0 +1,74 @@ +# Validation and limits + +The advance public CLAIM19385133 preceded candidate execution. Source8, +cases and schema bytes/code were frozen in separate pre-execution seals. +Primary first22:57:23.817903→22:57:24.349836UTC passed in0.514010s, +36,519,936B direct child peak RSS on macOS. Independent oracle first +22:57:49.878546→22:57:50.513346UTC passed in0.635019s,30,949,376B. +Neither read peer code or results before its first seal. Both firsts retain +full code/argv/OS-UTC/status/stdout/stderr/receipts; no first failures occurred. +Primary source7973ec334302d04df39d307b313f15d4abf3733082274138861d486e676d4aea +and oracle11a16a48536271d802d58e0456a2708a559f4ab889b391762ae28ba72018d4a7 +remain unchanged. + +Four additional primary normal/optimized retained/emission modes passed by +22:59:22.409263UTC,0.50–0.54s per run. Original RESULT and sidecar bytes +remain unchanged; a separate regeneration matches every decompressed +canonical sidecar value. Oracle normal/optimized --check-primary modes +passed by23:01:29.190721UTC,0.628–0.683s, comparing every actual submitted +header record as data. Canonical whole-profile SHA256 is +b9e98971c5202d76f34e439b86d634cfcb21bb6b0b3afa5b75599b2c0f914b20; +canonical decompressed small-certificate SHA256 is +9a0f1d17822fcf9c404b9fafe049faed6cc543ffde92c32569014693d4ce8c2d. +Gzip container bytes are immutable first evidence, but not regenerated +mathematical equality. RUN-RECORDS.json preserves exact run details; +its primary later RSS labels are cumulative child maxima, not per-child claims. + +All135(m,k)rows agree. Actual literalGL2/3/4 complete censuses total20,334 +headers, with every proper minor and actual tuple/fiber coverage checked. +The oracle uses independent column/rank/support DP and literal quotient-span +states at(7,6),374subspaces, not an imported product-formula implementation. +It also independently regenerates all actual small-header records. The exact +m7k6 example checks rank-one idempotence, common image, independence, +distinct noncommutation and36proper minors. CompleteGL7, prior2^30/2^42 +spectra and arbitrary-family/native/physical checks were not run. + +The separate static AI review passed the final proof/metadata and found no +material code/counting objection. Its sole terminology clarification changed +"rank-one marginal" to "corank-one full-guard marginal" to keep the excluded +first-pivot interface distinct. The preceding proof copy remains preserved; +final PROOF SHA256 is +51fbfb9ea8f4f5bcb5023abab0824d448f960676757b0d23c3f5c646e6f895d8. +This was prose only, without scientific code/input/receipt changes. + +Root's 21 external controls all rejected for their intended reasons. Its +harness was sealed before the first run at 23:10:38.591569 UTC; source SHA256 +2f0e37601771e20bb9cae4ecdf685717ad967b13b84d6e44e4bf4417faeff480. +Source/case/schema drift, missing receipts/certificate, duplicate/nonfinite +JSON, boolean version aliases, changed support histogram with preserved total, +example header/minor changes and comparison-flag type drift reject. The actual +small-header data checks also reject a passing-mask swap preserving the mask +histogram and a duplicate header with the same mask, so an aggregate-only +comparison would be insufficient. Boolean record masks and artifact version +aliases reject. Every retained external run exited 1 with its intended +first-line diagnostic; the temporary mutant copy was restored. The original +scientific code, inputs, receipts and submitted certificate are unchanged. +RUN-RECORDS.json retains all 21 cases and the pre-execution harness seal. + +After the science freeze at 23:17:28.551866 UTC, all four registered commands, +committed-byte/source-history/mode checks, official initial export and its +declared-input check passed on local commit 7404306b. The final official +archive and empty-PATH/read-only cold replay follow this documentation commit; +they are not yet claimed here. Hosted CI and publication remain pending. +The first staging attempt correctly refused paths outside the sparse checkout; +using git add --sparse staged only this package. No scientific bytes changed. +Passing transport checks does not establish supplier admission or formal/human +theorem acceptance. + +The all-dimension theorem rests on PROOF.md, not the finite domains. Conditions +include binary field, complete equally weighted invertible headers, +independent normalized covectors and all kernels sharing the same image. +The mixed one-pair/four-orthogonal reading, rank-one first-pivot request model, +odd fields, restricted headers, header production/selection/emission/dispatch, +restoration/stock/precision and full paid caller/outer obligations remain open. +No source executable/peer code was imported or executed, and no frontier changed. diff --git a/research/common-image-full-guard-family/VERIFY.json b/research/common-image-full-guard-family/VERIFY.json new file mode 100644 index 0000000000..048d0151b7 --- /dev/null +++ b/research/common-image-full-guard-family/VERIFY.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/common-image-full-guard-family/SMALL-GL.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Closed count plus literal complete GL2/3/4 orbit/minor/fiber checks and actual retained20334header records" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Closed count plus literal complete GL2/3/4 orbit/minor/fiber checks and actual retained20334header records" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/oracle.py", + "--check-primary", + "{package}/RESULT.json" + ], + "timeout_seconds": 180, + "checks": "Independent rank/support DP,374span states and actual submitted20334header-record comparisons" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/oracle.py", + "--check-primary", + "{package}/RESULT.json" + ], + "timeout_seconds": 180, + "checks": "Independent rank/support DP,374span states and actual submitted20334header-record comparisons" + } + ] +} diff --git a/research/common-image-full-guard-family/inputs/4275-PROOF.md b/research/common-image-full-guard-family/inputs/4275-PROOF.md new file mode 100644 index 0000000000..c36c313702 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/4275-PROOF.md @@ -0,0 +1,162 @@ +# Several corank-one requests with orthogonal kernels + +## Contract and claim type + +This is a scoped counting proof. Let K be a finite field of order q, let +2 <= k <= m, and let U_1, ..., U_k be rank-one idempotents on K^m with +U_s U_t = 0 for s != t. Put P_t = I - U_t. A header G in GL_m(K) passes a +request R when every leading principal minor of G R G^-1 of orders 1 +through rank(R) is nonzero. We count headers passing all k requests, with +each complete header weighted equally. + +For k = 2 this is the overlapping corank-one pair of #4261. For k >= 3 the +requests are pairwise commuting, pairwise overlapping when m > 2, and +neither nested nor orthogonal, so the laminar law of #4259 and the +orthogonal law of #4246 do not apply. + +## Theorem 1: transfer law over every finite field + +For a k by k matrix A over K, define + +```text +w(A) = 2q^k - 1 if A = 0, + q - 1 if rank(A) = 1, + 0 if rank(A) >= 2. + +S_k = {A : A_tt != 1 for every t}. +f_0 = indicator of the zero matrix. +f_(j+1)(B) = sum_(A in S_k) f_j(A) w(B - A), B in S_k. +C(q,m,k) = sum_(A in S_k) f_(m-1)(A) w(I_k - A). +D(q,m,k) = q^(k(m-k)) prod_(i=0)^(k-1) (q^m - q^i). +``` + +**Theorem 1.** The joint passing fraction is C(q,m,k)/D(q,m,k), and the +number of passing headers is C(q,m,k)|GL_(m-k)(K)|. The state space S_k has +q^(k(k-1))(q-1)^k elements. + +**Proof.** This is #4261's argument with a k by k partial Gram matrix. +Orthogonality gives K^m = im(U_1) + ... + im(U_k) + (intersection of the +kernels), so after a fixed basis change, which permutes the header domain, +U_t = e_t e_t^T. Let X = (u_1, ..., u_k) be the first k columns of G and Y +the first k rows of G^-1, with rows a_1, ..., a_k. Then YX = I_k and the +conjugated requests are I - u_t a_t. Every pair with YX = I_k arises, with +exactly |GL_(m-k)(K)| completions (an ordered basis of ker Y). There are +prod_(i= 2, a header passing all k requests +exists if and only if m >= k + 1. + +**Proof.** Existence: the k rectangles {t} x ([k] \ {t}) sum to J - I_k. +For m - 1 >= k, take them in any order followed by m - 1 - k zero steps; +every intermediate state has zero diagonal. Then append J. + +Necessity: suppose J - I_k = sum_(r=1)^n y_r x_r^T with supp(y_r) and +supp(x_r) disjoint, so x_r^T y_r = 0 for every r. Write it as Y'X' with Y' +of size k by n. If k is even, (J - I_k)^2 = kJ - 2J + I_k = I_k over F_2, so J - I_k is +invertible and n >= k. If k is +odd, E = J - I_k satisfies E^2 = E, has rank k - 1 and kernel spanned by +the all-ones vector. If n <= k - 1 then n = k - 1, Y' is injective and X' +is surjective, and Y'X'Y'X' = Y'X' gives X'Y' = I_(k-1). Its diagonal +entries are x_r^T y_r = 0, a contradiction. Hence n >= k in both cases, +that is m >= k + 1. QED. + +At m = k + 1 every step is a rectangle. The replay finds exactly 2 k! +ordered decompositions for k = 3, 4 (the row and column decompositions in +every order), and 2 for k = 2. This count is a finite observation for +k <= 4, not a theorem. + +Over F_3 the threshold is different: the replay finds 480 passing headers +at m = k = 3, so the binary threshold is not field-independent. + +## Theorem 4: strict negative correlation for k = 3 over F_2 + +**Theorem 4.** For every m >= 2, Pr(all three pass) < s_m^3, where +s_m = 3^(m-1)/((2^m - 1)2^(m-1)) is the single corank-one fraction of #4227. + +**Proof.** For m <= 3 the joint count is zero. For m >= 4 the ratio is + +```text +rho_m = (N_n / 27^n) * (2^m - 1)^2 / ((2^m - 2)(2^m - 4)), +``` + +where N_n is the numerator in the corollary. Put x = (7/9)^n. Then +N_n/27^n <= 1 - 6x + 57(19/27)^n, since the remaining bases are at most 19 +and their signed multiplicities have absolute sum 57. For n >= 42, +57(19/27)^n <= x because 57(19/21)^42 < 1. +With X = 2^m, (X - 1)^2/((X - 2)(X - 4)) = 1 + (4X - 7)/((X - 2)(X - 4)) +<= 1 + 8/X for X >= 16, and 8/2^m = 4/2^n <= x for n >= 4. Hence +rho_m <= (1 - 5x)(1 + x) < 1 for n >= 42. The verifier checks rho_m < 1 +exactly for 4 <= m <= 400. QED. + +Since |Z(c)| <= 3^k - 2 for every c != 0 (sigma = 0 gives +1, and a sigma +with a single 1 and a single 2 on an entry of c gives -1), the joint fraction has the same +leading term 3^(kn) 2^(k - 2km) as the product of marginals for every k, +so the ratio tends to one. The sign of the approach is proved here only for +k <= 3. + +## Scope + +The transfer theorem covers every finite field; the replay implements the +prime fields F_2 (k <= 4) and F_3 (k <= 3). Theorems 2-4 are binary. The +proofs are written mathematics without a proof-kernel check. The algebraic +count supplies no request producer, header selection or emission, +dispatch, dirty return, stock or physical cost; neither a supplier nor a +complete multiplication theorem follows. diff --git a/research/common-image-full-guard-family/inputs/4275-README.md b/research/common-image-full-guard-family/inputs/4275-README.md new file mode 100644 index 0000000000..830650a2a4 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/4275-README.md @@ -0,0 +1,133 @@ +# Exact full-guard law for k corank-one requests with orthogonal kernels + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped counting proof with finite corroboration.** Let +U_1, ..., U_k be pairwise orthogonal rank-one idempotents on F_q^m, and +P_t = I - U_t. A complete header G passes a request when all leading +principal minors of G P_t G^-1 through its rank are nonzero. All k requests +use the same G. This answers open question 2 of +[#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261), which +proves the case k = 2. + +[PROOF.md](PROOF.md) proves: + +1. **Transfer law, every finite field.** The joint fraction is + C(q,m,k)/D(q,m,k), computed by a walk on k by k partial Gram matrices with + diagonal entries different from 1, with + D = q^(k(m-k)) prod_(i= 2.** A common passing header exists over + F_2 exactly when m >= k + 1. The proof is a rank and idempotence argument + on J - I. +4. **Three requests over F_2.** + + ```text + C(2,m,3) = (27^n - 6*21^n + 6*19^n - 6*17^n + 16*15^n - 18*13^n + + 9*11^n - 2*9^n) / 64, + Pr(all three pass) = C(2,m,3) / ((2^m-1)(2^m-2)(2^m-4) 2^(3m-9)). + ``` + + At m = 4 this is 1/1680, against (9/40)^3 for independent marginals. The + three passing events are strictly negatively correlated for every m >= 2. + +Over F_3 the threshold differs: 480 of 11,232 headers (5/117) pass three +requests at m = 3. + +## Reproduction and evidence + +From the repository root, with any CPython 3.12 replacing this local path: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/corankone-triple-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/corankone-triple-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/corankone-triple-header-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/corankone-triple-header-law --check-source-history +``` + +The scientific marker is `PASS_CORANKONE_TRIPLE_HEADER_LAW`. Its generated +JSON holds every transfer count, the binary spectra, the census counts and +SHA-256 hashes of every package file. Nothing is written to disk and no +receipt is stored. Each verifier run takes about 20 seconds locally. + +The finite corroboration: + +- **Literal census of 31,614 complete GL headers**: F_2 at m = 2, 3, 4 and + F_3 at m = 2, 3, with k up to min(m, 4). Each header is inverted, each + conjugated request is formed as a full matrix, and no-pivot elimination + checks its guards. Every joint count equals the transfer count times + |GL_(m-k)|. At F_2, m = 4 the k = 3 count is 12 headers. +- **Transfer counts**: F_2 for k = 1..4 (m up to 40, 40, 30, 12) and F_3 + for k = 1..3 (m up to 10, 8, 5). The rank-one weights are enumerated from + all (y, x) pairs, not taken from the formula. +- **Character law**: the binary spectra for k <= 4 are computed from Z(c) + over all characters and match the transfer at every listed m. The k = 3 + closed form matches for m <= 30. +- **Threshold**: zero counts for m <= k and positive counts for m > k, + k = 2, 3, 4. At m = k + 1 the counts are 2, 12, 48. +- **Correlation**: the k = 3 joint fraction is checked exactly against the + cube of the marginal for 4 <= m <= 400; PROOF.md covers larger m. +- **Boundaries**: k = 1 reproduces #4227's marginal (3^n over F_2, + 2*7^n over F_3); binary k = 2 reproduces #4261's closed form for m <= 40; + F_3 at k = m = 2 reproduces #4239's 1/6. +- **Controls**: omitting the zero-step multiplicity, assuming independence, + dropping the negative characters, and admitting on first guards only + (4,536 versus 12 headers at F_2, m = 4, k = 3) each change a checked value. + +## Scope and remaining obligations + +The transfer theorem covers every finite field; the replay implements F_2 +and F_3 only. The closed form is for k = 3 over F_2. The count 2 k! at the +threshold is observed for k = 3, 4 and is not proved. Fixed idempotents with +pairwise orthogonal rank-one kernels and a complete, equally weighted GL +header domain are assumed. No density is asserted for restricted header +subsets. + +No request producer, header selection or emission, dispatch, dirty return, +stock, precision or physical invoice is supplied. Those costs remain +unknown, not zero. No new kappa, selected-frontier change, supplier +admission or complete multiplication theorem is claimed. Independent human +and formal proof-kernel review are unclaimed. Selected cold replay, Lean and +Docker were not run. + +The verifier is standard-library Python with bounded loops and no +recursion. The largest transfer has 5,832 states (F_3, k = 3). CPython +allocates integers and tuples dynamically; the declared finite domains +bound that allocation. + +## Related work and credit + +- [#4261](https://github.com/CrocSwap/integer-mult-bounds/pull/4261) proves + the k = 2 transfer and binary law; this package generalizes its partial + Gram argument. Its binary closed form agrees numerically for m <= 40. +- [#4227](https://github.com/CrocSwap/integer-mult-bounds/pull/4227) + supplies the corank-one determinant identity and marginal law, used as a + cited step and checked numerically at k = 1. +- [#4239](https://github.com/CrocSwap/integer-mult-bounds/pull/4239) gives + the orthogonal rank-one law; its q = 3, m = 2 value 1/6 agrees. +- [#4246](https://github.com/CrocSwap/integer-mult-bounds/pull/4246) and + [#4259](https://github.com/CrocSwap/integer-mult-bounds/pull/4259) cover + orthogonal and laminar families. The requests here are neither when + m > 2 and k >= 2. + +These preceding counting packages were produced by Nick Petalas. Cinna +Davis supplied the #4100 BIT.md request context; the retained normalizer +lineage is due to source527, commdata2338 and Jose Manuel. No unmerged +predecessor code is imported. + +## Open next questions + +1. Is the binary count at the threshold m = k + 1 equal to 2 k! for every + k >= 3, so that only the row and column rectangle decompositions of + J - I occur? Checked for k = 3, 4; k = 5 needs a vectorized walk. +2. Is the binary joint fraction strictly below the product of marginals for + every k >= 4? The single-entry characters give the second eigenvalue + 7*3^(k-2) with sign -1 and multiplicity k(k-1); the rest of the negative + spectrum is not bounded here. +3. Can the odd-q transfer be reduced, for example by the symmetric group + acting on the k requests, to a closed form? +4. Does an actual producer admit a fully charged shared-header caller for + such a family? A joint density is not a physical saving. diff --git a/research/common-image-full-guard-family/inputs/4807-PROOF.md b/research/common-image-full-guard-family/inputs/4807-PROOF.md new file mode 100644 index 0000000000..8c0baf7570 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/4807-PROOF.md @@ -0,0 +1,139 @@ +# A common-covector pair has a different dependence law + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let K=F_q be any finite field, m>=2, and let a,c be independent columns +in K^m. Let b be a row with ba=bc=1. Put U=ab, V=cb, P=I-U, Q=I-V. +Thus U,V are distinct rank-one idempotents with UV=U and VU=V. Both +products are nonzero. Their complementary projectors P,Q have a common +image ker(b). This is outside the orthogonal and one-way coupling hypotheses. + +For a complete header G chosen uniformly from GL_m(K), let E_P mean that +every leading principal minor of GPG^-1 of orders 1 through m-1 is +nonzero. Define E_Q in the same way. Write n=m-1 and + +```text +alpha = q^2-q+1, +delta = q^2+(q-1)^3. +``` + +Then the exact joint passing probability is + +```text + (q-1)(delta^n-alpha^n) +J(q,m) = ----------------------------------------- . (1) + (q^m-1)(q^m-q) q^(m-2) +``` + +In particular, over F_2 the events are strictly positively correlated for +every m>=2. At m=2 the joint probability is 1/3 and each marginal is 1/2. +This refutes extension of the known negative-correlation statements to +arbitrary two-way coupled rank-one kernels. It does not contradict their +stated hypotheses. + +Claim type: scoped counting proof with finite corroboration. + +## Header orbit and the guard + +Conjugation takes the triple to (Ga,Gc,bG^-1). GL_m(K) acts transitively +on all triples (a,c,b) satisfying independence and ba=bc=1. To see this, +take a,c-a as the first two basis vectors. The second lies in ker(b). +Extend it to a basis of ker(b), and b has coordinates (1,0,...,0). +The same construction for any other triple gives the required change of +basis. Every triple therefore has the same number of complete-header +preimages, by the stabilizer coset bijection. + +There are (q^m-1)(q^m-q) ordered independent pairs a,c. For each pair, +the two independent linear equations ba=bc=1 have q^(m-2) solutions b. +Consequently the denominator in (1) is the number of triples in this orbit. + +The rank-one determinant identity gives + +```text +det(P[1:k,1:k]) = 1 - sum_(i=1)^k b_i a_i, +det(Q[1:k,1:k]) = 1 - sum_(i=1)^k b_i c_i. +``` + +This is the marginal guard identity of Nick Petalas #4227. We use its +partial-sum method, also used in #4261, and count the new common-covector +orbit directly. For every proper prefix, both partial sums must avoid 1; +at the final coordinate both sums equal 1. + +## Count first, subtract dependent pairs + +Temporarily allow all a,c, retaining ba=bc=1. At one coordinate the +increment is (b_i a_i,b_i c_i). A zero increment has q^2+q-1 preimages: +q^2 choices with b_i=0, and q-1 with b_i nonzero and a_i=c_i=0. +Every nonzero increment has q-1 preimages, one for each nonzero b_i. +Thus the increment weight is q^2 times the zero indicator plus the +constant q-1 on K^2. + +The safe state set S=(K minus {1})^2 has N=(q-1)^2 elements. Its weighted +transition matrix is q^2 I+(q-1)11^T. Every row sum is +q^2+(q-1)N=delta. Start at (0,0) in S. After n safe transitions the +total path weight is delta^n. The terminal state (1,1) is outside S, +so the last increment is nonzero from every safe state and has weight +q-1. The number of all passing triples before enforcing independence is +(q-1)delta^n. + +If a,c are dependent, the endpoint conditions force c=a. Indeed a is +nonzero, write c=t a, and 1=bc=t ba=t. Conversely every diagonal pair +c=a with ba=1 is a dependent triple. There are no other dependent cases. + +For these diagonal triples the scalar increment b_i a_i has 2q-1 +preimages at zero and q-1 at every nonzero element. On K minus {1}, +the safe transition matrix is q I+(q-1)11^T, with row sum +q+(q-1)^2=alpha. The last step again has weight q-1. Therefore exactly +(q-1)alpha^n of the passing triples have dependent columns. Subtracting +them gives the numerator of (1). Dividing by the independent-triple orbit +count proves (1), in every characteristic and every finite field. + +## Binary positive correlation in every dimension + +The cited single-request law #4227 gives + +```text +p(q,m) = (q-1)alpha^n / ((q^m-1)q^(m-1)). +``` + +At q=2, alpha=3 and delta=5, and direct cancellation yields + +```text +J(2,m) / p(2,m)^2 + = [2^(n+1)(2^(n+1)-1)/(2^(n+1)-2)] (5^n-3^n)/9^n. (2) +``` + +Since 5>9/2, replacing 5^n by (9/2)^n strictly decreases (2). The +resulting lower bound is + +```text +2(2^(n+1)-1)/(2^(n+1)-2) * (1-(2/3)^n). +``` + +This is at least 1 exactly when 3^n>=2^(n+1)-1. The latter inequality +holds for every n>=1. It is equality at n=1; if it holds at n then +3^(n+1)>=3*2^(n+1)-3>=2^(n+2)-1, since 2^(n+1)>=2. +The replacement of 5^n was strict even at n=1, so J(2,m)>p(2,m)^2 +for every m>=2. This is a written dimension-uniform proof, rather than +an inference from a finite census. + +## Credit and limits + +The two-way-coupling question is Open next question 1 of Nick Petalas +[#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778), following +#4769/#4274's one-way law. The marginal identity and probability are from +#4227; #4261 supplies the predecessor partial-sum/header counting method. +The common-covector orbit, its dependent-pair subtraction, formula (1), +and the binary positive-correlation proof are the new contribution here. +Cinna Davis supplied the BIT request context. source527, commdata2338 and +Jose Manuel retain the normalizer and recursive-closure lineage credit. + +Only this common-covector pair and complete uniformly weighted headers are +covered. The proof does not classify arbitrary two-way pairs, larger +families, restricted header catalogues, or odd-field correlation signs. +Selection, emission, dispatch, dirty restoration, stock, precision and the +physical caller bill remain unknown. No supplier admission, new kappa, +selected-frontier change or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/common-image-full-guard-family/inputs/4807-README.md b/research/common-image-full-guard-family/inputs/4807-README.md new file mode 100644 index 0000000000..08535a3694 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/4807-README.md @@ -0,0 +1,104 @@ +# Positive correlation for a common-covector full-guard pair + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped counting proof with finite corroboration. Over any finite +field F_q, let a,c be independent columns, b a row with ba=bc=1, and +P=I-ab, Q=I-cb on F_q^m, m>=2. For complete uniformly weighted GL_m(F_q) +headers, the joint full-guard passing fraction is exactly + +```text + (q-1)[(q^2+(q-1)^3)^(m-1) - (q^2-q+1)^(m-1)] +J(q,m) = ------------------------------------------------- . + (q^m-1)(q^m-q)q^(m-2) +``` + +Over F_2 these two guard events are strictly positively correlated in every +dimension m>=2. At m=2, J=1/3 exceeds the marginal product 1/4; at m=3, +J=4/21 and each marginal is 9/28. Thus negative correlation for the known +orthogonal and one-way cases does not extend to every two-way pair. + +[PROOF.md](PROOF.md) counts the common-covector header orbit by two partial +sums, subtracts exactly the equal-column paths, and proves the binary +comparison for all dimensions. This answers one case of Open next question 1 +in [#4778](https://github.com/CrocSwap/integer-mult-bounds/pull/4778). That +question and #4769/#4274's contrasting one-way law retain Nick Petalas's +credit, as do #4227's marginal law and #4261's partial-sum/header method. +Cinna Davis supplied the BIT request context; source527, commdata2338 and +Jose Manuel retain the normalizer and recursive-closure lineage credit. +No predecessor implementation is imported or replayed. + +## Reproduction and evidence + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/common-covector-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/common-covector-header-law/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/common-covector-header-law +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/common-covector-header-law --check-source-history +``` + +Another CPython 3.12 installation may replace the local interpreter path. +The direct marker is `PASS_COMMON_COVECTOR_HEADER_LAW`. The verifier writes +no files. It prints a generated receipt with every domain's counts and +SHA256 hashes of all six package files. Both registered modes keep explicit +checks active, including optimized Python. + +The verifier enumerates all 34,290 complete headers in eight domains: +GL_2 over F_2,F_3,F_4,F_5,F_7, GL_3 over F_2,F_3, and GL_4 over F_2. +It inverts each header, conjugates both literal projectors and tests every +leading minor through rank m-1. Both marginals and the joint count agree. +F_4 is F_2[x]/(x^2+x+1), rather than integers modulo four. + +A separate vector enumeration counts all 26,070 independent orbit triples +in nine domains: q=2,m=2..5; q=3 or 4,m=2..3; q=5,m=2. Ten coordinate +transfers enumerate the actual increment factorizations for widths one and +two over F_2,F_3,F_4,F_5,F_7, at path lengths zero through eight. Their +difference agrees with the joint formula at m=2..9. Exact rational checks +corroborate binary positive correlation in all 255 dimensions m=2..256. +Fourteen fixture, mutation and invalid-input controls distinguish the +field arithmetic, independence, orthogonal substitution, omitted diagonal +subtraction, omitted row fiber and invalid finite-check parameters. + +## Scope and implementation limits + +The all-field and all-dimension claims rest on the written proof. Finite +execution corroborates the explicitly enumerated domains. Only two distinct +rank-one kernels with a common right covector and complete equally weighted +headers are covered. Other two-way pairs, larger families, restricted +headers and odd-field correlation signs are outside the proved claims. + +Header selection, emission, dispatch, dirty restoration, stock, precision, +producer compatibility and the complete paid physical caller remain unknown. +No new kappa, supplier admission, selected-frontier change or complete +multiplication theorem is claimed. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and the selected operator replay are unrun. + +[TASK.json](TASK.json) records the change from the formal-interface card to +this algebraic side question. [SOURCES.json](SOURCES.json) binds predecessor +text, the catalogue and selected record as historical provenance on canonical +main. There are no runtime dependencies outside this package and no pending +Git-object dependency. Provenance/history checks require full Git history; +the direct verifier also runs from a standalone exported package. + +Power of Ten inspection finds no recursion or subprocesses in the verifier. +Every loop is bounded by fixed domains: at most 65,536 candidate matrices +of size four, 64 vectors per triple coordinate, 49 transfer states, nine +transfer rounds and 255 correlation dimensions. Functions fit within 60 +lines. Explicit require checks enforce input and mathematical contracts. +CPython allocates dynamically, a managed-runtime deviation from fixed +allocation; the stated domains bound live collections. Diagnostics use +warnings as errors. No shared implementation is changed. + +## Open next questions + +1. Determine the law for two-way pairs with independent covectors. Start + with one normalized pair whose two cross products are nonzero; its + partial-Gram orbit differs from the shared-covector model here. +2. Determine the correlation signs for this common-covector family over + odd fields. Compare the new joint formula with #4227's marginal squared, + starting with q*delta-alpha^2=q-1; a quantified sign proof is unclaimed. +3. Find a named physical producer and fully charged shared-header caller. + Pin its header domain before charging selection, emission, dispatch, + dirty restoration, precision and stock. Those costs are unknown. diff --git a/research/common-image-full-guard-family/inputs/6515-PROOF.md b/research/common-image-full-guard-family/inputs/6515-PROOF.md new file mode 100644 index 0000000000..fcc1b10217 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/6515-PROOF.md @@ -0,0 +1,175 @@ +# Six orthogonal full-guard events lie below the product of their marginals + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +This answers the k=6 case of the open product inequality in +[discussion comment 19144831](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144831). +Nick Petalas's #4275 supplies the character law and the m=k threshold. +Ryanson Jonathan's #4599 and #4607 settle k=4 and k=5. The 19/21 remainder +gap is Nick Petalas's #5146. No new κ is claimed. + +## Statement + +Let m ≥ 6. Let U_1, …, U_6 be pairwise orthogonal rank-one idempotents on +F_2^m, and let G be uniform in GL_m(F_2). Event E_t says that every leading +principal minor of G(I−U_t)G^{−1}, of orders 1 through m−1, is nonzero. +Write n = m−1, X = 2^m and + +```text +s_m = 3^n / ((X−1) 2^n). +``` + +**Theorem.** For every integer m ≥ 6, + +```text +Pr(E_1 ∩ ⋯ ∩ E_6) < s_m^6. +``` + +At m = 6 the joint probability is 0. The ratio tends to 1 from below. The +proof is a scoped counting argument with one exhaustive 2^30-character +spectrum and an integer tail for every larger dimension. It is not a +negative-association theorem for other events, a supplier admission, or a +selected-frontier change. + +## 1. Reduction + +A basis change takes U_t to e_t e_tᵀ and only permutes complete headers. +#4275, Theorem 2, counts the headers whose first six diagonal guards all +pass. With N_n = Σ_c (−1)^{|c|} Z(c)^n and K = 30, + +```text +Z(c) = Σ_{σ in {0,1,2}^6} (−1)^{Σ_{i≠j} c_ij [σ_i=1][σ_j=2]}, +D_n = N_n / 2^{30}, +Pr = D_n / (2^{6n−30} (X−1)(X−2)(X−4)(X−8)(X−16)(X−32)) + = N_n / (2^{6n} (X−1)(X−2)(X−4)(X−8)(X−16)(X−32)). +``` + +The same theorem gives the one-event count 3^n, hence the marginal s_m. +Dividing Pr by s_m^6 cancels 2^{6n} and one factor of X−1, and produces + +```text +ρ_m = (N_n / 729^n) · H(X), +H(X) = (X−1)^5 / ((X−2)(X−4)(X−8)(X−16)(X−32)). +``` + +The subset form used by the enumerator, + +```text +Z(c) = Σ_{S: every j∉S has even incoming parity from S} 2^{6−|S|}, +``` + +is the closed form obtained by summing the label-2 coordinates in Z(c). +The verifier checks it against the literal three-state sum on every +zero-diagonal character at k=3 and k=4, and checks that the same enumerator +reproduces #4275's published k=3 coefficients and #4607's leading k=5 +coefficients 243^n − 20·189^n + 60·171^n. + +## 2. The signed spectrum + +The enumerator walks all 2^30 edge masks by a Gray code. Each step flips +one arc and updates the incoming-parity mask of the 2^{4} source sets that +contain that arc. The resulting 176 nonzero coefficients begin + +```text +N_n = 729^n − 30·567^n + 120·513^n + R_n. +``` + +Here 567 = 7·3^4 and 513 = 19·3^3. #5146 already separates these from +every matrix with two or more entries, whose character is at most 513. +The verifier evaluates the three-state sum on all 30 single arcs and on +all 120 two-arrow stars (six orientations on each triple of vertices, +every other entry zero). Each arc has Z = 567 and odd weight. Each star +has Z = 513 and weight 2. The absolute coefficients sum to 2^30, so no +character value contains both signs. Those two evaluations are therefore +the entire levels: coefficient −30 at 567 and +120 at 513. +Every other character has Z ≤ 495, and the absolute sum of those +coefficients is A = 1,073,741,673. Thus + +```text +R_n ≤ A·495^n, N_n ≤ 729^n − 30·567^n + 120·513^n + A·495^n. +``` + +Two direct counts fall out of the same table. N_n = 0 for 0 ≤ n ≤ 5, so +there is no positive walk of length less than 6 and the joint event is +empty at m = 6. At n = 6, N_6 / 2^30 = 23,040, an exact positive header +count at m = 7. Adding one to the single-arc coefficient makes N_5 nonzero, +so that vanishing is not a rounding accident. + +## 3. Dimensions 7 ≤ m ≤ 130 + +For n from 6 through 129 the verifier compares the integers + +```text +N_n · (X−1)^5 < 729^n · (X−2)(X−4)(X−8)(X−16)(X−32). +``` + +Each comparison is strict. Floating point already rounds ρ_m to 1 at these +dimensions; the sign is carried by the integer slack. Representative exact +ratios are about 0.000270 at m = 7, 0.00996 at m = 8, 0.3767 at m = 13 and +0.9988 at m = 41. + +## 4. Every larger dimension + +Let L(n) = 27·567^n − 120·513^n − A·495^n. The spectrum bound and L(n) ≥ 0 +give + +```text +N_n ≤ 729^n − 30·567^n + 120·513^n + A·495^n = 729^n − 3·567^n − L(n) + ≤ 729^n − 3·567^n. +``` + +The verifier finds L(129) > 0, and also that 26·567^{129} does not cover +the same remainder, so three single-arc modes are what this cap leaves at +the threshold. Expanding the definition gives + +```text +L(n+1) − 567 L(n) = 120·513^n·54 + A·495^n·72 > 0, +``` + +so L(n+1) > 567 L(n) and L stays positive. + +It remains to show (729^n − 3·567^n) H(X) < 729^n. Expanding the +denominator gives the integer identity + +```text +(X−1)^5 − (X−2)(X−4)(X−8)(X−16)(X−32) + = 57X^4 − 1230X^3 + 9910X^2 − 31739X + 32767. +``` + +For X ≥ 128 the positive lower terms satisfy 9910X^2 ≤ X^4 and +32767 ≤ X^4, so the difference is at most 59X^4. Therefore it is enough +that + +```text +3·567^n · (X−1)^5 > 59 · X^4 · 729^n, X = 2^{n+1}. +``` + +The verifier checks this at n = 129, where X = 2^{130}. If P(n) and N(n) +are the two sides, the next order is 2X, so + +```text +P(n+1)/P(n) = 567·((2X−1)/(X−1))^5 > 567·32 = 18144, +N(n+1)/N(n) = 16·729 = 11664. +``` + +The fifth-power ratio is strictly larger than 2 because +(2X−1)/(X−1) = 2 + 1/(X−1). A strict gap at n = 129 therefore stays +strict at every larger n. Also 729/567 = 9/7 > 1, and the verifier finds +729^{129} > 3·567^{129}, so 729^n > 3·567^n remains true and the +comparison upper bound stays nonnegative. The degree-four majorization +was checked at X = 128, the smallest integer in its hypothesis, and both +9910 ≤ X^2 and 32767 ≤ X^4 become looser as X grows. Hence ρ_m < 1 for +every m ≥ 130. Section 3 already includes m = 130, and sections 2 through +4 together cover every m ≥ 6. + +## Scope + +**Covered.** Exactly six fixed, pairwise orthogonal rank-one requests over +F_2, with complete headers weighted equally, at every m ≥ 6. + +**Not settled.** k ≥ 7 inside the strip k+1 ≤ m ≤ 8(k(k−1)+1), odd +characteristic, restricted header families and nonorthogonal kernels. +#5146 already supplies a loose eventual bound past that strip; this package +does not rerun it and does not improve it for k ≥ 7. + +**Not claimed.** A physical saving, a supplier, a new κ, or proof-kernel +review. Header probabilities are not an executed caller. diff --git a/research/common-image-full-guard-family/inputs/6515-README.md b/research/common-image-full-guard-family/inputs/6515-README.md new file mode 100644 index 0000000000..83ec7c9f99 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/6515-README.md @@ -0,0 +1,61 @@ +# Six-event binary full-guard product inequality + +**Claim type: scoped counting proof with an exhaustive finite spectrum. No new κ.** + +For every m ≥ 6, six pairwise orthogonal rank-one full-guard events on a +uniform matrix G ∈ GL_m(F_2) are strictly rarer than the sixth power of one +such event. At m = 6 the joint count is 0. At m = 7 it is exactly 23,040 +headers. The ratio then increases toward 1 and stays below it. + +This is the k = 6 case left open by JoyboyBrian's handoff +[comment 19144831](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144831). +The character law is Nick Petalas's #4275. The k = 5 theorem is Ryanson +Jonathan's #4607. The single-arc and two-star eigenvalues are the sharp +#5146 spectrum, used here only at k = 6. Selected κ stays +781451/250000000. + +## Result + +The proof enumerates all 2^30 zero-diagonal characters. Their signed +transform is + +```text +N_n = 729^n − 30·567^n + 120·513^n + R_n, R_n ≤ 1073741673·495^n. +``` + +Exact integer comparison gives the strict ratio for 7 ≤ m ≤ 130. For every +larger m, that tail fits under 27 single-arc modes. The three modes left +over dominate the degree-four gap between (X−1)^5 and the six-event GL +denominator. Details, the induction, and the limits are in `PROOF.md`. + +## Reproduce + +From the repository root, CPython 3.12 and gcc, standard library only: + +```sh +python3.12 -B research/six-event-guard-correlation/verify.py +python3.12 -B scripts/research_package.py --package research/six-event-guard-correlation +``` + +The verifier compiles `spectrum.c`, checks the three-state sum against the +subset form at k = 3 and k = 4, matches the published k = 3 and leading k = 5 +coefficients, then checks the k = 6 theorem. It prints +`PASS_SIX_EVENT_GUARD_CORRELATION`. One normal run is the certificate. The +2^30 pass takes under a minute on this host. No files are written into the +package. Lean, Docker, selected-frontier replay and an independent human +review were not run. + +## Open next questions + +1. **k ≥ 7 in the finite strip.** The same product inequality is open for + seven or more orthogonal guards below the #5146 eventual range. The first + step is a support-truncated spectrum, or an exact count of length-k + rectangle decompositions of J−I, at k = 7. The blocker is that the raw + character space has order 2^42, so the k = 6 Gray code does not extend. +2. **Nonorthogonal kernels.** A single shared direction can change both the + marginal and the joint count. The first step is one explicit pair of + nonorthogonal rank-one idempotents at m = 7 whose six-event ratio meets + or exceeds 1, or a reduction to the orthogonal case. Nothing in this + package prices that configuration. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/common-image-full-guard-family/inputs/6515-TASK.json b/research/common-image-full-guard-family/inputs/6515-TASK.json new file mode 100644 index 0000000000..9e13962481 --- /dev/null +++ b/research/common-image-full-guard-family/inputs/6515-TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "independent-moment", + "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "invoice", + "signed moment", + "productive target", + "independent recount" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "For every m >= 6, six pairwise orthogonal rank-one full-guard events on a uniform element of GL_m(F_2) are strictly rarer than the sixth power of one such event.", + "scope_change_reason": "Discussion handoff 19144831 files the binary full-guard product inequality under this task id. The pinned card asks whether a serialized target/paid invoice independently supports a claimed improvement. The proved statement is a signed comparison of six header events, not a supplier bill, and it does not change the selected frontier.", + "bottleneck_link": "The inequality is an independent signed moment of six complete-header events. It does not audit a supplier contract, admit a physical saving, or raise kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the k=6 inequality is proved for every m >= 6. Do not open k >= 7 and do not change the selected frontier.", + "outcome": "completed", + "evidence": "Exact signed spectrum of all 2^30 zero-diagonal characters: 176 bases, N_n = 729^n - 30*567^n + 120*513^n + R_n with R_n <= 1073741673*495^n. The 30 arcs and 120 two-arrow stars are the whole 567 and 513 levels. N_n = 0 for n < 6, and N_6/2^30 = 23040 headers at m = 7. Exact integer slack is positive for n = 6..129. For every n >= 129 the remainder fits under 27 single-arc modes, and the remaining 3 modes absorb the degree-four GL gap. A one-unit change of the arc coefficient makes N_5 nonzero.", + "author": "unpaidmoon, with substantial Cursor Grok assistance", + "ai_assistance": "Substantial Cursor Grok assistance; no independent human review. Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the same strict product inequality hold for every k >= 7 and every m with k+1 <= m <= 8(k(k-1)+1)?", + "why_it_matters": "k = 6 was the first open width in discussion comment 19144831. The inherited #5146 bound already covers the eventual range n >= 8(k(k-1)+1), so the missing theorem is the finite strip.", + "first_step": "At k = 7, bound or enumerate the characters above a support-truncated cutoff, or count the length-7 rectangle decompositions of J-I, and compare the resulting numerator with H(X) through the end of the strip.", + "blocked_by": "The raw character space has order 2^42, so the k = 6 Gray-code enumeration does not extend." + }, + { + "question": "Can one shared direction between two rank-one kernels push the six-event ratio to 1 or above at m = 7?", + "why_it_matters": "Orthogonality is an essential hypothesis of the character reduction. A single shared direction changes both the marginal and the joint count.", + "first_step": "Exhibit one explicit pair of nonorthogonal rank-one idempotents at m = 7 whose six-event ratio meets or exceeds 1, or reduce that configuration to the orthogonal case.", + "blocked_by": "None. This package prices only pairwise orthogonal kernels." + } + ] +} diff --git a/research/common-image-full-guard-family/inputs/6694-README.md b/research/common-image-full-guard-family/inputs/6694-README.md new file mode 100644 index 0000000000..58bbe1ff1d --- /dev/null +++ b/research/common-image-full-guard-family/inputs/6694-README.md @@ -0,0 +1,107 @@ +# Seven orthogonal full-guard events lie below the product of their marginals + +This contribution was produced by Nick Petalas. Apache-2.0. Independent human +and formal proof-kernel review are unclaimed. + +**Claim type: scoped counting proof resting on an exact finite certificate. No κ.** + +Over F_2, let U_1, ..., U_7 be pairwise orthogonal rank-one idempotents on F_2^m +and let G be uniform in GL_m(F_2). Event E_t says every leading principal minor of +orders 1 through m-1 of G(I-U_t)G^-1 is nonzero. With n = m-1, X = 2^m and +s_m = 3^n / ((X-1) 2^n) the probability of one event: + +```text +for every m >= 7: Pr(E_1 ∩ ... ∩ E_7) < s_m^7 +``` + +At m = 7 the joint probability is 0 (a passing header needs m >= k+1). At m = 8 it +is 29/5201587077120, about 5.575e-12, against s_8^7 of about 6.063e-9. The ratio +tends to 1 from below: 1 - rho_m = 42 (7/9)^(m-1) (1 + O((19/21)^(m-1))). + +This answers open next question 1 of unpaidmoon's [PR6515](https://github.com/CrocSwap/integer-mult-bounds/pull/6515) +(`research/six-event-guard-correlation`): the same inequality for seven events, +inside the strip 8 <= m <= 344 that it leaves open. The proof uses Nick Petalas's +character law (PR4275) as a cited premise and does not use the k = 6 theorem of +PR6515, the remainder bound of PR5146 or the k = 4, 5 theorems. + +## New step + +The signed spectrum of all 2^42 seven-vertex characters is computed exactly, in +about 40 seconds on one core, instead of by a 2^42 Gray-code walk. `spectrum.c` +(i) reduces the first five vertices to their 9,608 orbits under S_5, and +(ii) evaluates all 2^12 arc patterns of the last vertex from two 64-entry tables, +because Z(c) = F1(u) + F2(v) there ([PROOF.md](PROOF.md) section 2). The table +`SPECTRUM_K7.txt` has 493 entries; N_0 = ... = N_6 = 0 and N_7 / 2^42 = 29,816,640 = +7! * 5916. Strict inequality is checked with exact integers for every 6 <= n <= 400, and +an integer tail bound (L(187) < 0 < L(188)) closes every larger m. + +## Evidence + +From the repository root; a C compiler (`cc`, `gcc` or `clang`) is required. + +```sh +python3.12 -I -B research/seven-event-guard-correlation/verify.py # PASS_SEVEN_EVENT_GUARD_CORRELATION +python3.12 -I -B research/seven-event-guard-correlation/verify.py --brute6 # PASS_SEVEN_EVENT_GUARD_BRUTE6 +python3.12 -B scripts/research_package.py --package research/seven-event-guard-correlation +python3.12 -B scripts/check_research_commit.py --package research/seven-event-guard-correlation --check-source-history +``` + +The default replay regenerates the k = 7 spectrum and compares it byte for byte with +`SPECTRUM_K7.txt`; validates the enumerator against labelled brute force at k = 3, 4, +5, against the literal three-state definition at k = 3, 4, and against the spectra +printed in the pinned PR4275, PR4599 and PR4607 files; checks the subset form +against the definition on random characters at k = 5, 6, 7; checks the spectrum +facts, the exact range, the tail bound, the closing inequalities and the rate; and +runs six rejection controls (a one-unit change to a top coefficient, a doubled top +coefficient, a shifted subset weight, a doctored k = 4 spectrum, an altered pinned +statement, a wrong tail threshold). `--brute6` checks the orbit-reduced k = 6 +spectrum against labelled brute force over all 2^30 matrices. It also reproduces the +k = 6 figures reported in PR6515 (176 entries; 1, -30, 120 at 729, 567, 513) as a +by-product. `--labelled7` (not registered; about 7 minutes on 18 cores) repeats the +k = 7 run over every labelled five-vertex digraph with weight one and no orbit +reduction; it covers all 2^42 characters and gives the same 493-entry table. + +Local runs (CPython 3.12.15, macOS arm64, 18 cores, compiler `-std=c11 -O2 -Wall +-Wextra -Wpedantic -Werror`): the default replay takes 13.3 s wall (46 CPU-seconds, +four shards; one shard needs 37 s for the k = 7 table alone), also with `-O`; `--brute6` +takes 31.6 s (125 CPU-seconds). These are check durations, not a speed comparison. + +## Limitations + +* The spectrum is a finite computation by a program. It is validated as listed above + but not re-derived by hand, and no independent re-implementation is supplied. +* Covered: exactly seven pairwise orthogonal rank-one requests over F_2, complete + uniform headers, every m >= 7. +* Not settled: k >= 8, odd characteristic, nonorthogonal or restricted request + families, negative association of six or seven indicators (a stronger statement), + any physical sampling, selection or restoration cost. No supplier, κ or selected + frontier change. Lean, Docker and the selected cold replay were not run. + +## Open next questions + +Structured copies are in [TASK.json](TASK.json). + +1. **k = 8.** Does the inequality hold for every m >= 9? *First step:* extend + `spectrum.c` to eight vertices (a 30-bit base mask with 1,540,944 orbits under + S_6, and 128 x 128 sweeps), compressing the two tables to value histograms. + An extrapolation from the k = 7 timing gives roughly 30 core-hours (not run). + *Blocker:* compute time, not mathematics. +2. **All k.** The computed tables show levels 3^k, 7*3^(k-2), 19*3^(k-3), 55*3^(k-4) + with coefficients 1, -k(k-1), k(k-1)(k-2), -8*C(k,4) for k = 4..7 (checked by + `verify.py`, not proved), every Z odd and one sign per Z value. *First step:* + combine PR6440's third-level classification with a uniform bound on the remainder. + *Blocker:* no all-k bound on characters below the first levels. +3. **Shared kernel directions** (PR6515 open question 2). *First step:* test whether + PR4240's joint law for nonorthogonal rank-one requests extends to several requests + with one shared direction. *Blocker:* not examined here. + +## Credit + +Nick Petalas (PR4275) supplies the character law, the transfer and the binary +threshold; Nick Petalas (PR4599) the four-event inequality; Ryanson Jonathan +(PR4607) the five-event inequality and spectrum; Nick Petalas (PR5146) the remainder +bound; Nick Petalas (PR6440) the equality classification of the third level; +unpaidmoon (PR6515) the six-event inequality, the open question and the +enumeration-plus-tail method adapted here. The orbit reduction, the two-table sweep +and the k = 7 table are new in this package. The Weierstrass product inequality and +Walsh-Hadamard transform are classical. Predecessor packages are unchanged. diff --git a/research/common-image-full-guard-family/oracle.py b/research/common-image-full-guard-family/oracle.py new file mode 100644 index 0000000000..9efd4ec2ba --- /dev/null +++ b/research/common-image-full-guard-family/oracle.py @@ -0,0 +1,497 @@ +#!/usr/bin/env python3 +"""Independent binary column-span and literal full-guard oracle. + +Credit unpaidmoon6515 and Nick Petalas4807/4275/6694, the retained +rank-one/header lineage and classical orbit-stabilizer counting. +Substantial OpenAI Codex assistance. Apache-2.0. No primary or +predecessor implementation is imported or executed. +""" + +import argparse +from collections import defaultdict +from fractions import Fraction +from functools import lru_cache +import gzip +import hashlib +import itertools +import json +from pathlib import Path +import sys + + +ROOT = Path(__file__).resolve().parent +PIN_SHA = "680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9" +CASE_SHA = "3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273" +SCHEMA_SHA = "c01cd12853adcce258701b3d8e56bfff7ba9d370223dcecccc62200ef8bd087a" +COMMON = {"schema_version", "source_manifest_sha256", "case_manifest_sha256", "family", "small_gl", "example"} +FAMILY_KEYS = {"m", "k", "support_histogram", "orbit_numerator", "orbit_denominator", "probability", "header_fiber"} +SMALL_KEYS = {"m", "gl_count", "mask_histogram", "joint_first_k", "record_sha256"} +EXAMPLE_KEYS = {"m", "k", "u", "v_rows", "header_rows", "proper_minors", "joint_probability", + "single_probability", "product_probability", "ratio", "ratio_gt_one"} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def digest(value): + return sha((canonical(value) + "\n").encode()) + + +def unique(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key: " + key) + result[key] = value + return result + + +def bad_number(value): + raise ValueError("noninteger JSON number: " + value) + + +def parse(raw): + return json.loads(raw, object_pairs_hook=unique, + parse_float=bad_number, parse_constant=bad_number) + + +def pair(value): + return [value.numerator, value.denominator] + + +def domain(m, k): + require(type(m) is int and type(k) is int, "dimension/arity must be integers, not bool") + require(2 <= m <= 16 and 1 <= k <= m, "finite oracle domain is2<=m<=16,1<=k<=m") + + +def authenticate(): + for name, expected in (("SOURCE-PINS.json", PIN_SHA), ("CASES.json", CASE_SHA), ("SCHEMA.json", SCHEMA_SHA)): + require(sha((ROOT / name).read_bytes()) == expected, "source/cases/schema digest changed") + source = parse((ROOT / "SOURCE-PINS.json").read_bytes()) + require(len(source["files"]) == 8, "eight inert source objects required") + for row in source["files"]: + raw = (ROOT / row["local_path"]).read_bytes() + require(len(raw) == row["bytes"] and sha(raw) == row["sha256"], "pinned source bytes changed") + blob = b"blob " + str(len(raw)).encode() + b"\0" + raw + require(hashlib.sha1(blob).hexdigest() == row["git_blob"], "pinned Git blob changed") + cases = parse((ROOT / "CASES.json").read_bytes()) + parse((ROOT / "SCHEMA.json").read_bytes()) + return cases + + +def rank_support_count(m, k): + """Count actual column-pair options by quotient rank and zero-u support.""" + domain(m, k) + states = {(0, 0): 1} + for unused in range(m - 1): + next_states = defaultdict(int) + for (rank, zeros), count in states.items(): + next_states[rank, zeros] += count + next_states[rank, zeros + 1] += count * (1 << (rank + 1)) + outside = (1 << k) - (1 << (rank + 1)) + if outside: + next_states[rank + 1, zeros + 1] += count * outside + states = next_states + histogram = [[zeros, states.get((k - 1, zeros), 0)] for zeros in range(m)] + unrestricted = {0: 1} + for unused in range(m - 1): + after = defaultdict(int) + for rank, count in unrestricted.items(): + after[rank] += count * (1 << (rank + 1)) + outside = (1 << k) - (1 << (rank + 1)) + if outside: + after[rank + 1] += count * outside + unrestricted = after + denominator = ((1 << m) - 1) * unrestricted.get(k - 1, 0) + return sum(count for unused, count in histogram), denominator, histogram + + +def insert(basis, value): + """Canonical reduced binary row basis, with descending pivot positions.""" + for row in basis: + value = min(value, value ^ row) + if not value: + return basis + pivot = value.bit_length() - 1 + result = [row ^ value if row & (1 << pivot) else row for row in basis] + return tuple(sorted(result + [value], reverse=True)) + + +def quotient(value, k): + mask = (1 << (k - 1)) - 1 + return (value & mask) ^ (mask if value >> (k - 1) else 0) + + +@lru_cache(maxsize=None) +def literal_next_columns(basis, k): + return tuple(insert(basis, quotient(column, k)) for column in range(1 << k)) + + +def literal_span_count(m, k): + domain(m, k) + require((m, k) == (7, 6), "literal-span fixture is the frozen7,6 case") + states = {((), 0): 1} + layers = [] + for unused in range(m - 1): + after = defaultdict(int) + for (basis, zeros), count in states.items(): + after[basis, zeros] += count + for target_basis in literal_next_columns(basis, k): + after[target_basis, zeros + 1] += count + states = after + layers.append(len({basis for basis, unused in states})) + full = tuple(1 << index for index in reversed(range(k - 1))) + histogram = [[zeros, states.get((full, zeros), 0)] for zeros in range(m)] + return {"zero_u_histogram": histogram, "quotient_span_counts_by_layer": layers, + "full_rank_orbit_count": sum(count for unused, count in histogram)} + + +def identity(m): + return tuple(1 << index for index in range(m)) + + +def multiply(left, right): + rows = [] + for mask in left: + value = 0 + for index, row in enumerate(right): + if mask & (1 << index): + value ^= row + rows.append(value) + return tuple(rows) + + +def inverse(rows): + m = len(rows) + values = [row | (1 << (m + index)) for index, row in enumerate(rows)] + for column in range(m): + pivot = next((index for index in range(column, m) if values[index] >> column & 1), None) + if pivot is None: + return None + values[column], values[pivot] = values[pivot], values[column] + for index in range(m): + if index != column and values[index] >> column & 1: + values[index] ^= values[column] + return tuple(value >> m for value in values) + + +def leading_determinants(rows): + result = [] + for size in range(1, len(rows)): + mask = (1 << size) - 1 + result.append(int(inverse(tuple(row & mask for row in rows[:size])) is not None)) + return result + + +def request(u, covector, m): + return tuple((1 << index) ^ (covector if u >> index & 1 else 0) for index in range(m)) + + +def independent_covectors(m): + final = 1 << (m - 1) + return [final] + [final | (1 << index) for index in range(m - 1)] + + +def validate_family(u, covectors, m): + require(type(u) is int and 0 < u < (1 << m), "invalid common image vector") + require(type(covectors) is list and 1 <= len(covectors) <= m, "invalid covector family size") + require(all(type(value) is int and 0 < value < (1 << m) for value in covectors), "invalid covector encoding") + require(all((u & value).bit_count() % 2 == 1 for value in covectors), "kernel is not idempotent") + require(len(insert_all(covectors)) == len(covectors), "covectors must be independent") + + +def literal_headers(m): + require(type(m) is int and m in (2, 3, 4), "literal headers require dimension2,3,4") + requests = [request(1 << (m - 1), covector, m) for covector in independent_covectors(m)] + headers, passed, histogram, records = 0, [0] * m, [0] * (1 << m), [] + for rows in itertools.product(range(1 << m), repeat=m): + back = inverse(rows) + if back is None: + continue + headers += 1 + require(multiply(rows, back) == identity(m) and multiply(back, rows) == identity(m), "header inverse differs") + outcomes = [] + for original in requests: + actual = multiply(multiply(rows, original), back) + outcomes.append(all(leading_determinants(actual))) + for k in range(1, m + 1): + passed[k - 1] += int(all(outcomes[:k])) + mask = sum(int(value) << index for index, value in enumerate(outcomes)) + histogram[mask] += 1 + code = sum(row << (m * index) for index, row in enumerate(rows)) + records.append([code, mask]) + records.sort() + return {"m": m, "gl_count": headers, "mask_histogram": histogram, + "joint_first_k": passed, "record_sha256": digest(records)}, records + + +def special_witness(): + m, u = 7, 1 << 6 + covectors = [u | (1 << index) for index in range(6)] + validate_family(u, covectors, m) + idempotents = [tuple(covector if u >> row & 1 else 0 for row in range(m)) for covector in covectors] + require(len(set(idempotents)) == 6 and len(insert_all(covectors)) == 6, "six distinct independent kernels required") + for value in idempotents: + require(multiply(value, value) == value, "kernel is not idempotent") + require(all(multiply(a, b) != multiply(b, a) for a, b in itertools.combinations(idempotents, 2)), + "common-image kernels unexpectedly commute") + minors = [leading_determinants(request(u, value, m)) for value in covectors] + require(all(all(row) for row in minors), "identity witness full guards fail") + return {"m": m, "k": 6, "u": u, "v_rows": covectors, + "header_rows": list(identity(m)), "proper_minors": minors} + + +def insert_all(values): + result = () + for value in values: + result = insert(result, value) + return result + + +def rejected(function, value): + try: + function(value) + except ValueError: + return True + return False + + +def controls(): + bad = request(2, 2, 3) + require(leading_determinants(bad) == [1, 0], "first-pivot-only control failed") + result = {"boolean_dimension_rejected": rejected(lambda m: domain(m, 1), True), + "unsupported_dimension_rejected": rejected(lambda m: domain(m, 1), 17), + "zero_arity_rejected": rejected(lambda k: domain(7, k), 0), + "boolean_arity_rejected": rejected(lambda k: domain(7, k), True), + "too_many_requests_rejected": rejected(lambda k: domain(7, k), 8), + "duplicate_json_rejected": rejected(parse, '{"x":1,"x":2}'), + "nonfinite_json_rejected": rejected(parse, '{"x":NaN}'), + "float_json_rejected": rejected(parse, '{"x":1.0}'), + "singular_header_rejected": inverse((1, 1)) is None, + "first_pivot_only_detected": not all(leading_determinants(bad)), + "dependent_covectors_rejected": rejected(lambda rows: validate_family(1, rows, 3), [1, 1]), + "nonidempotent_kernel_rejected": rejected(lambda rows: validate_family(1, rows, 3), [2]), + "boolean_covector_rejected": rejected(lambda rows: validate_family(1, rows, 3), [True])} + require(all(type(value) is bool and value for value in result.values()), "oracle control failed") + return result + + +def general_linear_count(m): + states = {0: 1} + for unused in range(m): + after = defaultdict(int) + for rank, count in states.items(): + after[rank] += count * (1 << rank) + if rank < m: + after[rank + 1] += count * ((1 << m) - (1 << rank)) + states = after + return states[m] + + +def family_rows(cases): + require(cases["family_cases"] == [[m, k] for m in range(2, 17) for k in range(1, m + 1)], + "frozen family domain differs") + rows = [] + for m, k in cases["family_cases"]: + numerator, denominator, histogram = rank_support_count(m, k) + gl = general_linear_count(m) + require(gl % denominator == 0, "header orbit does not have integer fiber") + probability = Fraction(numerator, denominator) + if k == 1: + require(probability == Fraction(3 ** (m - 1), ((1 << m) - 1) * (1 << (m - 1))), "prior marginal mismatch") + if k == 2: + prior = Fraction(5 ** (m - 1) - 3 ** (m - 1), ((1 << m) - 1) * ((1 << m) - 2) * (1 << (m - 2))) + require(probability == prior, "prior4807 binary pair mismatch") + rows.append({"m": m, "k": k, "support_histogram": [count for unused, count in histogram], + "orbit_numerator": numerator, "orbit_denominator": denominator, + "probability": pair(probability), "header_fiber": gl // denominator}) + return rows + + +def make_example(cases, rows): + example = special_witness() + for key, expected in cases["example"].items(): + require(example[key] == expected, "explicit example differs from frozen tuple/header") + row = next(row for row in rows if (row["m"], row["k"]) == (7, 6)) + probability = Fraction(*row["probability"]) + marginal = Fraction(3 ** 6, ((1 << 7) - 1) * (1 << 6)) + product = marginal ** 6 + example.update({"joint_probability": pair(probability), "single_probability": pair(marginal), + "product_probability": pair(product), "ratio": pair(probability / product), + "ratio_gt_one": probability > product}) + require(example["ratio_gt_one"], "explicit six-event product comparison not positive") + return example + + +def generate(cases): + family = family_rows(cases) + small, actual_records = [], [] + require(cases["small_gl_dimensions"] == [2, 3, 4], "literal GL domain changed") + for m in cases["small_gl_dimensions"]: + profile, records = literal_headers(m) + small.append(profile) + actual_records.append({"m": m, "records": records}) + for k, count in enumerate(profile["joint_first_k"], 1): + row = next(row for row in family if (row["m"], row["k"]) == (m, k)) + require(Fraction(count, profile["gl_count"]) == Fraction(*row["probability"]), "literal GL orbit fraction differs") + span = literal_span_count(7, 6) + row = next(row for row in family if (row["m"], row["k"]) == (7, 6)) + require([count for unused, count in span["zero_u_histogram"]] == row["support_histogram"], "actual quotient-span support histogram differs") + value = {"schema_version": 1, "source_manifest_sha256": PIN_SHA, "case_manifest_sha256": CASE_SHA, + "family": family, "small_gl": small, "example": make_example(cases, family)} + diagnostic = {"family_cases": len(family), "complete_headers": sum(row["gl_count"] for row in small), + "literal_span": span, "controls": controls(), "receipt_controls": receipt_controls(value), + "code_sha256": sha(Path(__file__).read_bytes())} + return value, diagnostic, {"schema_version": 1, "domains": actual_records} + + +def nonnegative(value, name): + require(type(value) is int and value >= 0, name + " must be nonnegative integer, not bool") + + +def rational(value): + require(type(value) is list and len(value) == 2 and all(type(item) is int for item in value), "rational needs two integer entries") + require(value[1] > 0 and pair(Fraction(*value)) == value, "rational must be reduced with positive denominator") + + +def check_family(rows): + order = [(m, k) for m in range(2, 17) for k in range(1, m + 1)] + require(type(rows) is list and len(rows) == len(order), "family length invalid") + for row, (m, k) in zip(rows, order): + require(type(row) is dict and set(row) == FAMILY_KEYS, "family record keys invalid") + for name in FAMILY_KEYS - {"support_histogram", "probability"}: + nonnegative(row[name], "family " + name) + require((row["m"], row["k"]) == (m, k), "family order invalid") + hist = row["support_histogram"] + require(type(hist) is list and len(hist) == m, "support histogram length invalid") + for item in hist: + nonnegative(item, "support histogram count") + require(sum(hist) == row["orbit_numerator"] and row["orbit_denominator"] > 0 and row["header_fiber"] > 0, + "orbit count/fiber invalid") + rational(row["probability"]) + require(Fraction(*row["probability"]) == Fraction(row["orbit_numerator"], row["orbit_denominator"]), "orbit fraction differs") + + +def check_small(rows): + require(type(rows) is list and len(rows) == 3, "small GL profile count invalid") + for row, m in zip(rows, (2, 3, 4)): + require(type(row) is dict and set(row) == SMALL_KEYS, "small GL keys invalid") + require(type(row["m"]) is int and row["m"] == m, "small GL dimension invalid") + nonnegative(row["gl_count"], "GL count") + for key, size in (("mask_histogram", 1 << m), ("joint_first_k", m)): + require(type(row[key]) is list and len(row[key]) == size, "small GL histogram length invalid") + for item in row[key]: + nonnegative(item, "small GL count") + require(item <= row["gl_count"], "small GL count exceeds headers") + require(sum(row["mask_histogram"]) == row["gl_count"], "mask histogram count differs") + require(type(row["record_sha256"]) is str and len(row["record_sha256"]) == 64 + and all(char in "0123456789abcdef" for char in row["record_sha256"]), "GL record digest invalid") + + +def check_example(value): + require(type(value) is dict and set(value) == EXAMPLE_KEYS, "example keys invalid") + require(type(value["m"]) is int and value["m"] == 7 and type(value["k"]) is int and value["k"] == 6, "example dimension/arity invalid") + validate_family(value["u"], value["v_rows"], 7) + require(len(value["v_rows"]) == 6, "example must have six requests") + require(type(value["header_rows"]) is list and len(value["header_rows"]) == 7 + and all(type(row) is int and 0 <= row < 128 for row in value["header_rows"]), "example header invalid") + minors = value["proper_minors"] + require(type(minors) is list and len(minors) == 6, "example minor count invalid") + require(all(type(row) is list and len(row) == 6 and all(type(v) is int and v in (0, 1) for v in row) for row in minors), "example minors must be binary integers") + for key in ("joint_probability", "single_probability", "product_probability", "ratio"): + rational(value[key]) + require(type(value["ratio_gt_one"]) is bool, "example comparison must be bool") + + +def validate_receipt(value): + require(type(value) is dict and set(value) == COMMON, "receipt schema keys invalid") + require(type(value["schema_version"]) is int and value["schema_version"] == 1, "receipt schema_version must be integer1") + require(value["source_manifest_sha256"] == PIN_SHA and value["case_manifest_sha256"] == CASE_SHA, "receipt source/case binding differs") + check_family(value["family"]) + check_small(value["small_gl"]) + check_example(value["example"]) + + +def receipt_controls(value): + mutants = {} + bad = parse(canonical(value)) + bad["schema_version"] = True + mutants["boolean_version_rejected"] = bad + bad = parse(canonical(value)) + del bad["example"] + mutants["missing_profile_key_rejected"] = bad + bad = parse(canonical(value)) + bad["extra"] = 1 + mutants["extra_profile_key_rejected"] = bad + bad = parse(canonical(value)) + bad["family"][0]["support_histogram"][0] = False + mutants["boolean_histogram_rejected"] = bad + bad = parse(canonical(value)) + bad["example"]["ratio"][1] = True + mutants["boolean_rational_rejected"] = bad + result = {name: rejected(validate_receipt, bad) for name, bad in mutants.items()} + require(all(result.values()), "strict receipt control failed") + return result + + +def check_actual_records(path, expected): + with gzip.open(path, "rb") as stream: + raw = stream.read(8388609) + require(len(raw) <= 8388608, "actual GL record artifact exceeds8MiB") + value = parse(raw) + require(type(value) is dict and set(value) == {"schema_version", "domains"}, "actual GL artifact keys invalid") + require(type(value["schema_version"]) is int and value["schema_version"] == 1, "actual GL artifact version invalid") + require(type(value["domains"]) is list and len(value["domains"]) == 3, "actual GL artifact domains invalid") + for row, target in zip(value["domains"], expected["domains"]): + require(type(row) is dict and set(row) == {"m", "records"}, "actual GL domain keys invalid") + require(type(row["m"]) is int and row["m"] == target["m"], "actual GL domain order invalid") + require(type(row["records"]) is list and len(row["records"]) == len(target["records"]), "actual GL record count invalid") + for record in row["records"]: + require(type(record) is list and len(record) == 2 and all(type(v) is int for v in record), "actual GL record needs two integers") + require(0 <= record[0] < (1 << (row["m"] ** 2)) and 0 <= record[1] < (1 << row["m"]), "actual GL record out of range") + require(canonical(value) == canonical(expected), "actual complete primary GL records differ") + return {"actual_gl_records_compared": sum(len(row["records"]) for row in value["domains"]), + "actual_gl_canonical_sha256": digest(value), "decompressed_bytes": len(raw)} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path) + parser.add_argument("--check-primary", type=Path) + args = parser.parse_args() + require(not (args.emit and args.check_primary), "blind first emission cannot read primary data") + cases = authenticate() + retained = None if args.emit else parse((ROOT / "ORACLE.json").read_bytes()) + if retained is not None: + validate_receipt(retained) + value, diagnostics, actual_records = generate(cases) + validate_receipt(value) + if args.emit: + with args.emit.open("x") as stream: + json.dump(value, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + require(canonical(value) == canonical(retained), "retained oracle receipt differs") + if args.check_primary: + primary = parse(args.check_primary.read_bytes()) + validate_receipt(primary) + require(canonical(primary) == canonical(value), "actual complete primary receipt differs") + diagnostics["primary_data_comparison"] = check_actual_records(args.check_primary.parent / "SMALL-GL.json.gz", actual_records) + print("PASS_COMMON_IMAGE_FULL_GUARD_ORACLE " + canonical(diagnostics)) + + +if __name__ == "__main__": + try: + main() + except (ValueError, KeyError, TypeError, OSError) as error: + print("FAIL_COMMON_IMAGE_FULL_GUARD_ORACLE: " + str(error), file=sys.stderr) + sys.exit(1) diff --git a/research/common-image-full-guard-family/verify.py b/research/common-image-full-guard-family/verify.py new file mode 100644 index 0000000000..888d1a160f --- /dev/null +++ b/research/common-image-full-guard-family/verify.py @@ -0,0 +1,302 @@ +#!/usr/bin/env python3 +"""Binary full-guard common-image orbit formula and complete small-header census.""" +from collections import Counter +from fractions import Fraction +import argparse +import gzip +import hashlib +import json +import math +from pathlib import Path +import re +import sys + +ROOT = Path(__file__).resolve().parent +SOURCE_HASH = '680b0d75e9419b4577dd0710a8c430c512f12f9ae70ba9d0ce6c91acc3fbefc9' +CASE_HASH = '3da07e088ca190dc480ce52aab01c44816d334fe32b82ba88a9787f380e99273' +SCHEMA_HASH = 'c01cd12853adcce258701b3d8e56bfff7ba9d370223dcecccc62200ef8bd087a' + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def canonical(value): + return (json.dumps(value, sort_keys=True, separators=(',', ':')) + '\n').encode() + + +def unique(pairs): + value = {} + for key, item in pairs: + require(key not in value, 'duplicate JSON key') + value[key] = item + return value + + +def bad_number(value): + raise ValueError('nonfinite JSON number: ' + value) + + +def parse(raw): + return json.loads(raw, object_pairs_hook=unique, parse_constant=bad_number) + + +def same_typed(a, b): + if type(a) is not type(b): + return False + if isinstance(a, dict): + return a.keys() == b.keys() and all(same_typed(a[k], b[k]) for k in a) + if isinstance(a, list): + return len(a) == len(b) and all(same_typed(x, y) for x, y in zip(a, b)) + return a == b + + +def authenticate(): + for name, expected in [('SOURCE-PINS.json', SOURCE_HASH), ('CASES.json', CASE_HASH), ('SCHEMA.json', SCHEMA_HASH)]: + require(sha((ROOT / name).read_bytes()) == expected, 'immutable ' + name) + manifest = parse((ROOT / 'SOURCE-PINS.json').read_bytes()) + require(type(manifest) is dict and len(manifest['files']) == 8, 'eight inert sources') + for row in manifest['files']: + path = (ROOT / row['local_path']).resolve() + require(path.parent == (ROOT / 'inputs').resolve(), 'source containment') + raw = path.read_bytes() + require(len(raw) == row['bytes'] and sha(raw) == row['sha256'], 'source bytes/SHA256') + require(hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() == row['git_blob'], 'source Git blob') + return parse((ROOT / 'CASES.json').read_bytes()) + + +def rational(value): + return [value.numerator, value.denominator] + + +def gl_order(m): + return math.prod((1 << m) - (1 << i) for i in range(m)) + + +def available_columns(j, k): + if j < k - 1: + return 0 + return (1 << j) * math.prod((1 << j) - (1 << i) for i in range(k - 1)) + + +def family_row(m, k): + require(type(m) is int and type(k) is int and m >= 2 and 1 <= k <= m, 'common-image dimensions') + histogram = [math.comb(m - 1, j) * available_columns(j, k) for j in range(m)] + numerator = sum(histogram) + denominator = ((1 << m) - 1) * available_columns(m - 1, k) + require(gl_order(m) % denominator == 0, 'integer header fiber') + fiber = gl_order(m) // denominator + require(fiber == (1 << ((k - 1) * (m - k))) * gl_order(m - k), 'stabilizer block count') + return {'m': m, 'k': k, 'support_histogram': histogram, 'orbit_numerator': numerator, + 'orbit_denominator': denominator, 'probability': rational(Fraction(numerator, denominator)), + 'header_fiber': fiber} + + +def inverse(rows, m): + work = [row | (1 << (m + i)) for i, row in enumerate(rows)] + for col in range(m): + pivot = next((r for r in range(col, m) if (work[r] >> col) & 1), None) + if pivot is None: + return None + work[col], work[pivot] = work[pivot], work[col] + for r in range(m): + if r != col and ((work[r] >> col) & 1): + work[r] ^= work[col] + return [row >> m for row in work] + + +def rank(rows, m): + work = list(rows); pivot_row = 0 + for col in range(m): + pivot = next((r for r in range(pivot_row, len(work)) if (work[r] >> col) & 1), None) + if pivot is None: + continue + work[pivot_row], work[pivot] = work[pivot], work[pivot_row] + for r in range(pivot_row + 1, len(work)): + if (work[r] >> col) & 1: + work[r] ^= work[pivot_row] + pivot_row += 1 + return pivot_row + + +def multiply(left, right, m): + value = [] + for row in left: + result = 0 + for j in range(m): + if (row >> j) & 1: + result ^= right[j] + value.append(result) + return value + + +def apply(rows, vector): + return sum(((row & vector).bit_count() % 2) << i for i, row in enumerate(rows)) + + +def row_apply(row, matrix, m): + result = 0 + for j in range(m): + if (row >> j) & 1: + result ^= matrix[j] + return result + + +def outer(u, v, m): + return [v if (u >> i) & 1 else 0 for i in range(m)] + + +def projector(u, v, m): + return [row ^ (1 << i) for i, row in enumerate(outer(u, v, m))] + + +def minors(rows, m): + return [int(rank([row & ((1 << size) - 1) for row in rows[:size]], size) == size) + for size in range(1, m)] + + +def validate_tuple(u, covectors, m): + require(type(u) is int and 0 < u < (1 << m), 'nonzero common image vector') + require(all(type(v) is int and 0 < v < (1 << m) for v in covectors), 'covector encodings') + require(all((u & v).bit_count() % 2 == 1 for v in covectors), 'idempotence pairing') + require(rank(covectors, m) == len(covectors), 'independent covectors') + + +def small_gl(m): + last = 1 << (m - 1) + covectors = [last] + [last | (1 << i) for i in range(m - 1)] + validate_tuple(last, covectors, m) + projectors = [projector(last, v, m) for v in covectors] + records, histogram = [], [0] * (1 << m) + frequencies = [Counter() for _ in range(m)] + passing_orbits = [set() for _ in range(m)] + for code in range(1 << (m * m)): + header = [(code >> (m * i)) & ((1 << m) - 1) for i in range(m)] + inv = inverse(header, m) + if inv is None: + continue + mask = 0 + for i, p in enumerate(projectors): + conjugate = multiply(multiply(header, p, m), inv, m) + if all(minors(conjugate, m)): + mask |= 1 << i + records.append([code, mask]); histogram[mask] += 1 + transformed_u = apply(header, last) + transformed_v = [row_apply(v, inv, m) for v in covectors] + for k in range(1, m + 1): + key = (transformed_u, *transformed_v[:k]) + frequencies[k - 1][key] += 1 + if mask & ((1 << k) - 1) == (1 << k) - 1: + passing_orbits[k - 1].add(key) + require(len(records) == gl_order(m), 'complete GL census') + joints = [sum(count for mask, count in enumerate(histogram) if mask & ((1 << k) - 1) == (1 << k) - 1) for k in range(1, m + 1)] + for k in range(1, m + 1): + closed = family_row(m, k) + require(len(frequencies[k - 1]) == closed['orbit_denominator'], 'complete actual orbit coverage') + require(set(frequencies[k - 1].values()) == {closed['header_fiber']}, 'literal uniform conjugation fibers') + require(len(passing_orbits[k - 1]) == closed['orbit_numerator'], 'actual passing orbit count') + require(Fraction(joints[k - 1], len(records)) == Fraction(*closed['probability']), 'literal full-minor joint') + profile = {'m': m, 'gl_count': len(records), 'mask_histogram': histogram, + 'joint_first_k': joints, 'record_sha256': sha(canonical(records))} + return profile, {'m': m, 'records': records} + + +def example(spec): + m, k, u, vs, header = (spec[key] for key in ['m', 'k', 'u', 'v_rows', 'header_rows']) + validate_tuple(u, vs, m) + us = [outer(u, v, m) for v in vs] + for i, first in enumerate(us): + require(rank(first, m) == 1 and multiply(first, first, m) == first, 'literal rank-one idempotent') + nonzero_columns = {apply(first, 1 << j) for j in range(m)} - {0} + require(nonzero_columns == {u}, 'literal common image') + for j in range(i): + require(first != us[j] and multiply(first, us[j], m) == us[j] + and multiply(us[j], first, m) == first, 'distinct noncommuting family') + inv = inverse(header, m); require(inv is not None, 'example complete header') + guards = [minors(multiply(multiply(header, projector(u, v, m), m), inv, m), m) for v in vs] + require(all(all(row) for row in guards), 'literal complete proposed header') + joint = Fraction(*family_row(m, k)['probability']) + single = Fraction(3 ** (m - 1), ((1 << m) - 1) * (1 << (m - 1))) + product = single ** k; ratio = joint / product + require(joint == Fraction(22, 2667) and ratio > 1, 'six-family exact comparison') + return {'m': m, 'k': k, 'u': u, 'v_rows': vs, 'header_rows': header, + 'proper_minors': guards, 'joint_probability': rational(joint), + 'single_probability': rational(single), 'product_probability': rational(product), + 'ratio': rational(ratio), 'ratio_gt_one': ratio > 1} + + +def controls(): + require(minors(projector(7, 2, 3), 3) == [1, 0], 'first-pivot-only versus full-guard counterexample') + require(rank([4, 4], 3) < 2, 'duplicate rank control') + require(rank([8, 9, 10, 11], 4) == 3, 'distinct but dependent covectors control') + require((4 & 1).bit_count() % 2 == 0, 'nonidempotent wrong terminal column') + require(available_columns(0, 2) == 0 and available_columns(1, 2) < 4, 'rank constraint cannot be dropped') + for m in range(2, 17): + n = m - 1 + require(family_row(m, 1)['probability'] == rational(Fraction(3 ** n, ((1 << m) - 1) * (1 << n))), 'credited marginal k1') + prior_pair = Fraction(5 ** n - 3 ** n, ((1 << m) - 1) * ((1 << m) - 2) * (1 << (m - 2))) + require(family_row(m, 2)['probability'] == rational(prior_pair), 'credited transpose4807 k2') + require(not same_typed({'v': 1}, {'v': True}) and not same_typed({'v': 1}, {'v': 1.0}), 'strict number aliases') + + +def admit(value): + require(type(value) is dict and set(value) == {'schema_version', 'source_manifest_sha256', 'case_manifest_sha256', 'family', 'small_gl', 'example'}, 'receipt keyset') + require(type(value['schema_version']) is int and value['schema_version'] == 1, 'receipt version') + for key in ['source_manifest_sha256', 'case_manifest_sha256']: + require(type(value[key]) is str and re.fullmatch('[0-9a-f]{64}', value[key]), 'receipt digest') + require(type(value['family']) is list and len(value['family']) == 135, 'family domain') + for row in value['family']: + require(type(row) is dict and set(row) == {'m', 'k', 'support_histogram', 'orbit_numerator', 'orbit_denominator', 'probability', 'header_fiber'}, 'family keyset') + require(all(type(row[key]) is int for key in ['m', 'k', 'orbit_numerator', 'orbit_denominator', 'header_fiber']), 'family integers') + require(type(row['support_histogram']) is list and all(type(n) is int and n >= 0 for n in row['support_histogram']), 'support integer histogram') + return value + + +def compute(): + cases = authenticate() + families = [family_row(m, k) for m, k in cases['family_cases']] + small, domains = [], [] + for m in cases['small_gl_dimensions']: + profile, domain = small_gl(m); small.append(profile); domains.append(domain) + controls() + result = {'schema_version': 1, 'source_manifest_sha256': SOURCE_HASH, 'case_manifest_sha256': CASE_HASH, + 'family': families, 'small_gl': small, 'example': example(cases['example'])} + return admit(result), {'schema_version': 1, 'domains': domains} + + +def read_small(path): + with gzip.open(path, 'rb') as stream: + raw = stream.read(8388609) + require(len(raw) <= 8388608, 'small-GL decompressed bound') + return parse(raw) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', type=Path) + parser.add_argument('--write-small', type=Path) + args = parser.parse_args(); result, artifact = compute() + if args.write_small: + args.write_small.write_bytes(gzip.compress(canonical(artifact), mtime=0)) + path = args.write_small if args.write_small else ROOT / 'SMALL-GL.json.gz' + require(same_typed(read_small(path), artifact), 'all actual header-code/full-mask rows/types') + if args.emit: + args.emit.write_bytes(canonical(result)) + else: + retained = admit(parse((ROOT / 'RESULT.json').read_bytes())) + require(same_typed(retained, result), 'whole family/header/example profile') + print(json.dumps({'status': 'pass', 'family_cases': 135, 'complete_headers': 20334, + 'all_full_guards': True, 'seven_dimensional_header': 'explicit only'}, sort_keys=True)) + + +if __name__ == '__main__': + try: + main() + except (ValueError, OSError, KeyError, TypeError) as error: + print('FAIL: ' + str(error), file=sys.stderr) + raise SystemExit(1) from error