Separate the shared-row sum from the operator 2-norm (no new κ)

research/gaussian-operator-lift/README.md

@@ -0,0 +1,124 @@
+# The shared-row sum does not lift to the operator 2-norm
+
+**Claim type:** a separation between a row sum and an operator norm.
+**No new κ.** The ideal-gap gauges stay hypotheses. The selected record
+remains `23/10000`.
+
+## Question
+
+#4512 adds two section errors on the shared global row and asks whether
+that sum lifts to `||B - C||_2 < 2 ε`, with `ε = p^6 exp(-p^2)`. The named
+step is to decide whether the two operators in the polynomial split are
+these two section inverses, and whether their polynomials agree off the
+matched rows.
+
+## Lemma
+
+They are not the same hypothesis.
+
+1. **One polynomial, in the norm of the whole object.** #4490 states that
+   the pair of inverses `(B, C)` meets `||B - C|| < 2 ε` once both are
+   within `ε` of the same polynomial. #4509 repeats that sentence at
+   ceiling `9 p^2`. The norm is the norm of `B - C`, not the norm of one
+   row.
+
+2. **Two polynomials, identified only on rows at distance `A`.** #4491
+   gives `||P - H_sec^{-1}||_2 < ε` for each section that meets the #4452
+   gauge, and it says the core row is a row of that operator. HALO's exact
+   sentence applies to any row at distance `A = ceil(p^{48})` from a
+   section boundary. It does not identify the section polynomial with the
+   global polynomial on the other rows.
+
+3. **A small row does not bound the operator 2-norm.** Let
+
+```text
+M = [ 3  0 ]
+    [ 0  9 ].
+```
+
+The first row has squared Euclidean length `3^2 = 9`, and `9 < 8^2`.
+The second standard basis vector is sent to `(0, 9)`, whose squared
+length is `81`, and `81 > 8^2`. Since `||M||_2 ≥ ||M e_2||_2`, the
+operator 2-norm is not strictly below 8. The shared-row sum can hold
+while `||B - C||_2 < 2 ε` fails.
+
+4. **A zero row does not force the operators to agree.** The matrix with
+   rows `(0, 0)` and `(0, 2)` has first-row squared length 0 and sends
+   `e_2` to a vector of squared length 4. Row agreement does not give
+   `||P_B - P_C||_2 = 0`. The triangle then keeps an extra term. The
+   integer upper bound `3 + 2 + 3 = 8` is not strictly below `2 · 4`.
+
+The locality audit already says some row at distance exactly `(2J - 1) W`
+differs from the global row, and it bounds a core row of the inverse
+difference by `2 p^{10} exp(-p^2)`. That is a different split. It is not
+this operator comparison.
+
+## Proof
+
+The bridge identity is `B - C = (B - P) + (P - C)` for one polynomial `P`
+in one normed space. Substituting two section polynomials produces
+
+```text
+B - C = (B - P_B) + (P_B - P_C) + (P_C - C).
+```
+
+#4491 bounds the first and third terms in the operator 2-norm only under
+the two gauges, and only against each section's own polynomial. HALO
+removes `P_B - P_C` on a row at distance `A`. The displayed matrix shows
+that removing it on one row does not remove it from `||·||_2`. Comparing
+squared lengths avoids a square root: both vectors are integer, and the
+Euclidean norm is strictly smaller exactly when the squared length is
+strictly smaller.
+
+This package does not assert that the Gaussian section polynomials differ
+by the displayed matrix. It asserts that the rows inherited from #4491 do
+not imply the operator hypothesis used by #4490 and #4509.
+
+## Not covered
+
+- A bound on `||P_sec - P_global||_2` off the rows at distance `A`.
+- Either ideal-gap hypothesis `1 - 1/(8 p^2)`.
+- The global-inverse summand `||P - H^{-1}||`.
+- Editing the #4100 notes. They still say `g p^{10 g} exp(-p^2)`.
+- Any new κ.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-operator-lift --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-operator-lift
+```
+
+Base `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, priority revision 7, selection
+refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T03:07:14Z and was
+that commit.
+
+Overlap snapshot: open PRs fetched 2026-10-22T03:09:20Z (299 records) and
+discussions fetched 2026-10-22T03:10:01Z (3390 records). A search for
+`operator 2-norm`, `shared global row` and `same polynomial` returned #4512,
+which asks this question, #4511, which still asks for one common polynomial,
+and #4490, which states that hypothesis. The other hits use "the same
+polynomial" for unrelated series. No result shows that a small row forces
+`||B - C||_2 < 2 ε`. A search miss is not a novelty certificate. #4490 is
+the one-polynomial triangle. #4491 is the operator section error. HALO is
+the distance-A row sentence.
+
+## Open next questions
+
+1. **Is `||P_sec - P_global||_2` bounded off the rows at distance `A`?**
+   The operator hypothesis needs one polynomial, and the matched rows do
+   not determine the difference. The first step is to use the locality
+   audit's sharp row at distance exactly `(2J - 1) W` as a witness that
+   equality can fail, then look for an upper bound. Do not reuse the
+   `2 p^{10}` inverse split as that bound.
+
+## Credit
+
+- The one-polynomial triangle is #4490's, repeated at ceiling 9 by #4509.
+- The operator section error and the core-row sentence are #4491's.
+- The shared-row sum that this package does not lift is #4512's.
+- The sharp row at distance `(2J - 1) W`, and the two-term `p^{10}` bound,
+  are the locality audit's.
+- The exact-row sentence at distance `A` is #4100's.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-operator-lift/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/gaussian-core-row/README.md",
+      "usage": "input",
+      "git_blob": "700035aa60ff1345dbb4dc7dd1c5a26b9eecc673",
+      "sha256": "e5f958c71589dfca1b287246f9af129fdf4da4f20c840e2ac20186ab95282b07"
+    },
+    {
+      "path": "research/gaussian-tensor-bridge/README.md",
+      "usage": "input",
+      "git_blob": "15b1447cba922c52c84d3b4266046bae4bbdb260",
+      "sha256": "40880289a092629c8ba0cdd7660c1ee553e0071cbe6f3e18e3c2e49cf37eb4d8"
+    },
+    {
+      "path": "research/halo-locality-witness-audit/README.md",
+      "usage": "input",
+      "git_blob": "03b244baf61b427edbccd29698a05583b5405dd6",
+      "sha256": "fc87657cb3e89a74b9462483cc15713f0122256a623fefa65c887e2118f81276"
+    },
+    {
+      "path": "research/unconditional-batched-crt/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    }
+  ]
+}

research/gaussian-operator-lift/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Decide whether the shared-row sum of two section errors lifts to the operator hypothesis ||B - C||_2 < 2 epsilon. Keep the same-polynomial hypothesis and the distance-A row restriction explicit.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only separates the shared-row sum from the operator 2-norm. It does not prove the ideal gaps, does not bound the polynomial difference, and does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the operator lift left open by the two core-row sum.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the row sum is separated from ||B - C||_2. Do not bound ||P_sec - P_global||_2, do not prove the ideal gaps, do not edit the #4100 notes, and do not claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-operator-lift",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the operator counterexample and the package text.",
+  "open_questions": [
+    {
+      "question": "Is the operator norm of the section polynomial minus the global polynomial bounded off the rows at distance A?",
+      "why_it_matters": "||B - C||_2 < 2 epsilon needs both section inverses within epsilon of one polynomial. The rows at distance A do not determine that operator difference.",
+      "first_step": "Use the locality audit's sharp row at distance exactly (2J-1)W as a witness that equality can fail, then look for an upper bound on the operator norm. Do not reuse the 2 p^10 inverse split as that bound.",
+      "blocked_by": "HALO identifies the section polynomial with the global polynomial only for rows at distance A, and each ideal-gap gauge remains a hypothesis."
+    }
+  ]
+}

research/gaussian-operator-lift/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/gaussian-core-row/README.md",
+    "research/gaussian-tensor-bridge/README.md",
+    "research/halo-locality-witness-audit/README.md",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "A shared row with squared length 9 is strictly below 8^2, while the same matrix sends e_2 to a vector of squared length 81. A zero row does not force the operator 2-norm to vanish. The bridge asks for one polynomial in that operator norm, and HALO's exact row is only at distance A."
+    }
+  ]
+}

research/gaussian-operator-lift/verify.py

@@ -0,0 +1,80 @@
+#!/usr/bin/env python3
+"""Separate a shared-row sum from the operator 2-norm.
+
+Every comparison is an integer identity. The ideal-gap gauges stay hypotheses.
+"""
+
+from __future__ import annotations
+
+import hashlib
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PACKAGE = ROOT / "research" / "gaussian-operator-lift"
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def pins_and_phrases() -> None:
+    sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8"))
+    for row in sources["files"]:
+        if row["usage"] == "input":
+            assert digest(ROOT / row["path"]) == row["sha256"], row["path"]
+    halo = (ROOT / "research/unconditional-batched-crt/HALO.md").read_text(encoding="utf-8")
+    core = (ROOT / "research/gaussian-core-row/README.md").read_text(encoding="utf-8")
+    bridge = (ROOT / "research/gaussian-tensor-bridge/README.md").read_text(encoding="utf-8")
+    audit = (ROOT / "research/halo-locality-witness-audit/README.md").read_text(encoding="utf-8")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    assert "For any row at distance A=ceil(p^48) from a section" in halo
+    assert "EXACTLY the corresponding row of the global P_i" in halo
+    assert "||P - H_sec^{-1}||_2 < p^6 exp(-p^2)," in core
+    assert "and the core row is a row of that operator." in core
+    assert "meets `||B - C|| < 2 ε` once both are within `ε` of the" in bridge
+    assert "distance exactly (2J-1)W differs" in audit
+    assert "||H_sec^-1-P_sec|| + ||P-H^-1|| <= 2p^10 exp(-p^2)." in audit
+    assert selected["kappa"] == "23/10000"
+
+
+def apply_row(matrix: tuple[tuple[int, int], tuple[int, int]], vector: tuple[int, int]) -> tuple[int, int]:
+    return (
+        matrix[0][0] * vector[0] + matrix[0][1] * vector[1],
+        matrix[1][0] * vector[0] + matrix[1][1] * vector[1],
+    )
+
+
+def squared_length(vector: tuple[int, int]) -> int:
+    return vector[0] * vector[0] + vector[1] * vector[1]
+
+
+def operator_gap() -> None:
+    # The first row is strictly below the two-error cap. The operator is not.
+    small_row = ((3, 0), (0, 9))
+    assert squared_length(small_row[0]) == 3 * 3
+    assert 3 * 3 < 8 * 8
+    image = apply_row(small_row, (0, 1))
+    assert image == (0, 9)
+    assert squared_length(image) == 9 * 9
+    assert 9 * 9 > 8 * 8
+    # A zero row does not force the operator difference to vanish.
+    zero_row = ((0, 0), (0, 2))
+    assert squared_length(zero_row[0]) == 0
+    assert squared_length(apply_row(zero_row, (0, 1))) == 2 * 2
+    assert 2 * 2 > 0
+    # An upper bound that meets twice the cap is not a strict operator bound.
+    assert 3 + 2 + 3 == 8
+    assert not (8 < 2 * 4)
+
+
+def main() -> None:
+    pins_and_phrases()
+    operator_gap()
+    print("PASS_GAUSSIAN_OPERATOR_LIFT")
+
+
+if __name__ == "__main__":
+    main()