From fd1b2f3e103f11734750a0fe93aa2431fd5468ad Mon Sep 17 00:00:00 2001 From: SHIN09-git Date: Wed, 4 Nov 2026 02:53:14 +0800 Subject: [PATCH 1/3] Retain the depth-four source note and original depth-five witnesses --- .../chain-all-depth-powers/.gitattributes | 2 + .../source/6652-README.md | 192 ++++++++++++++++ .../chain-all-depth-powers/source/LICENSE | 201 ++++++++++++++++ .../source/depth5-witnesses.json | 217 ++++++++++++++++++ 4 files changed, 612 insertions(+) create mode 100644 research/chain-all-depth-powers/.gitattributes create mode 100644 research/chain-all-depth-powers/source/6652-README.md create mode 100644 research/chain-all-depth-powers/source/LICENSE create mode 100644 research/chain-all-depth-powers/source/depth5-witnesses.json diff --git a/research/chain-all-depth-powers/.gitattributes b/research/chain-all-depth-powers/.gitattributes new file mode 100644 index 0000000000..20cd7d6852 --- /dev/null +++ b/research/chain-all-depth-powers/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +source/** -text diff --git a/research/chain-all-depth-powers/source/6652-README.md b/research/chain-all-depth-powers/source/6652-README.md new file mode 100644 index 0000000000..f9edc0a6d3 --- /dev/null +++ b/research/chain-all-depth-powers/source/6652-README.md @@ -0,0 +1,192 @@ +# Repetition law for balanced depth-four chain schedules + +This package answers Open next question 2 of SHIN09-git's +[PR6080](https://github.com/CrocSwap/integer-mult-bounds/pull/6080) +(`research/chain-cyclic-schedules`): at depth four, which exact repetition +conditions replace the depth-three parity gate and cubic shift? + +**Answer.** A repeated block v^d, with v holding n copies of each letter and +m = dn, is correct for target c exactly when + +```text +(d odd or n even) and (3 does not divide d, or 3 divides n) and d | c, +``` + +and v itself is correct modulo n for target c/d. The cubic shift C(d,3)n^3, +which survives at depth three, and the new quartic shift C(d,4)n^4 both vanish +modulo m once the two gates hold. A new **triple gate** takes the place of the +depth-three cubic target shift. + +**Corollary.** If gcd(c,m) = 1, in particular for c = 1, no correct balanced +depth-four word has a nontrivial rotation symmetry. Every cyclic class then has +exactly 4m words, so 4m divides W4(m,c). At depth three a unit-target word can +repeat three times; at depth four it cannot repeat at all. + +Claim type: **scoped proof with bounded finite corroboration**. No κ, supplier, +paid-profile saving or physical speedup is claimed. The alphabet is unchanged; +this is a counting side result. + +## Contract + +Work over a nonzero unital ring of exact characteristic m >= 2 with five roles +z0 = x, z1, z2, z3, z4 = y, arbitrary initial data, immutable x and arbitrary +compatible linear maps. Letter l is one complete call z_l += B_l z_{l-1}, for +l = 1..4. A balanced word has m copies of each letter. Let N_ij count the +scattered subwords i(i+1)...j. Appending letter j adds N_{i,j-1} to N_ij for +i < j and increments N_jj, so by induction + +```text +z_j(final) = z_j(initial) + sum_{i<=j} N_ij B_j ... B_i z_{i-1}(initial). +``` + +This is the depth-four form of the interval identity in Nick Petalas's +chain-tariff proof (retained as `research/chain-cyclic-schedules/source/chain-tariff-PROOF.md`, +building on PR4249); the same induction and the same specialization argument +(identity maps, one initial register on at a time, exact characteristic) apply +unchanged. Hence a balanced word is correct for target c iff + +```text +N12 = N23 = N34 = N13 = N24 = 0 (mod m) and N14 = c (mod m). +``` + +Write W4(n,c) for the number of balanced words with n copies of each letter +satisfying these congruences modulo n. The convention W4(1,0) = 24 counts all +permutations of 1234 (congruences modulo 1 are vacuous), as in PR6080. + +## Proof + +**Composition formula.** Let w = v^d. An occurrence of the subword for the +interval I = [i,j] picks its letters from copies of v with nondecreasing copy +index. Grouping letters by copy splits I into consecutive nonempty parts +I_1,...,I_r placed in r distinct copies in increasing order, so + +```text +N_I(v^d) = sum over compositions (I_1,...,I_r) of I of C(d,r) * prod_k N_{I_k}(v). +``` + +With N_ll(v) = n and a = N12(v), b = N23(v), e = N34(v), p = N13(v), q = N24(v), +t = N14(v), and C_r = C(d,r): + +```text +N12(w) = d a + C_2 n^2 (likewise b, e) +N13(w) = d p + C_2 n(a+b) + C_3 n^3 (likewise q with b, e) +N14(w) = d t + C_2 (n q + a e + p n) + C_3 n^2 (a + b + e) + C_4 n^4. +``` + +**Pair gate.** This is PR6080's argument unchanged: N12(w), N23(w), N34(w) +are 0 modulo dn iff (d odd or n even) and a, b, e are 0 modulo n. Write +a = n alpha, b = n beta, e = n epsilon. Then C_2 n^2 = dn (d-1)n/2 with +(d-1)n even, so every term C_2 n^2 X with integer X is 0 modulo dn. + +**Triple gate.** Under the pair gate, N13(w) = d p + C_3 n^3 (mod dn). +This is 0 modulo dn iff d divides C_3 n^3 and p = -C_3 n^3/d (mod n). +Now C_3 n^3/d = (d-1)(d-2) n^3/6. The factor (d-1)(d-2) is always even, and +divisible by 3 unless 3 | d. So d | C_3 n^3 iff (3 does not divide d or 3 | n). +In that case C_3 n^3/(dn) = (d-1)(d-2) n^2/6 is also an integer, so the shift +is 0 modulo n and the condition is just p = 0 (mod n). The same holds for q. + +**Target.** Under both gates write p = n pi, q = n kappa. The C_2 term of +N14(w) is C_2 n^2 (kappa + alpha epsilon + pi), which is 0 modulo dn. The C_3 +term is C_3 n^3 (alpha + beta + epsilon), also 0 modulo dn. For the quartic +shift, C_4 n^4/(dn) = (d-1)(d-2)(d-3) n^3/24. If d is odd, (d-1)(d-3) is a +product of consecutive even numbers, so 8 divides it; if d is even then n is +even and 8 | n^3. One of d-1, d-2, d-3 is divisible by 3 unless 3 | d, and +then 3 | d-3. So the quartic shift is 0 modulo dn. Hence N14(w) = d t (mod dn), +which equals c modulo dn iff d | c and t = c/d (mod n). ∎ + +**Fixed points and classes.** As in PR6080, a word fixed by a rotation of +order d is v^d with v balanced of size n = m/d, and d must divide m. So + +```text +F_d(m,c) = W4(m/d, c/d) if (d odd or m/d even), (3 ∤ d or 3 | m/d) and d | c; + = 0 otherwise. +O(m,c) = (1/(4m)) sum_{d|m} phi(d) F_d(m,c). +``` + +Möbius inversion over divisors gives each least-period population exactly as +in PR6080. If gcd(c,m) = 1, every d > 1 fails d | c, so F_d = 0 for d > 1, +which proves the corollary. For c = 0, the gates alone decide: for example +m = 2 and m = 3 admit no periodic correct word, because d = 2 with n = 1 fails +the pair gate and d = 3 with n = 1 fails the triple gate. + +## Evidence + +`verify.py` uses the Python standard library only. It is a bounded checker of +the written proof, not a proof of every modulus. + +- Literal chronological interval counts of v^d agree with the composition + formula for all **1,508,928** (block, d) pairs: every block with n = 1, 2 and + d = 1..12, and every one of the 369,600 blocks with n = 3 and d = 1..4. +- The gate law agrees with literal correctness of v^d for every block, d and + target c in 0..m-1: **11,482,992** word-target checks, moduli up to m = 24. + The resulting fixed-point counts equal the F_d formula in every case. +- Full literal census for m = 1, 2, 3: W4(2,0) = 816 in 102 classes, + W4(3,0) = 24,984 in 2,082 classes, and W4(2,1) = W4(3,1) = W4(3,2) = 0. + Every correct word at m = 2, 3 is primitive. Least periods, rotation closure + and the Burnside sum agree with the class counts. +- The coefficient shift lemma (pair shift iff pair gate; d | C_3 n^3 iff triple + gate; dn | C_3 n^3 and dn | C_4 n^4 under both gates) for all d <= 240, + n <= 60. +- Five false claims are rejected by an explicit counterexample: dropping the + pair gate, dropping the triple gate, keeping the depth-three cubic target + shift, adding a quartic target shift, and not dividing the target by d. + +The zero nonzero-target counts at m = 2, 3 agree with Nick Petalas's +[PR4279](https://github.com/CrocSwap/integer-mult-bounds/pull/4279), which shows +that no balanced word is correct for c != 0 at m = 2..5. The corollary is +therefore vacuous for m <= 5. It is nonvacuous for 6 <= m <= 64, where +[PR4263](https://github.com/CrocSwap/integer-mult-bounds/pull/4263) and +[PR4280](https://github.com/CrocSwap/integer-mult-bounds/pull/4280) exhibit +balanced correct words for every c != 0. This package does not recheck those +witnesses; it only cites them for nonvacuity. + +## Reproduce + +From the repository root with CPython 3.12 (about 25 seconds locally): + +```sh +python3.12 -B research/chain-depth-four-repetition-law/verify.py +python3.12 -B scripts/research_package.py --package research/chain-depth-four-repetition-law +``` + +The verifier is read-only and prints a JSON receipt containing +`PASS_CHAIN_DEPTH_FOUR_REPETITION_LAW` and each package file's SHA-256. + +## Sources and overlap + +Base commit `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Exact provenance pins +are in [SOURCES.json](SOURCES.json). Predecessors: + +- SHIN09-git, [PR6080](https://github.com/CrocSwap/integer-mult-bounds/pull/6080): + depth-three repetition law, Burnside/Möbius transform and the question + answered here. The pair-gate argument and fixed-point reduction are theirs. +- Nick Petalas, [PR4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249) + and the chain-tariff proof: interval identity and correctness criterion. +- Nick Petalas, [PR6037](https://github.com/CrocSwap/integer-mult-bounds/pull/6037): + depth-three counts W(m,c). +- Nick Petalas, PR4263, PR4279 and PR4280: depth-four shortest lengths and + count vectors. They do not quotient rotations or count balanced words. + +Searches of merged README files and PR titles/bodies for depth-four rotation, +period and repetition laws found only PR6080's open question. No match is not +proof of novelty. + +## Open next questions + +Structured versions are in [TASK.json](TASK.json). + +1. What is the repetition law at general depth L? Depth three keeps a cubic + target shift; depth four loses every shift. First apply the composition + formula at depth five and reduce the four- and five-part shifts modulo dn + under the depth-four gates. Mixed products of lower interval counts appear + there and need their own argument. +2. What are the exact counts W4(m,c) and cyclic class numbers O(m,c) for + m >= 4? The law above turns any such census into class counts, but only + m <= 3 is counted here. First write a chronological residue DP over prefix + letter counts and the six off-diagonal interval residues; m = 4 has about + 2.6 million states. PR4280's row model may give a smaller state space. + +## Credit + +This package was produced by Nick Petalas. Predecessor credit is listed above. +New work is Apache-2.0. diff --git a/research/chain-all-depth-powers/source/LICENSE b/research/chain-all-depth-powers/source/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/chain-all-depth-powers/source/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/chain-all-depth-powers/source/depth5-witnesses.json b/research/chain-all-depth-powers/source/depth5-witnesses.json new file mode 100644 index 0000000000..aebd77d7a6 --- /dev/null +++ b/research/chain-all-depth-powers/source/depth5-witnesses.json @@ -0,0 +1,217 @@ +{ + "schema_version": 1, + "description": "One word per listed (m, c) with exactly m copies of each call 1..5; found by search_witnesses.c. Pairs absent from a row were not found by the bounded search; absence is not a proof of impossibility.", + "witnesses": { + "5": { + "1": "3452312415342513243152415" + }, + "6": { + "3": "432515234514352342421311523451" + }, + "7": { + "1": "41545521341233132545311545421342223", + "2": "12342513251144325514123351523435442", + "3": "12125323435155411325321243145245434", + "4": "54553233125115243415124134234421235" + }, + "8": { + "1": "3521314132344545354123551543521431222214", + "2": "1345523512523415432434511524432412115233", + "3": "5123212413445241251535234535111343245342", + "4": "4454453324115142333532415245153322211251", + "6": "2523412331151553423151354523421244512344" + }, + "9": { + "1": "233315251125314354323414452131445541255322241", + "2": "432122154132334554135412531344535254321221154", + "3": "252354122535332114232523541455511324414344131", + "4": "334251344221432112355455355431124122135244315", + "5": "145423343525315255312232431424125432551141431", + "6": "331345524411315511225233452512344433452421251", + "7": "412511352524243412135231454411435215323543523", + "8": "143155244514351231352444152342215335142352312" + }, + "10": { + "1": "45124315542123335224255312215133415544214134312435", + "2": "14523234444513154353122145515522233542312543114213", + "3": "12434322154433222535214511321423541545155233135144", + "4": "33111233451543234145535454254523312413512412124522", + "5": "13333415143121523325112242452112454553454534542123", + "6": "11454313225122435211131223524534443555214335541423", + "7": "31234525323143514552212213524134153412513454134254", + "8": "44543222432321242515353154351351111445532141324523", + "9": "54452532224553152412335344145411553312134232421113" + }, + "11": { + "1": "4441535214213534342225313414542111215333124453252351255", + "2": "2325253254115435324421454344511341215332452313515123214", + "3": "4121244133421532441553513124342122525353454343552131215", + "4": "2234242432545531353324131114511312243254551321442341555", + "5": "1244132351152554552431124231354542231445234511234135323", + "6": "3543534134414113325412311552552422241533455232432152411", + "7": "2353224535234521451421531242344431355452153341131522141", + "8": "1232245535135541353345321414345424511134423252112523124", + "9": "5111234124553454541221334152132532543422351314532543412", + "10": "4412535322415313111413521344231524442553451524322313525" + }, + "12": { + "1": "134524544135212143321541314224253125351342551341133525254342", + "2": "435231531523114244542415543332151111553213244135445433225222", + "3": "415555542212142523433511432142121331131524343544452523453213", + "4": "242553122124535314114514212232215155313452135344134432345453", + "5": "213513113545114534444121552442525243323254113352435225124133", + "6": "345333545343522315112444313551512524222542131315241314412524", + "7": "523431211122231553343542143432412412313155234544544355152152", + "8": "343324232211235155153254435342533512414441111122424334512555", + "9": "323241311243225524455514154432331432342411155532413552511234", + "10": "435352245415325235115435214231131542223132454531512413314244", + "11": "232454341254445355342212311534154431425123314515253311223521" + }, + "13": { + "1": "21324451513512314234324144413553541323355212245215422143113525543", + "2": "32113113433342555324115324512432442145554225311343245553224211514", + "3": "31113423112221445244355231255353254252433451441133525124134253541", + "4": "54132212313324452445341235512125311452415532143313523124554124453", + "5": "33432132442451224341315553215521444434135522512422535141535113321", + "6": "44253551324332134512554131245143115513524225414434332533421221215", + "7": "23414512525553151524352453315113234421513422345112441322343443215", + "8": "43351315213215442531524422315321435453455141412423545222512133413", + "9": "44123421515142355512453521451224432433432453552332132154111453213", + "10": "54525313251525431324155143142132245414121123443432532523143425351", + "11": "12414253554235142112235434332525143112435451245143443221151535233", + "12": "31234551553431344124531412232113242555213543152214213531243425445" + }, + "14": { + "1": "1544111511515415552334232333121223523325123344324545322542414215445431", + "2": "3334511525453514125112314112322441553231315254142334244455542342213235", + "3": "1551235552432344122434531142345415552234113223223341415524331145123541", + "4": "2335315432511113122334143251443111243424452532552132431523425254455451", + "5": "5254344411241241255242355345432125513324211143331554315342552231412331", + "6": "3135452425223143415422142121353314242315411153445315232351251324545543", + "7": "3453243552412352313222114354141111243215243423521334551414315554422355", + "8": "2433334241455254141233332245125125512132244152151235154154144233551433", + "9": "3215345242323331414125132132353521531454422241532155154315451432544142", + "10": "3454112544245552235523444212531351111121345353223113324314153252434452", + "11": "5143522345354122413231545521154553454124122131141324243233213415345523", + "12": "1354132251254253542214112521453442213334331254553135241455212345133414", + "13": "1133212421455522113152124323354531445535325445414112135242332434354521" + }, + "15": { + "1": "414314151455252531354232344452245131433532231431424153451231531321122545522", + "2": "154314315241113321424153552433524214422352543141513341345322423355512125542", + "3": "433244452241121153542213245414514315323433214413321525514352251515423531235", + "4": "144345413452131211233555453452425552423123331211314343551254453114223521224", + "5": "241154123124425531153332231224135545255551412144434331323324415555324214312", + "6": "143134451422242422332235543314151252352153454551113132224554151353314154324", + "7": "454532514151323234223133232541531143245451115551242541344211542152433342235", + "8": "515354321234251342412243413231314521535315125431424441132245511453554232325", + "9": "422541533553121552421354433433151551522453135324242141224541534341122321341", + "10": "345144234254151114323253132244551333211423354443322121235551145242145312555", + "11": "232543132522535445111522211245144312314244435454343143313235525131514155223", + "12": "241235412532512332334143555313443435141511454512432214155222431142423155253", + "13": "544124513242154411322533244115512551243552512534231142211345351333432434235", + "14": "453552334315543524233421145151235431452524531132414514224511511224231234323" + }, + "16": { + "1": "33325245113454332211451522244525114251453243553311435123422213151521253445143344", + "2": "34543231434113212344535431455435535131212323414522342255352511245444121152311225", + "3": "23551524534443353352324533124552222131442455311411225141522114343343213415412155", + "4": "34152553434534321513214352511454213451223321141525334524523354144231112255242413", + "5": "53452315252144324343431323155215431134412531431211115522435332252445254125434512", + "6": "55553445451322141312312122325312232323511234354554454414445532231243141455311231", + "7": "55443141212534512421523452534541451331525343122253111355415224142321534433123432", + "8": "24311324341135452252411125345521553132525222114155122443335341435452412433354341", + "9": "24353313334341522421112431454441341433124213215425253343555152512541525521252431", + "10": "24321215134134454141334532433215423141251152212335553355241432154225234452513154", + "11": "53522244152415312314523114151534534324145532533152214234453233415113521542314242", + "12": "12121554455233454133143325545524211232155241243425444242542511123335231133154331", + "13": "25351541521143313232152342354253522335152354221512142343144435544114142133125454", + "14": "22214545121511415335541335431543325523514411334124515545322323241142345212343224", + "15": "43525521155452312135515413334413413241343444515525121213442255253214414323212323" + }, + "17": { + "1": "2551233222542551113144532125113541424243131542523524352211114253424134344433335354155", + "2": "4353122345512114332353114111215235453555434312445552512422214334434432123551221442513", + "3": "1235554342434235521115151442253235511234414115245423335432233552323124425411114421533", + "4": "2434224333153411251432314541233513355433423115242554144534223454521515521212552123411", + "5": "3114333525524312135143231444434454453525225235353211432114453322415131111525521224524", + "6": "3433234111412542113524242351431434215411232112442323453355251124544335352125452551553", + "7": "1123145112422534113555143334321543122322444241335423355242514141533125445552352311425", + "8": "2512554143323455112214524435425432312324223155114343545143512435343311215225514134123", + "9": "1442541324435132152533145244325553152153155141212431341543143245231422332152443512523", + "10": "3224323521532335121522352441144325151545441355332412141322415141553215453444334231152", + "11": "1323534535414254145412442323345421215533152331344215352411441241532551315215222451332", + "12": "1532214231552311552322142322444445521411113331344135155332335214442522444135551324553", + "13": "2513533353231153442145225444431411311315454243153124352142211123254221524425535553432", + "14": "4341235423252211543342543153435434231542325231415435551311135515251114152342424243212", + "15": "1523411243534244113151544535133232224353211451424334522435554515214413122535352143212", + "16": "2312341215541351334455523332122352244423533454534335111455454411111213214242225152534" + }, + "18": { + "1": "432554243341534415345244233452331234415511454313254152121125124514123334232212531512153255", + "2": "213441413242331113542353122513325115453434515552312123444242225543354525412421145143235135", + "3": "321541342443333252432311431414213234225432423111425431155155535545242325132442115455311255", + "4": "341435451335115533135542133234241312323425213545225444521513241551131434224522154142423251", + "5": "115214524312511545512332254555233133422434335154554351425243234414214431511114252232412333", + "6": "351422341411115545122553352342335253524452322125213453243312141523451441145453231441543321", + "7": "152425445234251214353553153251532131352111231251221344451545133542324523434134423541242314", + "8": "151544513244445443521533332352141435511335523443244512322112151254433122515511231322244532", + "9": "422514515344412233241531513222155344522135414355454544352132353132512351433124443212111523", + "10": "312332215442423513243422531514545421155521154324443331334451513142211532215535244513534212", + "11": "411345434252553112435323153124443415211214224145255345351524311243242244312332351315535251", + "12": "145133443533544551444422125352535424131252343421241212522332135353515211235441512351413142", + "13": "323255521111154533142513122241111541455433222125234351341553523321432234545244434435144532", + "14": "323534234124325324245453353455415333551522334221123114221455251212141244545441135131542311", + "15": "432314244524154351212144321352355421511253513121253544223441535211124312342244533534133555", + "16": "111234543412553131332312454522335545325221425443122332144211311554231352241454135412344555", + "17": "443455535255322512454114551535122413311121332322324421235331542331143411421543521245432454" + }, + "19": { + "1": "23322322425213451155433411144532523154341355153355114253443452244324113451352415225121143243215", + "2": "45515351242533341424114325533251554141213535425144524123411112335341322532241434132125455234322", + "3": "35221155253241333213134315543142542222255333234124551245342414443451415513311143242515553411224", + "4": "21342245151553214141354244123535344231351122331252552451525524151143433335532514344144213231422", + "5": "53332512431545521233425254112221124534435332421335513214114543311441332232521444254311514455525", + "6": "42122135215544135315522122232423343253141341245551222131543552344443435134414313553122415145315", + "7": "12421341234255445431132234525115534115245343433214125241353522315454312111254234213334551543252", + "8": "24513215234235313254545123444543241151412415414235232313411453423345225125323211415512555343231", + "9": "43421145552233344215312345543311521322231322312443155235554422453531215124155114151344324254341", + "10": "34125421432312155213431355543353521144234511225334125344222234521532452354151111425143431424355", + "11": "54522331432532554432212433214145543315554351521131324135433115421353554112242441125351243421422", + "12": "15325455213431314444313344255453412512242114434134255213523432342511335342153524232125155212151", + "13": "21513322413521323432134255352453231444243414423215151351452153115111433213455245251523544244253", + "14": "55334353313421131314535534225214134244552441131312521231213325512215253544152144524443543421522", + "15": "42414531212525321123512254235135353214344232245213125145444555144423134335311511533113452452432", + "16": "15215243212323535114215543442552215252311244213544331135112121454453334133413134452242234355554", + "17": "22112535514413333344445135425334152211254315215332544512325232514113245211354134522413451425342", + "18": "32542253454121455152213315221521215443335531415443324134351544454233453144131522511332223541122" + }, + "20": { + "1": "3232335151132455122521143421452514532445452443333234532131124212544453543112151132555152253412441334", + "2": "5311521421533315534152421445144424431211133443514421542334234122542553351231322522455531221353354125", + "3": "1235432153152453343254213111314345454532145141121133225245255242324443542225113453335232152445513141", + "4": "4324343332541542512313515144315325535244241514232422251135114251451344225233233451423115354451221351", + "5": "2335343451211512145325114432521435511344255544432252153323532234251134312544344322545551123231142141", + "6": "5322533111124422334352525144345441155535135322351211433255411234314244234153242551215332351414124245", + "7": "3551444542353214535225242525424252433314323132545534552235114443331322312112114151315241143151132445", + "8": "4511352421451222124411524243123334525331155432511115433143255225514451442543353353113445542342231322", + "9": "1255324422145441245342133232234451153331334225234142521523352145531515341533345125152414521445132114", + "10": "1321155142422341352323354345341421535512421431121422454313433112121521243332435553444435242515515525", + "11": "5123441543354341515242132433211254541545232121321125143532333135241524535415443522155434342152243112", + "12": "3245435111133331551525544241312121214441134131352342421152423234333322442515254312254555452245355314", + "13": "2534112221153523445312531542325521512424455553134441321334552422242334445333415533132121111451453421", + "14": "1445411555523452541444241531323253513133352353522121544545311122234241541133114243214322524331422535", + "15": "5451344255431121332341512324434513515523125243312525554445334112224152152234115143133132324452435412", + "16": "5114434543544251115211354243315223541255532125234333512115145232413425252234534324115153142432134234", + "17": "2434415243543231542353314243524511122144412211551255315435424512111443544233324331523552133151235252", + "18": "5451221155341144355422432545432415111455353222524354121124255153334433314241313313453145122423222513", + "19": "2142354212344243153215422422325411112154131542151223153151541245534235333234343333245451455425453151" + } + }, + "m4_minimal_words": { + "1": "5523234534232123452343232111", + "2": "553345433212334543321211", + "3": "2345234553232123234534232111" + }, + "m4_description": "Depth five at m = 4: one shortest word per c, read back from the exhaustive BFS distance table (lengths 28, 24, 28)." +} From 9b8290041b4d3df17c73cdb0c9160c99775038b9 Mon Sep 17 00:00:00 2001 From: SHIN09-git Date: Wed, 4 Nov 2026 03:13:27 +0800 Subject: [PATCH 2/3] Classify balanced chain powers at all depths and count the short quintic classes --- research/chain-all-depth-powers/EXPECTED.json | 589 ++++++++++++++++++ research/chain-all-depth-powers/OVERLAP.json | 72 +++ research/chain-all-depth-powers/PROOF.md | 256 ++++++++ research/chain-all-depth-powers/README.md | 129 ++++ research/chain-all-depth-powers/ROOT-COUNT.md | 76 +++ research/chain-all-depth-powers/SOURCES.json | 85 +++ research/chain-all-depth-powers/TASK.json | 70 +++ research/chain-all-depth-powers/VALIDATION.md | 26 + research/chain-all-depth-powers/VERIFY.json | 46 ++ .../chain-all-depth-powers/audit_mutations.py | 102 +++ research/chain-all-depth-powers/census.py | 97 +++ research/chain-all-depth-powers/law.py | 80 +++ research/chain-all-depth-powers/oracle.py | 107 ++++ .../chain-all-depth-powers/order_checks.py | 58 ++ .../chain-all-depth-powers/quintic_rows.py | 119 ++++ research/chain-all-depth-powers/verify.py | 150 +++++ 16 files changed, 2062 insertions(+) create mode 100644 research/chain-all-depth-powers/EXPECTED.json create mode 100644 research/chain-all-depth-powers/OVERLAP.json create mode 100644 research/chain-all-depth-powers/PROOF.md create mode 100644 research/chain-all-depth-powers/README.md create mode 100644 research/chain-all-depth-powers/ROOT-COUNT.md create mode 100644 research/chain-all-depth-powers/SOURCES.json create mode 100644 research/chain-all-depth-powers/TASK.json create mode 100644 research/chain-all-depth-powers/VALIDATION.md create mode 100644 research/chain-all-depth-powers/VERIFY.json create mode 100644 research/chain-all-depth-powers/audit_mutations.py create mode 100644 research/chain-all-depth-powers/census.py create mode 100644 research/chain-all-depth-powers/law.py create mode 100644 research/chain-all-depth-powers/oracle.py create mode 100644 research/chain-all-depth-powers/order_checks.py create mode 100644 research/chain-all-depth-powers/quintic_rows.py create mode 100644 research/chain-all-depth-powers/verify.py diff --git a/research/chain-all-depth-powers/EXPECTED.json b/research/chain-all-depth-powers/EXPECTED.json new file mode 100644 index 0000000000..fae78a19c6 --- /dev/null +++ b/research/chain-all-depth-powers/EXPECTED.json @@ -0,0 +1,589 @@ +{ + "census": { + "fixed_target_bins": 804, + "orbits": { + "targets": 24, + "units": 10 + }, + "repeated_word_checks": 309184, + "rows": { + "L2_n1": { + "blocks": 2, + "classes": [ + 1 + ], + "counts": [ + 2 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 16 + }, + "L2_n2": { + "blocks": 6, + "classes": [ + 1, + 1 + ], + "counts": [ + 4, + 2 + ], + "fixed_target_bins": 72, + "repeated_word_checks": 48 + }, + "L2_n3": { + "blocks": 20, + "classes": [ + 2, + 1, + 1 + ], + "counts": [ + 8, + 6, + 6 + ], + "fixed_target_bins": 108, + "repeated_word_checks": 160 + }, + "L2_n4": { + "blocks": 70, + "classes": [ + 3, + 2, + 3, + 2 + ], + "counts": [ + 20, + 16, + 18, + 16 + ], + "fixed_target_bins": 144, + "repeated_word_checks": 560 + }, + "L3_n1": { + "blocks": 6, + "classes": [ + 2 + ], + "counts": [ + 6 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 48 + }, + "L3_n2": { + "blocks": 90, + "classes": [ + 7, + 0 + ], + "counts": [ + 42, + 0 + ], + "fixed_target_bins": 72, + "repeated_word_checks": 720 + }, + "L3_n3": { + "blocks": 1680, + "classes": [ + 30, + 4, + 0 + ], + "counts": [ + 270, + 24, + 0 + ], + "fixed_target_bins": 108, + "repeated_word_checks": 13440 + }, + "L4_n1": { + "blocks": 24, + "classes": [ + 6 + ], + "counts": [ + 24 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 192 + }, + "L4_n2": { + "blocks": 2520, + "classes": [ + 102, + 0 + ], + "counts": [ + 816, + 0 + ], + "fixed_target_bins": 72, + "repeated_word_checks": 20160 + }, + "L5_n1": { + "blocks": 120, + "classes": [ + 24 + ], + "counts": [ + 120 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 960 + }, + "L5_n2": { + "blocks": 113400, + "classes": [ + 2552, + 0 + ], + "counts": [ + 25520, + 0 + ], + "fixed_target_bins": 12, + "repeated_word_checks": 226800 + }, + "L6_n1": { + "blocks": 720, + "classes": [ + 120 + ], + "counts": [ + 720 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 5760 + }, + "L7_n1": { + "blocks": 5040, + "classes": [ + 720 + ], + "counts": [ + 5040 + ], + "fixed_target_bins": 36, + "repeated_word_checks": 40320 + } + }, + "total_blocks": 123698 + }, + "coefficients": { + "binomial_tests": 195072, + "d_range": [ + 1, + 128 + ], + "lower_vanishings": 59815, + "n_range": [ + 1, + 24 + ], + "surviving_boundaries": 2841 + }, + "credited_witnesses": { + "correct_powers": 552, + "powered_words": 1211, + "witness_splits": 519, + "witnesses": 173 + }, + "divisor_grid": { + "depths": [ + 2, + 16 + ], + "divisibility_comparisons": 979380, + "moduli": "2..96 and 125,175,250,350,360,900", + "targets": 102225, + "unit_targets": 53715 + }, + "examples": { + "bad_fifth_level": { + "depth": 6, + "interval_residues": { + "1": [ + 0, + 0, + 0, + 0, + 0, + 0 + ], + "2": [ + 0, + 0, + 0, + 0, + 0 + ], + "3": [ + 0, + 0, + 0, + 0 + ], + "4": [ + 0, + 0, + 0 + ], + "5": [ + 10, + 10 + ] + }, + "modulus": 50, + "repeats": 25 + }, + "correct_words": [ + { + "block": [ + 4, + 1, + 5, + 4, + 5, + 5, + 2, + 1, + 3, + 4, + 1, + 2, + 3, + 3, + 1, + 3, + 2, + 5, + 4, + 5, + 3, + 1, + 1, + 5, + 4, + 5, + 4, + 2, + 1, + 3, + 4, + 2, + 2, + 2, + 3 + ], + "depth": 5, + "dirty_basis_cases": 24, + "modulus": 35, + "period": 35, + "repeats": 5, + "target": 12 + }, + { + "block": [ + 1, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 5 + ], + "depth": 5, + "dirty_basis_cases": 24, + "modulus": 20, + "period": 10, + "repeats": 10, + "target": 4 + }, + { + "block": [ + 1, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 5 + ], + "depth": 5, + "dirty_basis_cases": 24, + "modulus": 50, + "period": 10, + "repeats": 25, + "target": 10 + }, + { + "block": [ + 1, + 1, + 2, + 2, + 3, + 3, + 4, + 4, + 5, + 5, + 6, + 6 + ], + "depth": 6, + "dirty_basis_cases": 28, + "modulus": 16, + "period": 12, + "repeats": 8, + "target": 0 + }, + { + "block": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "depth": 7, + "dirty_basis_cases": 32, + "modulus": 7, + "period": 7, + "repeats": 7, + "target": 1 + }, + { + "block": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11 + ], + "depth": 11, + "dirty_basis_cases": 48, + "modulus": 11, + "period": 11, + "repeats": 11, + "target": 1 + } + ], + "empty_root_witness": { + "period": 50, + "word": [ + 3, + 1, + 2, + 3, + 4, + 5, + 2, + 5, + 3, + 2, + 3, + 1, + 4, + 3, + 5, + 1, + 4, + 5, + 5, + 2, + 2, + 1, + 2, + 2, + 1, + 3, + 5, + 2, + 4, + 1, + 3, + 4, + 1, + 5, + 3, + 4, + 1, + 2, + 5, + 1, + 3, + 4, + 5, + 4, + 1, + 3, + 4, + 2, + 5, + 4 + ] + }, + "unbalanced_4748": { + "counts": [ + 2, + 4, + 4, + 4, + 4, + 2 + ], + "dirty_basis_cases": 28, + "period": 10, + "target": 1, + "word": [ + 1, + 2, + 3, + 4, + 5, + 6, + 5, + 4, + 3, + 2, + 1, + 2, + 3, + 4, + 5, + 6, + 5, + 4, + 3, + 2 + ] + } + }, + "quintic": { + "2": { + "gaps": { + "accepted_gap_pairs": 15888, + "all_words": 113400, + "middle_words": 90, + "restored_middle": 42, + "row": [ + 25520, + 0 + ] + }, + "split": { + "compatible_pairs": 113400, + "cut": 5, + "prefix_keys": 241, + "prefix_words": 2220, + "reverse_suffix_words": 2220, + "row": [ + 25520, + 0 + ] + } + }, + "3": { + "gaps": { + "accepted_gap_pairs": 2278152, + "all_words": 168168000, + "middle_words": 1680, + "restored_middle": 270, + "row": [ + 4697520, + 0, + 0 + ] + }, + "split": { + "compatible_pairs": 168168000, + "cut": 7, + "prefix_keys": 3084, + "prefix_words": 65100, + "reverse_suffix_words": 281400, + "row": [ + 4697520, + 0, + 0 + ] + } + }, + "m15": { + "W_target_3_modulo_75": 45, + "nonprimitive_words": [ + 0, + 0, + 0, + 4697520, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "period_15_classes": 313168 + } + }, + "retained_sources": { + "source/6652-README.md": "ee228e3adaf3becd65b63f42f328099095d06c94125a4447e71512faf100f7d1", + "source/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "source/depth5-witnesses.json": "ea320e9f069de8864952ad4b5e492875c1102bd1d12074f606b8aad2b54fe254" + }, + "status": "PASS_CHAIN_ALL_DEPTH_POWERS", + "zero_spectra": { + "examples": { + "L4_m64": [ + 8, + 16, + 32, + 64, + 128, + 256 + ], + "L5_m20": [ + 50, + 100 + ], + "L5_m360": [ + 150, + 300, + 450, + 600, + 900, + 1800 + ], + "L7_m84": [ + 294, + 588 + ] + }, + "explicit_words": 585 + } +} diff --git a/research/chain-all-depth-powers/OVERLAP.json b/research/chain-all-depth-powers/OVERLAP.json new file mode 100644 index 0000000000..0930f34ad3 --- /dev/null +++ b/research/chain-all-depth-powers/OVERLAP.json @@ -0,0 +1,72 @@ +{ + "entry": { + "searched_at": "2026-11-03T18:56:28.481574+00:00", + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "terms": [ + "chain-depth-four-repetition-law", + "chain-cyclic-schedules", + "depth-five repetition", + "general depth L", + "unit-target repetition", + "prime depth" + ], + "coverage": { + "local": { + "head": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "records": 8918, + "head_records": 8917, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-11-03T18:52:00.117779+00:00", + "complete_pagination": true, + "records": 635 + }, + "discussions": { + "fetched_at": "2026-11-03T18:55:30.179172+00:00", + "complete_pagination": true, + "records": 6754 + }, + "closed_prs": { + "fetched_at": "2026-11-03T18:56:27.712514+00:00", + "complete_pagination": true, + "records": 5528 + } + }, + "warnings": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 7 + }, + "nearest": [ + { + "pr": 6080, + "addition": "Depth-three repetition and cyclic grouping are credited inputs." + }, + { + "pr": 6652, + "head": "e364eeb19e5268967189ed12aa4813ee73edf3dc", + "addition": "Depth-four law and explicit arbitrary-depth follow-up; current result covers every depth." + }, + { + "pr": 4281, + "addition": "Depth-five existence witnesses, including the n=7 target-one block." + }, + { + "pr": 4748, + "addition": "Unbalanced binary depth-six unit square, used as a scope boundary." + } + ], + "targeted_pr_queries": [ + "6080", + "6652", + "chain repetition", + "prime depth", + "balanced necklace", + "4,697,520", + "4697520", + "W5(3,0)", + "313,168" + ], + "scope": "Open and closed/merged PR metadata, indexed Discussion records, local README/task notes and separate exact-head source inspection. Historical diffs, unpublished work and literature priority are outside this coverage." +} diff --git a/research/chain-all-depth-powers/PROOF.md b/research/chain-all-depth-powers/PROOF.md new file mode 100644 index 0000000000..7082bcc951 --- /dev/null +++ b/research/chain-all-depth-powers/PROOF.md @@ -0,0 +1,256 @@ +# Repetition at every depth of the balanced unsigned chain + +For a balanced block with n copies of each of L letters, repeat it d times +and set m=dn. Define q to be the least prime divisor of d that does not +divide n. Set q=∞ when there is no such prime. The comparison of q with L +determines the power law. At qL the target is multiplied by d. At q=L exactly one shift survives. Its +value is (d/L)n^L modulo m. + +This answers open question 1 of Nick Petalas's depth-four study. The +induction below handles every target, including zero, and the mixed products +of lower interval counts at every depth. [PR #6652](https://github.com/CrocSwap/integer-mult-bounds/pull/6652) + +## Model and starting result + +Let L≥2 and m≥2. Letter j is the complete call `z_j += B_j z_(j-1)`. +All roles are distinct, z_0 is immutable, their initial values are arbitrary +and the maps are arbitrary compatible linear maps over a nonzero unital +ring of exact characteristic m. The desired endpoint restores every +intermediate and adds c B_L ⋯ B_1 z_0 to z_L. A balanced word contains +m copies of each letter. Target residues include c=0. + +Write N_I(v) for the number of scattered copies of the consecutive label +sequence I=[i,j]. Their positions in v need only increase. The coefficient +on the initial z_(i-1) in the final z_j is N_I(v) B_j ⋯ B_i. Appending +letter j proves this identity by induction. Thus all proper interval counts +must vanish modulo m, and N_[1,L] must equal c. Sufficiency follows from the +expansion. Necessity follows by choosing identity maps over the ring itself +and turning on each initial role separately. This is the credited chain +criterion. [PR #4249](https://github.com/CrocSwap/integer-mult-bounds/pull/4249) · [PR #4257](https://github.com/CrocSwap/integer-mult-bounds/pull/4257) + +Let W_L(n,t) count literal balanced blocks correct modulo n for t. Use +W_L(1,0)=L! as a counting convention. When n=1 every permutation meets +the vacuous congruences. The physical ring contract starts at m=2. + +In word combinatorics this interval encoding is the transpose of the +classical Parikh matrix for the ordered alphabet. [Mateescu, A. Salomaa, +K. Salomaa and Yu (2001)](https://www.numdam.org/item/ITA_2001__35_6_551_0/) + +## 1. The first surviving coefficient + +Write C(d,j)=0 for j>d. For 2≤jj, so j +costs no factor of ℓ. At ℓ|n, the factor n^(j−1) supplies at least j−1 +powers of ℓ, which is at least the exponent of ℓ in j. This proves (1), +including when q=∞. + +At finite q=p, write C(d,p)=(d/p)C(d−1,p−1). The last binomial coefficient +is 1 modulo p. Its numerator factors d−1 through d−p+1 reduce to the +nonzero residue classes, as do the denominator factors. Consequently + +```text +C(d,p)n^p = (d/p)n^p (mod dn), d does not divide (d/p)n^p. (2) +``` + +Indeed the difference on the left is a multiple of d n^p, and p∤n. +Equations (1) and (2) locate the *first* offending level. No conditions on +later pure coefficients are necessary. + +## 2. Power law and fixed points + +The integer composition identity used in #6652 is also the matrix power +formula in Theorem 3.1 of Atanasiu, Poovanandran and Teh. The contribution +here is its modular reduction under balanced endpoint constraints. +[Parikh Matrices for Powers of Words](https://arxiv.org/pdf/1808.04102) + +The identity groups a scattered interval +by the distinct copies of v used in v^d. For every division of I into +j consecutive nonempty intervals I_1,…,I_j, its contribution is + +```text +C(d,j) N_(I_1)(v) ⋯ N_(I_j)(v). +``` + +Summing over divisions gives N_I(v^d), including d N_I(v) from j=1. +Take all intervals in increasing length. Singletons have count n in the +block and dn in the repeated word. Suppose the smaller proper interval +counts in v are multiples of n. Each j-part product with j≥2 is then a +multiple of n^j. For length hL. (3) +``` + +Only the first case uses division by L, and L is then a prime divisor of d. +The top count of v^d equals d times the full-interval count of v, plus s, +modulo dn. This proves the full +repetition criterion. + +**Fixed-count formula.** For d|m and n=m/d, the number F_d of correct words +fixed by a rotation of order d is + +```text +0 if qL the power is the identity. Thus +ℓ=L, which recovers the only possible prime and the target residue. +The original balanced-word argument supplies the exact number in (8). + +## 5. Concrete checks at depth five + +At L=5 an order d is obstructed if a prime among 2 or 3 divides d but +not n. A surviving fifth-level shift occurs precisely when 5|d and 5∤n +under the lower gates. For d=10,n=2 the sorted block repeats correctly at +m=20,c=4 with period 10. This attains the divisor bound D=10 for a nonzero +nonunit target. + +At the same depth with m=50, targets 5 and 10 agree modulo 5. They give +D=5 and D=25 respectively. At target 10 the block 1122334455 repeated +25 times attains period 10. This is where checking the congruence only +modulo 5 would lose the distinction modulo 25 in (6). + +For a nonzero unit example, take Nick Petalas's (n,t)=(7,1) witness + +```text +41545521341233132545311545421342223 +``` + +Repeating it five times gives m=35 and c=5+7^5=12 modulo 35. The resulting +175-call word has least period 35. The verifier also executes it on every +dirty basis input with noncommuting two-coordinate maps. [PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281) + +At modulus 15, equation (4) reduces *all* nonprimitive depth-five targets +to a single three-residue row at modulus 3. Two complete counts give +4,697,520 words of least period 15 at target 3, forming 313,168 shorter +classes. Every other target has zero nonprimitive words. [Finite certificate](ROOT-COUNT.md) + +The proof concerns the complete-call algebraic endpoint and its cyclic +multiplicities. Physical scheduling prices depend on the caller and its +implementation. The κ and supplier decisions belong to that separate cost +analysis. + +The balance hypothesis matters. Nick Petalas's depth-six binary word +`(1234565432)^2` has unit target 1 and period 10. Its six letter counts +are (2,4,4,4,4,2), whereas a balanced binary word would have two of each +letter. The verifier replays its full endpoint as a boundary example. +[PR #4748](https://github.com/CrocSwap/integer-mult-bounds/pull/4748) diff --git a/research/chain-all-depth-powers/README.md b/research/chain-all-depth-powers/README.md new file mode 100644 index 0000000000..c512f7bbff --- /dev/null +++ b/research/chain-all-depth-powers/README.md @@ -0,0 +1,129 @@ +# Which balanced chain schedules can repeat? + +At every depth L≥2, a single prime determines whether a repeated block can +reach the required endpoint. Let d be the repetition factor, n the copies +of each label in one block, and m=dn. Find the smallest prime q dividing d +but not n, with q=∞ if none exists. + +| Relation | Result for a block that is correct modulo n for target t | +|---|---| +| qL | The repeated target is d t modulo m. | +| q=L | The repeated target is d t+(d/L)n^L modulo m. | + +For q≥L the shorter block must also satisfy every proper interval condition. +These rules give the exact count fixed by each rotation in terms of the +shorter literal count W. They answer open question 1 of the depth-four +study. [Proof](PROOF.md) · [PR #6652](https://github.com/CrocSwap/integer-mult-bounds/pull/6652) + +Three consequences make the rule concrete. + +- For target zero the shortest rotation period is L times the product of + the distinct primes dividing m that are at most L. The proof constructs + every allowed least period. For L=5,m=360 the minimum is 150. +- For a unit target, a nonprimitive word can exist only at prime depth + L=p, with m=pn, p∤n and c=n^p modulo p. It repeats exactly p times and + the shorter-block multiplicity decides existence. A retained 35-letter + block gives a 175-letter unit-target word of least period 35 at m=35,c=12. +- Of all length-75 correct words at L=5,m=15, exactly 4,697,520 have a + shorter period. All have c=3 and form 313,168 classes of period 15. + Two complete, separately implemented counts of the small root row + establish the number. [Numerical certificate](ROOT-COUNT.md) + +The proof also gives a closed divisor D whose divisors are exactly the +arithmetically eligible rotation orders. The distinction between eligibility +and existence matters. At L=5,m=10,c=7 the candidate order 5 has zero +fixed words because W_5(2,1)=0. An explicit correct primitive word for this +target is checked. + +## Reproduce + +From the repository root, using Python 3.12 and its standard library, + +```sh +python3.12 -I -W error -B research/chain-all-depth-powers/verify.py +python3.12 -I -O -W error -B research/chain-all-depth-powers/verify.py +python3.12 -I -W error -B research/chain-all-depth-powers/audit_mutations.py +python3.12 -B scripts/research_package.py --package research/chain-all-depth-powers +``` + +The scientific verifier reads only the exported package. Its JSON output +contains `PASS_CHAIN_ALL_DEPTH_POWERS`, the recomputed [EXPECTED.json](EXPECTED.json) +data and every package file's SHA-256. The fault-injection command uses +temporary private copies. See [validation](VALIDATION.md) for the observed +environment and publication checks. + +## Evidence and limits + +- A position-based subsequence counter and a chronological integer matrix + executor check all 123,698 blocks in the specified domains. The corpus + covers n=1 through depth 7, n=2 through depth 5, n=3 through depth 3 + and (L,n)=(2,4). There are 309,184 direct repeated-word comparisons + and 804 fixed-point count bins. For 24 small (L,m,c) cases, literal + rotation classes and least periods agree with the divisor transforms. +- The two depth-five counters group words by prefix/suffix and by the + middle three labels, respectively. They cover the full multinomial + mass of 168,168,000 at n=3 and 113,400 at n=2. At n=2 the row also + agrees with the separate literal word census. +- An arithmetic check covers 195,072 binomial coefficients for 1≤n≤24 + and 1≤d≤128. The closed divisor formula agrees with direct unreduced + binomial gates in 979,380 order tests over 102,225 (L,m,c) cases, including + 53,715 unit targets. Depths are 2..16. Moduli are 2..96 and six larger + composites through 900. There are 585 constructed zero-target words + with literally checked least periods. +- All 173 retained depth-five witnesses are executed at byte-pinned + source and raised to seven powers each. The run also checks 519 prefix/ + inverse-suffix joins on their positive targets. Six balanced examples + and the credited unbalanced depth-six boundary have complete basis checks + with noncommuting two-coordinate maps, including a singular family. +- The mutation audit attempts 17 specific code and data changes in both + Python modes, plus two unchanged positive probes. Each mutation must + reach its named semantic check. + +The finite evidence supports a written proof for all depths, moduli and +targets in the balanced unsigned model. W at larger roots remains an input +to the counting transform. The engines share the same assisted author and +Python integer semantics. Physical routing, precision, supplier prices and +independent mathematical review have separate obligations. + +The largest half-word search in the registered verifier has 5^8 lexical +candidates. The largest gap-weight matrix has 220² entries. Full enumeration +stops at the stated corpus; powers of upstream words stop at d=12. Python +performs bounded dynamic allocations. The checker launches no network calls, +and each mutation subprocess has an explicit timeout. + +## Task, overlap and credit + +The `connector-alphabet-change` card is recorded as changed. We investigate +period accounting for the existing complete calls. This supplies exact +deduplication and census checks for future connector studies. Improving κ +would require a priced supplier contract. The orientation baseline reproduced +its 945 pairings. Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8. [Task](TASK.json) · [Overlap coverage](OVERLAP.json) + +Nick Petalas supplied the depth-four law, the depth-five witnesses and the +unbalanced depth-six example. SHIN09-git's depth-three work supplied the +cyclic fixed-point formulation. The earlier complete-call model credits +Ross Richardson's #943/#934 lineage. The depth-four source note at +`e364eeb19e5268967189ed12aa4813ee73edf3dc` is retained byte-for-byte in +publication ancestor `fd1b2f3e103f11734750a0fe93aa2431fd5468ad`; its original +head, path and blob accompany the retained pin. [Exact source manifest](SOURCES.json) · [#6080](https://github.com/CrocSwap/integer-mult-bounds/pull/6080) · [#6652](https://github.com/CrocSwap/integer-mult-bounds/pull/6652) · [#4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281) · [#4748](https://github.com/CrocSwap/integer-mult-bounds/pull/4748) + +The Parikh matrix encoding, its integer power expansion, Burnside's lemma and +Möbius inversion are classical. Our contribution is the reduction modulo dn, +the eligible-order divisor, the sharp zero-target spectrum, and the scoped +depth-five counts. [Mateescu et al.](https://www.numdam.org/item/ITA_2001__35_6_551_0/) · [Atanasiu, Poovanandran and Teh, Theorem 3.1](https://arxiv.org/pdf/1808.04102) + +Prepared for SHIN09-git with substantial OpenAI Codex assistance in +derivation, implementation, checking and writing. Apache-2.0. + +## Open next questions + +1. What is W_5(7,1)? It is the exact number of repeated words at m=35,c=12. + The retained witness proves positivity. Start by profiling the middle-gap + method at n=4 against the n=2,3 baselines before committing to the larger + count. Growth of the middle words and gap pairs is the obstacle. +2. How do the gates change for unequal positive letter counts? Start with + the (2,4,4,4,4,2) binary profile of #4748. A length-p pure term then + contains the product of nonuniform singleton counts, so the obstruction + used for a balanced block can disappear. diff --git a/research/chain-all-depth-powers/ROOT-COUNT.md b/research/chain-all-depth-powers/ROOT-COUNT.md new file mode 100644 index 0000000000..692727fa9e --- /dev/null +++ b/research/chain-all-depth-powers/ROOT-COUNT.md @@ -0,0 +1,76 @@ +# A numerical consequence at depth five and modulus fifteen + +Among the correct balanced words of length 75, exactly 4,697,520 have a +nontrivial repetition. They all have target 3, least period 15 and form +313,168 cyclic classes. The other fourteen target residues have no shorter +classes. The total number of primitive length-75 words is a separate count. + +Here orders dividing 15 are 1, 3, 5 and 15. Orders 3 and 15 fail at a proper +interval of length three. For order 5 the shorter block has three copies of +each letter. The shift is 3^5=3 modulo 15. Only c=3,8,13 admit a root, +with respective residues 0,1,2 modulo 3. The two exact methods below give + +```text +W_5(3,0), W_5(3,1), W_5(3,2) = 4,697,520, 0, 0. +``` + +Every repeated word therefore has maximal repetition 5, giving the claimed +number of classes after division by 15. In particular W_5(15,3)=45 modulo +75, while W_5(15,c)=0 modulo 75 at every other c. [General law](PROOF.md) + +## Count by a prefix and an inverse suffix + +Split a balanced length-15 word after its seventh letter. Enumerate the +65,100 prefixes of length 7 and the 281,400 reversed suffixes of length 8 +having at most three copies of each label. Keep their exact five letter +counts. Complementary counts enforce balance. + +Let P denote the unitriangular prefix action and S the suffix action, with +chronological composition S P. The target condition S P=I+cE is equivalent +to P=S^(-1)+cE, since E is the bottom-left matrix unit. To compute S^(-1), +process the reversed suffix with a negative shear at each call. Equivalently, +the interval of length h in its unsigned action acquires the sign (-1)^h. + +For a prefix, key a histogram by its five counts and nine proper nonsingleton +interval residues (four pairs, three triples, two intervals of length four). +Store the three top residues with their multiplicities. For each inverse +suffix look up the complementary counts and the same proper residues. +Singleton residues already match because the counts add to three. The +prefix top minus the inverse suffix top gives c. Each complete word has +one split, including its order within the two halves. + +There are 3,084 prefix keys in this run. Summing the compatible prefix/suffix +multiplicities before the endpoint restriction gives 168,168,000, the full +multinomial number. The sign and multiplication order are also checked at +519 cuts in the 173 credited positive-target witnesses at other moduli. + +## Count by the middle three letters + +Delete labels 1 and 5. The remaining balanced middle word has three each +of 2,3,4. Of the 1,680 such words, 270 have the required vanishing 23,34,234 +counts. For each one place the three 1s and three 5s in the ten gaps around +the nine middle positions. There are 220 placements on each side. + +For a given placement, let b_i count 1s before middle position i and a_k +count 5s after middle position k. The three remaining proper intervals +starting at 1 are obtained by summing b_i over the 2 positions, the 23 +pairs and the 234 triples, respectively. Apply the analogous sums of a_k +over the 4 positions, the 34 pairs and the 234 triples for intervals ending +at 5. All six sums must vanish modulo three. Then the top residue is + +```text +Σ b_i a_k modulo 3, over all middle triples i 1 and gcd(c, m) == 1: + pair = unit_repeat_root(depth, m, c) + exceptional = rows[depth, pair[0]]["counts"][pair[1]] if pair else 0 + check(count - exceptional == exact[1], "unit primitive count") + check(depth*m*row["classes"][c] == count + (depth-1)*exceptional, "unit orbit count") + units += 1 + inspected += 1 + return dict(targets=inspected, units=units) + + +def full_census(): + rows = {(h, n): scan(h, n, ds) for h, n, ds in domain()} + orbits = verify_orbits(rows) + summary = {f"L{h}_n{n}": {k: v for k, v in row.items() if k != "periods"} + for (h, n), row in rows.items()} + check(rows[3, 3]["counts"] == [270, 24, 0], "PR6037 depth-three count") + check(rows[4, 2]["counts"] == [816, 0], "PR6652 depth-four count") + check(rows[5, 2]["counts"][1] == 0, "depth-five binary obstruction") + return dict(rows=summary, orbits=orbits, + total_blocks=sum(r["blocks"] for r in rows.values()), + repeated_word_checks=sum(r["repeated_word_checks"] for r in rows.values()), + fixed_target_bins=sum(r["fixed_target_bins"] for r in rows.values())) diff --git a/research/chain-all-depth-powers/law.py b/research/chain-all-depth-powers/law.py new file mode 100644 index 0000000000..03d5b69a4e --- /dev/null +++ b/research/chain-all-depth-powers/law.py @@ -0,0 +1,80 @@ +"""All-depth balanced chain power law. SHIN09-git with OpenAI Codex. Apache-2.0.""" +from math import gcd, isqrt + + +def first_missing_prime(repeats, block_size): + """Least prime dividing repeats but not block_size. None means infinity.""" + if repeats < 1 or block_size < 1: + raise ValueError("positive repeat count and block size required") + remaining = repeats + while (shared := gcd(remaining, block_size)) != 1: + remaining //= shared + if remaining == 1: + return None + for candidate in range(2, isqrt(remaining) + 1): + if remaining % candidate == 0: + return candidate + return remaining + + +def shift(depth, block_size, repeats): + """None means a proper interval obstructs every target.""" + if depth < 2: + raise ValueError("depth must be at least two") + prime = first_missing_prime(repeats, block_size) + if prime is not None and prime < depth: + return None + if prime == depth: + modulus = repeats * block_size + return (repeats // depth) * pow(block_size, depth, modulus) % modulus + return 0 + + +def lifted_target(depth, block_size, repeats, base_target): + offset = shift(depth, block_size, repeats) + if base_target is None or offset is None: + return None + return (repeats * base_target + offset) % (block_size * repeats) + + +def root_target(depth, block_size, repeats, target): + """Return the unique required residue for the shorter block, if allowed.""" + offset = shift(depth, block_size, repeats) + if offset is None or (target - offset) % repeats: + return None + return ((target - offset) // repeats) % block_size + + +def unit_repeat_root(depth, modulus, target): + """The only possible nonprimitive unit case, still subject to W(root)>0.""" + if depth < 2 or modulus < 2 or gcd(target, modulus) != 1: + raise ValueError("unit target required") + if first_missing_prime(depth, 1) != depth or modulus % depth: + return None + block_size = modulus // depth + residue = pow(block_size, depth, modulus) + if block_size % depth == 0 or (target - residue) % depth: + return None + return (block_size, ((target - residue) // depth) % block_size) + + +def order_bound(depth, modulus, target): + """Orders that pass the arithmetic gates are exactly the divisors of D.""" + if depth < 2 or modulus < 1: + raise ValueError("invalid depth or modulus") + rest, radical, edge_power = modulus, 1, 1 + for prime in range(2, min(depth, modulus) + 1): + if rest % prime: + continue + # Every smaller prime has already been removed in full. + radical *= prime + power = 1 + while rest % prime == 0: + rest //= prime + power *= prime + if prime == depth: + edge_power = power + bound = gcd(target, modulus // radical) + if edge_power > 1 and (target - modulus // depth) % edge_power == 0: + bound *= depth + return bound diff --git a/research/chain-all-depth-powers/oracle.py b/research/chain-all-depth-powers/oracle.py new file mode 100644 index 0000000000..5ecaa6c65f --- /dev/null +++ b/research/chain-all-depth-powers/oracle.py @@ -0,0 +1,107 @@ +"""Independent literal oracles. No import of the repetition formula. +SHIN09-git with OpenAI Codex assistance. Apache-2.0. +""" +from bisect import bisect_left +from itertools import accumulate + + +def balanced_words(depth, copies): + """Enumerate the multiset permutations in lexicographic order.""" + word = [letter for letter in range(1, depth + 1) for _ in range(copies)] + while True: + yield tuple(word) + pivot = len(word) - 2 + while pivot >= 0 and word[pivot] >= word[pivot + 1]: + pivot -= 1 + if pivot < 0: + return + successor = len(word) - 1 + while word[successor] <= word[pivot]: + successor -= 1 + word[pivot], word[successor] = word[successor], word[pivot] + word[pivot + 1:] = reversed(word[pivot + 1:]) + + +def positional_counts(word, depth): + """Integer subsequence counts from the position sets of successive labels.""" + positions = [[] for _ in range(depth + 1)] + for index, label in enumerate(word): + positions[label].append(index) + intervals = {} + for start in range(1, depth + 1): + weights = [1] * len(positions[start]) + intervals[start, start] = len(weights) + for end in range(start + 1, depth + 1): + prefix = [0, *accumulate(weights)] + weights = [prefix[bisect_left(positions[end - 1], pos)] + for pos in positions[end]] + intervals[start, end] = sum(weights) + return intervals + + +def literal_matrix(word, depth): + """Execute every call on the integer basis of all dirty scalar roles.""" + rows = [[int(i == j) for j in range(depth + 1)] for i in range(depth + 1)] + for label in word: + source, target = rows[label - 1], rows[label] + for j in range(label): + target[j] += source[j] + return rows + + +def matrix_target(rows, modulus): + depth = len(rows) - 1 + for end in range(1, depth + 1): + for column in range(end): + if (end, column) != (depth, 0) and rows[end][column] % modulus: + return None + return rows[depth][0] % modulus + + +def position_target(counts, depth, modulus): + if any(value % modulus for key, value in counts.items() if key != (1, depth)): + return None + return counts[1, depth] % modulus + + +def primitive_period(word): + return next(k for k in range(1, len(word) + 1) if word[k:] + word[:k] == word) + + +def canonical_rotation(word): + return min(word[k:] + word[:k] for k in range(len(word))) + + +def phi(n): + from math import gcd + return sum(gcd(k, n) == 1 for k in range(1, n + 1)) + + +def map_vector(label, vector, modulus, singular): + first, second = vector + if singular and label == 1: + return (first % modulus, 0) + if label % 2: + return ((first + second) % modulus, second) + return (first, (first + second) % modulus) + + +def dirty_basis(word, depth, modulus, target): + """Two families of noncommuting 2x2 maps, every dirty input basis vector.""" + cases = 0 + for singular in (False, True): + for column in range(2 * (depth + 1)): + initial = [(int(column == 2*j), int(column == 2*j + 1)) + for j in range(depth + 1)] + actual = list(initial) + for label in word: + add = map_vector(label, actual[label - 1], modulus, singular) + actual[label] = tuple((x + y) % modulus for x, y in zip(actual[label], add)) + expected, product = list(initial), initial[0] + for label in range(1, depth + 1): + product = map_vector(label, product, modulus, singular) + expected[depth] = tuple((x + target*y) % modulus for x, y in zip(initial[depth], product)) + if actual != expected: + raise ValueError("noncommuting dirty endpoint") + cases += 1 + return cases diff --git a/research/chain-all-depth-powers/order_checks.py b/research/chain-all-depth-powers/order_checks.py new file mode 100644 index 0000000000..217d619a34 --- /dev/null +++ b/research/chain-all-depth-powers/order_checks.py @@ -0,0 +1,58 @@ +"""Check the closed divisor formula against raw integer coefficients.""" +from math import comb, gcd + +from census import check +from law import order_bound, root_target, unit_repeat_root +from oracle import literal_matrix, matrix_target, primitive_period + + +def compare_divisors(): + cases = order_tests = unit_tests = 0 + for h in range(2, 17): + for m in (*range(2, 97), 125, 175, 250, 350, 360, 900): + divisors = [d for d in range(1, m+1) if m % d == 0] + raw = {} + for d in divisors: + n = m//d + pure = [(comb(d, j) * pow(n, j, m)) % m for j in range(2, h+1)] + raw[d] = (any(pure[:-1]), pure[-1]) + for c in range(m): + bound = order_bound(h, m, c) + nontrivial = [] + for d in divisors: + blocked, offset = raw[d] + allowed = not blocked and (c - offset) % d == 0 + check(allowed == (bound % d == 0), "closed divisor arithmetic") + check(allowed == (root_target(h, m//d, d, c) is not None), "root eligibility") + if allowed and d > 1: + nontrivial.append((d, m//d, ((c-offset)//d) % (m//d))) + order_tests += 1 + if gcd(c, m) == 1: + pair = unit_repeat_root(h, m, c) + check(nontrivial == ([(h, *pair)] if pair else []), "unit root arithmetic") + unit_tests += 1 + cases += 1 + return dict(depths=[2, 16], moduli="2..96 and 125,175,250,350,360,900", + targets=cases, unit_targets=unit_tests, divisibility_comparisons=order_tests) + + +def zero_spectra(): + cases = 0 + examples = {} + for h in (2, 3, 4, 5, 7, 8, 11): + for m in (*range(2, 25), 60, 64, 72, 84, 120, 210, 360): + bound = order_bound(h, m, 0) + periods = [] + for d in range(1, bound+1): + if bound % d: + continue + n = m//d + word = tuple(label for label in range(1, h+1) for _ in range(n))*d + check(matrix_target(literal_matrix(word, h), m) == 0, "zero witness endpoint") + period = primitive_period(word) + check(period == h*n, "exact zero-target period") + periods.append(period) + cases += 1 + if (h, m) in ((5, 360), (7, 84), (4, 64), (5, 20)): + examples[f"L{h}_m{m}"] = sorted(periods) + return dict(explicit_words=cases, examples=examples) diff --git a/research/chain-all-depth-powers/quintic_rows.py b/research/chain-all-depth-powers/quintic_rows.py new file mode 100644 index 0000000000..574af09a3a --- /dev/null +++ b/research/chain-all-depth-powers/quintic_rows.py @@ -0,0 +1,119 @@ +"""Two exact counters for the small roots in the depth-five shift. +SHIN09-git with OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from itertools import combinations_with_replacement, product +from math import comb, factorial, prod + +from census import check +from law import root_target +from oracle import balanced_words, literal_matrix + +# Excluding the known singletons and the target leaves nine interval entries. +PROPER = [(j, i-1, j-i+1) for j in range(2, 6) for i in range(1, j) + if (i, j) != (1, 5)] + + +def halves(length, n): + for word in product(range(1, 6), repeat=length): + counts = tuple(word.count(i) for i in range(1, 6)) + if max(counts) <= n: + yield word, counts + + +def signature(word, n, inverse): + matrix = literal_matrix(word, 5) + sign = -1 if inverse else 1 + proper = tuple((sign**span * matrix[j][k]) % n for j, k, span in PROPER) + return proper, sign*matrix[5][0] % n + + +def split_row(n, cut): + """Join a literal prefix P with inverse suffix S^-1 using S P = I+cE.""" + prefix, mass = {}, Counter() + left = right = compatible = 0 + row = [0]*n + for word, counts in halves(cut, n): + proper, top = signature(word, n, False) + bucket = prefix.setdefault((counts, proper), [0]*n) + bucket[top] += 1 + mass[counts] += 1 + left += 1 + for reversed_suffix, counts in halves(5*n-cut, n): + complement = tuple(n-c for c in counts) + # Negating every shear multiplies an interval by (-1)^length. + proper, inverse_top = signature(reversed_suffix, n, True) + for t, ways in enumerate(prefix.get((complement, proper), ())): + row[(t-inverse_top) % n] += ways + compatible += mass.get(complement, 0) + right += 1 + check(compatible == factorial(5*n)//factorial(n)**5, "split multinomial mass") + return dict(row=row, cut=cut, prefix_words=left, reverse_suffix_words=right, + prefix_keys=len(prefix), compatible_pairs=compatible) + + +def placements(n): + result = [] + for gaps in combinations_with_replacement(range(3*n+1), n): + counts = tuple(gaps.count(i) for i in range(3*n+1)) + before = tuple(sum(g <= i for g in gaps) for i in range(3*n)) + result.append((counts, before, tuple(n-x for x in before))) + return result + + +def middle_features(word): + first, second, third = [[i for i, x in enumerate(word) if x == label] for label in (1, 2, 3)] + ab = [(i, j) for i in first for j in second if i < j] + bc = [(j, k) for j in second for k in third if j < k] + triples = [(i, k) for i, j in ab for k in third if j < k] + return first, third, ab, bc, triples + + +def gap_row(n): + options = placements(n) + weights = [[prod(comb(x+y, x) for x, y in zip(a[0], b[0])) for b in options] + for a in options] + mass_per_middle = sum(map(sum, weights)) + row = [0]*n + total = restored = accepted = 0 + for middle in balanced_words(3, n): + total += 1 + first, third, ab, bc, triples = middle_features(middle) + if any(len(f) % n for f in (ab, bc, triples)): + continue + restored += 1 + starts = (first, [i for i, j in ab], [i for i, k in triples]) + ends = (third, [k for j, k in bc], [k for i, k in triples]) + left = [(u, b) for u, (_, b, _) in enumerate(options) + if all(sum(b[i] for i in indices) % n == 0 for indices in starts)] + right = [(v, a) for v, (_, _, a) in enumerate(options) + if all(sum(a[k] for k in indices) % n == 0 for indices in ends)] + for u, b in left: + for v, a in right: + residue = sum(b[i]*a[k] for i, k in triples) % n + row[residue] += weights[u][v] + accepted += 1 + mass = total*mass_per_middle + check(mass == factorial(5*n)//factorial(n)**5, "gap multinomial mass") + return dict(row=row, middle_words=total, restored_middle=restored, + accepted_gap_pairs=accepted, all_words=mass) + + +def small_quintic_rows(): + result = {} + for n in (2, 3): + cut = 5*n//2 + split, gaps = split_row(n, cut), gap_row(n) + check(split["row"] == gaps["row"], "split and gap W5 rows differ") + result[str(n)] = dict(split=split, gaps=gaps) + check(result["2"]["split"]["row"] == [25520, 0], "literal quintic binary row") + nonprimitive = [] + for c in range(15): + check(all(root_target(5, 15//d, d, c) is None for d in (3, 15)), "unexpected order at m=15") + t = root_target(5, 3, 5, c) + nonprimitive.append(0 if t is None else result["3"]["split"]["row"][t]) + check([i for i, v in enumerate(nonprimitive) if v] == [3], "m=15 periodic targets") + check(nonprimitive[3] % 15 == 0, "m=15 period population") + result["m15"] = dict(nonprimitive_words=nonprimitive, period_15_classes=nonprimitive[3]//15, + W_target_3_modulo_75=nonprimitive[3] % 75) + return result diff --git a/research/chain-all-depth-powers/verify.py b/research/chain-all-depth-powers/verify.py new file mode 100644 index 0000000000..5e6d9f0ca2 --- /dev/null +++ b/research/chain-all-depth-powers/verify.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Read-only replay of the all-depth balanced power law. Standard library only.""" +from collections import Counter +from hashlib import sha256 +import json +from math import comb, factorial +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from census import check, full_census +from law import first_missing_prime, lifted_target, order_bound, root_target, unit_repeat_root +from order_checks import compare_divisors, zero_spectra +from quintic_rows import signature, small_quintic_rows +from oracle import dirty_basis, literal_matrix, matrix_target, primitive_period + + +def verify_pins(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + retained = {} + for source in manifest["files"]: + local = source.get("vendored_as") + if local: + digest = sha256((HERE / local).read_bytes()).hexdigest() + check(digest == source["sha256"], "retained source bytes differ: " + local) + retained[local] = digest + return retained + + +def coefficient_grid(): + cases = boundary = safe = 0 + for n in range(1, 25): + for d in range(1, 129): + m = n*d + predicted = first_missing_prime(d, n) + first = None + for j in range(2, d+1): + residue = (comb(d, j) * pow(n, j, m)) % m + if residue and first is None: + first = j + if predicted is None or j < predicted: + check(residue == 0, "lower binomial coefficient") + safe += 1 + if j == predicted: + check(residue == (d//j)*pow(n, j, m) % m and residue % d != 0, + "first surviving coefficient") + boundary += 1 + cases += 1 + check(first == predicted, "least obstructing pure level") + return dict(n_range=[1, 24], d_range=[1, 128], binomial_tests=cases, + lower_vanishings=safe, surviving_boundaries=boundary) + + +def source_witness_checks(): + rows = json.loads((HERE / "source/depth5-witnesses.json").read_text())["witnesses"] + blocks = tests = surviving = splits = 0 + for size, targets in rows.items(): + n = int(size) + for target, encoded in targets.items(): + t, word = int(target), tuple(map(int, encoded)) + check(Counter(word) == {label: n for label in range(1, 6)}, "witness balance") + check(matrix_target(literal_matrix(word, 5), n) == t, "witness source endpoint") + for cut in (len(word)//3, len(word)//2, 2*len(word)//3): + prefix, prefix_top = signature(word[:cut], n, False) + suffix, inverse_top = signature(word[cut:][::-1], n, True) + check(prefix == suffix and (prefix_top-inverse_top) % n == t, "witness inverse-suffix join") + splits += 1 + for d in (2, 3, 4, 5, 6, 10, 12): + actual = matrix_target(literal_matrix(word*d, 5), n*d) + expected = lifted_target(5, n, d, t) + check(actual == expected, "retained witness repetition") + tests += 1 + surviving += actual is not None + blocks += 1 + return dict(witnesses=blocks, powered_words=tests, correct_powers=surviving, witness_splits=splits) + + +def examples(): + source = json.loads((HERE / "source/depth5-witnesses.json").read_text())["witnesses"] + configs = [ + (5, 7, 5, tuple(map(int, source["7"]["1"])), 12), + (5, 2, 10, tuple(x for x in range(1, 6) for _ in range(2)), 4), + (5, 2, 25, tuple(x for x in range(1, 6) for _ in range(2)), 10), + (6, 2, 8, tuple(x for x in range(1, 7) for _ in range(2)), 0), + (7, 1, 7, tuple(range(1, 8)), 1), + (11, 1, 11, tuple(range(1, 12)), 1), + ] + rows = [] + for h, n, d, block, c in configs: + word = block*d + check(matrix_target(literal_matrix(word, h), n*d) == c, "example endpoint") + period = primitive_period(word) + check(period == h*n, "example period") + checked = dirty_basis(word, h, n*d, c) + rows.append(dict(depth=h, modulus=n*d, target=c, repeats=d, period=period, + block=list(block), dirty_basis_cases=checked)) + empty_root_word = tuple(map(int, source["10"]["7"])) + check(matrix_target(literal_matrix(empty_root_word, 5), 10) == 7 and + primitive_period(empty_root_word) == 50, "nonvacuous empty-root boundary") + unbalanced = (1, 2, 3, 4, 5, 6, 5, 4, 3, 2)*2 + unbalanced_counts = [unbalanced.count(i) for i in range(1, 7)] + check(unbalanced_counts == [2, 4, 4, 4, 4, 2] and primitive_period(unbalanced) == 10 + and matrix_target(literal_matrix(unbalanced, 6), 2) == 1, "PR4748 balance boundary") + h, n, d = 6, 2, 25 + blocks = tuple(x for x in range(1, h+1) for _ in range(n)) + matrix = literal_matrix(blocks*d, h) + residues = {length: [matrix[i+length][i] % (n*d) for i in range(h+1-length)] + for length in range(1, h)} + check(all(not any(residues[j]) for j in range(1, 5)), "lower four levels") + check(residues[5] == [10, 10], "first forbidden level is five") + return dict(correct_words=rows, empty_root_witness=dict(word=list(empty_root_word), period=50), + unbalanced_4748=dict(word=list(unbalanced), counts=unbalanced_counts, period=10, + target=1, dirty_basis_cases=dirty_basis(unbalanced, 6, 2, 1)), + bad_fifth_level=dict(depth=h, modulus=n*d, + repeats=d, interval_residues={str(k): v for k, v in residues.items()})) + + +def build(): + pins = verify_pins() + grid = coefficient_grid() + corpus = full_census() + examples_checked = examples() + witness_checks = source_witness_checks() + check(root_target(5, 2, 5, 7) == 1, "binary-root residue") + check(unit_repeat_root(5, 10, 7) == (2, 1), "eligible empty unit root") + check(corpus["rows"]["L5_n2"]["counts"][1] == 0, "empty unit root population") + for h in (2, 3, 5, 7): + check(corpus["rows"][f"L{h}_n1"]["counts"] == [factorial(h)], "unit prime sharpness") + check(order_bound(5, 10, 7) == 5, "arithmetic order need not be attained") + check(order_bound(5, 20, 4) == 10, "sharp nonunit order bound") + check(order_bound(5, 50, 10) == 25 and order_bound(5, 50, 5) == 5, + "full prime-power target congruence") + return dict(status="PASS_CHAIN_ALL_DEPTH_POWERS", retained_sources=pins, + divisor_grid=compare_divisors(), zero_spectra=zero_spectra(), quintic=small_quintic_rows(), + coefficients=grid, census=corpus, examples=examples_checked, + credited_witnesses=witness_checks) + + +def main(): + result = build() + expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8")) + check(result == expected, "retained result differs") + files = {p.relative_to(HERE).as_posix(): sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.rglob("*")) if p.is_file() and "__pycache__" not in p.parts} + print(json.dumps(dict(result=result, files=files), sort_keys=True)) + + +if __name__ == "__main__": + main() From f1a14864f86d15f44671c98735cfd8328f3a1f7b Mon Sep 17 00:00:00 2001 From: SHIN09-git Date: Wed, 4 Nov 2026 03:23:49 +0800 Subject: [PATCH 3/3] Verify quintic counts by traversing all 168168000 literal words --- research/chain-all-depth-powers/EXPECTED.json | 24 ++++++ research/chain-all-depth-powers/OVERLAP.json | 52 +++++++++++- research/chain-all-depth-powers/PROOF.md | 7 +- research/chain-all-depth-powers/README.md | 27 +++++-- research/chain-all-depth-powers/ROOT-COUNT.md | 22 ++++- research/chain-all-depth-powers/SOURCES.json | 7 ++ research/chain-all-depth-powers/TASK.json | 2 +- research/chain-all-depth-powers/VALIDATION.md | 33 ++++++++ .../literal/LiteralQuintic.java | 81 +++++++++++++++++++ .../literal/RESULT.json | 27 +++++++ research/chain-all-depth-powers/verify.py | 17 +++- 11 files changed, 288 insertions(+), 11 deletions(-) create mode 100644 research/chain-all-depth-powers/literal/LiteralQuintic.java create mode 100644 research/chain-all-depth-powers/literal/RESULT.json diff --git a/research/chain-all-depth-powers/EXPECTED.json b/research/chain-all-depth-powers/EXPECTED.json index fae78a19c6..24a20fb96f 100644 --- a/research/chain-all-depth-powers/EXPECTED.json +++ b/research/chain-all-depth-powers/EXPECTED.json @@ -480,6 +480,30 @@ ] } }, + "literal_receipt": { + "rows": [ + { + "leaves": 113400, + "n": 2, + "prefixes": 326011, + "row": [ + 25520, + 0 + ] + }, + { + "leaves": 168168000, + "n": 3, + "prefixes": 492911196, + "row": [ + 4697520, + 0, + 0 + ] + } + ], + "source_sha256": "3c9701f3c5c55adb008c6f2013471aac4b98e80630e2829d2d4386d431b21846" + }, "quintic": { "2": { "gaps": { diff --git a/research/chain-all-depth-powers/OVERLAP.json b/research/chain-all-depth-powers/OVERLAP.json index 0930f34ad3..3a117fbd4c 100644 --- a/research/chain-all-depth-powers/OVERLAP.json +++ b/research/chain-all-depth-powers/OVERLAP.json @@ -55,6 +55,10 @@ { "pr": 4748, "addition": "Unbalanced binary depth-six unit square, used as a scope boundary." + }, + { + "pr": 6037, + "addition": "Original depth-three literal W rows; its m=3 row is used as a positive finite control." } ], "targeted_pr_queries": [ @@ -68,5 +72,51 @@ "W5(3,0)", "313,168" ], - "scope": "Open and closed/merged PR metadata, indexed Discussion records, local README/task notes and separate exact-head source inspection. Historical diffs, unpublished work and literature priority are outside this coverage." + "scope": "Open and closed/merged PR metadata, indexed Discussion records, local README/task notes and separate exact-head source inspection. Historical diffs, unpublished work and literature priority are outside this coverage.", + "final": { + "searched_at": "2026-11-03T19:19:30.363549+00:00", + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "terms": [ + "chain-depth-four-repetition-law", + "chain-cyclic-schedules", + "arbitrary-depth repetition", + "chain-all-depth-powers", + "W5(3,0)", + "313,168", + "prime depth" + ], + "coverage": { + "local": { + "head": "9b8290041b4d3df17c73cdb0c9160c99775038b9", + "records": 8919, + "head_records": 8919, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-11-03T19:15:00.698283+00:00", + "complete_pagination": true, + "records": 635 + }, + "discussions": { + "fetched_at": "2026-11-03T19:18:28.983646+00:00", + "complete_pagination": true, + "records": 6755 + }, + "closed_prs": { + "fetched_at": "2026-11-03T19:19:29.465018+00:00", + "complete_pagination": true, + "records": 5528 + } + }, + "warnings": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 9 + }, + "source_rechecked": { + "pr": 6652, + "head": "e364eeb19e5268967189ed12aa4813ee73edf3dc", + "state": "open", + "observed_at": "2026-11-03T19:14:55Z" + } } diff --git a/research/chain-all-depth-powers/PROOF.md b/research/chain-all-depth-powers/PROOF.md index 7082bcc951..896092ea7b 100644 --- a/research/chain-all-depth-powers/PROOF.md +++ b/research/chain-all-depth-powers/PROOF.md @@ -130,6 +130,10 @@ The first formula counts stabilizing pairs and divides by group size. For the second, each word of maximal repetition e contributes to F_d exactly when d|e. These are transforms of the underlying literal counts W_L. [PR #6080](https://github.com/CrocSwap/integer-mult-bounds/pull/6080) +At L=3 the only proper-level prime gate is at 2. The cubic term of #6080 +agrees with (3) by (1) and (2). At L=4 the proper gates are at 2 and 3; +the shift is always zero. This recovers the depth-four reduction in #6652. + ## 3. One divisor for every arithmetically eligible order Let R be the product of the **distinct** primes ℓ|m with ℓ≤L. Start with @@ -240,7 +244,8 @@ Repeating it five times gives m=35 and c=5+7^5=12 modulo 35. The resulting dirty basis input with noncommuting two-coordinate maps. [PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281) At modulus 15, equation (4) reduces *all* nonprimitive depth-five targets -to a single three-residue row at modulus 3. Two complete counts give +to a single three-residue row at modulus 3. Two independent groupings +and a literal enumeration give 4,697,520 words of least period 15 at target 3, forming 313,168 shorter classes. Every other target has zero nonprimitive words. [Finite certificate](ROOT-COUNT.md) diff --git a/research/chain-all-depth-powers/README.md b/research/chain-all-depth-powers/README.md index c512f7bbff..6a774485e9 100644 --- a/research/chain-all-depth-powers/README.md +++ b/research/chain-all-depth-powers/README.md @@ -27,7 +27,7 @@ Three consequences make the rule concrete. block gives a 175-letter unit-target word of least period 35 at m=35,c=12. - Of all length-75 correct words at L=5,m=15, exactly 4,697,520 have a shorter period. All have c=3 and form 313,168 classes of period 15. - Two complete, separately implemented counts of the small root row + Two different groupings and a literal traversal of the small root row establish the number. [Numerical certificate](ROOT-COUNT.md) The proof also gives a closed divisor D whose divisors are exactly the @@ -53,6 +53,18 @@ data and every package file's SHA-256. The fault-injection command uses temporary private copies. See [validation](VALIDATION.md) for the observed environment and publication checks. +An optional single-file program with its own direct evaluator enumerates +every balanced word at n=2 and n=3. From the repository root with a JDK +supporting single-file source launch (tested with OpenJDK 21), run + +```sh +java -Xmx128m research/chain-all-depth-powers/literal/LiteralQuintic.java +``` + +The registered Python replay checks the retained Java source hash and both +recorded rows. The command above performs the actual JVM enumeration. +[Literal receipt](literal/RESULT.json) + ## Evidence and limits - A position-based subsequence counter and a chronological integer matrix @@ -82,9 +94,11 @@ environment and publication checks. The finite evidence supports a written proof for all depths, moduli and targets in the balanced unsigned model. W at larger roots remains an input -to the counting transform. The engines share the same assisted author and -Python integer semantics. Physical routing, precision, supplier prices and -independent mathematical review have separate obligations. +to the counting transform. The two grouped counters use Python integers. +The literal walk uses Java integers for interval counts bounded by 3^5 +and long counters for visits. All three implementations have the same +assisted author. Physical routing, precision, supplier prices and independent +mathematical review have separate obligations. The largest half-word search in the registered verifier has 5^8 lexical candidates. The largest gap-weight matrix has 220² entries. Full enumeration @@ -102,7 +116,10 @@ its 945 pairings. Canonical base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. [Task](TASK.json) · [Overlap coverage](OVERLAP.json) Nick Petalas supplied the depth-four law, the depth-five witnesses and the -unbalanced depth-six example. SHIN09-git's depth-three work supplied the +unbalanced depth-six example. His earlier depth-three census supplies the +positive-control row (270,24,0). [PR #6037](https://github.com/CrocSwap/integer-mult-bounds/pull/6037) + +SHIN09-git's depth-three work supplied the cyclic fixed-point formulation. The earlier complete-call model credits Ross Richardson's #943/#934 lineage. The depth-four source note at `e364eeb19e5268967189ed12aa4813ee73edf3dc` is retained byte-for-byte in diff --git a/research/chain-all-depth-powers/ROOT-COUNT.md b/research/chain-all-depth-powers/ROOT-COUNT.md index 692727fa9e..351be3edea 100644 --- a/research/chain-all-depth-powers/ROOT-COUNT.md +++ b/research/chain-all-depth-powers/ROOT-COUNT.md @@ -7,8 +7,9 @@ classes. The total number of primitive length-75 words is a separate count. Here orders dividing 15 are 1, 3, 5 and 15. Orders 3 and 15 fail at a proper interval of length three. For order 5 the shorter block has three copies of -each letter. The shift is 3^5=3 modulo 15. Only c=3,8,13 admit a root, -with respective residues 0,1,2 modulo 3. The two exact methods below give +each letter. The shift is 3^5=3 modulo 15. Only c=3,8,13 pass the target +congruence, selecting shorter residues 0,1,2 modulo 3. The two groupings +below and an uncompressed enumeration give ```text W_5(3,0), W_5(3,1), W_5(3,2) = 4,697,520, 0, 0. @@ -74,3 +75,20 @@ of all 113,400 ten-letter words. These engines are separate implementations with the same assisted author and Python integer runtime. The small root census is a finite exact computation. The general theorem supplies its use at the larger modulus. + +## Literal cross-check + +The optional [single-file Java program](literal/LiteralQuintic.java) traverses +the full balanced prefix tree. From each prefix it tries each label with +remaining capacity exactly once. Each push applies its complete shear to +the integer dirty-basis matrix. On return, subtracting the same source row +restores the prefix matrix. At a leaf the singletons are fixed by balance; +the program tests the nine other proper intervals and reads the top entry. +It finishes with the identity matrix after undoing all pushes. Every full +word has a unique prefix path. + +For n=3 it visited 492,911,196 prefixes including the empty prefix and all +168,168,000 full words. It independently returned (4,697,520,0,0). The +n=2 walk visited 326,011 prefixes and 113,400 full words. The empty +nonzero-target entries agree with the earlier depth-five length bounds. +[Observed output and source hash](literal/RESULT.json) · [PR #4281](https://github.com/CrocSwap/integer-mult-bounds/pull/4281) diff --git a/research/chain-all-depth-powers/SOURCES.json b/research/chain-all-depth-powers/SOURCES.json index 6112689b40..2dc29d79da 100644 --- a/research/chain-all-depth-powers/SOURCES.json +++ b/research/chain-all-depth-powers/SOURCES.json @@ -66,6 +66,13 @@ "usage": "provenance", "git_blob": "33662ab27a770fba9a83bf2a3a18ac9b7234c5c3", "sha256": "494ed1cf437e96e73053cf9836e6859ad85701a75690dfcbbd09d3e9da58d506" + }, + { + "path": "research/chain-balanced-multiplicities/RESULT.json", + "usage": "provenance", + "git_blob": "506af526b6779b83e44851130084833022d15684", + "sha256": "bc762de01371b93d846a3c0a391de938ef31f6906333b410068319cfc39f5419", + "role": "Nick Petalas PR6037 small depth-three count control." } ], "external_background": [ diff --git a/research/chain-all-depth-powers/TASK.json b/research/chain-all-depth-powers/TASK.json index ae99eb5b99..5c15bc7df0 100644 --- a/research/chain-all-depth-powers/TASK.json +++ b/research/chain-all-depth-powers/TASK.json @@ -48,7 +48,7 @@ "budget_minutes": 60, "stop_rule": "Stop at the uniform proof, two independent W5 rows for n=2,3, bounded direct oracle and mutation controls, and a reproducible contribution PR. Larger literal W rows and unequal count profiles are follow-ups.", "outcome": "completed", - "evidence": "PROOF.md and ROOT-COUNT.md; EXPECTED.json generated from 309184 direct powers, two full small-root counters, the raw coefficient and divisor grids, credited witnesses and explicit boundaries.", + "evidence": "PROOF.md and ROOT-COUNT.md; EXPECTED.json generated from 309184 direct powers, two full small-root counters, the raw coefficient and divisor grids, credited witnesses and explicit boundaries. A separate Java traversal visits all 168168000 size-three complete words, with its actual output and source hash retained in literal/RESULT.json.", "author": "SHIN09-git with OpenAI Codex assistance", "ai_assistance": "Substantial OpenAI Codex assistance in derivation, literature and repository checks, coding, validation and writing. The independent algorithms have one assisted author.", "open_questions": [ diff --git a/research/chain-all-depth-powers/VALIDATION.md b/research/chain-all-depth-powers/VALIDATION.md index 070df61983..458d7dc274 100644 --- a/research/chain-all-depth-powers/VALIDATION.md +++ b/research/chain-all-depth-powers/VALIDATION.md @@ -24,3 +24,36 @@ The full theorem is a written argument. The finite computation covers the domains and exact checks in README.md. The two algorithms were written by the same assisted author. The selected supplier's full cold replay and formal proof-kernel review are separate from this package. + +## Source history and read-only export + +The proof and Python counters at commit +`9b8290041b4d3df17c73cdb0c9160c99775038b9` passed committed-byte, metadata, +full source-history and export checks in a separately cloned, nonshallow +canonical Git history. The publication commits were transferred as a Git +bundle above the canonical base. Base files needed by the filtered clone +were retrieved from their exact upstream revision and verified against +their Git blob IDs. The official history check verified both the canonical +base and the retained dependency ancestor. + +The official export had SHA-256 +`c8236c073d602800e2e9eb0865d8a27cf8490fb476f4278e4ae07cb2b18af68f`. +After marking its contents read-only and removing Git from PATH, the full +normal and optimized Python receipts matched. Their runs took 9.028 s and +8.828 s. The two positive probes and 34 semantic rejections passed in +114.373 s. All 21 files, including the export manifest, kept their contents. + +## Uncompressed quintic count + +After this snapshot a separate single-file Java traversal checked both +small root rows directly. OpenJDK 21.0.10 visited all 113,400 n=2 words +and all 168,168,000 n=3 words. Its raw counts agree with both grouped +engines. The local source-launch run for both sizes took 5.012 seconds. +The [receipt](literal/RESULT.json) binds the actual output to the Java +source. The registered verifier also compares the retained output and +source digest with its freshly computed counts. + +Publication checks for the final package apply to its exact commit and are +reported in the PR. Running the optional Java command repeats the literal +enumeration. Running the registered Python command checks the grouped +counters and the bound literal receipt. diff --git a/research/chain-all-depth-powers/literal/LiteralQuintic.java b/research/chain-all-depth-powers/literal/LiteralQuintic.java new file mode 100644 index 0000000000..94400533d6 --- /dev/null +++ b/research/chain-all-depth-powers/literal/LiteralQuintic.java @@ -0,0 +1,81 @@ +/* + * Literal depth-five census. SHIN09-git with OpenAI Codex assistance. + * Apache-2.0. Run with a JDK supporting single-file source launch. + */ +import java.util.Arrays; + +class LiteralQuintic { + private static final int LABELS = 5; + + private static long factorial(int value) { + long result = 1; + for (int k = 2; k <= value; k++) result *= k; + return result; + } + + private static int endpoint(int[][] action, int modulus) { + // Singletons equal modulus by construction. Retain all nine other + // proper intervals, then read the bottom-left target coefficient. + for (int end = 2; end <= LABELS; end++) { + for (int column = 0; column < end - 1; column++) { + if (end == LABELS && column == 0) continue; + if (action[end][column] % modulus != 0) return -1; + } + } + return action[LABELS][0] % modulus; + } + + private static void shear(int[][] action, int label, int sign) { + for (int column = 0; column < label; column++) { + action[label][column] += sign * action[label-1][column]; + } + } + + private static String enumerate(int n) { + if (n != 2 && n != 3) throw new IllegalArgumentException("n must be 2 or 3"); + int length = LABELS * n; + int[] used = new int[LABELS+1], next = new int[length+1], chosen = new int[length]; + int[][] action = new int[LABELS+1][LABELS+1]; + for (int i = 0; i <= LABELS; i++) action[i][i] = 1; + long[] row = new long[n]; + long leaves = 0, prefixes = 1; + int depth = 0; + next[0] = 1; + while (true) { + if (depth == length) { + leaves++; + int target = endpoint(action, n); + if (target >= 0) row[target]++; + } else { + int label = next[depth]; + while (label <= LABELS && used[label] == n) label++; + if (label <= LABELS) { + next[depth] = label + 1; + chosen[depth] = label; + used[label]++; + shear(action, label, 1); + next[++depth] = 1; + prefixes++; + continue; + } + } + if (depth == 0) break; + int label = chosen[--depth]; + shear(action, label, -1); + used[label]--; + } + long mass = factorial(length); + for (int i = 0; i < LABELS; i++) mass /= factorial(n); + if (leaves != mass) throw new IllegalStateException("incomplete multinomial census"); + // Pop/push are inverses. At exit all dirty basis rows must be the identity. + for (int i = 0; i <= LABELS; i++) + for (int j = 0; j <= LABELS; j++) + if (action[i][j] != (i == j ? 1 : 0)) throw new IllegalStateException("undo mismatch"); + return "{\"n\":" + n + ",\"leaves\":" + leaves + ",\"prefixes\":" + prefixes + + ",\"row\":" + Arrays.toString(row) + "}"; + } + + public static void main(String[] args) { + System.out.println("[" + enumerate(2) + "," + enumerate(3) + "]"); + } +} diff --git a/research/chain-all-depth-powers/literal/RESULT.json b/research/chain-all-depth-powers/literal/RESULT.json new file mode 100644 index 0000000000..d7cbf0a6f7 --- /dev/null +++ b/research/chain-all-depth-powers/literal/RESULT.json @@ -0,0 +1,27 @@ +{ + "status": "PASS_LITERAL_QUINTIC_ENUMERATION", + "seconds": 5.012, + "java": "openjdk 21.0.10 2026-01-20 LTS\nOpenJDK Runtime Environment Microsoft-13106404 (build 21.0.10+7-LTS)\nOpenJDK 64-Bit Server VM Microsoft-13106404 (build 21.0.10+7-LTS, mixed mode, sharing)", + "source_sha256": "3c9701f3c5c55adb008c6f2013471aac4b98e80630e2829d2d4386d431b21846", + "rows": [ + { + "n": 2, + "leaves": 113400, + "prefixes": 326011, + "row": [ + 25520, + 0 + ] + }, + { + "n": 3, + "leaves": 168168000, + "prefixes": 492911196, + "row": [ + 4697520, + 0, + 0 + ] + } + ] +} diff --git a/research/chain-all-depth-powers/verify.py b/research/chain-all-depth-powers/verify.py index 5e6d9f0ca2..d370b92427 100644 --- a/research/chain-all-depth-powers/verify.py +++ b/research/chain-all-depth-powers/verify.py @@ -131,12 +131,27 @@ def build(): check(order_bound(5, 20, 4) == 10, "sharp nonunit order bound") check(order_bound(5, 50, 10) == 25 and order_bound(5, 50, 5) == 5, "full prime-power target congruence") + quintic = small_quintic_rows() + literal = recorded_literal(quintic) return dict(status="PASS_CHAIN_ALL_DEPTH_POWERS", retained_sources=pins, - divisor_grid=compare_divisors(), zero_spectra=zero_spectra(), quintic=small_quintic_rows(), + divisor_grid=compare_divisors(), zero_spectra=zero_spectra(), quintic=quintic, + literal_receipt=literal, coefficients=grid, census=corpus, examples=examples_checked, credited_witnesses=witness_checks) +def recorded_literal(quintic): + receipt = json.loads((HERE / "literal/RESULT.json").read_text(encoding="utf-8")) + digest = sha256((HERE / "literal/LiteralQuintic.java").read_bytes()).hexdigest() + check(digest == receipt["source_sha256"], "literal JVM source hash") + check([item["n"] for item in receipt["rows"]] == [2, 3], "literal JVM domains") + for item in receipt["rows"]: + independent = quintic[str(item["n"])]["gaps"] + check(item["row"] == independent["row"] and item["leaves"] == independent["all_words"], + "literal JVM receipt differs from independent counters") + return dict(source_sha256=digest, rows=receipt["rows"]) + + def main(): result = build() expected = json.loads((HERE / "EXPECTED.json").read_text(encoding="utf-8"))