Add the two core-row section errors (no new κ)

research/gaussian-second-row/README.md

@@ -0,0 +1,108 @@
+# Two core rows add their section errors
+
+**Claim type:** a second application of the core-row reading, then a sum.
+**No new κ.** Both ideal-gap gauges stay hypotheses. The selected record
+remains `23/10000`.
+
+## Question
+
+#4511 asks whether a second core row supplies `||C - P|| < ε` for another
+section inverse against the same global polynomial, and then whether the two
+errors add. Here `ε = p^6 exp(-p^2)`.
+
+## Lemma
+
+Let `p ≥ 2` be an integer and let `A = ceil(p^{48})`. Take two outputs, each
+kept at distance `A` from every face. The distance comparison in #4491 does
+not name which output is chosen, so it applies to both: `R < p^{26} < A`.
+
+For each output, #4491 gives two sentences:
+
+1. **Row identity, with no gauge.** The section-polynomial row is the global
+   polynomial row.
+2. **One section error, under that section's own #4452 gauge.** Then
+   `||P - H_sec^{-1}||_2 < ε`, and the core row is a row of that operator.
+
+On those two matched rows the section polynomials equal the same global
+polynomial row, so the polynomial cross term is zero there. Write `B` and
+`C` for the two section inverses. The row difference splits as
+
+```text
+row(B) - row(C) = (row(B) - row(P)) + (row(P) - row(C)).
+```
+
+Each parenthesis is one section error. Two positive integers strictly below
+4, namely 3 and 3, sum to 6, and `6 < 2 * 4`. Two strict errors therefore
+add to a strict two-error bound on that shared row.
+
+A polynomial gap of 2 between the rows spends the room: `3 + 2 + 3 = 8`,
+and 8 is not strictly below 8. The row identity is what removes that gap.
+One error alone is 3, which is not the two-error sum 6.
+
+## Proof
+
+#4491 proves `R < p^{26} < p^{48} = A` for every integer `p ≥ 2` and every
+admissible bandwidth `W`. Nothing in that comparison depends on a row index,
+so the second output clears the same radius. HALO's sentence that a row at
+distance `A` equals the corresponding row of the global polynomial therefore
+applies to each output. Where both rows equal that global row, they equal
+each other, and the cross term in the split above is zero.
+
+Each operator sentence remains conditional on its own section meeting the
+#4452 gauge. One section's gauge does not cover the other section. This
+package does not re-prove either sentence. It only adds the two errors
+after both readings are granted.
+
+The integer shadow uses a cap of 4 and two errors of 3. Their sum is
+strictly below twice the cap. Inserting a gap of 2 makes the sum equal
+twice the cap, so the strict bound fails. The same arithmetic shows that
+dropping either error leaves a quantity other than the two-error sum.
+
+## Not covered
+
+- Either ideal-gap hypothesis `1 - 1/(8 p^2)`.
+- The operator norm `||B - C||_2` of the two section inverses. Off the
+  matched rows the section polynomials need not agree.
+- The global-inverse summand `||P - H^{-1}||` on the same row. #4491 leaves
+  that summand open.
+- 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-second-row --check-only
+python3.12 -B scripts/research_package.py --package research/gaussian-second-row
+```
+
+Base `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`, priority revision 7, selection
+refresh κ = `23/10000`. Upstream was fetched at 2026-10-22T03:04:25Z and was
+that commit.
+
+Overlap snapshot: open PRs fetched 2026-10-22T03:04:33Z (297 records) and
+discussions fetched 2026-10-22T03:05:16Z (3385 records). A search for
+`second core row`, `second section inverse` and `two core rows` returned
+#4511, which asks this question. A search for `both pieces are strictly
+below` returned the ceiling-10 split and the ceiling-9 split. Both leave
+the two section errors as hypotheses. A search miss is not a novelty
+certificate. #4491 is the reading applied twice. HALO is the row sentence.
+
+## Open next questions
+
+1. **Does the shared-row sum lift to `||B - C||_2 < 2 ε`?** The sum above
+   holds where both section polynomials equal the same global row. #4509
+   uses the two-error bound as an operator norm. The first step is to
+   decide whether those two operators are these section inverses, and
+   whether their polynomials agree off the matched rows.
+
+## Credit
+
+- The row identity and each section error are #4491's, applied once to
+  each output.
+- The triangle shape is #4509's. This package supplies the two row errors
+  that triangle was missing.
+- The question is #4511's.
+- The core distance and the exact-row sentence are #4100's.
+- The locality audit's two `p^{10}` errors are a different bound.
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. Apache-2.0.

research/gaussian-second-row/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/unconditional-batched-crt/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    }
+  ]
+}

research/gaussian-second-row/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": "Apply the #4491 core-row reading to a second output at distance ceil(p^48) and add the two section errors on the shared global row, keeping both ideal-gap gauges explicit.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This package only adds the two inherited section errors on the matched rows. It does not prove the ideal gaps, does not lift the sum to an operator norm, and does not claim a new kappa.",
+  "bottleneck_link": "The selected frontier is unchanged. This is the second section error left open by the one-row attribution.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the two core-row errors are added on the shared global row. Do not prove the ideal gaps, do not lift the sum to ||B - C||_2, 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-second-row",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the two-row sum and the package text.",
+  "open_questions": [
+    {
+      "question": "Does the shared-row sum lift to the operator hypothesis ||B - C||_2 < 2 epsilon?",
+      "why_it_matters": "Two core rows add to a strict two-error bound only where both section polynomials equal the same global row. #4509 uses that bound as an operator norm.",
+      "first_step": "Decide whether the two operators in that split are these two section inverses, and whether their section polynomials agree off the matched rows.",
+      "blocked_by": "Each section still needs its own ideal-gap gauge, and the polynomials are identified only on the core rows."
+    }
+  ]
+}

research/gaussian-second-row/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/gaussian-core-row/README.md",
+    "research/unconditional-batched-crt/HALO.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same distance A clears p^26 for a second core output. Under a separate #4452 gauge for each section, the two section errors add on the shared global row: 3 + 3 = 6 < 2 * 4. A polynomial gap of 2 makes 3 + 2 + 3 = 8, which is not strictly below 8."
+    }
+  ]
+}

research/gaussian-second-row/verify.py

@@ -0,0 +1,64 @@
+#!/usr/bin/env python3
+"""Add two core-row section errors on the shared global row.
+
+Every comparison is an integer identity. Both 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-second-row"
+
+
+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")
+    selected = json.loads(
+        (ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")
+    )
+    assert "A=ceil(p^48)" in halo
+    assert "EXACTLY the corresponding row of the global P_i" in halo
+    assert "Keep outputs at distance A" in halo
+    assert "Its section-polynomial row is the global polynomial row." in core
+    assert "meets the #4452 gauge" in core
+    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 "The global-inverse summand" in core
+    assert selected["kappa"] == "23/10000"
+
+
+def two_rows() -> None:
+    # The distance comparison does not name a row, so a second output uses it too.
+    assert 48 - 26 == 22
+    assert 2**22 > 1
+    # On the shared global row the cross term is zero, and two strict errors add.
+    assert (8 - 5) == (8 - 6) + (6 - 5)
+    assert 3 + 3 == 6
+    assert 6 < 2 * 4
+    # A polynomial gap of 2 spends the strict room.
+    assert 3 + 2 + 3 == 8
+    assert not (8 < 2 * 4)
+    # One error is not the two-error sum.
+    assert 3 != 6
+
+
+def main() -> None:
+    pins_and_phrases()
+    two_rows()
+    print("PASS_GAUSSIAN_SECOND_ROW")
+
+
+if __name__ == "__main__":
+    main()