diff --git a/research/sl2z-power-length/PROOF.md b/research/sl2z-power-length/PROOF.md new file mode 100644 index 0000000000..9c5c833a6b --- /dev/null +++ b/research/sl2z-power-length/PROOF.md @@ -0,0 +1,136 @@ +# Exact integer-transvection length of the shear powers + +This proof was produced by Nick Petalas. Apache-2.0. + +## Model and theorem + +Use the faithful matrices + +```text +X(t) = [[1,t],[0,1]], Y(t) = [[1,0],[t,1]], t in Z \ {0}, +B = X(2)Y(2) = [[5,2],[2,1]]. +``` + +Every letter costs one, independently of the size of its integer coefficient. +There are no free matrix operations. Let lambda(M) be the minimum letter count +for the exact matrix M. Then, for every integer k >= 1, + +```text +lambda(B^k) = 2k. +``` + +The first previously unresolved power in unpaidmoon's PR4146 is k=3: +its exact length is six, rather than the inherited interval four through six. +This is a scoped group-word theorem. It does not price a physical operation or +establish a complete multiplication theorem. + +## Cited classical theorem + +For nonzero integers a,b, a division chain has successive equations +`r_(j-2) = q_j r_(j-1) + r_j`, starting at `(r_-1,r_0)=(a,b)` and ending +at the first zero remainder. The quotients may be arbitrary integers and +remainders need not decrease. **The least-absolute-remainder algorithm +minimizes the number of divisions among all such terminating chains.** +Either nearest quotient is allowed at a tie. + +This is the classical shortest-division-chain theorem over Z, with the +arbitrary-remainder extension due to D. Lazard, *Le meilleur algorithme +d'Euclide pour k[X] et Z*, C. R. Acad. Sci. Paris 284 (1977), 1–4. +The distinction between unrestricted remainders and the older +Kronecker–Vahlen version is recorded in the introduction of +[M. Vaskouski and N. Kondratyonok, *Shortest division chains in unique +factorization domains*, J. Symbolic Computation 77 (2016), 175–188](https://doi.org/10.1016/j.jsc.2016.02.003). +We use that theorem as a cited mathematical result, not as a new result or +an implication established by our finite verifier. No monotone-remainder +assumption is imposed on a candidate matrix word. + +## The two exact division lengths + +Define the Pell sequence by `s_0=0`, `s_1=1` and +`s_(j+1)=2s_j+s_(j-1)`. Multiplying `[[2,1],[1,0]]` twice gives B, hence +induction gives + +```text +B^k = [[s_(2k+1), s_(2k)], [s_(2k), s_(2k-1)]]. +``` + +For j >= 2, `0 < s_(j-1) <= s_j/2`, with equality only when j=2. +Consequently quotient two is a nearest integer in every division + +```text +s_(j+1) = 2s_j + s_(j-1), j=2k,...,1. +``` + +The last equation is `s_2=2s_1+0`. This least-remainder chain has exactly +2k divisions. At the only tie, `s_3/s_2=5/2`, we choose quotient two. +Choosing three instead gives remainder minus one and the same two final +divisions. +Also `s_(2k)/s_(2k+1) < 1/2`, so the reversed starting pair has the +nearest quotient zero, followed by the same 2k divisions. The classical +theorem therefore gives the exact shortest chain lengths + +```text +ell(s_(2k+1),s_(2k)) = 2k, +ell(s_(2k),s_(2k+1)) = 2k+1. +``` + +## Every matrix word yields one of those chains + +Take any word `G_1 ... G_L = B^k`. Consecutive letters in the same family +can be merged by adding their coefficients; a zero sum deletes the pair. +Repeat until families alternate. This never increases L. Since B^k is +nonidentity, the resulting word is nonempty. + +Let `(a,c)^T` be the first column of B^k. Remove letters from the left by +applying `G_1^-1`, then `G_2^-1`, and so on to this column. After all L +removals the column is `(1,0)^T`. An X(t) removal replaces a by `a-tc`; +a Y(t) removal replaces c by `c-ta`. + +Stop at the first removal that makes either coordinate zero. The +coordinates were both nonzero beforehand, so every operation up to this +point is an ordinary integer division equation. Alternation makes the +successive remainders exactly a division chain. Its initial ordered pair +is `(a,c)` if the first letter is X, and `(c,a)` if it is Y. Its length +is at most L, even if the full word continues after that first zero. + +Here `(a,c)=(s_(2k+1),s_(2k))`. Thus an X-first word has L >= 2k and a +Y-first word has L >= 2k+1. In particular every word has L >= 2k. +The literal word `(X(2)Y(2))^k` has 2k letters and endpoint B^k, proving +the theorem. The stronger Y-first inequality refers to a reduced +alternating word; it is not needed for attainment. + +## Exact model-local bill and boundary + +In PR4146's two-role reading, lambda letters are rank-one children of +width two and the untouched role is counted in W=2. The exact moment is +therefore `k*2^(a-1)`. With only the active role counted, W=1, it is +`k*2^a`. These substitute the new exact count into the inherited model; +they do not supply a native implementation or alter its admission status. + +Integer coefficients are essential. Over Q the three-letter word + +```text +X(12/5) Y(70) X(2/5) = B^3 = [[169,70],[70,29]] +``` + +is a literal endpoint identity. It is a scope control, not a word in the +integer alphabet. Similarly a quotient representation may erase B and +does not preserve the faithful length. Arbitrary free address maps, +extra matrix generators, or different coefficient tariffs change the model. + +## Credit and proof status + +unpaidmoon supplies the arbitrary-integer alphabet and unresolved length +interval in PR4146, and the unit-alphabet comparison in PR4126. +Cinna Davis / 1337isnot1337 supplies X, Y, B and the formal target in +PR3905. ToikY supplies the caller and quotient boundaries in PR3937 and +PR3947. The classical division-chain theorem retains Lazard's credit and +the Kronecker–Vahlen lineage described above. The new repository result +is its application giving the exact all-k faithful length and bill. +No literature-priority claim is made. + +The universal lower bound is the argument above using the cited classical +theorem. Exact finite checks corroborate the Pell identities, chain lengths, +attaining words and hypothesis controls; they do not enumerate arbitrary +integer coefficients or prove Lazard's theorem. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/sl2z-power-length/README.md b/research/sl2z-power-length/README.md new file mode 100644 index 0000000000..dc9f3875b7 --- /dev/null +++ b/research/sl2z-power-length/README.md @@ -0,0 +1,135 @@ +# Exact integer-transvection length of every shear power + +This contribution was produced by Nick Petalas. Apache-2.0. + +For `X(t)=[[1,t],[0,1]]`, `Y(t)=[[1,0],[t,1]]`, and +`B=X(2)Y(2)=[[5,2],[2,1]]`, let each nonzero integer t cost one letter. +Then the exact faithful matrix-word length is + +```text +lambda(B^k) = 2k, for every integer k >= 1. +``` + +This is a **scoped proof with exact finite corroboration**. unpaidmoon's +[PR4146](https://github.com/CrocSwap/integer-mult-bounds/pull/4146) leaves +`4 <= lambda(B^k) <= 2k` for k >= 2 and explicitly does not claim equality. +The first new instance is `lambda(B^3)=6`. The new proof settles that gap +for all powers, using the classical shortest-division-chain theorem over Z. +The exact two-role moment in the inherited rank-only model is `k*2^(a-1)`. +No physical supplier, complete multiplication theorem or new kappa is claimed. + +## Proof and evidence + +[PROOF.md](PROOF.md) identifies the classical theorem and its unrestricted +remainder hypothesis. Left removal of any alternating matrix word gives a +division chain from one orientation of the first column. Pell coordinates +give shortest chain lengths 2k and 2k+1 for those two orientations. The +literal word `(X(2)Y(2))^k` attains 2k. Negative and arbitrarily large integer +coefficients are covered by the written argument. + +The standalone verifier independently multiplies all 64 attaining words, +compares them with Pell coordinates, validates both least-remainder traces, +and compares literal inverse removals with those traces. It enumerates every +word of length zero through five in the twelve-letter alphabet with +coefficients in `{-3,-2,-1,1,2,3}`, looking for B cubed. This bounded census +corroborates the first new instance; it does not replace the all-integer proof. + +Twelve rejection controls damage traces, a target, letter contracts, the +integer-coefficient requirement, or one of the six attaining calls. Two +additional scope checks distinguish the mod-two quotient and the tariff +obtained by expanding coefficients into unit letters. The literal identity +`X(12/5)Y(70)X(2/5)=B^3` shows why rational coefficients are outside the theorem. + +`RESULT.json` is generated by the verifier and binds the finite evidence to +the proof, code and metadata hashes. It is compared with exact regeneration +on every ordinary replay. No predecessor verifier is imported or executed. + +## Reproduction + +From the repository root, CPython 3.12 and its standard library suffice: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/sl2z-power-length/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/sl2z-power-length/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sl2z-power-length +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sl2z-power-length --check-source-history +``` + +Other machines may substitute their CPython 3.12 interpreter. To regenerate +the result without overwriting a file: + +```sh +python3.12 -W error -B research/sl2z-power-length/verify.py --write /tmp/sl2z-power-result.json +python3.12 -W error -B research/sl2z-power-length/verify.py --certificate /tmp/sl2z-power-result.json +``` + +Local verification used CPython 3.12.15 on macOS 27.0.1 arm64. Both +registered commands passed individually in about 0.11 seconds. The direct +output is: + +```text +PASS_SL2Z_POWER_LENGTH powers=64 minimum=2k short_words=271453 hits=0 rejection_controls=12 classical_division_chain_theorem=cited no_new_kappa +``` + +## Sources, scope and overlap + +Base canonical main is `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority +revision 7. The selected source-binding control passed. SOURCES.json pins +PR4146's retained README as provenance, with its author credit unchanged. +The `bit-new-register-model` card is explicitly changed to this faithful +address-word length question. A native conversion and complete physical +invoice remain missing; another formal construction round is not proposed. + +Credit unpaidmoon #4146 at `9d167104f45dcc4f9ff3b7b207c894af8cf1d49f` +for the larger alphabet, recurrence question and previous length interval, +and #4126 for the unit-letter comparison. Credit Cinna Davis / 1337isnot1337 +#3905 for the integer-shear target and dirty-role context, ToikY #3937/#3947 +for the caller and quotient boundaries, and the retained eumemic/huxint +register lineage. Lazard's classical theorem and its Kronecker–Vahlen +predecessors are credited in the proof, with a primary research citation. +Only the new exact application is claimed here. No literature-priority claim +or independent human and formal proof-kernel review is claimed. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145562) +followed live open PRs and handoffs, recent account contributions, distinctive +main/merged searches and a question-specific local reservation. The cached +scan covered 314 open PRs and 4,390 Discussion records with complete remote +pagination. Its local notes were sparse, and unpublished work and arbitrary +diffs remain coverage limits. No matching open same-object PR was found at +claim time. No predecessor result was audited or reverified as the deliverable. + +The proof uses the published classical division-chain theorem. The verifier +does not reprove it or enumerate all integer words. Physical encoding, +compiler, precision, hosting, fixed-tape, selected cold replay and Lean +obligations are unrun and outside this contribution. The selected frontier +is unchanged. + +## Verification implementation limits + +The finite verifier has no recursion or unbounded search queue. Powers stop +at 64, words at length five over twelve letters, and least-remainder inputs +at 1024 bits with at most 1026 divisions. Every function fits within 60 +physical lines. Runtime contracts remain active under optimized Python. + +Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: Python +integers, Fractions, tuples, dictionaries and JSON allocate dynamically. +The finite bounds above cap all live data; the input certificate is capped +at one megabyte. Rule 9 has a Python arithmetic-dispatch deviation, confined +to standard integers and Fractions with direct, visible calls. The control +word is the only Fraction calculation. Exact endpoint and normal/optimized +replays check both paths. A fixed-capacity native implementation would be +needed if allocation or dispatch guarantees became a caller requirement. +Warning-strict replays supply the available runtime diagnostics; no repository +build configuration is changed. + +## Open next questions + +Can a genuinely different native operation contract implement the faithful +integer action at a favorable complete tariff? This would determine whether +the exact formal count has any supplier use. Start with the single X(2) +operation and account for the shift, arbitrary dirty data, restoration and +all frame conversions. A named admissible caller and a full physical bill +are the blockers. The present theorem closes the word-shortening route for +the stated integer alphabet and does not provide that implementation. + +Structured questions and blockers are in TASK.json. diff --git a/research/sl2z-power-length/RESULT.json b/research/sl2z-power-length/RESULT.json new file mode 100644 index 0000000000..dd67e5f0bd --- /dev/null +++ b/research/sl2z-power-length/RESULT.json @@ -0,0 +1,820 @@ +{ + "bounded_word_census": { + "coefficients": [ + -3, + -2, + -1, + 1, + 2, + 3 + ], + "hits": [], + "length_limit": 5, + "words": 271453, + "words_by_length": [ + 1, + 12, + 144, + 1728, + 20736, + 248832 + ] + }, + "claim_type": "scoped-proof", + "controls": { + "mod_two_endpoint": [ + 1, + 0, + 0, + 1 + ], + "rational_three_letter_endpoint": [ + 169, + 70, + 70, + 29 + ], + "rejections": 12, + "unit_expansion_letters": 12 + }, + "finite_powers": [ + { + "direct_divisions": 2, + "k": 1, + "matrix": [ + 5, + 2, + 2, + 1 + ], + "minimum": 2, + "reverse_divisions": 3 + }, + { + "direct_divisions": 4, + "k": 2, + "matrix": [ + 29, + 12, + 12, + 5 + ], + "minimum": 4, + "reverse_divisions": 5 + }, + { + "direct_divisions": 6, + "k": 3, + "matrix": [ + 169, + 70, + 70, + 29 + ], + "minimum": 6, + "reverse_divisions": 7 + }, + { + "direct_divisions": 8, + "k": 4, + "matrix": [ + 985, + 408, + 408, + 169 + ], + "minimum": 8, + "reverse_divisions": 9 + }, + { + "direct_divisions": 10, + "k": 5, + "matrix": [ + 5741, + 2378, + 2378, + 985 + ], + "minimum": 10, + "reverse_divisions": 11 + }, + { + "direct_divisions": 12, + "k": 6, + "matrix": [ + 33461, + 13860, + 13860, + 5741 + ], + "minimum": 12, + "reverse_divisions": 13 + }, + { + "direct_divisions": 14, + "k": 7, + "matrix": [ + 195025, + 80782, + 80782, + 33461 + ], + "minimum": 14, + "reverse_divisions": 15 + }, + { + "direct_divisions": 16, + "k": 8, + "matrix": [ + 1136689, + 470832, + 470832, + 195025 + ], + "minimum": 16, + "reverse_divisions": 17 + }, + { + "direct_divisions": 18, + "k": 9, + "matrix": [ + 6625109, + 2744210, + 2744210, + 1136689 + ], + "minimum": 18, + "reverse_divisions": 19 + }, + { + "direct_divisions": 20, + "k": 10, + "matrix": [ + 38613965, + 15994428, + 15994428, + 6625109 + ], + "minimum": 20, + "reverse_divisions": 21 + }, + { + "direct_divisions": 22, + "k": 11, + "matrix": [ + 225058681, + 93222358, + 93222358, + 38613965 + ], + "minimum": 22, + "reverse_divisions": 23 + }, + { + "direct_divisions": 24, + "k": 12, + "matrix": [ + 1311738121, + 543339720, + 543339720, + 225058681 + ], + "minimum": 24, + "reverse_divisions": 25 + }, + { + "direct_divisions": 26, + "k": 13, + "matrix": [ + 7645370045, + 3166815962, + 3166815962, + 1311738121 + ], + "minimum": 26, + "reverse_divisions": 27 + }, + { + "direct_divisions": 28, + "k": 14, + "matrix": [ + 44560482149, + 18457556052, + 18457556052, + 7645370045 + ], + "minimum": 28, + "reverse_divisions": 29 + }, + { + "direct_divisions": 30, + "k": 15, + "matrix": [ + 259717522849, + 107578520350, + 107578520350, + 44560482149 + ], + "minimum": 30, + "reverse_divisions": 31 + }, + { + "direct_divisions": 32, + "k": 16, + "matrix": [ + 1513744654945, + 627013566048, + 627013566048, + 259717522849 + ], + "minimum": 32, + "reverse_divisions": 33 + }, + { + "direct_divisions": 34, + "k": 17, + "matrix": [ + 8822750406821, + 3654502875938, + 3654502875938, + 1513744654945 + ], + "minimum": 34, + "reverse_divisions": 35 + }, + { + "direct_divisions": 36, + "k": 18, + "matrix": [ + 51422757785981, + 21300003689580, + 21300003689580, + 8822750406821 + ], + "minimum": 36, + "reverse_divisions": 37 + }, + { + "direct_divisions": 38, + "k": 19, + "matrix": [ + 299713796309065, + 124145519261542, + 124145519261542, + 51422757785981 + ], + "minimum": 38, + "reverse_divisions": 39 + }, + { + "direct_divisions": 40, + "k": 20, + "matrix": [ + 1746860020068409, + 723573111879672, + 723573111879672, + 299713796309065 + ], + "minimum": 40, + "reverse_divisions": 41 + }, + { + "direct_divisions": 42, + "k": 21, + "matrix": [ + 10181446324101389, + 4217293152016490, + 4217293152016490, + 1746860020068409 + ], + "minimum": 42, + "reverse_divisions": 43 + }, + { + "direct_divisions": 44, + "k": 22, + "matrix": [ + 59341817924539925, + 24580185800219268, + 24580185800219268, + 10181446324101389 + ], + "minimum": 44, + "reverse_divisions": 45 + }, + { + "direct_divisions": 46, + "k": 23, + "matrix": [ + 345869461223138161, + 143263821649299118, + 143263821649299118, + 59341817924539925 + ], + "minimum": 46, + "reverse_divisions": 47 + }, + { + "direct_divisions": 48, + "k": 24, + "matrix": [ + 2015874949414289041, + 835002744095575440, + 835002744095575440, + 345869461223138161 + ], + "minimum": 48, + "reverse_divisions": 49 + }, + { + "direct_divisions": 50, + "k": 25, + "matrix": [ + 11749380235262596085, + 4866752642924153522, + 4866752642924153522, + 2015874949414289041 + ], + "minimum": 50, + "reverse_divisions": 51 + }, + { + "direct_divisions": 52, + "k": 26, + "matrix": [ + 68480406462161287469, + 28365513113449345692, + 28365513113449345692, + 11749380235262596085 + ], + "minimum": 52, + "reverse_divisions": 53 + }, + { + "direct_divisions": 54, + "k": 27, + "matrix": [ + 399133058537705128729, + 165326326037771920630, + 165326326037771920630, + 68480406462161287469 + ], + "minimum": 54, + "reverse_divisions": 55 + }, + { + "direct_divisions": 56, + "k": 28, + "matrix": [ + 2326317944764069484905, + 963592443113182178088, + 963592443113182178088, + 399133058537705128729 + ], + "minimum": 56, + "reverse_divisions": 57 + }, + { + "direct_divisions": 58, + "k": 29, + "matrix": [ + 13558774610046711780701, + 5616228332641321147898, + 5616228332641321147898, + 2326317944764069484905 + ], + "minimum": 58, + "reverse_divisions": 59 + }, + { + "direct_divisions": 60, + "k": 30, + "matrix": [ + 79026329715516201199301, + 32733777552734744709300, + 32733777552734744709300, + 13558774610046711780701 + ], + "minimum": 60, + "reverse_divisions": 61 + }, + { + "direct_divisions": 62, + "k": 31, + "matrix": [ + 460599203683050495415105, + 190786436983767147107902, + 190786436983767147107902, + 79026329715516201199301 + ], + "minimum": 62, + "reverse_divisions": 63 + }, + { + "direct_divisions": 64, + "k": 32, + "matrix": [ + 2684568892382786771291329, + 1111984844349868137938112, + 1111984844349868137938112, + 460599203683050495415105 + ], + "minimum": 64, + "reverse_divisions": 65 + }, + { + "direct_divisions": 66, + "k": 33, + "matrix": [ + 15646814150613670132332869, + 6481122629115441680520770, + 6481122629115441680520770, + 2684568892382786771291329 + ], + "minimum": 66, + "reverse_divisions": 67 + }, + { + "direct_divisions": 68, + "k": 34, + "matrix": [ + 91196316011299234022705885, + 37774750930342781945186508, + 37774750930342781945186508, + 15646814150613670132332869 + ], + "minimum": 68, + "reverse_divisions": 69 + }, + { + "direct_divisions": 70, + "k": 35, + "matrix": [ + 531531081917181734003902441, + 220167382952941249990598278, + 220167382952941249990598278, + 91196316011299234022705885 + ], + "minimum": 70, + "reverse_divisions": 71 + }, + { + "direct_divisions": 72, + "k": 36, + "matrix": [ + 3097990175491791170000708761, + 1283229546787304717998403160, + 1283229546787304717998403160, + 531531081917181734003902441 + ], + "minimum": 72, + "reverse_divisions": 73 + }, + { + "direct_divisions": 74, + "k": 37, + "matrix": [ + 18056409971033565286000350125, + 7479209897770887057999820682, + 7479209897770887057999820682, + 3097990175491791170000708761 + ], + "minimum": 74, + "reverse_divisions": 75 + }, + { + "direct_divisions": 76, + "k": 38, + "matrix": [ + 105240469650709600546001391989, + 43592029839838017630000520932, + 43592029839838017630000520932, + 18056409971033565286000350125 + ], + "minimum": 76, + "reverse_divisions": 77 + }, + { + "direct_divisions": 78, + "k": 39, + "matrix": [ + 613386407933224037990008001809, + 254072969141257218722003304910, + 254072969141257218722003304910, + 105240469650709600546001391989 + ], + "minimum": 78, + "reverse_divisions": 79 + }, + { + "direct_divisions": 80, + "k": 40, + "matrix": [ + 3575077977948634627394046618865, + 1480845785007705294702019308528, + 1480845785007705294702019308528, + 613386407933224037990008001809 + ], + "minimum": 80, + "reverse_divisions": 81 + }, + { + "direct_divisions": 82, + "k": 41, + "matrix": [ + 20837081459758583726374271711381, + 8631001740904974549490112546258, + 8631001740904974549490112546258, + 3575077977948634627394046618865 + ], + "minimum": 82, + "reverse_divisions": 83 + }, + { + "direct_divisions": 84, + "k": 42, + "matrix": [ + 121447410780602867730851583649421, + 50305164660422142002238655969020, + 50305164660422142002238655969020, + 20837081459758583726374271711381 + ], + "minimum": 84, + "reverse_divisions": 85 + }, + { + "direct_divisions": 86, + "k": 43, + "matrix": [ + 707847383223858622658735230185145, + 293199986221627877463941823267862, + 293199986221627877463941823267862, + 121447410780602867730851583649421 + ], + "minimum": 86, + "reverse_divisions": 87 + }, + { + "direct_divisions": 88, + "k": 44, + "matrix": [ + 4125636888562548868221559797461449, + 1708894752669345122781412283638152, + 1708894752669345122781412283638152, + 707847383223858622658735230185145 + ], + "minimum": 88, + "reverse_divisions": 89 + }, + { + "direct_divisions": 90, + "k": 45, + "matrix": [ + 24045973948151434586670623554583549, + 9960168529794442859224531878561050, + 9960168529794442859224531878561050, + 4125636888562548868221559797461449 + ], + "minimum": 90, + "reverse_divisions": 91 + }, + { + "direct_divisions": 92, + "k": 46, + "matrix": [ + 140150206800346058651802181530039845, + 58052116426097312032565778987728148, + 58052116426097312032565778987728148, + 24045973948151434586670623554583549 + ], + "minimum": 92, + "reverse_divisions": 93 + }, + { + "direct_divisions": 94, + "k": 47, + "matrix": [ + 816855266853924917324142465625655521, + 338352530026789429336170142047807838, + 338352530026789429336170142047807838, + 140150206800346058651802181530039845 + ], + "minimum": 94, + "reverse_divisions": 95 + }, + { + "direct_divisions": 96, + "k": 48, + "matrix": [ + 4760981394323203445293052612223893281, + 1972063063734639263984455073299118880, + 1972063063734639263984455073299118880, + 816855266853924917324142465625655521 + ], + "minimum": 96, + "reverse_divisions": 97 + }, + { + "direct_divisions": 98, + "k": 49, + "matrix": [ + 27749033099085295754434173207717704165, + 11494025852381046154570560297746905442, + 11494025852381046154570560297746905442, + 4760981394323203445293052612223893281 + ], + "minimum": 98, + "reverse_divisions": 99 + }, + { + "direct_divisions": 100, + "k": 50, + "matrix": [ + 161733217200188571081311986634082331709, + 66992092050551637663438906713182313772, + 66992092050551637663438906713182313772, + 27749033099085295754434173207717704165 + ], + "minimum": 100, + "reverse_divisions": 101 + }, + { + "direct_divisions": 102, + "k": 51, + "matrix": [ + 942650270102046130733437746596776286089, + 390458526450928779826062879981346977190, + 390458526450928779826062879981346977190, + 161733217200188571081311986634082331709 + ], + "minimum": 102, + "reverse_divisions": 103 + }, + { + "direct_divisions": 104, + "k": 52, + "matrix": [ + 5494168403412088213319314492946575384825, + 2275759066655021041292938373174899549368, + 2275759066655021041292938373174899549368, + 942650270102046130733437746596776286089 + ], + "minimum": 104, + "reverse_divisions": 105 + }, + { + "direct_divisions": 106, + "k": 53, + "matrix": [ + 32022360150370483149182449211082676022861, + 13264095873479197467931567359068050319018, + 13264095873479197467931567359068050319018, + 5494168403412088213319314492946575384825 + ], + "minimum": 106, + "reverse_divisions": 107 + }, + { + "direct_divisions": 108, + "k": 54, + "matrix": [ + 186639992498810810681775380773549480752341, + 77308816174220163766296465781233402364740, + 77308816174220163766296465781233402364740, + 32022360150370483149182449211082676022861 + ], + "minimum": 108, + "reverse_divisions": 109 + }, + { + "direct_divisions": 110, + "k": 55, + "matrix": [ + 1087817594842494380941469835430214208491185, + 450588801171841785129847227328332363869422, + 450588801171841785129847227328332363869422, + 186639992498810810681775380773549480752341 + ], + "minimum": 110, + "reverse_divisions": 111 + }, + { + "direct_divisions": 112, + "k": 56, + "matrix": [ + 6340265576556155474967043631807735770194769, + 2626223990856830547012786898188760780851792, + 2626223990856830547012786898188760780851792, + 1087817594842494380941469835430214208491185 + ], + "minimum": 112, + "reverse_divisions": 113 + }, + { + "direct_divisions": 114, + "k": 57, + "matrix": [ + 36953775864494438468860791955416200412677429, + 15306755143969141496946874161804232321241330, + 15306755143969141496946874161804232321241330, + 6340265576556155474967043631807735770194769 + ], + "minimum": 114, + "reverse_divisions": 115 + }, + { + "direct_divisions": 116, + "k": 58, + "matrix": [ + 215382389610410475338197708100689466705869805, + 89214306872958018434668458072636633146596188, + 89214306872958018434668458072636633146596188, + 36953775864494438468860791955416200412677429 + ], + "minimum": 116, + "reverse_divisions": 117 + }, + { + "direct_divisions": 118, + "k": 59, + "matrix": [ + 1255340561797968413560325456648720599822541401, + 519979086093778969111063874274015566558335798, + 519979086093778969111063874274015566558335798, + 215382389610410475338197708100689466705869805 + ], + "minimum": 118, + "reverse_divisions": 119 + }, + { + "direct_divisions": 120, + "k": 60, + "matrix": [ + 7316660981177400006023755031791634132229378601, + 3030660209689715796231714787571456766203418600, + 3030660209689715796231714787571456766203418600, + 1255340561797968413560325456648720599822541401 + ], + "minimum": 120, + "reverse_divisions": 121 + }, + { + "direct_divisions": 122, + "k": 61, + "matrix": [ + 42644625325266431622582204734101084193553730205, + 17663982172044515808279224851154725030662175802, + 17663982172044515808279224851154725030662175802, + 7316660981177400006023755031791634132229378601 + ], + "minimum": 122, + "reverse_divisions": 123 + }, + { + "direct_divisions": 124, + "k": 62, + "matrix": [ + 248551090970421189729469473372814871029093002629, + 102953232822577379053443634319356893417769636212, + 102953232822577379053443634319356893417769636212, + 42644625325266431622582204734101084193553730205 + ], + "minimum": 124, + "reverse_divisions": 125 + }, + { + "direct_divisions": 126, + "k": 63, + "matrix": [ + 1448661920497260706754234635502788141981004285569, + 600055414763419758512382581064986635475955641470, + 600055414763419758512382581064986635475955641470, + 248551090970421189729469473372814871029093002629 + ], + "minimum": 126, + "reverse_divisions": 127 + }, + { + "direct_divisions": 128, + "k": 64, + "matrix": [ + 8443420432013143050795938339643913980856932710785, + 3497379255757941172020851852070562919437964212608, + 3497379255757941172020851852070562919437964212608, + 1448661920497260706754234635502788141981004285569 + ], + "minimum": 128, + "reverse_divisions": 129 + } + ], + "schema_version": 1, + "source_sha256": { + "PROOF.md": "5b3e8c4ac0b160b628fb744a7d3b400a5f1ff06857d35a01353fc8d84d98fb02", + "README.md": "6c16acc2dabdd2bf5e6858024486a223603ff38206b2a8dd311dbc662f13dd57", + "SOURCES.json": "2c6dad0c081ef57eb9a8d306876b85d09c590e510061eda9ccd3d1c52fd8e1c5", + "TASK.json": "e8d97f08fa06fb1e5570296642c5c66aaa12ae66fa721d06661c402af74cf5a5", + "VERIFY.json": "38ff0db71bc56e7449377e3c5c58d43383d6fe8f06d7f42e636c5233f289d185", + "verify.py": "5527aefa7d9e7b0841901bf6752e25b9268cb32790ab923a79ab46f57a0c9c76" + }, + "theorem": "lambda(B^k)=2k for all integers k>=1" +} diff --git a/research/sl2z-power-length/SOURCES.json b/research/sl2z-power-length/SOURCES.json new file mode 100644 index 0000000000..302605e290 --- /dev/null +++ b/research/sl2z-power-length/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/sl2z-transvection-moment/README.md", + "usage": "provenance", + "git_blob": "279c57fe84ab0d8b025870e6d7cc128a870e4bf7", + "sha256": "5247d54f8b49ddc286cd1b8213f6a10f0d184137153a9b2e056b12daf781a8eb" + } + ] +} diff --git a/research/sl2z-power-length/TASK.json b/research/sl2z-power-length/TASK.json new file mode 100644 index 0000000000..4b9a0d0ce1 --- /dev/null +++ b/research/sl2z-power-length/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the exact faithful integer-transvection length of B^k for every k>=1, with arbitrary nonzero integer coefficients charged one letter.", + "scope_change_reason": "PR4146 leaves a strict gap in the exact word count. This is a scoped algebraic length theorem building on its explicit model, rather than a new register identity or native supplier.", + "bottleneck_link": "The exact length removes possible word shortening from the rank-only integer-transvection bill. Conversion, physical costs and supplier admission remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved exact length result. Do not expand into other alphabets or a native construction.", + "outcome": "completed", + "evidence": "PROOF.md proves lambda(B^k)=2k using the cited classical shortest-division-chain theorem. RESULT.json records 64 exact finite power fixtures, a complete explicitly bounded short-word census, and rejection/scope controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed admissible native operation contract realize the faithful integer action with a favorable complete tariff?", + "why_it_matters": "The exact formal count does not supply a native conversion or a useful supplier.", + "first_step": "Price one faithful X(2) update, including its shift, arbitrary dirty data, restoration and every frame conversion.", + "blocked_by": "A named admissible caller and a complete physical implementation bill are absent." + } + ] +} diff --git a/research/sl2z-power-length/VERIFY.json b/research/sl2z-power-length/VERIFY.json new file mode 100644 index 0000000000..8a46c3e408 --- /dev/null +++ b/research/sl2z-power-length/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact Pell/matrix endpoints and least-remainder traces through k=64; complete bounded short-word census for B^3; active rejection and coefficient/quotient/tariff controls; generated source-hash certificate equality." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact evidence with optimized Python, proving runtime checks do not depend on assertions." + } + ] +} diff --git a/research/sl2z-power-length/verify.py b/research/sl2z-power-length/verify.py new file mode 100644 index 0000000000..93683486ac --- /dev/null +++ b/research/sl2z-power-length/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of PROOF.md; standard library, no Git/network.""" + +import argparse +import hashlib +import json +from fractions import Fraction +from itertools import product +from pathlib import Path + + +IDENTITY = (1, 0, 0, 1) +BASE = (5, 2, 2, 1) +POWER_LIMIT = 64 +COEFFICIENTS = (-3, -2, -1, 1, 2, 3) +SHORT_LIMIT = 5 +PACKAGE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(left, right): + a, b, c, d = left + e, f, g, h = right + return (a * e + b * g, a * f + b * h, + c * e + d * g, c * f + d * h) + + +def letter(family, coefficient): + require(family in ("X", "Y"), "unknown letter family") + require(isinstance(coefficient, (int, Fraction)), "nonrational coefficient") + require(coefficient != 0, "zero coefficient is not a paid letter") + if family == "X": + return (1, coefficient, 0, 1) + return (1, 0, coefficient, 1) + + +def word_matrix(word): + require(len(word) <= 2 * POWER_LIMIT, "word exceeds finite-check bound") + result = IDENTITY + for family, coefficient in word: + result = multiply(result, letter(family, coefficient)) + return result + + +def pell_values(last_index): + require(1 <= last_index <= 2 * POWER_LIMIT + 1, "Pell index out of range") + values = [0, 1] + for index in range(2, last_index + 1): + values.append(2 * values[index - 1] + values[index - 2]) + return values + + +def nearest_chain(a, b): + require(isinstance(a, int) and isinstance(b, int), "noninteger chain input") + require(a != 0 and b != 0, "chain starts with zero") + require(max(abs(a).bit_length(), abs(b).bit_length()) <= 1024, + "chain input exceeds 1024 bits") + initial = (a, b) + quotients, remainders = [], [] + # Each noninitial remainder at least halves the preceding divisor. + for _ in range(abs(b).bit_length() + 2): + floor = a // b + quotient = floor + if abs(a - (floor + 1) * b) < abs(a - floor * b): + quotient += 1 + remainder = a - quotient * b + quotients.append(quotient) + remainders.append(remainder) + if remainder == 0: + return {"initial": list(initial), "quotients": quotients, + "remainders": remainders} + a, b = b, remainder + raise ValueError("least-remainder iteration bound exhausted") + + +def validate_chain(chain): + a, b = chain["initial"] + quotients, remainders = chain["quotients"], chain["remainders"] + require(0 < len(quotients) == len(remainders) <= 1026, "bad trace lengths") + for index, (quotient, remainder) in enumerate(zip(quotients, remainders)): + require(b != 0, "division after a zero remainder") + require(a == quotient * b + remainder, "division identity fails") + require(2 * abs(remainder) <= abs(b), "not a least remainder") + require(remainder != 0 or index == len(quotients) - 1, + "trace continues past its first zero") + a, b = b, remainder + require(b == 0 and abs(a) == 1, "trace does not terminate at gcd one") + + +def removal_chain(word, matrix): + a, c = matrix[0], matrix[2] + first = word[0][0] + remainders = [] + for index, (family, coefficient) in enumerate(word): + expected = first if index % 2 == 0 else ("Y" if first == "X" else "X") + require(family == expected, "word is not alternating") + if family == "X": + a -= coefficient * c + remainders.append(a) + else: + c -= coefficient * a + remainders.append(c) + if a == 0 or c == 0: + return remainders + raise ValueError("word did not produce a zero coordinate") + + +def check_power(k, matrix, pell): + expected = (pell[2 * k + 1], pell[2 * k], pell[2 * k], pell[2 * k - 1]) + require(matrix == expected, "Pell matrix identity fails") + a, b, c, d = matrix + require(a * d - b * c == 1, "determinant is not one") + direct, reverse = nearest_chain(a, c), nearest_chain(c, a) + validate_chain(direct) + validate_chain(reverse) + require(direct["quotients"] == [2] * (2 * k), "direct length is not 2k") + require(reverse["quotients"] == [0] + [2] * (2 * k), + "reverse length is not 2k+1") + word = tuple((family, 2) for _ in range(k) for family in ("X", "Y")) + require(word_matrix(word) == matrix, "attaining word misses full endpoint") + require(removal_chain(word, matrix) == direct["remainders"], + "literal inverse removals disagree with division trace") + return {"k": k, "matrix": list(matrix), "minimum": 2 * k, + "direct_divisions": len(direct["quotients"]), + "reverse_divisions": len(reverse["quotients"])} + + +def all_powers(): + pell = pell_values(2 * POWER_LIMIT + 1) + matrix, records = IDENTITY, [] + for k in range(1, POWER_LIMIT + 1): + matrix = multiply(matrix, BASE) + records.append(check_power(k, matrix, pell)) + return records + + +def short_word_census(): + alphabet = tuple((family, coefficient) for family in ("X", "Y") + for coefficient in COEFFICIENTS) + matrices = tuple(letter(*entry) for entry in alphabet) + target = multiply(multiply(BASE, BASE), BASE) + counts, hits = [], [] + for length in range(SHORT_LIMIT + 1): + count = 0 + for indices in product(range(len(alphabet)), repeat=length): + matrix = IDENTITY + for index in indices: + matrix = multiply(matrix, matrices[index]) + count += 1 + if matrix == target: + hits.append(list(indices)) + require(count == len(alphabet) ** length, "incomplete word layer") + counts.append(count) + require(not hits, "bounded short word reaches B cubed") + return {"coefficients": list(COEFFICIENTS), "length_limit": SHORT_LIMIT, + "words_by_length": counts, "words": sum(counts), "hits": hits} + + +def expect_rejection(case, value): + try: + if case == "chain": + validate_chain(value) + elif case == "power": + check_power(3, value, pell_values(7)) + elif case == "letter": + letter(*value) + elif case == "integer": + require(all(isinstance(t, int) for _, t in value), + "rational word is outside the integer alphabet") + else: + raise RuntimeError("unknown rejection control") + except ValueError: + return 1 + raise ValueError("damaged control was accepted: " + case) + + +def controls(): + target = multiply(multiply(BASE, BASE), BASE) + chain = nearest_chain(target[0], target[2]) + bad_quotient = json.loads(json.dumps(chain)) + bad_quotient["quotients"][0] += 1 + bad_remainder = json.loads(json.dumps(chain)) + bad_remainder["remainders"][-1] = 1 + count = expect_rejection("chain", bad_quotient) + count += expect_rejection("chain", bad_remainder) + count += expect_rejection("power", (target[0] + 1,) + target[1:]) + count += expect_rejection("letter", ("Z", 2)) + count += expect_rejection("letter", ("X", 0)) + rational = (("X", Fraction(12, 5)), ("Y", 70), ("X", Fraction(2, 5))) + require(word_matrix(rational) == target, "rational boundary word fails") + count += expect_rejection("integer", rational) + word = tuple((family, 2) for _ in range(3) for family in ("X", "Y")) + for omitted in range(len(word)): + require(word_matrix(word[:omitted] + word[omitted + 1:]) != target, + "omitted call retained the endpoint") + count += 1 + require(tuple(entry % 2 for entry in target) == IDENTITY, + "mod-two quotient control changed") + require(sum(abs(t) for _, t in word) == 12, "unit-price boundary changed") + return {"rejections": count, "rational_three_letter_endpoint": list(target), + "mod_two_endpoint": list(IDENTITY), "unit_expansion_letters": 12} + + +def source_hashes(): + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + return {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in names} + + +def make_result(): + powers = all_powers() + census = short_word_census() + checked_controls = controls() + return {"schema_version": 1, "claim_type": "scoped-proof", + "theorem": "lambda(B^k)=2k for all integers k>=1", + "finite_powers": powers, "bounded_word_census": census, + "controls": checked_controls, "source_sha256": source_hashes()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group() + mode.add_argument("--write", type=Path, help="write a fresh generated result") + mode.add_argument("--certificate", type=Path, help="compare another result") + args = parser.parse_args() + result = make_result() + if args.write: + payload = json.dumps(result, indent=2, sort_keys=True) + "\n" + with args.write.open("x", encoding="utf-8") as output: + require(output.write(payload) == len(payload), "short certificate write") + else: + path = args.certificate or PACKAGE / "RESULT.json" + require(path.stat().st_size <= 1_000_000, "certificate exceeds 1 MB") + recorded = json.loads(path.read_text(encoding="utf-8")) + require(recorded == result, "certificate differs from exact regeneration") + print("PASS_SL2Z_POWER_LENGTH powers=64 minimum=2k " + f"short_words={result['bounded_word_census']['words']} " + f"hits=0 rejection_controls={result['controls']['rejections']} " + "classical_division_chain_theorem=cited no_new_kappa") + + +if __name__ == "__main__": + main()