Prove a fixed positive-metric Gram box obstruction (no new κ)

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.

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"
+    }
+  ]
+}

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"
+  }
+}

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."
+    }
+  ]
+}