diff --git a/research/weighted-gram-box/README.md b/research/weighted-gram-box/README.md new file mode 100644 index 0000000000..9fe7ee1ac1 --- /dev/null +++ b/research/weighted-gram-box/README.md @@ -0,0 +1,173 @@ +# A positive diagonal metric can destroy a full rational anchor box + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped exact obstruction.** There is a rational three-column weighted Gram +factorization `M=P D P^T`, with the fixed positive definite metric +`D=diag(1,3,1)`, four rows, nonzero diagonal and matched nonempty canonical +anchors, whose retained directed anchor box is exactly **three**. + +Sagar Thakrar's [#3612](https://github.com/CrocSwap/integer-mult-bounds/pull/3612) +proves full boxes for rational factors `P P^T`, and already gives an asymmetric +four-row matched-anchor obstruction. The new restriction here is `Q=P D` +for one positive diagonal metric. Thus a positive metric and matched anchors +together still do not extend the full-box theorem. This answers one concrete +higher-valuation boundary question from that package. It does not settle its +unrestricted asymmetric question or the F-star conjecture. + +## Construction and proof + +Use zero-based row indices and coordinate masks `1,2,4`. Put + +```text +P = [(1, 1, 0), (3, -1, 2), (3, -1, -6), (1, 0, 1)] +D = diag(1, 3, 1) +Q = P D = [(1, 3, 0), (3, -3, 2), (3, -3, -6), (1, 0, 1)] + +M = P Q^T = [ 4 0 0 1 ] + [ 0 16 0 5 ] + [ 0 0 48 -3 ] + [ 1 5 -3 2 ] +``` + +The metric is positive definite, so `M` is positive semidefinite. Its rank +is exactly three: the factorization gives an upper bound of three, and the +principal minor on rows `0,1,2` has determinant `4*16*48=3072`. + +For completeness, the retained canonical normalization from #3612 is as +follows. Delete any factor column that contributes identically zero. Let +`m_j=min_i v2(P_ij)`, `n_j=min_i v2(Q_ij)`, and +`gamma=min_j(m_j+n_j)`, ignoring zero entries in the minima. Normalize +`p_ij=2^(-m_j) P_ij` and `q_ij=2^(m_j-gamma) Q_ij`. The canonical anchors +`A_i,B_i` are their odd-coordinate supports, and the tied set is their +intersection. All column minima in this example are zero, so + +```text +A = B = (3, 3, 3, 5), gamma = 0. +``` + +Every tied set has two coordinates. The normalized diagonal valuations are +`(2,4,4,1)`. In particular the first three rows are outside #3612's sufficient +matched-row condition `v2(M_ii)=gamma+1`. + +A retained box consists of distinct kept rows, an order, and labels +`a_i subset A_i`, `b_i subset B_i`, with binary dot product +`a_i dot b_i=1`. For each earlier row `i` and later row `j`, the only +additional requirement is `M_ij=0 => a_i dot b_j=0`. + +Suppose a full four-row box existed. Restrict its order and labels to rows +`0,1,2`. Every off-diagonal scalar entry on that triple is zero. Its binary +label-dot matrix therefore has zero entries above the diagonal and ones +on the diagonal, and has rank three over F2. But all those source and target +labels lie in the same two-coordinate plane, so that matrix has rank at +most two. This contradiction proves `box<=3`, for every order and label. + +Rows `(0,1,3)` in that order with labels +`(a,b)=((1,1),(2,2),(1,1))` give a three-row witness. The only forward scalar +zero between those rows is `M_01=0`, and its labels are orthogonal. All +supports and diagonal parities hold. Hence **box=3**. + +This matrix cannot be reinterpreted as `R R^T` with rational `R` having +three columns: the displayed principal minor would then be the square of +a rational determinant, whereas `3072=3*32^2` is not a rational square. +Allowing more columns changes the three-total contract. Positivity alone +therefore does not recover the predecessor's hypothesis. + +## Exact corroboration + +The self-contained verifier recomputes `Q`, every matrix entry, canonical +anchors, the rank-three minor and the explicit witness. A separate exhaustive +pass through the definition enumerates every ordered subset and every +supported self-certifying label assignment. Each row has six label pairs. +The assignment counts include different orders and labels on the same subset; +they are not counts of distinct subsets or distinct boxes. + +| Kept rows | Assignments examined | Admissible assignments | +|---|---:|---:| +| 0 | 1 | 1 | +| 1 | 24 | 24 | +| 2 | 432 | 288 | +| 3 | 5,184 | 1,296 | +| 4 | 31,104 | 0 | + +Ten control groups cover the metric, shape, support, diagonal parity, +zero entries, distinct rows and directed order. All 125 dual column +rescalings with exponents in `{-2,-1,0,1,2}^3` preserve the recomputed matrix +and anchors. These are controls on this fixed example, not a broader metric +classification. Every check uses explicit exceptions and remains active under +`-O`. The verifier writes no files and emits a generated receipt bound to +SHA256 hashes of all five package files. There is no handwritten receipt. + +From the worktree root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/weighted-gram-box/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/weighted-gram-box/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/weighted-gram-box +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/weighted-gram-box --check-source-history +``` + +Another CPython 3.12 interpreter may replace that local path. The expected +markers are `PASS_WEIGHTED_GRAM_BOX`, `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_RESEARCH_COMMIT_BYTES`. Source documents are provenance only; no +predecessor executable is imported or replayed. + +## Scope, overlap and credit + +The claim is the written proof for this exact rational factorization. It is +also an exact finite counterexample to the stated positive-metric extension. +It is not a multiplication theorem, a physical decoder or a new kappa. +Native implementation, COPY pricing, frames, owners, dirty restoration, +precision, tape costs and supplier admission remain outside scope. Independent +human and formal proof-kernel review are unclaimed. Lean, Docker and the +selected supplier's operator replay were not run. + +The historical `complex-rank-shape-decoder` card is explicitly changed to +this algebraic side result. No complete paid-profile gain is claimed. Entry +orientation used the current selected-binding positive control. The source +first example and existing asymmetric obstruction in #3612 were read as +premises and motivation, without running its verifier. The new metric is the +changed premise; no family implementation expansion is proposed. + +Scientific base is `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision +7. The advance [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144846) +records the target. Live open PRs, recent account work, handoffs, local +reservations, distinctive main README and merged-PR searches were checked. +The entry overlap helper covered 331 open PRs and 4,340 Discussion records +with complete pagination. Sparse local notes were incomplete. Neither +coverage nor a no-match search proves absence of unpublished overlap. + +Credit Sagar Thakrar #3612 for the rational Gram theorem, the modulo-four +matched-row condition, the earlier asymmetric matched-anchor obstruction and +the open boundary question. Credit Aaron Wang/navinor #2914/#2978/#3031 for +the directed sub-anchor framework, asymmetric obstruction and valuation +lineage; DreamingOfClouds #1590/#2111 for the F-star/certificate lineage; and +the #3409/#3420/#3445 labeling predecessors retained by #3612. The binary +triangular-rank obstruction is inherited, not a new general method. The new +artifact is its explicit fixed-positive-metric realization. Predecessor +credit and source files are unchanged. + +## Open next questions + +Which positive rational diagonal metrics have the universal full-box property +for all rational three-column factors with nonempty canonical ties? Start +with `diag(1,d,1)`, distinguishing rational square classes and recomputing the +original canonical anchors. This example excludes `d=3`; it does not provide +a classification. The blocker is a uniform metric-sensitive invariant, rather +than another replay of this four-row example. + +## Implementation bounds + +Power of Ten inspection is confined to `verify.py`. Control flow is +nonrecursive, functions are below 60 lines, inputs have at most four rows and +three columns, rational input integers have at most 32 bits, and rescaling +exponents are bounded. The oracle's loops have an explicit bound +`sum_{k=0}^4 4!/(4-k)! * 28^k`; the actual fixture has six choices per row. +State is local apart from immutable fixture constants. Source files have +scoped reads and failures propagate. There is no generated code or dynamic +import. Rule 3 has a managed-runtime deviation: Python/Fraction allocate +within these fixed bounds during this finite command. Revisit fixed storage +before admitting unbounded input or using it in a steady service. Rule 10 +uses warning-strict normal/optimized execution and in-memory compilation. +External Python linters were unavailable locally; no repository-wide analyzer +configuration is changed. The registered timeout is 120 seconds per mode. diff --git a/research/weighted-gram-box/SOURCES.json b/research/weighted-gram-box/SOURCES.json new file mode 100644 index 0000000000..59926d0d67 --- /dev/null +++ b/research/weighted-gram-box/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/fstar-gram-full-box/PROOF.md", + "usage": "provenance", + "git_blob": "2fd06f16a0d3f1574be67f813b63e6e3511d0f12", + "sha256": "2c8bc3f6366623df140aab302013e563dd48f86c39261e6092160e0999ef0c80" + }, + { + "path": "research/fstar-gram-full-box/README.md", + "usage": "provenance", + "git_blob": "e18bb0811076001f9b7ad5d2452d44b9e1707e98", + "sha256": "f56831e403f632cf898dbbd74b10daa396f49e9b88d05f450dac4d034c5e3ce1" + } + ] +} diff --git a/research/weighted-gram-box/TASK.json b/research/weighted-gram-box/TASK.json new file mode 100644 index 0000000000..2bca48bbb3 --- /dev/null +++ b/research/weighted-gram-box/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact four-row positive-diagonal weighted-Gram counterexample to full canonical anchor-box retention.", + "scope_change_reason": "Take the higher-valuation boundary question of Sagar Thakrar PR3612 instead of seeking a complete paid decoder profile. The new premise is Q=P diag(1,3,1).", + "bottleneck_link": "Algebraic decoder side result: a positive metric and matched anchors do not justify extending the Gram full-retention theorem; native paid-profile improvement is not claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact counterexample with a proved upper bound and an attaining literal witness.", + "outcome": "completed", + "evidence": "README.md proof; verify.py exact matrix/normalization, 36,745 complete ordered label assignments, explicit witness, ten controls and 125 dual rescalings.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which positive rational diagonal metrics have universal full anchor-box retention for rational three-column weighted Gram factors?", + "why_it_matters": "Separates legitimate metric extensions from higher-valuation matched-anchor obstructions.", + "first_step": "Study diag(1,d,1) by rational square class with the original canonical normalization.", + "blocked_by": "A uniform metric-sensitive invariant is missing; this example only excludes d=3." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/weighted-gram-box/VERIFY.json b/research/weighted-gram-box/VERIFY.json new file mode 100644 index 0000000000..6bd6575c3f --- /dev/null +++ b/research/weighted-gram-box/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact fixed metric obstruction, exhaustive ordered label assignments, witness and failure controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact obligations under Python optimization." + } + ] +} diff --git a/research/weighted-gram-box/verify.py b/research/weighted-gram-box/verify.py new file mode 100644 index 0000000000..4895cce2af --- /dev/null +++ b/research/weighted-gram-box/verify.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Exact, read-only corroboration of the fixed weighted-Gram obstruction.""" +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + +P = ((1, 1, 0), (3, -1, 2), (3, -1, -6), (1, 0, 1)) +D = (1, 3, 1) +EXPECTED = ((4, 0, 0, 1), (0, 16, 0, 5), + (0, 0, 48, -3), (1, 5, -3, 2)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def shape(rows): + need(1 <= len(rows) <= 4, "one to four rows required") + need(all(len(row) == 3 for row in rows), "three columns required") + for row in rows: + for value in row: + need(type(value) in (int, Fraction), "exact rational required") + value = Fraction(value) + need(max(abs(value.numerator).bit_length(), + value.denominator.bit_length()) <= 32, "input capacity") + + +def valuation(value): + value = Fraction(value) + need(value != 0, "zero has no finite valuation") + a, b = abs(value.numerator), value.denominator + return (a & -a).bit_length() - (b & -b).bit_length() + + +def two_power(exponent): + need(-128 <= exponent <= 128, "exponent capacity") + return Fraction(2 ** max(0, exponent), 2 ** max(0, -exponent)) + + +def anchors(left, right): + shape(left) + shape(right) + need(len(left) == len(right), "factor row mismatch") + active = tuple(j for j in range(3) + if any(row[j] for row in left) + and any(row[j] for row in right)) + need(bool(active), "no active column") + m = {j: min(valuation(row[j]) for row in left if row[j]) for j in active} + n = {j: min(valuation(row[j]) for row in right if row[j]) for j in active} + gamma = min(m[j] + n[j] for j in active) + a = tuple(sum(1 << j for j in active if row[j] + and valuation(row[j]) - m[j] == 0) for row in left) + b = tuple(sum(1 << j for j in active if row[j] + and valuation(row[j]) + m[j] - gamma == 0) for row in right) + return a, b, gamma + + +def matrix(left, right): + shape(left) + shape(right) + need(len(left) == len(right), "factor row mismatch") + return tuple(tuple(sum(Fraction(x) * y for x, y in zip(p, q)) + for q in right) for p in left) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def accepts(m, a, b, order, labels): + size = len(m) + if len(order) != len(labels) or len(set(order)) != len(order): + return False + if any(type(i) is not int or not 0 <= i < size for i in order): + return False + for i, (x, y) in zip(order, labels): + if not 1 <= x < 8 or not 1 <= y < 8: + return False + if x & ~a[i] or y & ~b[i] or dot(x, y) != 1: + return False + return all(m[i][j] != 0 or dot(labels[u][0], labels[v][1]) == 0 + for u, i in enumerate(order) + for v, j in enumerate(order) if u < v) + + +def enumerate_boxes(m, a, b): + size = len(m) + need(1 <= size <= 4 and len(a) == len(b) == size, "oracle capacity") + need(all(m[i][i] != 0 for i in range(size)), "nonzero diagonal required") + choices = tuple(tuple((x, y) for x in range(1, 8) for y in range(1, 8) + if not x & ~a[i] and not y & ~b[i] and dot(x, y)) + for i in range(size)) + tested, valid = [0] * (size + 1), [0] * (size + 1) + # At most sum_{k=0}^4 (4!/(4-k)!) * 28^k assignments. + for k in range(size + 1): + for order in permutations(range(size), k): + for labels in product(*(choices[i] for i in order)): + tested[k] += 1 + if accepts(m, a, b, order, labels): + valid[k] += 1 + return tested, valid + + +def check_result(left, weights): + shape(left) + need(len(weights) == 3 and all(x > 0 for x in weights), "positive metric") + right = tuple(tuple(x * d for x, d in zip(row, weights)) for row in left) + m = matrix(left, right) + need(m == EXPECTED, "weighted matrix mismatch") + a, b, gamma = anchors(left, right) + need((a, b, gamma) == ((3, 3, 3, 5), (3, 3, 3, 5), 0), "anchor mismatch") + need(all(m[i][j] == 0 for i in range(3) for j in range(3) if i != j), + "principal triple must be mutually zero") + need(m[0][0] * m[1][1] * m[2][2] == 3072, "rank-three minor mismatch") + need(accepts(m, a, b, (0, 1, 3), ((1, 1), (2, 2), (1, 1))), + "attaining witness rejected") + return right, m, a, b + + +def expect_rejection(operation, message): + try: + operation() + except ValueError: + return + raise ValueError(message) + + +def controls(right, m, a, b): + expect_rejection(lambda: check_result(P, (1, 1, 1)), "unweighted mutation") + expect_rejection(lambda: check_result(P, (1, -3, 1)), "negative metric") + expect_rejection(lambda: anchors(P, right[:-1]), "factor shape") + need(not accepts(m, a, b, (0, 0), ((1, 1), (1, 1))), "duplicate row") + need(not accepts(m, a, b, (0,), ((4, 4),)), "unsupported label") + need(not accepts(m, a, b, (0,), ((1, 2),)), "diagonal parity") + need(not accepts(m, a, b, (0, 1), ((1, 1), (1, 1))), "zero constraint") + dm = ((1, 0), (1, 1)) + need(not accepts(dm, (1, 1), (1, 1), (0, 1), ((1, 1), (1, 1))), + "directed zero not checked") + need(accepts(dm, (1, 1), (1, 1), (1, 0), ((1, 1), (1, 1))), + "reverse direction incorrectly constrained") + expect_rejection(lambda: enumerate_boxes(((0,),), (1,), (1,)), + "zero diagonal accepted") + for exponents in product(range(-2, 3), repeat=3): + lp = tuple(tuple(x * two_power(e) for x, e in zip(row, exponents)) + for row in P) + rq = tuple(tuple(x / two_power(e) for x, e in zip(row, exponents)) + for row in right) + need(matrix(lp, rq) == m, "dual rescaling changed matrix") + need(anchors(lp, rq) == (a, b, 0), "canonical rescaling failed") + return 10, 125 + + +def receipt(payload): + root = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + payload["file_sha256"] = {name: sha256((root / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(payload, sort_keys=True)) + + +def main(): + right, m, a, b = check_result(P, D) + tested, valid = enumerate_boxes(m, a, b) + need(tested == [1, 24, 432, 5184, 31104], "enumeration coverage") + need(valid == [1, 24, 288, 1296, 0], "admissible assignment counts") + groups, rescalings = controls(right, m, a, b) + receipt({"status": "PASS_WEIGHTED_GRAM_BOX", "box": 3, "rows": 4, + "tested_by_size": tested, "valid_by_size": valid, + "controls": groups, "dual_rescalings": rescalings, + "claim_type": "scoped proof with finite exact corroboration"}) + + +if __name__ == "__main__": + main()