The written p^10 guards still cover the column-gap 2-norm ceiling (no new κ)

research/gaussian-twonorm-guard/README.md

@@ -0,0 +1,103 @@
+# The written p^10 guards do not move
+
+**Scoped ledger comparison for #4100's narrow inverse 2-norm. No new κ.**
+This decides open question 2 of #4402. It does not prove a column gap for
+`GAUSSIAN.md`'s rounded reference `H`.
+
+## Question
+
+`INVERSE-CONDITIONING.md` bounds the inverse 2-norm by
+
+```text
+sqrt((1/delta)(1/delta + 2 b rho/delta^2)).
+```
+
+#4402 replaces that, inside one phase run, by `1/sqrt(delta delta_col)`.
+Do any written precision guards in the #4100 notes change?
+
+## Callers and the exponents they write
+
+The search is the note directory `research/unconditional-batched-crt` on
+canonical main `12fa8c5c844be21bfefb38a19503fbd867a11244`. Older vendored
+copies of the fine-prime note are the same inherited statement, not a second
+ledger.
+
+| Note | Role | Exponents |
+| --- | --- | --- |
+| `INVERSE-CONDITIONING.md` | States the bandwidth formula. For this route it records `b < p` and `delta >= 1/(16p^2)`. | No separate power of `p`. |
+| `GAUSSIAN.md`, narrow paragraph | Applies the formula to `Haug` and its principal sections. | Both 2-norms `< p^10` eventually. |
+| `GAUSSIAN.md`, broad paragraph | Shifted-symbol bound. It does not use the bandwidth formula. | `< p^6`, with the `p^10` allowance called ample. |
+| `GAUSSIAN.md`, locality and normalizer | Repeats HALO's consequences and divides completed maps by a dyadic bound. | `p^-20`, `p^42`, `p^45`, error `p^10 exp(-p^2)`, `p^48`, `p^100`. |
+| `HALO.md` | Assumes both 2-norms are at most `p^10` and bandwidth `< p`. | Spectral interval `[p^-20, p^20]`, gap `p^-40`, `J = ceil(p^42)`, bandwidth `< p^45`, error `p^10 exp(-p^2)`, `A = ceil(p^48)`, core `L >= p^400`. |
+| `vendor/FINE-PRIME.md` §§4–5 | Inherited hypothesis `\|\|H\|\|_2, \|\|H^-1\|\|_2 <= p^10`. | `2^ceil(100 log2 p)`, the same halo exponents through `p^48`, and core exponent 128. |
+| `PROOF.md` | Uses the halo/core pair already chosen above. | Core exponent 400 and halo 48. It does not restate `p^10`. |
+| `AUDIT.md` | Names the conditioning notes. | No `p^10`. |
+
+## Comparison
+
+Take an integer `p >= 2`, bandwidth `b <= p - 1`, `delta >= 1/(16p^2)` and
+`rho = 1 - delta`. These are the floors the notes give the lemma. At that
+corner the squared bandwidth ceiling equals
+
+```text
+256 p^4 (1 + 2(p-1)(16p^2 - 1)).
+```
+
+The parenthesis expands as `32p^3 - 32p^2 - 2p + 3`, which is strictly below
+`32p^3`. The resulting square is strictly below `p^20`, so the 2-norm ceiling
+is strictly below `p^10`. The same corner is already at least `p^18` when
+`p = 2`, so no smaller single exponent stays under the ceiling for every
+integer `p >= 2`. The forward 2-norm square is strictly below `4p`, which is
+also below `p^20`.
+
+If `delta_col` meets the same floor, the column-gap ceiling is at most
+`16p^2`, and `(16p^2)^2 = 256 p^4` is strictly below `p^20` as well.
+
+Every later exponent in the table is a consequence of the hypothesis that
+both 2-norms are at most `p^10`. Both ceilings satisfy that hypothesis, so
+none of those exponents has to increase. This package does not decrease them.
+
+For every integer `p >= 19` the slack is larger than the notes use. At the
+`p = 19` corner the squared bandwidth ceiling is `6936029752576`, below
+`19^12`, so the 2-norm ceiling is below `p^6`. The column-gap ceiling is
+`5776`, below `19^3`. Their squared ratio is `207901`, below `19^6`. The
+room from that bandwidth ceiling up to `p^20` is more than a factor `p^8`.
+
+The broad `p^6` / `p^10` sentence is a different argument and does not read
+the bandwidth term.
+
+## What this does not say
+
+- It does not prove `delta_col >= 1/(16p^2)` for the rounded matrix `H`.
+  Cross-cut entries, truncation and rounding stay where #4402 left them.
+- It does not say the section error, the halo, or a multiplication exponent
+  moves. The selected κ is unchanged:
+  `836330098538459/500000000000000000`.
+- Upstream pin: main `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority
+  revision 7, checked 2026-10-21T16:32:11Z. Overlap refresh
+  2026-10-21T16:33:25Z covered 507 open PR bodies and 3240 discussions.
+  The live neighbor is #4402. Claim:
+  https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19102318
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/gaussian-twonorm-guard
+```
+
+## Open next questions
+
+If both 2-norms are assumed only up to `16p^2`, which of HALO's exponents
+20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease while keeping
+the same error and coverage conclusions? A decrease would be a ledger edit.
+It is not required for correctness, and it still would not apply to `H`
+until the column gap survives phase cuts, truncation and rounding.
+
+## Credit
+
+The conditioning lemma, the `p^10` guards and the halo exponents are #4100's.
+The column-gap question is pinterbanget's, in #4402, from #4336. The narrow
+kernel comes from PR1673 (Vlado Vojdanovski).
+
+Prepared by James Reed with substantial Cursor Grok 4.7 assistance. No
+independent human review. Apache-2.0.

research/gaussian-twonorm-guard/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/unconditional-batched-crt/AUDIT.md",
+      "usage": "input",
+      "git_blob": "cd59c5e786a3d37de027b8d0f7376fbb00d52efd",
+      "sha256": "2a6c84ba32c6febee0cbc205210a8935c481d40ec1d52d621442e03221cacc3d"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    },
+    {
+      "path": "research/unconditional-batched-crt/HALO.md",
+      "usage": "input",
+      "git_blob": "5f601b3c8ac368aa79aa1007effe5933a360237b",
+      "sha256": "a2adcf18614983e9255def6d3f5e59be0018a392e418d65e94323722838289cc"
+    },
+    {
+      "path": "research/unconditional-batched-crt/INVERSE-CONDITIONING.md",
+      "usage": "input",
+      "git_blob": "3853ffac91dfed5421b05533eb274a8646741071",
+      "sha256": "be3e4b729481b15a5ccc286b297908e4f9cef94c0c9144a28ee1cf58950d142a"
+    },
+    {
+      "path": "research/unconditional-batched-crt/PROOF.md",
+      "usage": "input",
+      "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c",
+      "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    }
+  ]
+}

research/gaussian-twonorm-guard/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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 #4100's written precision guards change when the inverse 2-norm input drops from INVERSE-CONDITIONING.md's bandwidth form to 1/sqrt(delta delta_col), listing each caller and exponent in research/unconditional-batched-crt.",
+  "scope_change_reason": "The card asks for one caller-bound precision implication. This comparison stays inside the written p^10 guards and GAUSSIAN.md's floors. It does not prove the column gap for the rounded matrix H.",
+  "bottleneck_link": "The selected frontier is unchanged. The comparison only classifies a precision guard inside the unselected #4100 construction.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the caller list and the comparison with p^10. Do not prove cross-cut entries, do not retune HALO's exponents, and do not claim a new kappa.",
+  "outcome": "completed",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/gaussian-twonorm-guard",
+  "author": "James Reed",
+  "ai_assistance": "Substantial help from Cursor Grok 4.7 on the caller inventory, the exact comparison and the package text.",
+  "open_questions": [
+    {
+      "question": "If both 2-norms are assumed only up to 16p^2, which of HALO's exponents 20, 42, 45 and 48, and GAUSSIAN's normalizer 100, can decrease while keeping the same error and coverage conclusions?",
+      "why_it_matters": "A decrease would change the halo and the normalizer. The present comparison shows those exponents need not increase, so a decrease is a separate ledger edit.",
+      "first_step": "Substitute the ceiling 16p^2 for p^10 in HALO's spectral interval and recompute the smallest integers J and A that keep the error at most exp(-p^2) and cover the polynomial bandwidth.",
+      "blocked_by": "None for that arithmetic. Applying a smaller exponent to H still requires the column gap after phase cuts, truncation and rounding."
+    }
+  ]
+}

research/gaussian-twonorm-guard/VERIFY.json

@@ -0,0 +1,26 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "research/unconditional-batched-crt/AUDIT.md",
+    "research/unconditional-batched-crt/GAUSSIAN.md",
+    "research/unconditional-batched-crt/HALO.md",
+    "research/unconditional-batched-crt/INVERSE-CONDITIONING.md",
+    "research/unconditional-batched-crt/PROOF.md",
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Pinned caller phrases, the p=2 corner below p^10 and not below p^9, and the p=19 ceilings below p^6 and p^3."
+    }
+  ]
+}