diff --git a/research/helper462-one-scale-shear-floor-10/README.md b/research/helper462-one-scale-shear-floor-10/README.md new file mode 100644 index 0000000000..b0fba3b42d --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/README.md @@ -0,0 +1,229 @@ +# One-scale helper-462 words need 10 shears + +**Proof that every one-scale zero-swap word has at least 10 elementary shears. No new κ.** +The selected record stays `363005817/100000000000`. + +PR #7055 proved that the elementary rank-drop depth of each one-scale block is +at most 2, so the shear length is at least 9. PR #7125 exhibits a word of +length 21 and leaves 9 through 21 open. A search that returns no shorter word +is not a lower bound. This package closes the bottom of that interval: length +9 is impossible under the same hypotheses, so the lower bound is 10. Twenty-one +remains an upper bound. Ten is not shown to be sharp. + +This is a proof. The length-9 shape is a finite case split. The remaining +obstruction is a finite set of rational pencils, one for each census matrix +and each coordinate position, and every rational coefficient is decided by a +generic depth together with the rational roots of explicit eliminants. It is +not a heuristic search, and it is not a census of the infinite set of words of +length 10 or more. + +## Scope + +Original card: `supplier-boundary-audit`, priority revision 8, base +`e54523517d0f03e58352e647c403a5af3e525a57`. Scope status: **refined**. + +The question is open question 1 of PR #7125, the request to raise the +rank-drop floor of #7055 from 9 to 10. The 21-shear word, the 26-shear word, +and the 29-shear word are not redone. The selected frontier is not changed. + +`current-priorities.md` on this base may still quote an older selected value. +The verifier reads `certificates/selected-result.json`. + +## Hypotheses + +Rows are numbered `0..7`. A letter is a shear `row_a += c * row_b` with +`a ≠ b` and `c ∈ Q \ {0}`, a single-coordinate scale, or an axis swap. A word +is applied to `I` from the first letter through the last, by left +multiplication. The pinned matcher `S` is the `matcher` field of +`research/bit-completed-backend-api/science/RESULT.json`. Its determinant is +`-16`. + +**Inherited hypotheses, as in #7030 and #7055.** Zero axis swaps and exactly +one scale. The determinant forces that scale to be `-16` on one row. Let `D` +be the corresponding diagonal matrix. Conjugation by `D` sends a shear to a +shear of the same length, with the coefficient multiplied by a ratio of +diagonal entries. It is enough to bound elementary factorizations of the eight +matrices `D^{-1} S`. Each of those matrices lies in `SL(8)` and has rank +distance 8 from `I`. The verifier checks the determinant, the special-linear +blocks, and the rank. + +An elementary shear changes `rank(· - I)` by at most 1. Write `ρ` for that +rank and `δ` for the elementary rank-drop depth: the longest chain of left +multiplications by `I - c E_{ij}` that each drop the rank by exactly 1. +Depth is at most the rank, because each step decreases it. A product of `ρ` +shears has depth `ρ`, since the partial products realize a chain of that +length and the opposite inequality is general. This is the depth lemma of +#7055. The positive control here is the same eight-shear word used there: it +has rank 8 and depth 8, so the depth function does attain the rank on some +elementary words. + +## The length-9 shape + +Let `A = D^{-1} S`, so `ρ(A) = 8`. Suppose `A = T_9 ⋯ T_1` with each `T_k` an +elementary shear, and write `P_0 = I`, `P_k = T_k P_{k-1}`, `r_k = ρ(P_k)`. +Then `r_0 = 0`, `r_9 = 8`, and each step changes the rank by at most 1. + +The sum of the nine changes is 8, and each change is in `{-1, 0, +1}`. If `p`, +`m`, and `z` count the increases, decreases, and stalls, then `p + m + z = 9` +and `p - m = 8`, so `2m + z = 1`. The only solution is `m = 0`, `z = 1`. +A length-9 word has exactly one rank-preserving shear and no rank-decreasing +shear. + +The first shear takes `I` to a rank-1 matrix, so the stall is not first. Let +it occur at rank `t`. The suffix after the stall consists of `8 - t` shears, +each increasing the rank by 1, from a matrix `Q` of rank `t` up to `A`. +Peeling that suffix is a left rank-drop chain of length `8 - t`, so +`δ(A) ≥ 8 - t`. The census below has `δ(A) ≤ 2`, hence `t ∈ {6, 7, 8}`. +The matrix `Q` is reached by left peels from `A`, so it is one of the census +matrices of rank `t`. + +The predecessor `P` of the stall satisfies `Q = T P` with `ρ(P) = ρ(Q) = t` +and with `P` a product of `t` rank-increasing shears from `I`. The depth lemma +gives `δ(P) = t`. Equivalently, `P = (I - c E_{ij}) Q` for some position and +some `c ∈ Q \ {0}`, the rank stays `t`, and the depth equals `t`. A chain of +`t` rank drops from such a `P` ends at `I`, and the suffix peels supply the +rest of the word. So a length-9 word exists if and only if some census matrix +of rank `t ∈ {6, 7, 8}` has a rank-preserving elementary shear whose result +has depth `t`. + +## The pencil is finite + +Fix a census matrix `Q` of rank `t` and a position `(i, j)`. For +`c ∈ Q` set + +`P(c) = (I - c E_{ij}) Q`. + +The gap `G(c) = P(c) - I` is affine of rank at most one in `c`: only row `i` +moves, and it moves by a fixed row of `Q`. Every minor is a polynomial in `c`. +Any minor larger than the generic rank is the zero polynomial, so a +specialization cannot raise the rank above the generic rank. Fraction-free +elimination pivots on entries that are not identically zero. At any `c` where +none of those pivot polynomials vanishes, the same pivots remain valid and the +rank equals the generic rank. The only candidates for a different rank are the +rational roots of those pivots. + +- If the generic rank is below `t`, no coefficient preserves rank `t`. +- If the generic rank is above `t`, the only coefficients that can land on + rank `t` are those pivot roots. Each is evaluated exactly. +- If the generic rank equals `t`, every coefficient outside the pivot roots + preserves rank. A root of a pivot drops the rank and is not a stall. Depth + on the preserving coefficients is the remaining point. + +On that preserving set, the rank-drop edges are the positions where both +standard-basis memberships hold and the pairing of #7055 is nonzero. The +unique coefficient is the reciprocal of that pairing. Membership and the +pairing are rational functions, read off one elimination of `G(c)`. A vector +that lies in the image generically stays in the image wherever the rank keeps +its generic value. A vector that lies outside enters only at the roots of the +inconsistency numerators. Those roots, the poles of the peel coefficients, and +the same data for every generic child are an explicit finite set `E ⊂ Q`. + +For `c ∉ E` the edge set is a subset of the generic edge set, and each child +is the specialization of the corresponding polynomial child. Depth is therefore +at most the generic depth. The walk that builds `E` also computes that generic +depth, and one rational sample outside `E` is required to reproduce it by the +numeric depth function. The two implementations are independent: integer +factorization of a specialized gap, against fraction-free elimination of the +polynomial gap. They must agree. Every rational root in `E` is then evaluated +by the numeric function, and only the coefficients that still have rank `t` +are kept. Matrix entries that appear in the walk have degree at most 2; the +verifier rejects a deeper entry. + +Degree 1 contributes one root, the slope ratio. Degree 2 contributes a +rational root exactly when the discriminant is a perfect square, tested by an +exact integer square root. Degree 3 and higher uses the rational-root theorem. +The constant and leading coefficients are factored completely, and primality +of every factor below `2^64` is the deterministic Miller-Rabin test with the +Sinclair bases. A coefficient of degree 3 or more with more than 64 bits is a +hard failure, not a skipped root. On every scale row the highest degree of a +polynomial whose roots were required is 8, and the verifier rejects any other +degree. No such coefficient exceeded the 64-bit factor bound: a larger one +aborts the run. + +The 3×3 control is the matrix reached by the shears `(0,1,-2)`, `(1,0,-2)`, +`(0,2,-2)`. It has rank 2 and depth 0. One elementary shear raises the depth +to 2 while keeping the rank. The same predicate that accepts every helper +census matrix rejects this one. The checker is not reporting "depth stays +small" because it cannot see a jump. + +## Census and the bound + +The verifier expands the whole rank-drop tree of each `D^{-1} S`. Every left +rank-drop shear is the unique cancelling coefficient of the #7055 pairing: +the target basis vector lies in the column space of the gap, the source basis +vector lies in the row space, and the pairing is nonzero. The census asks +that question for every ordered pair, by exact integer elimination. Every +reported peel is checked to drop the rank by 1, and the walk does not stop at +a preset rank. A missed edge would be a missed peel, so the depth bound is +the depth of this exhaustive tree. No branch reaches rank 5 or below, so the depth is at most 2 +and the length-9 shape applies. Distinct matrices are fewer than the arrival +counts of #7055: rows 0, 1, 2, and 4 have 37 arrivals at rank 6 and 20 +distinct matrices; row 5 has 4 arrivals and 2 distinct matrices. The edge +counts agree with #7055 either way. + +| scale row | `det(W - I)` | depth | distinct ranks 8, 7, 6 | max preserving depth at those ranks | +| --- | --- | --- | --- | --- | +| 0, 1, 2, 4 | 1/2 | 2 | 1, 33, 20 | 3, 2, 1 | +| 5 | 1/2 | 2 | 1, 36, 2 | 3, 2, 1 | +| 3, 6 | 21/8 | 1 | 1, 38, 0 | 2, 1 | +| 7 | 19/4 | 1 | 1, 48, 0 | 2, 1 | + +Every one of those depths is strictly below the rank of its matrix. No +rank-preserving shear of a census matrix has depth equal to the rank. Length +9 is impossible. + +Combined with the subadditive bound and the depth lemma, the shear length is +at least 10. The 21-shear word of #7125 remains an upper bound and is not +reproved here. The integers 10 through 21 stay open. Nothing in this argument +changes the selected κ. + +## What this does not say + +Ten is not shown to be sharp. A length-10 word has either two stalls or one +descent and one stall, and that case split is not taken. The bound uses +elementary coordinate shears, zero swaps, and one scale. It does not say that +`D^{-1} S` fails to be a product of nine arbitrary transvections. + +No owner, ROW, fallback, tape, precision, or physical generator is emitted. +No supplier is admitted. No P2 ordinary bill is computed. + +## Reproduce + +From the repository root, Python 3.12, standard library only: + +```sh +python3 -B research/helper462-one-scale-shear-floor-10/verify.py +python3 -I -B research/helper462-one-scale-shear-floor-10/verify.py +python3 -O -B research/helper462-one-scale-shear-floor-10/verify.py +python3 -B scripts/research_package.py --package research/helper462-one-scale-shear-floor-10 +``` + +Checks use an explicit failure function, so they stay active under `-O`. +The certificate uses four worker processes when the machine has them. On this +4-CPU machine the registered replay finished in 190.48 seconds, `python3 -O -B` +in 192.01 seconds, and `python3 -I -B` in 189.13 seconds. Expected last line +begins with `PASS_HELPER462_ONE_SCALE_SHEAR_FLOOR_10`. + +No Lean, Docker, or selected cold replay was run. + +## Open next questions + +1. Is 10 sharp for a one-scale zero-swap elementary word in the pinned + helper-462 matcher, or does a second obstruction force length at least 11? + The certificate rules out length 9, and the upper bound is still the + 21-shear word of PR #7125, so 10 through 21 remain open. A word of length + 10 would show that 10 is sharp. The useful first step is to classify a + length-10 rank profile: the changes sum to 8 over 10 steps, so either two + shears preserve rank or one descent accompanies one stall. The same census + is the place to look. It is blocked by the free coefficient of each + non-dropping shear; the length-9 case split does not cover two stalls. + +## Credit + +The rank subadditivity bound of 8 and the one-scale reduction are from PR +#7030. The depth lemma, the pairing criterion, and the bound of 9 are from PR +#7055. The upper bound of 21 is the word in PR #7125; this package does not +recompute it. The census edge counts match #7055; the rank-6 column here +counts distinct matrices rather than arrivals. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. diff --git a/research/helper462-one-scale-shear-floor-10/SOURCES.json b/research/helper462-one-scale-shear-floor-10/SOURCES.json new file mode 100644 index 0000000000..7a047e5dc1 --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-completed-backend-api/science/RESULT.json", + "usage": "input", + "git_blob": "55dca30281e3375d63a128c3de041e46c8a3c5ba", + "sha256": "965b650c0e49572e028f89a60943c64ad8dff9032fc93272b86cd1f9715a77b7" + } + ] +} diff --git a/research/helper462-one-scale-shear-floor-10/TASK.json b/research/helper462-one-scale-shear-floor-10/TASK.json new file mode 100644 index 0000000000..fdc37e7cf8 --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Under the zero-swap, one-scale hypotheses of the helper-462 rank-drop argument, can the elementary shear lower bound of 9 be raised to 10?", + "scope_change_reason": "The catalogue card asks a supplier-admission question. This package takes the allowed one-proposition variation and answers the named open question from PR #7125: whether the rank-drop floor of 9 for a one-scale zero-swap word in the pinned helper-462 matcher can be raised to 10. It does not admit a supplier and does not change the selected frontier.", + "bottleneck_link": "Side result on the pinned helper-462 matcher. It raises an elementary-word lower bound and does not change the selected kappa or a paid profile.", + "budget_minutes": 60, + "stop_rule": "Stop when every scale row's rank-drop census is certified and every rank-preserving elementary shear of every census matrix of rank 6, 7 or 8 has depth strictly below that rank, or when one such shear meets the rank and supplies a length-9 word.", + "outcome": "completed", + "evidence": "research/helper462-one-scale-shear-floor-10/README.md and verify.py. The length-9 shape is proved, and the stall search is a finite pencil certificate.", + "author": "unpaidmoon", + "ai_assistance": "substantial Cursor Grok assistance", + "open_questions": [ + { + "question": "Is 10 sharp for a one-scale zero-swap elementary word in the pinned helper-462 matcher, or does a second obstruction force length at least 11?", + "why_it_matters": "The certificate rules out length 9. The recorded upper bound is the 21-shear word of PR #7125, so the integers 10 through 21 stay open. A word of length 10 would show that 10 is sharp.", + "first_step": "Classify a length-10 word: the rank changes sum to 8 over 10 steps of size at most 1, so either there are two rank-preserving shears or one descent and one stall. The same census is the place to look.", + "blocked_by": "A non-dropping shear has a free rational coefficient. The length-9 case split does not cover two stalls, and no length-10 word is known." + } + ] +} diff --git a/research/helper462-one-scale-shear-floor-10/VERIFY.json b/research/helper462-one-scale-shear-floor-10/VERIFY.json new file mode 100644 index 0000000000..f446c20b09 --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/bit-completed-backend-api/science/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Selected kappa stays 363005817/100000000000. The pinned matcher has determinant -16, and each of the eight one-scale blocks D^{-1}S lies in SL(8) with rank distance 8 from I. An explicit 8-shear word attains depth 8. A 3x3 shear raises depth from 0 to 2 while preserving rank, so the depth checker is not blind to a jump. For every scale row the rank-drop tree matches the pinned census, never passes rank 6, and every left peel drops rank by 1. For every distinct census matrix of rank t in {6,7,8} and every elementary shear, the maximum depth over rational coefficients that preserve rank is the pinned value, strictly below t. A length-9 one-scale zero-swap word is therefore impossible, and the shear lower bound is 10. No kappa change." + } + ] +} diff --git a/research/helper462-one-scale-shear-floor-10/shearcert.py b/research/helper462-one-scale-shear-floor-10/shearcert.py new file mode 100644 index 0000000000..76b3ea5dd7 --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/shearcert.py @@ -0,0 +1,736 @@ +"""Exact rank-drop depth of one-parameter elementary shears. + +Polynomials are tuples of integers, lowest degree first. The numeric depth +oracle factors the gap with integer row operations. The symbolic walk uses +fraction-free elimination over Z[c]. +""" +from fractions import Fraction +from math import gcd + +"""Fraction-free Bareiss elimination over Z[c], tuples of ints.""" +from fractions import Fraction + +def trim(a): + a=list(a) + while len(a)>1 and a[-1]==0: + a.pop() + return tuple(a) + +def add(a,b): + n=max(len(a),len(b)) + o=[0]*n + for i,x in enumerate(a): o[i]+=x + for i,x in enumerate(b): o[i]+=x + return trim(o) + +def sub(a,b): + return add(a, tuple(-x for x in b)) + +def mul(a,b): + if a==(0,) or b==(0,): + return (0,) + o=[0]*(len(a)+len(b)-1) + for i,x in enumerate(a): + if not x: continue + for j,y in enumerate(b): + if y: o[i+j]+=x*y + return trim(o) + +def scale(a,k): + if k==0 or a==(0,): + return (0,) + if k==1: + return a + return trim(tuple(x*k for x in a)) + +def eq(a,b): + return trim(a)==trim(b) + +def is_zero(a): + return a==(0,) or a==() + +def exact_quo(a,b): + """Exact quotient in Z[c]. b divides a.""" + a=list(trim(a)); b=list(trim(b)) + if b==[0]: + raise ZeroDivisionError + if a==[0]: + return (0,) + if len(a)= len(B): + if not A or A[-1] == 0: + if A: + A.pop() + else: + break + continue + factor = A[-1] / B[-1] + shift = len(A) - len(B) + for i, bv in enumerate(B): + A[i + shift] -= factor * bv + while A and A[-1] == 0: + A.pop() + if not A: + A = [Fraction(0)] + den = 1 + for x in A: + den = den * x.denominator // gcd(den, x.denominator) + return divc(trim(tuple(int(x * den) for x in A))) + +def pgcd(a, b): + a, b = divc(trim(a)), divc(trim(b)) + if is_zero(a): + return b if not is_zero(b) else (1,) + if is_zero(b): + return a + while not is_zero(b): + a, b = b, divc(prem(a, b)) + if len(a) > 40: + raise RuntimeError("gcd degree %s" % len(a)) + if a[-1] < 0: + a = neg(a) + return a + +def cancel(n, d): + g = pgcd(n, d) + if len(g) == 1 and abs(g[0]) == 1: + return n, d + return exact_quo(n, g), exact_quo(d, g) + +class RF: + __slots__ = ("n", "d") + def __init__(self, n, d=None): + n = trim(n) + d = ONE if d is None else trim(d) + if is_zero(d): + raise ZeroDivisionError("zero den") + if d[-1] < 0: + n, d = neg(n), neg(d) + g = gcd(content(n), content(d)) + if g > 1: + n = tuple(x // g for x in n) + d = tuple(x // g for x in d) + n, d = cancel(n, d) + self.n = n + self.d = d + def __add__(self, other): + return RF(add(mul(self.n, other.d), mul(other.n, self.d)), mul(self.d, other.d)) + def __sub__(self, other): + return RF(sub(mul(self.n, other.d), mul(other.n, self.d)), mul(self.d, other.d)) + def __mul__(self, other): + return RF(mul(self.n, other.n), mul(self.d, other.d)) + def __truediv__(self, other): + if is_zero(other.n): + raise ZeroDivisionError("div0") + return RF(mul(self.n, other.d), mul(self.d, other.n)) + def ev(self, value): + return ev(self.n, value) / ev(self.d, value) + def is_zero(self): + return is_zero(self.n) + +def eliminate(rows, rhs_columns): + """rhs_columns: list of columns, each a list of n polys (row-major per column).""" + n = len(rows) + k = len(rhs_columns) + A = [[rows[i][j] for j in range(n)] + [rhs_columns[c][i] for c in range(k)] for i in range(n)] + prev = ONE + rank = 0 + pivot_of_row = {} + witnesses = [] + col = 0 + while rank < n and col < n: + piv = next((i for i in range(rank, n) if not is_zero(A[i][col])), None) + if piv is None: + col += 1 + continue + if piv != rank: + A[rank], A[piv] = A[piv], A[rank] + pivval = A[rank][col] + witnesses.append(trim(pivval)) + for i in range(rank + 1, n): + factor = A[i][col] + nrow = [ZERO] * col + for j in range(col, n + k): + num = sub(mul(pivval, A[i][j]), mul(factor, A[rank][j])) + nrow.append(exact_quo(num, prev)) + A[i] = nrow + prev = pivval + pivot_of_row[rank] = col + rank += 1 + col += 1 + return A, rank, pivot_of_row, witnesses + +def backsolve(A, rank, pivot_of_row, rhs_index, n): + xs = [RF(ZERO) for _ in range(n)] + col_rhs = n + rhs_index + for r in range(rank - 1, -1, -1): + col = pivot_of_row[r] + acc = RF(A[r][col_rhs]) + for j in range(col + 1, n): + if not is_zero(A[r][j]): + acc = acc - RF(A[r][j]) * xs[j] + xs[col] = acc / RF(A[r][col]) + return xs + +_ROOTS = {} + +def rat_roots(poly): + """Every rational root. Degree 1 is the slope ratio. Degree 2 uses the + discriminant: an integer quadratic has a rational root exactly when its + discriminant is a perfect square. Higher degree uses the rational-root + theorem with a complete factorization of coefficients below 2^64. + """ + poly = divc(trim(poly)) + STATS["maxrootdeg"] = max(STATS.get("maxrootdeg", 0), max(0, len(poly) - 1)) + cached = _ROOTS.get(poly) + if cached is not None: + return cached + found = _rat_roots_body(poly) + _ROOTS[poly] = found + return found + +def _rat_roots_body(poly): + if len(poly) > 3: + for coef in poly: + if abs(coef).bit_length() > 64: + raise RuntimeError( + "degree %s coefficient has %s bits; factorization is not certified" + % (len(poly) - 1, abs(coef).bit_length())) + if is_zero(poly) or len(poly) == 1: + return [] + if len(poly) == 2: + return [Fraction(-poly[0], poly[1])] + if len(poly) == 3: + # Coefficients are lowest degree first: constant, linear, leading. + constant, linear, leading = poly + disc = linear * linear - 4 * leading * constant + if disc < 0: + return [] + root = _isqrt(disc) + if root * root != disc: + return [] + found = [Fraction(-linear + root, 2 * leading), Fraction(-linear - root, 2 * leading)] + for cand in found: + if ev(poly, cand) != 0: + raise RuntimeError("quadratic formula missed %s" % cand) + return _uniq(found) + g = content(poly) + poly = tuple(c // g for c in poly) + if poly[0] == 0: + return _uniq([Fraction(0)] + rat_roots(poly[1:])) + ps = divisors(abs(poly[0])) + qs = divisors(abs(poly[-1])) + roots = [] + for p in ps: + for q in qs: + for sign in (1, -1): + cand = Fraction(sign * p, q) + if ev(poly, cand) == 0: + roots.append(cand) + return _uniq(roots) + +def _isqrt(n): + if n < 0: + raise ValueError("negative") + x = int(n ** 0.5) if n.bit_length() < 1000 else 1 << ((n.bit_length() + 1) // 2) + while True: + y = (x + n // x) // 2 if x else n + if y >= x: + return x + x = y + +def _uniq(vals): + out, seen = [], set() + for v in vals: + if v not in seen: + seen.add(v) + out.append(v) + return out + +_div_cache = {} + +def divisors(n): + n = abs(int(n)) + if n in _div_cache: + return _div_cache[n] + factors = factorize(n) + divs = [1] + i = 0 + while i < len(factors): + p = factors[i] + e = 0 + while i < len(factors) and factors[i] == p: + e += 1 + i += 1 + power = 1 + extra = [] + for _ in range(e): + power *= p + extra.extend(d * power for d in divs) + divs.extend(extra) + _div_cache[n] = divs + return divs + +def factorize(n): + n = abs(int(n)) + factors = [] + for p in (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47): + while n % p == 0: + factors.append(p) + n //= p + if n > 1: + factors.extend(_split(n)) + factors.sort() + return factors + +def _split(n): + if n == 1: + return [] + if _prime(n): + return [n] + d = _rho(n) + if d is None or d == n: + raise RuntimeError("failed to factor %s bits" % n.bit_length()) + return _split(d) + _split(n // d) + +def _rho(n): + if n % 2 == 0: + return 2 + for c in (1, 3, 5, 7, 11, 13): + x = y = 2 + d = 1 + while d == 1: + x = (x * x + c) % n + y = (y * y + c) % n + y = (y * y + c) % n + d = gcd(abs(x - y), n) + if 1 < d < n: + return d + return None + +def _prime(n): + """Deterministic Miller-Rabin for n < 2^64. Larger integers are refused.""" + if n < 2: + return False + if n >= 1 << 64: + raise RuntimeError("primality above 2^64 is not certified here") + small = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37) + for p in small: + if n == p: + return True + if n % p == 0: + return False + # Jim Sinclair's base set decides every integer below 2^64. + d = n - 1 + s = 0 + while d % 2 == 0: + s += 1 + d //= 2 + for a in (2, 3, 5, 7, 11, 13, 23, 29, 31, 37): + x = pow(a, d, n) + if x == 1 or x == n - 1: + continue + for _ in range(s - 1): + x = pow(x, 2, n) + if x == n - 1: + break + else: + return False + return True + +def _solve_scaled(matrix, rhs_scale): + """Solve matrix x = rhs_scale e_k over Q for each k. matrix has integer entries.""" + width = len(matrix) + work = [matrix[i][:] + [rhs_scale if i == k else 0 for k in range(width)] for i in range(width)] + span = 2 * width + pivot_of = {} + row = 0 + col = 0 + while row < width and col < width: + piv = None + for i in range(row, width): + if work[i][col] != 0: + piv = i + break + if piv is None: + col += 1 + continue + if piv != row: + work[row], work[piv] = work[piv], work[row] + pivot_value = work[row][col] + for i in range(width): + if i == row: + continue + factor = work[i][col] + if factor == 0: + continue + g = gcd(factor, pivot_value) + mul_row = pivot_value // g + mul_piv = factor // g + pivot_row = work[row] + # Scale the whole row. Entries left of the pivot are not zero on + # earlier pivot rows, and mul_row need not be 1. + updated = [mul_row * work[i][j] - mul_piv * pivot_row[j] for j in range(span)] + g2 = 0 + for value in updated: + g2 = gcd(g2, value) + if g2 > 1: + updated = [value // g2 for value in updated] + work[i] = updated + pivot_of[col] = row + row += 1 + col += 1 + sols = [] + for k in range(width): + inconsistent = False + for i in range(width): + if work[i][width + k] == 0: + continue + if all(work[i][j] == 0 for j in range(width)): + inconsistent = True + break + if inconsistent: + sols.append(None) + continue + solution = [Fraction(0) for _ in range(width)] + # Other pivot columns were cleared, and free variables stay 0, so each + # pivot row contributes exactly rhs / pivot. + for column, index in pivot_of.items(): + solution[column] = Fraction(work[index][width + k], work[index][column]) + sols.append(solution) + return sols + + +def batch_edges(matrix): + """Every left rank-drop step, from one integer factorization of the gap and one of its transpose.""" + n = len(matrix) + den = 1 + for row in matrix: + for entry in row: + den = den * entry.denominator // gcd(den, entry.denominator) + # G = N / den, so G x = e_k iff N x = den e_k. Rank and images agree. + numeric = [[int((matrix[i][j] - (1 if i == j else 0)) * den) for j in range(n)] for i in range(n)] + columns = _solve_scaled(numeric, den) + transposed = [[numeric[r][c] for r in range(n)] for c in range(n)] + rows = _solve_scaled(transposed, den) + edges = [] + for target in range(n): + if columns[target] is None: + continue + for source in range(n): + if target == source or rows[source] is None: + continue + pairing = rows[source][target] + if pairing == 0: + continue + edges.append((target, source, 1 / pairing)) + return edges + + +def depth_matrix(matrix, memo): + key = tuple(tuple(row) for row in matrix) + hit = memo.get(key) + if hit is not None: + return hit + steps = batch_edges(matrix) + if not steps: + memo[key] = 0 + return 0 + best = 0 + for target, source, coefficient in steps: + child = left_peel(matrix, target, source, coefficient) + best = max(best, 1 + depth_matrix(child, memo)) + memo[key] = best + return best + +def matrix_from_gap(gap): + size = len(gap) + return [[gap[i][j] + (1 if i == j else 0) for j in range(size)] for i in range(size)] + +STATS = {"nodes": 0, "maxdeg": 0, "maxbits": 0, "roots": 0, "maxrootdeg": 0} +MEMO = {} + +def pencil_rows(matrix, target, source): + size = len(matrix) + clear = 1 + for row in matrix: + for entry in row: + clear = clear * entry.denominator // gcd(clear, entry.denominator) + rows = [] + for i in range(size): + row = [] + for j in range(size): + base = matrix[i][j] - (1 if i == j else 0) + if i != target: + row.append(const(int(base * clear))) + else: + row.append(trim((int(base * clear), int(-matrix[source][j] * clear)))) + rows.append(row) + return rows, const(clear), size + +def depth_at_rows(rows, den, size, value, memo): + den_v = ev(den, value) + if den_v == 0: + raise RuntimeError("denominator vanished") + gap = [[ev(rows[i][j], value) / den_v for j in range(size)] for i in range(size)] + return depth_matrix(matrix_from_gap(gap), memo), rank_of(gap) + +def _lower_rank_hits(rows, den, size, witnesses, rank_target): + """Generic rank is above the stall rank, so only top-pivot roots can preserve it.""" + roots = [] + for poly in witnesses: + roots.extend(rat_roots(poly)) + roots = [root for root in _uniq(roots) if root != 0] + best = -1 + where = None + for root in roots: + depth, rank = depth_at_rows(rows, den, size, root, MEMO) + if rank == rank_target and depth > best: + best = depth + where = (root, rank) + return best, where, 0, len(roots), STATS + +def certified_max_depth(matrix, target, source, rank_target=None): + """Max of δ((I - c E_{target,source}) matrix) over c in Q, and the argmax. + + If rank_target is set, only c that keep rank(gap) == rank_target matter. + A specialization cannot raise rank above the generic rank, so a pencil whose + generic rank is below the target contributes nothing, and one whose generic + rank is above the target can hit the target only at roots of the top pivots. + """ + rows, den, size = pencil_rows(matrix, target, source) + if rank_target is not None: + _A, rank, _piv, witnesses = eliminate(rows, []) + if rank < rank_target: + return -1, None, 0, 0, STATS + if rank > rank_target: + return _lower_rank_hits(rows, den, size, witnesses, rank_target) + polys = [] + generic = walk(rows, den, polys, size, 0) + roots = [] + for poly in polys: + roots.extend(rat_roots(poly)) + roots = [r for r in _uniq(roots) if r != 0] + memo = MEMO + def depth_at(value): + gap = [] + den_v = ev(den, value) + for i in range(size): + gap.append([ev(rows[i][j], value) / den_v for j in range(size)]) + # rows/den is the TRUE gap only at the top call, where den is the + # constant clear and rows are clear * gap. Yes. + return depth_matrix(matrix_from_gap(gap), memo), rank_of_local(gap) + # The top `rows/den` equals the true gap. Children are not evaluated here. + best = -1 + where = None + # generic sample + sample = Fraction(1) + banned = set(roots) + k = 1 + while sample in banned or sample == 0: + k += 1 + sample = Fraction(k) + d_sample, r_sample = depth_at(sample) + if d_sample != generic: + raise RuntimeError("generic depth %s != sample %s at %s" % (generic, d_sample, sample)) + if rank_target is not None and r_sample != rank_target: + raise RuntimeError("sample rank %s != target %s" % (r_sample, rank_target)) + best = d_sample if rank_target is None or r_sample == rank_target else -1 + where = (sample, r_sample) + for root in roots: + # Rank is cheap. A root whose rank leaves the stall target cannot be the + # zero-step of a length-9 word, so its depth is not required. + den_v = ev(den, root) + gap = [[ev(rows[i][j], root) / den_v for j in range(size)] for i in range(size)] + r_root = rank_of(gap) + if rank_target is not None and r_root != rank_target: + continue + d_root = depth_matrix(matrix_from_gap(gap), memo) + if d_root > best: + best = d_root + where = (root, r_root) + return best, where, generic, len(roots), STATS + +def rank_of_local(gap): + return rank_of(gap) + +def walk(rows, den, polys, size, depth_so_far): + STATS["nodes"] += 1 + if depth_so_far > size: + raise RuntimeError("depth overflow") + for row in rows: + for entry in row: + STATS["maxdeg"] = max(STATS["maxdeg"], len(entry) - 1) + if entry: + STATS["maxbits"] = max(STATS["maxbits"], max(abs(c).bit_length() for c in entry)) + # Column membership and rank witnesses, plus row solves. + eye_cols = [[const(1 if i == k else 0) for i in range(size)] for k in range(size)] + A, rank, piv, witnesses = eliminate(rows, eye_cols) + for w in witnesses: + if len(w) > 1: + polys.append(w) + STATS["roots"] += 1 + col_in = [] + for k in range(size): + nums = [trim(A[r][size + k]) for r in range(rank, size)] + generically_in = all(is_zero(num) for num in nums) + col_in.append(generically_in) + if not generically_in: + for num in nums: + if not is_zero(num) and len(num) > 1: + polys.append(num) + # Transpose for row membership and pairings. true = rows/den, + # so solving rows^T y = e gives y_poly with y_true = den * y_poly. + transposed = [[rows[r][c] for r in range(size)] for c in range(size)] + AT, rank_t, piv_t, wit_t = eliminate(transposed, eye_cols) + if rank_t != rank: + raise RuntimeError("transpose rank") + for w in wit_t: + if len(w) > 1: + polys.append(w) + row_in = [] + solutions = [] + for k in range(size): + nums = [trim(AT[r][size + k]) for r in range(rank_t, size)] + generically_in = all(is_zero(num) for num in nums) + row_in.append(generically_in) + if not generically_in: + for num in nums: + if not is_zero(num) and len(num) > 1: + polys.append(num) + solutions.append(None) + else: + solutions.append(backsolve(AT, rank_t, piv_t, k, size)) + den_rf = RF(den) + best_child = -1 + n_edges = 0 + for tgt in range(size): + if not col_in[tgt]: + continue + for src in range(size): + if tgt == src or not row_in[src]: + continue + pairing = solutions[src][tgt] * den_rf + if pairing.is_zero(): + continue + # gamma = 1/pairing + gamma = RF(ONE) / pairing + n_edges += 1 + if len(gamma.d) > 1: + polys.append(gamma.d) + child_rows, child_den = child_gap(rows, den, tgt, src, gamma, size) + child_depth = walk(child_rows, child_den, polys, size, depth_so_far + 1) + if child_depth > best_child: + best_child = child_depth + if n_edges == 0: + return 0 + return 1 + best_child + +def child_gap(rows, den, tgt, src, gamma, size): + gden = gamma.d + gnum = gamma.n + new_den = mul(den, gden) + out = [] + unit = [const(1 if j == src else 0) for j in range(size)] + for i in range(size): + if i != tgt: + out.append([mul(gden, entry) for entry in rows[i]]) + continue + row = [] + for j in range(size): + term = sub(mul(gden, rows[i][j]), mul(gnum, rows[src][j])) + # subtract gamma * e_src, i.e. gnum*den on column src + if j == src: + term = sub(term, mul(gnum, den)) + row.append(trim(term)) + out.append(row) + return out, new_den diff --git a/research/helper462-one-scale-shear-floor-10/verify.py b/research/helper462-one-scale-shear-floor-10/verify.py new file mode 100644 index 0000000000..c58650c47d --- /dev/null +++ b/research/helper462-one-scale-shear-floor-10/verify.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +"""One-scale zero-swap helper-462 words have at least 10 elementary shears. + +The rank-drop census has depth at most 2, so a word of length 9 would need +exactly one rank-preserving shear, at a census matrix of rank 6, 7 or 8, whose +predecessor still has depth equal to that rank. Every rational coefficient of +every such shear is covered by a generic depth plus the rational roots of the +pencil's eliminant. That depth stays strictly below the rank. No new kappa. + +Standard library only. Checks use an explicit failure function, so they stay +active under python -O. +""" + +from fractions import Fraction +import json +from multiprocessing import Pool +import os +from pathlib import Path +import sys +import time + +# Python -I omits the script directory. The package is one module. +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import shearcert +from shearcert import ( + apply_shear, + batch_edges, + certified_max_depth, + depth_matrix, + eye, + rank_of, + rat_roots, +) + +ROOT = Path(__file__).resolve().parents[2] +RESULT = ROOT / "research/bit-completed-backend-api/science/RESULT.json" +SELECTED = ROOT / "certificates/selected-result.json" +N = 8 +# Heavy scale rows first so four workers finish near the long pole, row 7. +SCALE_ORDER = (7, 5, 2, 6, 3, 0, 4, 1) + +# Distinct matrices. PR #7055 counted rank-6 arrivals before identifying equal +# matrices: 37 arrivals on rows 0, 1, 2 and 4, and 4 arrivals on row 5. Those +# arrivals are the edge counts below. +EXPECTED = { + 0: {"depth": 2, "det": "1/2", "nodes": {8: 1, 7: 33, 6: 20}, "edges": {8: 33, 7: 37}, + "max_depth": {8: 3, 7: 2, 6: 1}}, + 1: {"depth": 2, "det": "1/2", "nodes": {8: 1, 7: 33, 6: 20}, "edges": {8: 33, 7: 37}, + "max_depth": {8: 3, 7: 2, 6: 1}}, + 2: {"depth": 2, "det": "1/2", "nodes": {8: 1, 7: 33, 6: 20}, "edges": {8: 33, 7: 37}, + "max_depth": {8: 3, 7: 2, 6: 1}}, + 3: {"depth": 1, "det": "21/8", "nodes": {8: 1, 7: 38}, "edges": {8: 38, 7: 0}, + "max_depth": {8: 2, 7: 1}}, + 4: {"depth": 2, "det": "1/2", "nodes": {8: 1, 7: 33, 6: 20}, "edges": {8: 33, 7: 37}, + "max_depth": {8: 3, 7: 2, 6: 1}}, + 5: {"depth": 2, "det": "1/2", "nodes": {8: 1, 7: 36, 6: 2}, "edges": {8: 36, 7: 4}, + "max_depth": {8: 3, 7: 2, 6: 1}}, + 6: {"depth": 1, "det": "21/8", "nodes": {8: 1, 7: 38}, "edges": {8: 38, 7: 0}, + "max_depth": {8: 2, 7: 1}}, + 7: {"depth": 1, "det": "19/4", "nodes": {8: 1, 7: 48}, "edges": {8: 48, 7: 0}, + "max_depth": {8: 2, 7: 1}}, +} + +TIGHT_WORD = ( + (0, 1, Fraction(-1)), + (1, 0, Fraction(1, 2)), + (2, 3, Fraction(1)), + (3, 2, Fraction(2)), + (4, 5, Fraction(1)), + (5, 4, Fraction(3)), + (6, 7, Fraction(3)), + (7, 6, Fraction(3)), +) + + +def need(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def difference(matrix): + return [[matrix[i][j] - (1 if i == j else 0) for j in range(len(matrix))] + for i in range(len(matrix))] + + +def determinant(matrix): + work = [row[:] for row in matrix] + size = len(work) + det = Fraction(1) + sign = 1 + for column in range(size): + pivot = next((row for row in range(column, size) if work[row][column] != 0), None) + if pivot is None: + return Fraction(0) + if pivot != column: + work[column], work[pivot] = work[pivot], work[column] + sign = -sign + pivot_value = work[column][column] + det *= pivot_value + for row in range(column + 1, size): + if work[row][column] == 0: + continue + factor = work[row][column] / pivot_value + for index in range(column, size): + work[row][index] -= factor * work[column][index] + return sign * det + + +def load_matcher(): + data = json.loads(RESULT.read_text(encoding="utf-8")) + return [[Fraction(entry) for entry in row] for row in data["matcher"]] + + +def scale_matrix(matcher, row): + out = [entry[:] for entry in matcher] + for col in range(N): + out[row][col] /= Fraction(-16) + return out + + +def census(matrix): + """Every matrix reachable by left rank-drop peels, and the edge counts.""" + seen = set() + unique = {8: [], 7: [], 6: []} + nodes = {8: 0, 7: 0, 6: 0} + edges = {8: 0, 7: 0} + lowest = [None] + + def rec(current, rank): + key = tuple(tuple(entry) for entry in current) + if key in seen: + return + seen.add(key) + nodes[rank] = nodes.get(rank, 0) + 1 + if rank in unique: + unique[rank].append(current) + lowest[0] = rank if lowest[0] is None else min(lowest[0], rank) + steps = batch_edges(current) + if steps: + edges[rank] = edges.get(rank, 0) + len(steps) + for target, source, coefficient in steps: + child = shearcert.left_peel(current, target, source, coefficient) + child_rank = rank_of(difference(child)) + if child_rank != rank - 1: + raise SystemExit("FAIL: peel did not drop rank by 1") + rec(child, child_rank) + + root_rank = rank_of(difference(matrix)) + rec(matrix, root_rank) + tree_depth = root_rank - lowest[0] + return nodes, edges, unique, tree_depth, root_rank + + +def one_scale(scale_row): + for key in ("nodes", "maxdeg", "maxbits", "roots", "maxrootdeg"): + shearcert.STATS[key] = 0 + matcher = load_matcher() + matrix = scale_matrix(matcher, scale_row) + gap_det = determinant(difference(matrix)) + nodes, edges, unique, tree_depth, root_rank = census(matrix) + expected = EXPECTED[scale_row] + if str(gap_det) != expected["det"] or tree_depth != expected["depth"] or root_rank != 8: + raise SystemExit("FAIL: census header row %s det %s depth %s rank %s" % ( + scale_row, gap_det, tree_depth, root_rank)) + for rank, count in expected["nodes"].items(): + if nodes.get(rank, 0) != count: + raise SystemExit("FAIL: node count row %s rank %s got %s want %s" % ( + scale_row, rank, nodes.get(rank, 0), count)) + for rank, count in expected["edges"].items(): + if edges.get(rank, 0) != count: + raise SystemExit("FAIL: edge count row %s rank %s got %s want %s" % ( + scale_row, rank, edges.get(rank, 0), count)) + if any(rank < 6 and count for rank, count in nodes.items()): + raise SystemExit("FAIL: rank-drop tree on row %s reaches rank below 6: %s" % (scale_row, nodes)) + maxima = {} + for rank in (8, 7, 6): + if not unique[rank]: + continue + best = -1 + for matrix_node in unique[rank]: + for target in range(N): + for source in range(N): + if target == source: + continue + depth, _place, _generic, _nroots, _stats = certified_max_depth( + matrix_node, target, source, rank_target=rank) + if depth >= rank: + raise SystemExit( + "FAIL: row %s rank %s shear %s<-%s preserves rank with depth %s" + % (scale_row, rank, target, source, depth)) + if depth > best: + best = depth + maxima[rank] = best + if best != expected["max_depth"][rank]: + raise SystemExit("FAIL: row %s rank %s max depth %s want %s" % ( + scale_row, rank, best, expected["max_depth"][rank])) + if shearcert.STATS["maxdeg"] > 2: + raise SystemExit("FAIL: row %s pencil degree %s" % (scale_row, shearcert.STATS["maxdeg"])) + if shearcert.STATS["maxrootdeg"] != 8: + raise SystemExit("FAIL: row %s root degree %s" % (scale_row, shearcert.STATS["maxrootdeg"])) + print("ROW", scale_row, "depth", tree_depth, "max", maxima, + "rootdeg", shearcert.STATS["maxrootdeg"], flush=True) + return scale_row, maxima + + +def controls(matcher): + need(rat_roots((1, -3, 2)) and set(rat_roots((1, -3, 2))) == {Fraction(1, 2), Fraction(1)}, + "quadratic roots of 1 - 3x + 2x^2") + need(rat_roots((1, 0, 1)) == [], "x^2 + 1 has no rational root") + need(determinant(matcher) == Fraction(-16), "pinned matcher determinant") + selected = json.loads(SELECTED.read_text(encoding="utf-8")) + need(selected["kappa"] == "363005817/100000000000", "selected kappa moved") + # Eight tight shears attain rank distance 8 and depth 8. The obstruction + # below is not an artifact of the depth function. + tight = eye(8) + for target, source, coefficient in TIGHT_WORD: + tight = apply_shear(tight, target, source, coefficient) + need(rank_of(difference(tight)) == 8 and depth_matrix(tight, {}) == 8, + "tight 8-shear control") + # A 3x3 shear can raise depth by 2 while preserving rank. The same + # predicate that accepts the helper census rejects this matrix. + small = eye(3) + for target, source, coefficient in ((0, 1, -2), (1, 0, -2), (0, 2, -2)): + small = apply_shear(small, target, source, Fraction(coefficient)) + need(depth_matrix(small, {}) == 0 and rank_of(difference(small)) == 2, + "3x3 depth-0 base") + best, where, generic, _nroots, _stats = certified_max_depth(small, 0, 2) + need(generic == 0 and best == 2 and where[1] == 2, + "3x3 preserving shear must be seen to reach depth 2") + + +def main(): + t0 = time.time() + matcher = load_matcher() + controls(matcher) + for row in range(N): + block = scale_matrix(matcher, row) + need(determinant(block) == 1, "scale block %s is not in SL(8)" % row) + need(rank_of(difference(block)) == 8, "scale block %s rank" % row) + workers = min(4, os.cpu_count() or 1) + with Pool(workers) as pool: + results = pool.map(one_scale, SCALE_ORDER) + got = {row for row, _maxima in results} + need(got == set(range(N)), "missing scale rows %s" % (set(range(N)) - got)) + print("PASS_HELPER462_ONE_SCALE_SHEAR_FLOOR_10 seconds", round(time.time() - t0, 2)) + + +if __name__ == "__main__": + main()