Repository navigation
Price integer transvections on the shear target B^k. - #4146
Merged
Mister-Meeseeks merged 1 commit intoOct 20, 2026
Merged
Mister-Meeseeks merged 1 commit into
Mister-Meeseeks merged 1 commit into
Conversation
The unit alphabet already fails the supplier test. Allowing every nonzero integer coefficient makes B itself pass at two roles for a in [0, 1), and makes every higher power fail even before the idle role is dropped. Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
This was referenced Oct 20, 2026
Draft
Draft
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Change and mathematical scope
Scoped moment calculation for one larger shear alphabet. No new κ, no supplier admission, and no selected-frontier change. The selected conditional exponent remains
0.001672660197076918.PR #4126 shows that the unit alphabet
{X, X^{-1}, Y, Y^{-1}}makes every faithful word forB^kfail the strict supplier test. This package prices the explicitly larger alphabet of arbitrary integer transvectionseach letter one rank-1 child, with the same address width
m = 2and the same momentM(a) = (λ/W)·2^{a-1}. The three-bit quotient is not used as a bill.For
B = X^2 Y^2and every integerk ≥ 1:λ(B) = 2viaX^2 Y^2.λ(B^k) ≥ 4for everyk ≥ 2, because a length-2 word needs a diagonal entry equal to 1 and a length-3 word needsv_kto divideu_{k-1}-1, while0 < u_{k-1}-1 < v_k. The word(X^2 Y^2)^kgivesλ(B^k) ≤ 2k.W = 2, the single matrixBsatisfiesM(a) = 2^{a-1} < 1for everya ∈ [0, 1), andM(1) = 1. Every higher power fails the strict test.W = 1the strict test already fails forB.|t|unit shears restores length 4 forBand removes theW = 2pass.Status: partial. The length classification is a proof for every
k; the verifier checks the identities it uses throughB^{24}. This is not a register identity, not a native XOR bill, and not a multiplication theorem.Task and overlap
Base commit
bb4bccbf42844d2801487450727c2f63e10d1d0f. Catalogue cardbit-new-register-model, priority revision 6. Scope key7084092dd726e7ba1f2ffor the card method “Derive a target-specific relaxation bound for that same explicit alphabet.”Scope: changed. The card asks for a new register identity escaping the three-register obstruction. This package does not build that identity. It answers open question 1 of the unit-shear supplier inequality, a different object on the same bit-mechanism track. An optimistic pass for one matrix at one role count is not catalogue acceptance.
Nearest work:
Band the four-call unit word.λ ≥ 2k+1for unit letters and asks for a larger integer alphabet. This PR is that alphabet. It does not repeat the unit-letter proof.bit-new-register-modelpackages (span-four dirty auxiliary, span-six flagged exclusion). They do not price this shear alphabet.Session selection: eligible open handoffs on Discussion #1166, after excluding work already delivered this round, numbered from 1 so sibling sessions keep items 1–10. Fewer than 27 eligible items remained. Item index
(27-1) mod 12 = 2is the shear supplier/recurrence inequality (comments 19031016 and 19032401). #4126 already performed that item, so this PR is the distinct larger-alphabet remainder.Validation
Environment: Python 3.12.3, standard library only. No Lean, Docker, or selected cold replay.
Also run under
python3.12 -I -O -Werror -B. Observed:The finite script checks the recurrence, the word
(X^2 Y^2)^k, the determinant and companion identities, both closed forms on a sample of exponents, the unit breadth-first control (length 4), the strict moment on every rational in[0, 1]with denominator at most 8, rejection of the boundaryM = 1, and a damaged coefficient. The claim for everykis the divisibility argument inresearch/sl2z-transvection-moment/README.md. Exactλ(B^k) = 2kis not claimed.Credit
B, and the four-call unit word.Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
Open next questions
Package question 1: if a coefficient
t = 2is one shift plus a unit shear, rather than one child or two unit children, doesM(a) < 1still hold forBatW = 2? That price decides which of the two extremes this alphabet lands on. First step: name one native operation that implements the shift, charge its rank and any dirty auxiliary, and recompute the two-role moment. Blocker: the rank-only model has no such native shift. Inventing one would be a new alphabet.Workflow feedback (optional)
Handoff-first selection on Discussion #1166, then a one-alphabet stop after both role readings, matched the package guide. Feedback thread: #1200