diff --git a/research/four-layer-quadratic-parity/PROOF.md b/research/four-layer-quadratic-parity/PROOF.md new file mode 100644 index 0000000000..755097b2eb --- /dev/null +++ b/research/four-layer-quadratic-parity/PROOF.md @@ -0,0 +1,134 @@ +# Four agreement layers at quadratic degree + +All ranks and polynomials in this note are over the rationals. The same ranks +hold over the reals and complexes. Let n=4m, where m is an integer at least 4. +For Boolean n-vectors x and y, write t=sum_i x_i y_i and let H_n(x,y)=(-1)^t. +This is the 2^n by 2^n Walsh-Hadamard matrix. + +Define + +``` +P_m(t) = (-1)^m (2(t-m)^2 - 5)/3, +A_m(x,y) = P_m(sum_i x_i y_i). +``` + +The construction agrees with H_n at exactly the four overlap weights +m-2, m-1, m+1 and m+2. Both A_m and every polynomial interpolant of parity +on three consecutive overlap weights have exact rank + +``` +d_n = 1 + n + binom(n,2). +``` + +Among all such consecutive triples, the unique best one is m-1,m,m+1. +A_m agrees on strictly more entries for every m>=4. This compares two explicit +families. It does not assert an optimum over all rank-d_n matrices or all +quadratic polynomials. + +## Equality set + +Put u=t-m. At u=+-1, P_m=-(-1)^m; at u=+-2, P_m=(-1)^m. +These equal (-1)^t. At u=0 its absolute value is 5/3. At every integer +|u|>=3 its absolute value is at least 13/3. Thus there are no other equalities. +All four weights lie between 0 and n under the stated hypotheses. + +## Exact rank + +Let z_i=x_i y_i. Since z_i^2=z_i on Boolean inputs, the multilinear expansion is + +``` +3P_m(sum_i z_i) = c0 + c1 sum_i z_i + c2 sum_(i=m. The remaining +two comparisons are strict as well: + +``` +w_(m+1)/w_(m-2) = (3m+1)(3m+2) / (9(m^2-1)) > 1, +w_(m+2)/w_(m-1) = (9m^2-1) / (9(m+1)(m+2)) < 1. +``` + +Consequently the unique best triple starts at m-1 and has mass +B_m=w_(m-1)+w_m+w_(m+1). + +The four-layer mass F_m=w_(m-2)+w_(m-1)+w_(m+1)+w_(m+2) has gain + +``` +F_m-B_m = w_(m-2)+w_(m+2)-w_m + = w_m N(m) / D(m), +N(m) = 27m^4 - 36m^3 - 171m^2 - 128m - 12, +D(m) = 3(m+1)(m+2)(3m+1)(3m+2). +``` + +This follows by substituting + +``` +w_(m-2)/w_m = 9m(m-1)/((3m+1)(3m+2)), +w_(m+2)/w_m = m(3m-1)/(3(m+1)(m+2)). +``` + +For k=m-4>=0, direct expansion gives + +``` +N(k+4) = 27k^4 + 396k^3 + 1989k^2 + 3688k + 1348 > 0. +``` + +Both denominator and w_m are positive. This proves the strict improvement for +every m>=4. At n=16, d_n=137, F_4=2713419648, B_4=2633821596 and the gain is +79598052 entries, out of 4^16=4294967296 ordered pairs. + +## Limits + +The comparison is about exact entry agreement, not operator norm, per-row +error, rounded execution or a complete transform algorithm. The counts include +every row, without filtering by its Hamming weight. No claimed asymptotic +non-rigidity exponent or multiplication saving follows. + +The four-layer choice loses to the best consecutive triple at n=8 and n=12. +It is also not globally best among low-rank matrices. For example, at n=40 the +rank-one constant matrix 1 agrees on more entries. Its agreement count is +sum_(t even) w_t. The verifier checks that limitation explicitly. Higher degree, +row corrections, coefficient preparation, a physical consumer, and the full +paid/target invoice are separate obligations. diff --git a/research/four-layer-quadratic-parity/README.md b/research/four-layer-quadratic-parity/README.md new file mode 100644 index 0000000000..18969fbaba --- /dev/null +++ b/research/four-layer-quadratic-parity/README.md @@ -0,0 +1,88 @@ +# Four Hamming layers improve quadratic Walsh-Hadamard agreement + +This contribution was produced by Nick Petalas. + +Claim type: a scoped written proof with exact finite corroboration. For n=4m +and every integer m>=4, the rational matrix + +``` +A_m(x,y) = (-1)^m (2(sum_i x_i y_i - m)^2 - 5)/3 +``` + +has exact rank 1+n+binom(n,2). It agrees with the Walsh-Hadamard matrix on +strictly more entries than every quadratic parity interpolant on three +consecutive overlap weights, each of which has that same exact rank. + +At n=16, both ranks are 137. Agreement rises from 2633821596 entries to +2713419648, a gain of 79598052 out of 4294967296 entries. The four matching +weights are 2,3,5,6; the best consecutive triple is 3,4,5. + +[PROOF.md](PROOF.md) supplies the all-dimension proof, exact factorization, +unique best consecutive triple and positive rational gain formula. This settles +a small instance of the equal-degree polynomial-comparison question in Jacob +Alan Sussman / jacobalansussman's [PR #5817](https://github.com/CrocSwap/integer-mult-bounds/pull/5817), +Open next question 1. That package supplies the question. None of its external +complexity claims is needed or rechecked here. Alman and Williams's +[monomial-rank and consecutive-layer construction](https://arxiv.org/html/1611.05558#S3) +is classical background; the claimed new step is this four-layer construction +and exact comparison. A bounded repository/PR search found no matching result, +which is not proof of historical novelty. + +The original `complex-rank-shape-decoder` card is explicitly changed to this +low-rank side question. The first verified improvement ends this investigation. +It does not meet the card's complete supplier gate. No new kappa or selected +frontier change is claimed. + +## Reproduce + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/four-layer-quadratic-parity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/four-layer-quadratic-parity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/four-layer-quadratic-parity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/four-layer-quadratic-parity --check-source-history +``` + +Any CPython 3.12 executable can replace the local path. Only the standard +library is required. The direct verifier prints a generated JSON receipt with +SHA256 hashes of all six package files, then `PASS_FOUR_LAYER_QUADRATIC_PARITY`. +It writes no files. Explicit exception checks remain active under optimized +Python. + +Finite checks cover 125 dimensions n=16,20,...,512; ten exact pair-count cases, +including two dense enumerations; 10920 factorization entries; eight invertible +feature-minor cases; and 18 mutation, input-boundary and scope controls. Counts +at n=16 use exact Hamming-layer multiplicities and an independent sum by row +weight, rather than a dense replay of its roughly four billion entries. + +## Limitations + +This is an exact agreement comparison between two polynomial families over the +rationals, reals or complexes. It is not optimality among all quadratics or all +rank-137 matrices. At n=40 a rank-one constant matrix already agrees on more +entries than the four-layer construction. No numerical stability, operator-error +bound, per-row correction, physical native implementation, complete recursive +invoice, supplier admission or multiplication theorem is supplied. No Lean or +selected-supplier cold replay was run. Independent human and formal proof-kernel +review are unclaimed. + +The verifier's managed-runtime deviation from fixed-allocation Power of Ten +rules is bounded by n<=512, feature dimension at most 37 and dense enumeration +at n<=8. Its only indirect call is the rejection helper with four local check +functions. All loops have finite bounds and all receipts are generated. + +## Open next questions + +- What is the best exact agreement of a quadratic in the integer overlap, + including constants? First classify its two rational level sets at 1 and -1, + then optimize their binomial mass. This could distinguish a local improvement + from a global low-degree optimum; the present comparison does not do so. +- Does a higher-degree nonconsecutive equality set improve a useful complete + Walsh-Hadamard construction after row corrections and coefficient costs? + Begin with one fixed degree and an explicit factorization. A full transform + bill and legal consumer remain missing. + +Structured questions are in [TASK.json](TASK.json). The adjacent #5917 studies +acyclic Boolean-table tensor degree, a different model and question. No +predecessor's certificate is replayed as this deliverable. diff --git a/research/four-layer-quadratic-parity/SOURCES.json b/research/four-layer-quadratic-parity/SOURCES.json new file mode 100644 index 0000000000..090d03e7af --- /dev/null +++ b/research/four-layer-quadratic-parity/SOURCES.json @@ -0,0 +1,33 @@ +{ + "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/eth-claim-fft-impact/README.md", + "usage": "provenance", + "git_blob": "92600dd0ad418122b720be283fcc32badf5c6fe5", + "sha256": "2d6fcb3edb8eea26ba6ec89856b784165d30a75794552f28712e97e69a395366" + } + ], + "source_boundary": "No external execution inputs. PR5817 poses the question; its bytes and the source catalogue are pinned for provenance. The verifier reads only its own six package files.", + "external_sources": [ + { + "authors": "Josh Alman and Ryan Williams", + "title": "Probabilistic Rank and Matrix Rigidity", + "url": "https://arxiv.org/html/1611.05558#S3", + "scope": "Classical consecutive-layer interpolation and monomial-to-rank construction. No outside conjectural claim or asymptotic theorem is used." + } + ] +} diff --git a/research/four-layer-quadratic-parity/TASK.json b/research/four-layer-quadratic-parity/TASK.json new file mode 100644 index 0000000000..4266737eb7 --- /dev/null +++ b/research/four-layer-quadratic-parity/TASK.json @@ -0,0 +1,81 @@ +{ + "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": "Compare a four-layer quadratic Walsh-Hadamard surrogate with every consecutive-triple quadratic at identical exact rational rank, for n=4m and m>=4.", + "scope_change_reason": "Take the equal-degree polynomial-comparison question in Jacob Alan Sussman PR5817, Open next question 1. This is a low-rank side result, rather than a completed native decoder or supplier invoice.", + "bottleneck_link": "Low-rank Walsh-Hadamard surrogates are a possible transform interface. This package improves exact agreement within one degree-two family; physical correction and complete supplier charges remain unprovided.", + "budget_minutes": 60, + "stop_rule": "Package the first verified strict agreement gain; do not pursue quadratic optimality or higher degree.", + "outcome": "completed", + "evidence": "PROOF.md and the read-only verify.py, including independent row-weight counts, dense small counts, factorization and mutation controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the best exact agreement of a quadratic in integer overlap, including constants?", + "why_it_matters": "The construction only beats consecutive-triple interpolants, not every quadratic or low-rank matrix.", + "first_step": "Classify the two rational level sets at 1 and -1 and optimize their binomial mass.", + "blocked_by": "No global extremal classification is supplied." + }, + { + "question": "Can a higher-degree nonconsecutive equality set improve a complete Walsh-Hadamard construction?", + "why_it_matters": "Agreement gains need a legal consumer and a complete physical bill before affecting a transform supplier.", + "first_step": "Choose one degree, give an explicit factorization and charge row corrections and coefficient preparation.", + "blocked_by": "Physical correction, native realization and complete target/paid accounting are absent." + } + ] +} diff --git a/research/four-layer-quadratic-parity/VERIFY.json b/research/four-layer-quadratic-parity/VERIFY.json new file mode 100644 index 0000000000..e908d3cbe4 --- /dev/null +++ b/research/four-layer-quadratic-parity/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": 120, + "checks": "Exact layer comparison, independent finite counts, factorization, feature rank and rejecting mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same contracts remain enforced with assertions disabled." + } + ] +} diff --git a/research/four-layer-quadratic-parity/verify.py b/research/four-layer-quadratic-parity/verify.py new file mode 100644 index 0000000000..f226be2e39 --- /dev/null +++ b/research/four-layer-quadratic-parity/verify.py @@ -0,0 +1,187 @@ +"""Exact corroboration of the four-layer quadratic comparison; standard library.""" + +from hashlib import sha256 +from itertools import combinations +import json +from math import comb +from pathlib import Path + + +class VerificationError(RuntimeError): + """An explicit mathematical or resource contract failed.""" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise VerificationError(message) + + +def coefficients(center: int) -> tuple[int, int, int]: + """Coefficients of 3P after Boolean multilinearization, by support size.""" + if type(center) is not int or not 1 <= center <= 128: + raise ValueError("center must be an integer from 1 through 128") + sign = (-1) ** center + return sign * (2 * center * center - 5), sign * (2 - 4 * center), sign * 4 + + +def numerator(weight: int, center: int) -> int: + return (-1) ** center * (2 * (weight - center) ** 2 - 5) + + +def layer_weights(dimension: int) -> tuple[int, ...]: + if type(dimension) is not int or not 1 <= dimension <= 512: + raise ValueError("dimension must be an integer from 1 through 512") + return tuple(comb(dimension, t) * 3 ** (dimension - t) + for t in range(dimension + 1)) + + +def check_agreement(center: int, offset: int = 5, divisor: int = 3) -> None: + actual = tuple(t for t in range(4 * center + 1) + if (-1) ** center * (2 * (t - center) ** 2 - offset) + == divisor * (-1) ** t) + expected = (center - 2, center - 1, center + 1, center + 2) + require(actual == expected, "four-layer equality set changed") + + +def row_distribution(dimension: int) -> tuple[int, ...]: + """Count by row weight and overlap, independently of the four-symbol formula.""" + counts = [0] * (dimension + 1) + for row_weight in range(dimension + 1): + rows = comb(dimension, row_weight) + for overlap in range(row_weight + 1): + counts[overlap] += rows * comb(row_weight, overlap) * 2 ** ( + dimension - row_weight) + return tuple(counts) + + +def check_comparison() -> dict[str, object]: + for center in range(4, 129): + dimension = 4 * center + weights = layer_weights(dimension) + check_agreement(center) + require(sum(weights) == 4 ** dimension, "pair count does not close") + triples = tuple(sum(weights[s:s + 3]) for s in range(dimension - 1)) + best = sum(weights[center - 1:center + 2]) + require(triples.index(max(triples)) == center - 1, "wrong best triple") + require(triples.count(best) == 1, "best triple is not unique") + four = sum(weights[t] for t in (center - 2, center - 1, center + 1, center + 2)) + delta = four - best + polynomial = (27 * center ** 4 - 36 * center ** 3 - 171 * center ** 2 + - 128 * center - 12) + denominator = 3 * (center + 1) * (center + 2) * (3 * center + 1) * (3 * center + 2) + require(delta * denominator == weights[center] * polynomial, + "closed gain formula changed") + shift = center - 4 + positive = 27 * shift ** 4 + 396 * shift ** 3 + 1989 * shift ** 2 + 3688 * shift + 1348 + require(polynomial == positive and positive > 0, "positive shift failed") + weights = layer_weights(16) + four = sum(weights[t] for t in (2, 3, 5, 6)) + best = sum(weights[3:6]) + require((four, best, four - best) == (2713419648, 2633821596, 79598052), + "dimension-16 instance changed") + return {"dimensions": 125, "n16_rank": 137, "n16_four": four, + "n16_best_consecutive": best, "n16_gain": four - best} + + +def check_counts() -> int: + cases = 0 + for dimension in (4, 8, 12, 16, 20, 32, 40, 64): + require(row_distribution(dimension) == layer_weights(dimension), + "row enumeration disagrees with pair-layer formula") + cases += 1 + for dimension in (4, 8): + counts = [0] * (dimension + 1) + for x in range(1 << dimension): + for y in range(1 << dimension): + counts[(x & y).bit_count()] += 1 + require(tuple(counts) == layer_weights(dimension), "dense pair count failed") + cases += 1 + return cases + + +def features(dimension: int) -> tuple[int, ...]: + singles = tuple(1 << i for i in range(dimension)) + return (0,) + singles + tuple(a | b for a, b in combinations(singles, 2)) + + +def factor_value(x: int, y: int, masks: tuple[int, ...], coeff: tuple[int, int, int]) -> int: + return sum(coeff[mask.bit_count()] for mask in masks if (x & y) & mask == mask) + + +def check_factorization(coeff: tuple[int, int, int], center: int) -> int: + entries = 0 + for dimension in range(1, 7): + masks = features(dimension) + for x in range(1 << dimension): + for y in range(1 << dimension): + require(factor_value(x, y, masks, coeff) == numerator((x & y).bit_count(), center), + "rank factorization disagrees with the literal polynomial") + entries += 1 + return entries + + +def check_feature_rank() -> int: + cases = 0 + for dimension in range(1, 9): + masks = features(dimension) + require(len(masks) == 1 + dimension + comb(dimension, 2), "feature count failed") + for row, source in enumerate(masks): + for column, target in enumerate(masks): + zeta = int(source & target == target) + require(not zeta or column <= row, "feature minor is not triangular") + inverse_product = sum( + (-1) ** (middle.bit_count() - target.bit_count()) + for middle in masks + if source & middle == middle and middle & target == target) + require(inverse_product == int(row == column), "feature inverse failed") + for center in (4, 5): + require(all(coefficients(center)), "a feature coefficient vanished") + cases += 1 + return cases + + +def expect_rejection(function, *arguments) -> None: + try: + function(*arguments) + except (VerificationError, ValueError): + return + raise VerificationError("a deliberate mutation was accepted") + + +def check_controls() -> int: + for offset, divisor in ((4, 3), (6, 3), (5, 2), (5, 4)): + expect_rejection(check_agreement, 4, offset, divisor) + for coeff in ((26, -14, 4), (28, -13, 4), (27, -14, 2)): + expect_rejection(check_factorization, coeff, 4) + for invalid in (0, -1, 129, True): + expect_rejection(coefficients, invalid) + for invalid in (0, -1, 513, True): + expect_rejection(layer_weights, invalid) + for center in (2, 3): + weights = layer_weights(4 * center) + four = sum(weights[t] for t in (center - 2, center - 1, center + 1, center + 2)) + require(four < max(sum(weights[s:s + 3]) for s in range(4 * center - 1)), + "excluded small-dimension comparison changed") + weights = layer_weights(40) + four = sum(weights[t] for t in (8, 9, 11, 12)) + require(four < sum(weights[::2]), "constant-rank limitation control failed") + return 18 + + +def main() -> None: + result = check_comparison() + result["count_cases"] = check_counts() + result["factor_entries"] = sum(check_factorization(coefficients(m), m) for m in (4, 5)) + result["feature_rank_cases"] = check_feature_rank() + result["controls"] = check_controls() + package = Path(__file__).resolve().parent + names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + result["source_sha256"] = {name: sha256((package / name).read_bytes()).hexdigest() + for name in names} + result["claim_type"] = "scoped proof with exact finite corroboration" + print(json.dumps(result, sort_keys=True)) + print("PASS_FOUR_LAYER_QUADRATIC_PARITY") + + +if __name__ == "__main__": + main()