diff --git a/research/h6-commuting-repair/PROOF.md b/research/h6-commuting-repair/PROOF.md new file mode 100644 index 0000000000..673e9bc1e2 --- /dev/null +++ b/research/h6-commuting-repair/PROOF.md @@ -0,0 +1,133 @@ +# Commuting dyadic repairs of the H6 complement + +This scoped proof was produced by Nick Petalas. Its H6 spectral premises +and the unrestricted rank-560 comparison are cited from Ross Richardson's +[PR3655](https://github.com/CrocSwap/integer-mult-bounds/pull/3655), +head `7bf23e128e58a33c019268f57129629f603547f7`. They are not audited here. + +## Statement and inherited premises + +Put D=Z[1/2]. Let K be the symmetric dyadic H6 matrix on N=30960 ports +from the cited source, and put C=I-K. Its cited characteristic polynomial is + +```text +char_K(x) = x^30144 (x-39)^224 (x-45)^560 + (x^2+186x-6075)^16. +``` + +For every B in M_N(D) satisfying BK=KB and C+B in GL_N(D), + +```text +ker_Q B is contained in ker_Q K, +rank_Q B >= 816. +``` + +The minimum is exactly 816. B=K attains it because C+B=I and the cited +symmetry and characteristic polynomial give rank K=816. In particular, +every polynomial correction B=f(K) with dyadic coefficients obeys this +lower bound. The attaining correction cancels the kernel response. It +does not supply an encoder or a useful physical source operation. + +The cited unrestricted minimum is 560. Consequently every rank-560 dyadic +repair must fail to commute with K. The new cost of this commutation +restriction is exactly 256 rational rank units. These units are correction +matrix ranks, not Gaussian child ranks or paid native calls. + +## An invariant-kernel lemma + +Let C,B be finite square matrices over D with BC=CB and R=C+B in GL(D). +Let M=ker_D B. This submodule is saturated: if nonzero d in D and dx is +in M, then dBx=0 in a torsion-free module, so Bx=0. Because D is a PID, +M is free and is a direct summand of D^N. Its rank is dim_Q ker_Q B. +This also follows by clearing a denominator from any rational kernel +vector to obtain a vector in M. + +B commutes with R. It therefore commutes with R inverse, which has dyadic +entries. Both R and R inverse preserve M, so R restricts to a dyadic +automorphism of M. On M, R=C. It follows that C restricted to M is an +automorphism, and its determinant is a unit of D. + +In a D basis extending a basis of M, C is block upper triangular. Thus +the characteristic polynomial of C restricted to M is a monic divisor +of char_C in D[z]. Its constant coefficient is a dyadic unit. This is the +obstruction: an invariant kernel of a commuting correction cannot retain +a characteristic factor with a nonunit constant coefficient. + +The argument holds for every finite N. It permits arbitrary mixing inside +repeated eigenspaces. It does not assume that B is symmetric, diagonal, +normal, diagonalizable, or a polynomial in C. + +## Apply the lemma to H6 + +Substitution z=1-x gives the cited C characteristic factors + +```text +char_C(z) = (z-1)^30144 (z+38)^224 (z+44)^560 + (z^2-188z-5888)^16. +``` + +The quadratic is irreducible over Q. Its discriminant is +58896=144*409, and 20^2<409<21^2. Unique factorization in Q[z] implies +that the characteristic polynomial of C restricted to M has the form + +```text +(z-1)^a (z+38)^b (z+44)^c (z^2-188z-5888)^d, +0<=a<=30144, 0<=b<=224, 0<=c<=560, 0<=d<=16. +``` + +Its determinant, up to sign, has absolute factors + +```text +38^b 44^c 5888^d, +38=2*19, 44=4*11, 5888=256*23. +``` + +The 19-, 11- and 23-adic valuations are respectively b,c,d. A dyadic +unit has all three valuations zero, so b=c=d=0. Thus dim_Q ker B=a<=30144 +and rank B>=30960-30144=816. + +Furthermore C is diagonalizable over the reals because K is symmetric. +Its restriction to an invariant subspace has the same property. The only +remaining eigenvalue on M is 1, so C acts as the identity on M and K acts +as zero. This gives the stronger kernel containment in the statement. + +Together with B=K, this proves the exact minimum. No H6 matrix entries, +Smith factors, predecessor counts or source programs need to be replayed +to deduce this new consequence of the cited characteristic polynomial. + +## The hypotheses matter + +For C=diag(3,5), the dyadic correction + +```text +B = [[2,4],[-4,-8]], rank B=1, +C+B = [[5,4],[-4,-3]], det(C+B)=1 +``` + +does not commute with C. Every commuting dyadic repair of this C has +rank two, by the lemma. Thus an unrestricted low-rank repair can genuinely +escape the conclusion. This example is a control for the new hypothesis, +not a replacement for the H6 predecessor's rank-560 certificate. + +The ring hypothesis also matters. The commuting rational correction +B=diag(-14/5,0) has rank one and det(C+B)=1, but C+B=diag(1/5,5) is not a +matrix over D. Rational invertibility, or a determinant-one condition +without the dyadic entry condition, does not establish a dyadic automorphism. + +Extra directions change the contract. For the one-dimensional C=[3], +the two-dimensional matrix [[3,1],[-1,0]] is unimodular. The theorem fixes +the original dimension and endpoint and makes no claim about such stable +extensions or their dirty-helper restoration. + +## Verification boundary + +The standalone checker enumerates an explicitly bounded two-dimensional +matrix domain and checks new abstract attaining endpoints under dyadic +conjugation. It also checks the stated characteristic-factor application, +its irreducibility condition, altered factor certificates and essential +hypotheses. Its output counts every domain actually executed. + +The finite checks corroborate the invariant-kernel proof. They do not +establish the H6 spectrum, reconstruct its 30960-square matrix, audit the +rank-560 completion, synthesize a paid circuit or prove a multiplication +theorem. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/h6-commuting-repair/README.md b/research/h6-commuting-repair/README.md new file mode 100644 index 0000000000..2273f42aef --- /dev/null +++ b/research/h6-commuting-repair/README.md @@ -0,0 +1,113 @@ +# H6 commuting dyadic repairs need rank 816 + +For the H6 kernel K and its complement C=I-K, every dyadic correction B +with BK=KB and C+B invertible over Z[1/2] has rational rank at least +**816**. This is sharp: B=K makes the endpoint the identity. The stronger +conclusion is ker B contained in ker K. Polynomial corrections are included. + +Ross Richardson's [PR3655](https://github.com/CrocSwap/integer-mult-bounds/pull/3655) +gives the unrestricted rank-560 dyadic completion. That result and the H6 +spectrum are cited premises, not fresh audits. The new obstruction shows +that any rank-560 completion must break commutation with K. Restricting +to commuting corrections costs exactly 256 additional correction rank units. +Correction matrix rank is not a native Gaussian tariff. + +This is a scoped written proof with finite exact corroboration. It supplies +no physical source word, paid supplier, new kappa or selected-frontier change. +The rank-816 attainer cancels the useful kernel response and is only an +algebraic witness to sharpness. + +## Why the restriction matters + +A commuting correction has an invariant kernel. If C+B is a dyadic +automorphism, then its restriction to that kernel is C and must also be a +dyadic automorphism. The nonidentity H6 characteristic factors have odd +nonunit constant terms. None can remain on that kernel. The cited spectrum +therefore forces all 816 responsive dimensions to be changed. + +[PROOF.md](PROOF.md) gives the all-dimensional invariant-kernel argument and +the H6 application. It permits arbitrary mixing inside repeated eigenspaces +and does not assume B is symmetric or diagonalizable. A literal two-by-two +noncommuting correction demonstrates that the commutation hypothesis is +essential. Odd denominators and extra directions have separate controls. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/h6-commuting-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/h6-commuting-repair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/h6-commuting-repair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/h6-commuting-repair --check-source-history +``` + +Another CPython 3.12 executable may replace the local path. The last command +checks publication bytes after committing. Both registered scientific commands +print `PASS_H6_COMMUTING_REPAIR rank=816 no_new_kappa`. + +The verifier enumerates all 390,625 ordered pairs of two-by-two integer +matrices with entries in {-2,-1,0,1,2}. Exactly 12,465 pairs commute, and +6,552 also have a dyadic-unit repaired determinant. Every one satisfies +the invariant-kernel rank bound; 1,856 attain that bound. It checks 36 +literal dyadic conjugations of attaining abstract matrices, three altered +factor certificates, four hypothesis controls and ten invalid certificates. +These finite domains corroborate the proof; they do not establish the H6 +spectral premise by enumeration. + +The program needs no Git, network, predecessor executable or source import. +It emits a generated receipt bound to all six package files and writes no +files. SOURCES.json pins the historical source statements as provenance. +The registered metadata check authenticates those pins separately. + +## Limits and execution bounds + +The same 30,960-dimensional endpoint and the dyadic coefficient ring are +essential. Noncommuting corrections, rational coefficients with odd +denominators and stable extensions are outside the theorem. The H6 spectrum, +symmetry and unrestricted 560-row completion retain their cited status. +No dense H6 reconstruction, predecessor replay, native circuit, complete +cost/precision/tape/stock calculation or supplier admission is performed. +Independent human and formal proof-kernel review are unclaimed. + +The checker has no recursion or shared mutable state. Its largest nested +enumeration has exactly 625 squared iterations. Factor certificates have at +most eight factors of degree at most two, multiplicity at most 40,000, +128-bit coefficient numerators/denominators and total dimension at most +100,000. Matrix helpers consume fixed four-entry internal tuples. Every +function is shorter than 60 lines; exceptions preserve checks under -O. +Registered invocations enable warnings as errors. + +Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates its +integers, fractions and collections during the bounded one-shot replay. +The matrix box contains only 625 tuples, and the other finite domains and +factor limits above bound live data. This is not a persistent service or +a fixed-allocation native implementation. No metaprogramming, callback +dispatch or mutable global registry is used. + +## Open next questions + +- Construct explicit noncommuting coefficients for the predecessor's named + 560-row completion. Identify the spectral components they mix, then price + legal source frames, scalar work and dirt restoration. Those coefficients + and a physical word remain missing. +- Consider an enlarged dirty-helper interface only after specifying all + arbitrary inputs, required outputs and its complete paid/target invoice. + A stable extension changes the theorem's endpoint and can leave helper + dirt or restoration costs unpaid. + +The structured questions and blockers are in [TASK.json](TASK.json). +The original decoder card is explicitly changed to this algebraic side +obstruction. Selected-baseline metadata orientation passes; it is not a +scientific replay of the selected supplier. + +## Credit + +This contribution was produced by Nick Petalas. Ross Richardson supplies +PR3655's H6 dyadic repair and its retained spectral premises. Credit Dominik +Scholz's PR606 geometry/factorization, DreamingOfClouds' H6/Walsh proposal +and the retained PR1830 spectral, compensation and encoder lineage. +Saturated kernels over a PID, characteristic polynomials and odd-prime +valuations are classical. The new result is their invariant-kernel use to +prove the exact commuting-repair obstruction for this fixed source. +Apache-2.0. diff --git a/research/h6-commuting-repair/SOURCES.json b/research/h6-commuting-repair/SOURCES.json new file mode 100644 index 0000000000..c62ef3d0fc --- /dev/null +++ b/research/h6-commuting-repair/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/h6-dyadic-source-repair/PROOF.md", + "usage": "provenance", + "git_blob": "c0afff43035b2ec4c8ac3e0991473da4d420419e", + "sha256": "c58fe24fcbe26a577cea4e418f62041c5ad0e3cf1e8d7e85b4654674963eff5c" + }, + { + "path": "research/h6-dyadic-source-repair/README.md", + "usage": "provenance", + "git_blob": "f086ace2422585d1faa824652d936a5750e7179b", + "sha256": "a9b97857189465b716a7c6e46a0d3a2f266ce8f85edc70a7996fc965a791eb62" + } + ] +} diff --git a/research/h6-commuting-repair/TASK.json b/research/h6-commuting-repair/TASK.json new file mode 100644 index 0000000000..0a9ba99f4d --- /dev/null +++ b/research/h6-commuting-repair/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "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": "changed", + "actual_scope": "Exact minimum rank 816 of a commuting dyadic repair of the H6 complement, conditional on its cited spectrum; unrestricted rank 560 remains a cited predecessor result.", + "scope_change_reason": "A scoped decoder-side obstruction replaces the card construction search. The new restriction is commutation of the correction with the fixed H6 kernel, including polynomial corrections. This is not a new target in a predecessor call-count model.", + "bottleneck_link": "The H6 alternative decoder still needs a paid source completion. A rank-560 realization must mix different spectral components: every commuting repair has rank at least 816. Matrix rank is not a native tariff.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and locally corroborated obstruction; package it without attempting a larger construction or a paid circuit.", + "outcome": "completed", + "evidence": "PROOF.md proves the invariant-kernel lemma and exact H6 bound. verify.py corroborates it with bounded exact matrix domains, hypothesis controls and factor-certificate rejection.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the cited 560-row completion be synthesized by a noncommuting dyadic correction at legal H6 source frames?", + "why_it_matters": "The new obstruction rules out every commuting and polynomial correction at rank 560.", + "first_step": "Use the predecessor row-support certificate to produce explicit completion coefficients and identify which spectral components they mix.", + "blocked_by": "No coefficients, legal frame access, dirt restoration or paid physical word is supplied here." + }, + { + "question": "Can a useful enlarged dirty-helper interface preserve a spectral implementation while beating its complete recursive bill?", + "why_it_matters": "Stable extensions are outside the fixed-dimensional obstruction, but helper dirt and restoration are additional obligations.", + "first_step": "Specify every arbitrary input and required output and give a complete channel, restoration and productive-target invoice before searching.", + "blocked_by": "A commuting map on an enlarged space is a different contract; neither native legality nor its complete cost is established." + } + ], + "claim_type": "scoped written proof with finite exact corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228563" +} diff --git a/research/h6-commuting-repair/VERIFY.json b/research/h6-commuting-repair/VERIFY.json new file mode 100644 index 0000000000..81b2dd46d9 --- /dev/null +++ b/research/h6-commuting-repair/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Finite exact commuting-pair domain, dyadic conjugates, new H6 factor consequence, hypothesis controls and invalid factor certificates." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same mathematical checks under optimized Python; no assertions may disappear." + } + ] +} diff --git a/research/h6-commuting-repair/verify.py b/research/h6-commuting-repair/verify.py new file mode 100644 index 0000000000..861f7384d9 --- /dev/null +++ b/research/h6-commuting-repair/verify.py @@ -0,0 +1,223 @@ +"""Corroborate the commuting-repair obstruction; no predecessor replay. + +The unbounded result is proved in PROOF.md. All executable domains below +are fixed and finite. This program writes only deterministic stdout. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +from math import isqrt +from pathlib import Path +import json + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def dyadic(value: Fraction) -> bool: + denominator = value.denominator + return denominator & (denominator - 1) == 0 + + +def unit(value: int | Fraction) -> bool: + value = Fraction(value) + numerator = abs(value.numerator) + return dyadic(value) and numerator > 0 and numerator & (numerator - 1) == 0 + + +def square(value: Fraction) -> bool: + return value >= 0 and ( + isqrt(value.numerator) ** 2 == value.numerator + and isqrt(value.denominator) ** 2 == value.denominator + ) + + +def obstruction(factors: tuple) -> tuple[int, int]: + """Return total degree and bad-factor degree for a factored polynomial. + + Coefficients are in increasing order. Only irreducible monic degree-one + and degree-two factors are accepted. This is a degree certificate, not + a routine to recognize a matrix or establish its characteristic factors. + """ + need(1 <= len(factors) <= 8, "factor count") + total = bad = 0 + seen = set() + for coefficients, multiplicity in factors: + need(2 <= len(coefficients) <= 3, "factor degree") + need(type(multiplicity) is int and 1 <= multiplicity <= 40000, + "multiplicity") + coefficients = tuple(Fraction(x) for x in coefficients) + need(all(dyadic(x) for x in coefficients), "dyadic coefficients") + need(all(x.numerator.bit_length() <= 128 + and x.denominator.bit_length() <= 128 for x in coefficients), + "coefficient size") + need(coefficients[-1] == 1, "monic factor") + need(coefficients not in seen, "distinct factors") + seen.add(coefficients) + if len(coefficients) == 3: + constant, linear, _ = coefficients + need(not square(linear * linear - 4 * constant), + "irreducible quadratic required") + degree = len(coefficients) - 1 + total += degree * multiplicity + if not unit(coefficients[0]): + bad += degree * multiplicity + need(total <= 100000, "total dimension") + return total, bad + + +def det2(matrix: tuple) -> int | Fraction: + a, b, c, d = matrix + return a * d - b * c + + +def rank2(matrix: tuple) -> int: + return 2 if det2(matrix) else int(any(matrix)) + + +def mul2(left: tuple, right: tuple) -> tuple: + 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 add2(left: tuple, right: tuple) -> tuple: + return tuple(a + b for a, b in zip(left, right, strict=True)) + + +def good_degree2(matrix: tuple) -> int: + """Classify its monic quadratic over Q using trace and determinant.""" + trace = matrix[0] + matrix[3] + determinant = det2(matrix) + discriminant = trace * trace - 4 * determinant + if discriminant < 0 or isqrt(discriminant) ** 2 != discriminant: + return 2 if unit(determinant) else 0 + root = isqrt(discriminant) + need((trace + root) % 2 == 0, "integral rational root") + return int(unit((trace + root) // 2)) + int(unit((trace - root) // 2)) + + +def exhaustive_pairs() -> dict: + matrices = tuple(product(range(-2, 3), repeat=4)) + need(len(matrices) == 625, "complete matrix box") + commuting = accepted = sharp = 0 + ranks = [0, 0, 0] + for original in matrices: + floor = 2 - good_degree2(original) + for repair in matrices: + if mul2(original, repair) != mul2(repair, original): + continue + commuting += 1 + if not unit(det2(add2(original, repair))): + continue + accepted += 1 + observed = rank2(repair) + need(observed >= floor, "commuting rank obstruction") + ranks[observed] += 1 + sharp += int(observed == floor) + need(accepted > 0 and sharp > 0, "nonempty positive domain") + return {"pairs": len(matrices) ** 2, "commuting": commuting, + "accepted": accepted, "sharp": sharp, "accepted_ranks": ranks} + + +def changed_basis_cases() -> int: + """Literal dyadic conjugations of independent small repaired matrices.""" + values = tuple(Fraction(x, 2) for x in range(-4, 5)) + originals = ((1, 0, 0, -38), (-44, 0, 0, 1), + (0, 5888, 1, 188), (3, 0, 0, 5)) + checked = 0 + identity = (1, 0, 0, 1) + for original in originals: + expected = 2 - good_degree2(original) + repair = tuple(a - b for a, b in zip(identity, original, strict=True)) + need(rank2(repair) == expected, "attaining algebraic correction") + for value in values: + basis = (1, value, 0, 1) + inverse = (1, -value, 0, 1) + c = mul2(mul2(basis, original), inverse) + b = mul2(mul2(basis, repair), inverse) + need(all(dyadic(Fraction(x)) for x in c + b), "dyadic conjugate") + need(mul2(c, b) == mul2(b, c), "conjugated commutation") + need(add2(c, b) == identity and rank2(b) == expected, + "literal attaining endpoint and rank") + checked += 1 + return checked + + +def hypothesis_controls() -> dict: + original = (3, 0, 0, 5) + repair = (2, 4, -4, -8) + need(rank2(repair) == 1 and det2(add2(original, repair)) == 1, + "rank-one unrestricted unit repair") + need(mul2(original, repair) != mul2(repair, original), + "unrestricted witness must break commutation") + rational = (Fraction(-14, 5), 0, 0, 0) + need(rank2(rational) == 1 and det2(add2(original, rational)) == 1, + "rational determinant-one control") + need(not dyadic(rational[0]), "odd denominator must be excluded") + need(mul2(original, rational) == mul2(rational, original), + "rational control really commutes") + need(det2(original) != 0 and not unit(det2(original)), + "rational invertibility is insufficient") + need(det2((3, 1, -1, 0)) == 1, + "an auxiliary direction changes the interface") + factors = (((-1, 1), 30144), ((38, 1), 224), + ((44, 1), 560), ((-5888, -188, 1), 16)) + need(obstruction(factors) == (30960, 816), "new H6 application") + need(816 - 560 == 256, "gap from cited unrestricted rank") + mutants = ( + (((-1, 1), 30144), ((38, 1), 224), ((44, 1), 560)), + (((-1, 1), 30144), ((2, 1), 224), ((44, 1), 560), + ((-5888, -188, 1), 16)), + (((-1, 1), 30144), ((38, 1), 224), ((4, 1), 560), + ((-5888, -188, 1), 16)), + ) + for mutant in mutants: + need(obstruction(mutant) != (30960, 816), "damaged factor control") + return {"noncommuting_rank_one": list(repair), + "repaired_determinant": 1, "factor_mutations": len(mutants), + "hypothesis_controls": 4} + + +def rejection_controls() -> int: + invalid = ((), (((1, 2), 1),), (((1, 0, 1), 0),), + (((Fraction(1, 3), 1), 1),), (((1, 1), 40001),), + (((0, 1, 1), 1),), (((1, 1), 1), ((1, 1), 1)), + (((1 << 128, 1), 1),), + tuple(((x, 1), 1) for x in range(9)), + (((0, 1), 40000), ((3, 1), 40000), ((5, 1), 40000))) + for factors in invalid: + try: + obstruction(factors) + except ValueError: + continue + raise ValueError("invalid factor certificate accepted") + need(obstruction((((1, 0, 1), 40000), ((-1, 1), 20000))) + == (100000, 0), "dimension boundary") + need(obstruction((((1 << 127, 1), 1),)) == (1, 0), + "coefficient-size boundary") + return len(invalid) + + +def main() -> None: + result = {"claim_type": "scoped written proof with finite corroboration", + "h6_commuting_rank": 816, "cited_unrestricted_rank": 560, + "pairs": exhaustive_pairs(), + "dyadic_basis_cases": changed_basis_cases(), + "controls": hypothesis_controls(), + "invalid_certificates_rejected": rejection_controls()} + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + result["sha256"] = {name: sha256((root / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, sort_keys=True, indent=2)) + print("PASS_H6_COMMUTING_REPAIR rank=816 no_new_kappa") + + +if __name__ == "__main__": + main()