diff --git a/research/chain-balanced-multiplicities/README.md b/research/chain-balanced-multiplicities/README.md new file mode 100644 index 0000000000..c432642716 --- /dev/null +++ b/research/chain-balanced-multiplicities/README.md @@ -0,0 +1,133 @@ +# Balanced depth-three chain multiplicities break every unit symmetry + +**Claim type: finite certificate (exact counts for m = 2..24) with a short +scoped proof of its prime-characteristic consequence. No closed form, new +call count, tariff or kappa is claimed.** This contribution is produced by +Nick Petalas. + +## Object + +The unsigned depth-three dirty chain of +[research/chain-tariff](../chain-tariff/README.md) (PR #4257) has the calls +`1: z1 += B1 x`, `2: z2 += B2 z1` and `3: y += B3 z2` over a ring of exact +characteristic m. Its PROOF.md shows that a word is correct for the target +`y += c B3 B2 B1 x` exactly when every one-letter count and the subword counts +N12 and N23 vanish modulo m and N13 = c modulo m. Here Nij counts scattered +subwords i(i+1)...j. Let W(m,c) be the number of balanced words, with m copies +of each letter, that satisfy these conditions. The chain-tariff package asks +for a closed form for these multiplicities at arbitrary m. + +For the one-source depth-two connector, PR #4236 proves a count that depends +only on gcd(c,m) through Ramanujan sums. In particular, at prime m every +nonzero c has the same count. + +## Result + +**Finite certificate.** For every 3 <= m <= 24, the m-1 numbers +W(m,1), ..., W(m,m-1) are pairwise distinct. Consequently no nontrivial unit u +modulo m satisfies W(m,uc) = W(m,c) for all c. In this range, no formula for +W(m,c) can depend only on gcd(c,m), on c up to sign, or on any other +unit-invariant feature of c. The depth-two law therefore does not extend to +depth three, even at prime m. The first rows are: + +```text +m c=0 .. m-1 +2 42 0 +3 270 24 0 +4 2370 216 432 0 +5 15456 5340 6390 3000 2970 +6 216774 40320 96954 60228 84888 22320 +7 1636956 1102374 1231314 1119006 1214262 869862 1052352 +8 29455074 14150304 21697992 13892784 24824112 13586496 20537808 12071664 +``` + +[RESULT.json](RESULT.json) holds every exact count for m <= 24, with the +argmin and argmax nonzero residue per row. The zero entries are exactly the +exceptional targets (2,1), (3,2), (4,3) of the predecessor theorem. This +agrees with it and is not an independent audit of it. + +**Prime consequence (scoped proof).** Let p be prime, let V be the balanced +words with N12 = N23 = 0 modulo p, and let F(g) = sum over w in V of +zeta^(g N13(w)), with zeta a primitive p-th root of unity. Finite Fourier +inversion gives W(p,c) = (1/p) sum_g zeta^(-gc) F(g). The Galois automorphism +s_u (zeta to zeta^u) maps F(g) to F(ug). If s_u fixed F(1) for some unit +u != 1, then F(ug) = s_g(F(u)) = s_g(F(1)) = F(g) for every g != 0, and +F(0) is unchanged. Substituting g = u^(-1)h in the inversion formula then +gives W(p,uc) = W(p,c) for all c. The certificate excludes this for every +prime 3 <= p <= 23. Hence F(1) generates the full cyclotomic field Q(zeta_p) +there. At depth two the corresponding sum is rational at every prime, which is +why PR #4236's counts are equal. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/chain-balanced-multiplicities/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/chain-balanced-multiplicities/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/chain-balanced-multiplicities +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/chain-balanced-multiplicities --check-source-history +``` + +Any CPython 3.12 path can replace the local interpreter. Expected marker: +`PASS_CHAIN_BALANCED_MULTIPLICITIES max_m=24`. Each direct mode takes about +80 to 90 seconds locally (CPython 3.12, macOS arm64). These are check +durations, not performance claims. The verifier writes nothing unless given +`--write`, which regenerates RESULT.json. + +The verifier: + +- counts balanced words by a chronological dynamic program over the letter + counts and the residues of (N12, N23, N13), for m = 2..24; +- compares the complete residue distribution with an independent model for + m <= 7. That model fixes the A_k ones and B_k threes before the k-th 2, so + that N12 = sum A_k, N23 = sum (m - B_k) and N13 = sum A_k (m - B_k), and + weights each gap by a binomial interleaving count; +- compares it again with literal enumeration of every balanced word for m <= 5; +- checks the total mass (3m)!/(m!)^3 for every m; +- checks that the counts for nonzero residues are pairwise distinct and the + unit stabilizer is trivial for m = 3..24; +- as a positive control, reproduces PR #4236's equal depth-two counts + (binom(2p,p)-2)/p and full stabilizer at p = 2, 3, 5, 7, so the + distinctness test does detect equality when it holds; +- rejects a forged table with equal nonzero counts and compares the full + recomputation with RESULT.json. + +## Limits + +The certificate is finite: m <= 24. It does not prove distinctness, or even +nontrivial asymmetry, for larger m, and it gives no closed form. The +correctness criterion is the cited chain-tariff identity; no dirty-register +execution is repeated here. Only balanced words are counted. These are the +minimum words except at the three exceptional targets, whose minimum words +chain-tariff already counts. Multiplicity concerns schedule choice only. No +supplier caller, physical routing, admission, precision or outer +multiplication transfer is addressed. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +Structured versions with first steps and blockers are in [TASK.json](TASK.json). + +1. Does pairwise distinctness, or at least the trivial unit stabilizer, hold + for every m >= 3? At prime p this is the statement that F(1) is not fixed + by any nontrivial Galois automorphism. +2. Are the nonzero counts asymptotically equidistributed at prime m? The + relative spread falls to about 1.2e-7 at p = 23. Composite m stay far more + uneven, for example about 0.4% at m = 24 (spread is (max-min)/min). +3. Find a closed form or a holonomic recurrence for W(m,c). The certificate + only rules out unit-invariant shapes. + +## Credit and sources + +Nick Petalas's PR #4257 (research/chain-tariff, head +`91b4e49d0b80b0d8589f6e2cb23a0af75422e91b`) supplies the chain contract, the +interval-count correctness identity and the open question. Nick Petalas's +PR #4236 (research/unsigned-connector-residue-count, head +`bd9b426837cddd37338dd284e49cc2303de57ca0`) supplies the depth-two law used +for contrast and control. Rotation closure of correct chain words is observed +in research/depth5-chain-connector and is not used here. The complete-call +interface belongs to Ross Richardson's PR943/PR934 lineage and the +[universal connector](../universal-connector-boundary/README.md). Predecessor +results are cited, not rechecked. Pins are in [SOURCES.json](SOURCES.json). +New files are Apache-2.0. diff --git a/research/chain-balanced-multiplicities/RESULT.json b/research/chain-balanced-multiplicities/RESULT.json new file mode 100644 index 0000000000..506af526b6 --- /dev/null +++ b/research/chain-balanced-multiplicities/RESULT.json @@ -0,0 +1,463 @@ +{ + "balanced_counts": { + "10": [ + "6741578652", + "4679989200", + "6448414170", + "4700560080", + "6294527880", + "4865942100", + "6385100910", + "4722661080", + "6207295440", + "4643982780" + ], + "11": [ + "103966520994", + "102993204930", + "102235358082", + "102396100356", + "103115588532", + "102402283962", + "103208198214", + "101877228420", + "102439987782", + "101658692850", + "102112920888" + ], + "12": [ + "2220683565942", + "1794043350000", + "2059022210256", + "1842284425752", + "2118713742030", + "1778150784600", + "2148960751092", + "1784347776360", + "2108784411468", + "1847908709208", + "2067103426608", + "1755169970184" + ], + "13": [ + "38530109064648", + "38408860362522", + "38446223635872", + "38475075101658", + "38448201397164", + "38451602981064", + "38484193051434", + "38425192810446", + "38484531071454", + "38411027051982", + "38421870715488", + "38393080869468", + "38493387856092" + ], + "14": [ + "808172577659160", + "738965480678544", + "806859422030004", + "739115415609228", + "807265213137306", + "738197487800640", + "806761002071598", + "739759604685612", + "806636233594590", + "739223074696344", + "806774276954982", + "738938125213428", + "805914256360416", + "738570787903116" + ], + "15": [ + "15967720665428760", + "15820957783551510", + "15788984425851960", + "15934680254178450", + "15810983130410730", + "15802243668194484", + "15944844234786480", + "15824729026109070", + "15776887005480630", + "15936644942659890", + "15837022738773180", + "15779022408103500", + "15949999439065080", + "15807619499059170", + "15775007179275030" + ], + "16": [ + "339272283516824898", + "323183981099814048", + "338340164615398368", + "322973236971270144", + "339139546283955048", + "323205275835844512", + "338300184658683312", + "322900118476672128", + "339219853279383120", + "323223061197397152", + "338322310174185408", + "322976845559835840", + "339130993703537328", + "323162234813206560", + "338283049270273200", + "322916868540582336" + ], + "17": [ + "7016362063604527788", + "7016124620940427512", + "7015890054391059354", + "7016139801913433382", + "7016024746503159234", + "7015979867018175186", + "7016001399900224298", + "7016304224858630370", + "7016173243116229224", + "7015870039600124886", + "7016151000374920296", + "7015900942941657882", + "7016208457488359838", + "7015818903463436760", + "7015875711628795836", + "7016037189654896430", + "7016009307249323160" + ], + "18": [ + "152969581193896020474", + "148852970764034116572", + "152611652967963098364", + "149091469951762800864", + "152695385538799979070", + "148754760694466626656", + "152962634941754791164", + "148851121053717208008", + "152611937314074227574", + "149094106358286557952", + "152691506710294634982", + "148755877895351116368", + "152963973275284446552", + "148857056502816052944", + "152609267832933898926", + "149089011851493613296", + "152687241583188218226", + "148756535803306374588" + ], + "19": [ + "3282470615275403212026", + "3282456605652821013744", + "3282457911809211933444", + "3282454399015162642278", + "3282445890280233366108", + "3282471913946175183066", + "3282456851153571631146", + "3282444259434533358324", + "3282462184177270551132", + "3282457273985722142388", + "3282462185829820891812", + "3282458921153208129822", + "3282464319386671032342", + "3282444613604445173292", + "3282447304179273090942", + "3282445846627487841990", + "3282455821348797712692", + "3282449630841513342216", + "3282459628265130152766" + ], + "2": [ + "42", + "0" + ], + "20": [ + "72738274754022182072520", + "71733846909704375251080", + "72719452330999026035280", + "71726672348958875430120", + "72734376396812063927850", + "71736312338184793786296", + "72718278535839307815360", + "71728920944175594879360", + "72733930664075914566480", + "71732854925293824429480", + "72720803859471890262852", + "71727760283617184320560", + "72736722780155887954110", + "71732820291339683577000", + "72716964893906826421080", + "71730254758896201136560", + "72735525106065670954620", + "71734838896716629663760", + "72716669412804600420060", + "71726656003038291603480" + ], + "21": [ + "1605739257460465096761936", + "1605154012766710060292022", + "1604914672883371101374850", + "1605733707134151410815692", + "1605157466037655778241462", + "1604906376516623799054828", + "1605729788339671406423466", + "1605161661655994737719084", + "1604913369345497822783760", + "1605732816568795133107518", + "1605156992393682343071330", + "1604916912896412863735862", + "1605724066746114427290150", + "1605152962139214335184078", + "1604920525580575059184062", + "1605730575723507869888070", + "1605156229299955015009998", + "1604914323215879150876772", + "1605733329135227367381768", + "1605147853904096658262974", + "1604913035436668676724614" + ], + "22": [ + "36134267890536727230107490", + "35866457233917003406472364", + "36134234283284005470480120", + "35866439155728617511401436", + "36134248023133306714202700", + "35866454092337351733569880", + "36134260969595779815129228", + "35866438062058568640687000", + "36134245067636500365355500", + "35866426109716419815193816", + "36134235526833110352161982", + "35866457827501865224002012", + "36134257667914188681176124", + "35866432202204367568058628", + "36134242797988805204258964", + "35866456938459209726519856", + "36134244275951261953547232", + "35866452999425742631850352", + "36134238673992521943878646", + "35866435707989088202861080", + "36134228781599246368330590", + "35866433384449387110571620" + ], + "23": [ + "814029670554340980620640426", + "814029654233143776812602302", + "814029617760444674009405628", + "814029603030339488813195190", + "814029606566209387420648776", + "814029610158589140188293188", + "814029580316245291999017072", + "814029645483718904711321868", + "814029582740587396356587568", + "814029634253225557007940438", + "814029634819682646064986102", + "814029569931838499551352928", + "814029630025893266534244162", + "814029651738295494922196214", + "814029631248756756549675402", + "814029573131519169972588558", + "814029611978715843083153652", + "814029595551686194746741966", + "814029591283593539455391430", + "814029559626145648882814400", + "814029589229041484936154642", + "814029585448067484582598878", + "814029592295577372023597256" + ], + "24": [ + "18584382711354995772465208614", + "18508433917078281904723230192", + "18581870644389769248858566112", + "18509648102483541498446425488", + "18582939771653343294507442608", + "18507726393611424625062662544", + "18583974766812475751585240088", + "18508263874625401967877175872", + "18582272331059716825308348654", + "18509810503330218865203488304", + "18582545845216340911708417512", + "18507560444056980161899901856", + "18584374581232742949002000388", + "18508432748358987079985220768", + "18581867484432568572481241544", + "18509642067885542652377736432", + "18582946687807248637181630844", + "18507727558845523592040175872", + "18583977627206087830244983512", + "18508269849166417629004124400", + "18582264745022966518627050768", + "18509809335216503466913261344", + "18582542625848888564747785656", + "18507553468876187719360955088" + ], + "3": [ + "270", + "24", + "0" + ], + "4": [ + "2370", + "216", + "432", + "0" + ], + "5": [ + "15456", + "5340", + "6390", + "3000", + "2970" + ], + "6": [ + "216774", + "40320", + "96954", + "60228", + "84888", + "22320" + ], + "7": [ + "1636956", + "1102374", + "1231314", + "1119006", + "1214262", + "869862", + "1052352" + ], + "8": [ + "29455074", + "14150304", + "21697992", + "13892784", + "24824112", + "13586496", + "20537808", + "12071664" + ], + "9": [ + "372669012", + "297659664", + "292097772", + "344049198", + "311287158", + "283984218", + "342426744", + "285037542", + "290939742" + ] + }, + "distinct_nonzero_certificate": [ + { + "argmax_c": 1, + "argmin_c": 2, + "m": 3 + }, + { + "argmax_c": 2, + "argmin_c": 3, + "m": 4 + }, + { + "argmax_c": 2, + "argmin_c": 4, + "m": 5 + }, + { + "argmax_c": 2, + "argmin_c": 5, + "m": 6 + }, + { + "argmax_c": 2, + "argmin_c": 5, + "m": 7 + }, + { + "argmax_c": 4, + "argmin_c": 7, + "m": 8 + }, + { + "argmax_c": 3, + "argmin_c": 5, + "m": 9 + }, + { + "argmax_c": 2, + "argmin_c": 9, + "m": 10 + }, + { + "argmax_c": 6, + "argmin_c": 9, + "m": 11 + }, + { + "argmax_c": 6, + "argmin_c": 11, + "m": 12 + }, + { + "argmax_c": 12, + "argmin_c": 11, + "m": 13 + }, + { + "argmax_c": 4, + "argmin_c": 5, + "m": 14 + }, + { + "argmax_c": 12, + "argmin_c": 14, + "m": 15 + }, + { + "argmax_c": 8, + "argmin_c": 7, + "m": 16 + }, + { + "argmax_c": 7, + "argmin_c": 13, + "m": 17 + }, + { + "argmax_c": 12, + "argmin_c": 5, + "m": 18 + }, + { + "argmax_c": 5, + "argmin_c": 7, + "m": 19 + }, + { + "argmax_c": 12, + "argmin_c": 19, + "m": 20 + }, + { + "argmax_c": 3, + "argmin_c": 5, + "m": 21 + }, + { + "argmax_c": 6, + "argmin_c": 9, + "m": 22 + }, + { + "argmax_c": 1, + "argmin_c": 19, + "m": 23 + }, + { + "argmax_c": 12, + "argmin_c": 23, + "m": 24 + } + ], + "marker": "PASS_CHAIN_BALANCED_MULTIPLICITIES", + "max_m": 24 +} diff --git a/research/chain-balanced-multiplicities/SOURCES.json b/research/chain-balanced-multiplicities/SOURCES.json new file mode 100644 index 0000000000..833c9a9756 --- /dev/null +++ b/research/chain-balanced-multiplicities/SOURCES.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/chain-tariff/PROOF.md", + "usage": "input", + "git_blob": "d56fe647b056fb21360dd35dc2488feb770956e1", + "sha256": "14438bfb8f37d663a011dd47517fff83bca6447f37ffc5dfd433f88f4cbacb8b" + }, + { + "path": "research/unsigned-connector-residue-count/README.md", + "usage": "input", + "git_blob": "f221f46b41acfb85e8d5495287d6c3cdd141f349", + "sha256": "747bad959e5d3cc29b3a6444885e875f9c411945cb46449290d989f35d6476ed" + } + ], + "literature": [ + { + "pr": 4257, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4257", + "commit": "91b4e49d0b80b0d8589f6e2cb23a0af75422e91b", + "use": "Depth-three chain contract, interval-count correctness identity and the open multiplicity question. Cited, not rechecked." + }, + { + "pr": 4236, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4236", + "commit": "bd9b426837cddd37338dd284e49cc2303de57ca0", + "use": "Depth-two one-source multiplicity law, used as the contrasting shape and as an equal-count control at p=2,3,5,7." + }, + { + "path": "research/depth5-chain-connector/README.md", + "commit": "87f4a21e02c83fab559dcf1470dd0a97dfb89b8f", + "use": "Rotation closure of correct chain words; cited only, not used by the verifier." + } + ] +} diff --git a/research/chain-balanced-multiplicities/TASK.json b/research/chain-balanced-multiplicities/TASK.json new file mode 100644 index 0000000000..76ebdea6e5 --- /dev/null +++ b/research/chain-balanced-multiplicities/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "For the unsigned depth-three dirty chain of research/chain-tariff, count balanced correct words (m copies of each call) for every target c modulo m, m=2..24, and certify that the m-1 nonzero targets have pairwise distinct counts for 3<=m<=24. Consequently no formula depending only on gcd(c,m), or invariant under any nontrivial unit scaling of c, gives these multiplicities in that range, unlike the depth-two one-source law of PR4236.", + "scope_change_reason": "The card asks for a new connector operation. This keeps the alphabet and answers the chain-tariff open question on balanced minimum-word multiplicities as a counting side result: exact counts and a sharp obstruction to a gcd-only closed form, not a closed form.", + "bottleneck_link": "Side result: schedule multiplicity for a fixed connector word class. It does not change any call count, tariff, supplier bill or kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the exact counts and distinctness certificate once two independent models agree; leave a closed form and all-m statements as open questions.", + "outcome": "completed", + "evidence": "README.md; verify.py; RESULT.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Do the nonzero balanced counts stay pairwise distinct, or at least not unit-invariant, for every m >= 3?", + "why_it_matters": "An all-m statement would rule out every gcd-only or Ramanujan-sum closed form, not only for m <= 24.", + "first_step": "At prime p, show the character sum F(1) = sum over pair-valid balanced words of zeta_p^N13 is not fixed by any nontrivial Galois automorphism, for example by computing it modulo a prime above p.", + "blocked_by": "No structural formula for the joint (N12, N23, N13) distribution is known." + }, + { + "question": "Are the balanced counts asymptotically equidistributed over nonzero c at prime m?", + "why_it_matters": "The relative spread at p = 23 is about 1.2e-7, much smaller than at composite m. A quantitative bound would replace exact counting in schedule-choice arguments.", + "first_step": "Bound |F(gamma)| for gamma != 0 through the gap decomposition A_k, B_k used in verify.py.", + "blocked_by": "No cancellation estimate for the triple statistic sum A_k(m-B_k) is proved." + }, + { + "question": "Is there a closed form or a polynomial-in-m recurrence for W(m,c)?", + "why_it_matters": "It would answer the chain-tariff question; the certificate here shows only what shape it cannot take.", + "first_step": "Fit the 23-row table in RESULT.json against quasi-polynomial or holonomic ansatzes per residue class of m, then prove any fit.", + "blocked_by": "The table covers m <= 24 only; no candidate formula is known." + } + ] +} diff --git a/research/chain-balanced-multiplicities/VERIFY.json b/research/chain-balanced-multiplicities/VERIFY.json new file mode 100644 index 0000000000..1a1a4b9f19 --- /dev/null +++ b/research/chain-balanced-multiplicities/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/chain-tariff/PROOF.md", + "research/unsigned-connector-residue-count/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Chronological DP for m=2..24 against RESULT.json; independent gap model (m<=7) and literal word enumeration (m<=5) on the full (N12,N23,N13) residue distribution; multinomial mass; pairwise-distinct nonzero counts and trivial unit stabilizer for m=3..24; depth-two equal-count control at p=2,3,5,7; predecessor zero pattern; forged-table rejection." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "The same checks with Python assertions disabled; the verifier uses explicit checks." + } + ] +} diff --git a/research/chain-balanced-multiplicities/verify.py b/research/chain-balanced-multiplicities/verify.py new file mode 100644 index 0000000000..f086eb26e0 --- /dev/null +++ b/research/chain-balanced-multiplicities/verify.py @@ -0,0 +1,221 @@ +#!/usr/bin/env python3 +"""Exact balanced multiplicities of the unsigned depth-three chain. + +A balanced word has m copies of each letter 1, 2, 3. It is correct for +target c exactly when N12 = N23 = 0 and N13 = c modulo m, where Nij counts +scattered subwords i(i+1)...j (credited interval identity, research/chain-tariff). +This script counts those words for every m in 2..MAX_M and every c, checks +the counts by two independent models, and certifies that the m-1 nonzero +residues have pairwise distinct counts for 3 <= m <= MAX_M. +""" + +import hashlib +import json +import sys +from itertools import combinations +from math import comb, factorial +from pathlib import Path + +MAX_M = 24 +GAP_MAX_M = 7 +LITERAL_MAX_M = 5 +PACKAGE = Path(__file__).resolve().parent +MARKER = "PASS_CHAIN_BALANCED_MULTIPLICITIES" + + +def check(condition, message): + """Raise even under python -O.""" + if not condition: + raise SystemExit(f"FAIL: {message}") + + +def chrono_residues(m): + """Chronological DP: map (N12, N23, N13) mod m to word counts.""" + size = m * m * m + cells = [(p, q, r) for p in range(m) for q in range(m) for r in range(m)] + on_two = [[((p + a) % m * m + q) * m + r for p, q, r in cells] + for a in range(m + 1)] + on_three = [[(p * m + (q + b) % m) * m + (r + p) % m for p, q, r in cells] + for b in range(m + 1)] + layer = {(0, 0, 0): [1] + [0] * (size - 1)} + for _ in range(3 * m): + new = {} + for (a, b, c), vec in layer.items(): + moves = ((a < m, (a + 1, b, c), None), + (b < m, (a, b + 1, c), on_two[a]), + (c < m, (a, b, c + 1), on_three[b])) + for allowed, key, perm in moves: + if not allowed: + continue + out = new.setdefault(key, [0] * size) + for i, x in enumerate(vec): + if x: + out[i if perm is None else perm[i]] += x + layer = new + vec = layer[(m, m, m)] + return {cells[i]: x for i, x in enumerate(vec) if x} + + +def gap_residues(m): + """Independent model by the 1s and 3s preceding each 2. + + With A_k ones and B_k threes before the k-th 2, N12 = sum A_k, + N23 = sum (m - B_k) and N13 = sum A_k (m - B_k). Gap j between + consecutive 2s holds dA ones and dB threes in C(dA+dB, dA) orders. + """ + states = {(0, 0, 0, 0, 0): 1} + for _ in range(m): + new = {} + for (a, b, s12, s23, s13), w in states.items(): + for a2 in range(a, m + 1): + for b2 in range(b, m + 1): + key = (a2, b2, (s12 + a2) % m, (s23 + m - b2) % m, + (s13 + a2 * (m - b2)) % m) + weight = w * comb(a2 - a + b2 - b, a2 - a) + new[key] = new.get(key, 0) + weight + states = new + out = {} + for (a, b, s12, s23, s13), w in states.items(): + key = (s12, s23, s13) + out[key] = out.get(key, 0) + w * comb(2 * m - a - b, m - a) + return out + + +def literal_residues(m): + """Enumerate every literal balanced word and count its subwords.""" + out = {} + positions = range(3 * m) + for ones in combinations(positions, m): + rest = [i for i in positions if i not in ones] + for twos in combinations(rest, m): + word = [3] * (3 * m) + for i in ones: + word[i] = 1 + for i in twos: + word[i] = 2 + n1 = n12 = n2 = n23 = n13 = 0 + for letter in word: + if letter == 1: + n1 += 1 + elif letter == 2: + n12 += n1 + n2 += 1 + else: + n13 += n12 + n23 += n2 + key = (n12 % m, n23 % m, n13 % m) + out[key] = out.get(key, 0) + 1 + return out + + +def depth_two_counts(m): + """Control: one-source depth-two words B^m A^m, N_BA mod m.""" + out = [0] * m + for bs in combinations(range(2 * m), m): + seen = 0 + total = 0 + for i in range(2 * m): + if i in bs: + seen += 1 + else: + total += seen + out[total % m] += 1 + return out + + +def balanced_vector(residues, m): + return [residues.get((0, 0, c), 0) for c in range(m)] + + +def unit_stabilizer(m, w): + return [u for u in range(1, m) if all(w[u * c % m] == w[c] + for c in range(m)) and any(u * v % m == 1 for v in range(m))] + + +def check_models(): + for m in range(2, GAP_MAX_M + 1): + chrono = chrono_residues(m) + check(chrono == gap_residues(m), f"gap model differs at m={m}") + if m <= LITERAL_MAX_M: + check(chrono == literal_residues(m), f"literal differs at m={m}") + total = factorial(3 * m) // factorial(m) ** 3 + check(sum(chrono.values()) == total, f"mass at m={m}") + + +def check_depth_two_control(): + """At prime p the depth-two nonzero counts are equal (PR4236 law).""" + for p in (2, 3, 5, 7): + counts = depth_two_counts(p) + expected = (comb(2 * p, p) - 2) // p + check(counts[1:] == [expected] * (p - 1), f"depth-two control p={p}") + check(len(unit_stabilizer(p, counts)) == p - 1, + f"depth-two stabilizer p={p}") + + +def build_table(): + table = {} + for m in range(2, MAX_M + 1): + residues = chrono_residues(m) + total = factorial(3 * m) // factorial(m) ** 3 + check(sum(residues.values()) == total, f"mass at m={m}") + table[m] = balanced_vector(residues, m) + return table + + +def certificate(table): + rows = [] + for m in range(3, MAX_M + 1): + w = table[m] + nonzero = w[1:] + check(len(set(nonzero)) == m - 1, f"repeated nonzero count at m={m}") + check(unit_stabilizer(m, w) == [1], f"nontrivial stabilizer m={m}") + low = min(range(1, m), key=lambda c: w[c]) + high = max(range(1, m), key=lambda c: w[c]) + rows.append({"m": m, "argmin_c": low, "argmax_c": high}) + return rows + + +def check_controls(table): + exceptional = {(2, 1), (3, 2), (4, 3)} + for m in range(2, MAX_M + 1): + for c in range(1, m): + zero = table[m][c] == 0 + check(zero == ((m, c) in exceptional), f"positivity at {(m, c)}") + forged = dict(table) + forged[5] = [table[5][0], 1, 1, 1, 1] + rejected = True + try: + certificate(forged) + rejected = False + except SystemExit: + pass + check(rejected, "forged equal counts were accepted") + + +def receipt(table, rows): + body = {"marker": MARKER, "max_m": MAX_M, + "balanced_counts": {str(m): [str(x) for x in w] + for m, w in table.items()}, + "distinct_nonzero_certificate": rows} + text = json.dumps(body, indent=1, sort_keys=True) + "\n" + return body, text + + +def main(): + check_models() + check_depth_two_control() + table = build_table() + rows = certificate(table) + check_controls(table) + body, text = receipt(table, rows) + result_path = PACKAGE / "RESULT.json" + if "--write" in sys.argv[1:]: + result_path.write_text(text, encoding="utf-8") + stored = json.loads(result_path.read_text(encoding="utf-8")) + check(stored == body, "RESULT.json differs from recomputation") + digest = hashlib.sha256(text.encode()).hexdigest() + print(f"{MARKER} max_m={MAX_M} result_sha256={digest}") + + +if __name__ == "__main__": + main()