Prove exact integer-transvection length λ(B^k)=2k (no new κ)

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.

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.