Prove the narrow-row half-gap budget at 1/(16p^2).

research/narrow-row-half-gap/README.md

@@ -0,0 +1,210 @@
+# The narrow row keeps half its certified gap
+
+**Claim type:** one quantified implication for the #4100 narrow reference row.
+**No new κ.** The selected conditional value stays `60403/20000000 = 0.00302015`.
+
+`vendor/FINE-PRIME.md` says that deleting diagonal aliases preserves a
+polynomial gap, and that exponentially accurate band truncation and rounding
+preserve half of it. `GAUSSIAN.md` concludes that the rounded reference `H`
+has diagonal 1, row gap at least `1/(16p^2)` and row norm below 2. The
+coverage map still lists an explicit form of that half-gap sentence as open.
+This note supplies the budget the sentence does not write down.
+
+## Statement
+
+Fix an integer `p ≥ 1`. Write `log` for the natural logarithm, as required by
+the comparison `5 exp(-2a) ≤ 5/(16p)^8` in LOG-A §1 when `a ≥ 4 log(16p)`.
+Let `a ≥ 4 log(16p)` and `θ ≥ 1/(4p^2)`, and set
+
+```text
+S = exp(-2 a θ) + 5 exp(-2 a),    γ = 1 - S.
+```
+
+The parameter minimum is the worst case: both terms of `S` fall as `a` or `θ`
+grows. At that minimum,
+
+```text
+γ ≥ 1/(8p^2).
+```
+
+Let a real row have nonnegative diagonal `d` and off-diagonal absolute sum
+`Off`, with
+
+```text
+Off + |d - 1| ≤ S.
+```
+
+Form the reference row as follows.
+
+1. **Alias removal.** Replace the diagonal by 1 and leave the off-diagonal
+   entries unchanged.
+2. **Band truncation.** Replace any set of off-diagonal entries by 0.
+3. **Rounding.** Add a real perturbation whose off-diagonal absolute row sum
+   is at most `τ`, then set the diagonal back to 1.
+
+The resulting diagonal is 1 and the row gap is at least `γ - τ`. In
+particular, every
+
+```text
+τ ≤ 1/(16p^2)
+```
+
+leaves row gap at least `1/(16p^2)` and absolute row sum strictly below 2.
+Alias removal and truncation spend none of the certificate `γ`. Only rounding
+spends it, and the published half is exactly this uniform budget.
+
+A sufficient per-entry rule is: at most `2p` off-diagonal entries change, and
+each absolute value grows by at most `2^{-5p}`. At `p = 1` the total equals
+`1/(16p^2)`. For every `p ≥ 1`, `(1 + 1/p)^3 ≤ 8 ≤ 32`, so the same comparison
+persists at `p + 1`. The same count with `2^{-4p}` fails at `p = 1`. This does
+not identify #4100's unnamed precision constant with 5.
+
+Any defect at most `p^M 2^{-c p}`, for integers `c ≥ 1` and `M ≥ 0`, is inside
+the budget once `2^{c p} / p^{M+2}` is at least 16 and increasing. For `c = 1`
+the checker records a sufficient such `p` for every `M ≤ 8`: 11, 16, 22, 29,
+35, 42, 49, 57 and 64. FINE-PRIME's eventual row-norm bound
+`poly(p) 2^{-(C-o(1))p}` therefore meets `τ ≤ 1/(16p^2)` for every fixed
+`C > 0` and all large `p`. The implicit degree and the finite cutoff are not
+extracted here.
+
+## Proof
+
+**Ideal certificate.** Let `x = 2 a θ`. The minimum is
+`x ≥ 2 log(16p) / p^2`. The series remainder gives `exp(2) < 8`, so
+`log(16p) > 2`. Thus the minimum `x` is greater than 1 at `p = 1` and at
+`p = 2`.
+The same series gives `exp(1) > 8/3`, hence `1 - exp(-1) > 5/8`. For these two
+values of `p`,
+
+```text
+γ ≥ 5/8 - 5 (16p)^{-8} ≥ 1/(8p^2).
+```
+
+For the Taylor step, `f(x) = 1 - x + x^2/2 - exp(-x)` satisfies `f(0) = f'(0) = 0`
+and `f''(x) = 1 - exp(-x) ≥ 0` for `x ≥ 0`. Thus `f` and `f'` stay nonnegative,
+`exp(-x) ≤ 1 - x + x^2/2`, and
+
+```text
+1 - exp(-x) ≥ x(1 - x/2) ≥ x/2    for 0 ≤ x ≤ 1.
+```
+
+The partial sum of `exp(9/2)` through degree 5 exceeds 48, so the minimum `x`
+is at most 1 at `p = 3`. The partial sum of `exp(7/2)` through degree 2 exceeds
+2, and `(p+1)/p ≤ 4/3 < 2` for `p ≥ 3`, so `exp(p + 1/2) ≥ (p+1)/p`. Therefore
+`16p ≤ exp(p^2/2)` persists for every integer `p ≥ 3`, and the worst-case `x`
+stays at most 1. There
+
+```text
+1 - exp(-x) ≥ x/2 ≥ log(16p)/p^2 ≥ 2/p^2,
+γ ≥ 2/p^2 - 5 (16p)^{-8}.
+```
+
+Clearing the positive denominator is the integer comparison
+`15 · 2^{32} ≥ 40`, which is exactly `2/p^2 - 5/(16p)^8 ≥ 1/(8p^2)` at `p = 1`
+and is stronger for `p > 1`.
+
+**Three operations.** From `Off + |d - 1| ≤ S` and `d ≥ 0`:
+
+- if `d ≥ 1`, then `Off ≤ S - (d - 1)` and `1 - Off ≥ 1 - S`;
+- if `0 ≤ d < 1`, then `Off ≤ S - (1 - d)` and `1 - Off ≥ 2 - S - d ≥ 1 - S`.
+
+Zeroing an off-diagonal entry cannot increase an absolute sum, whatever its
+sign. A perturbation of off-diagonal absolute row sum `τ` increases that sum
+by at most `τ`, by the triangle inequality. Resetting the diagonal to 1
+discards only the diagonal part of the perturbation. The gap is therefore at
+least `γ - τ`.
+
+The budget is sharp relative to the certificate, whether or not the Gaussian
+tail meets it. A row with `d = 1` and `Off = 1 - 1/(8p^2)`, and with truncation
+removing nothing, is allowed by `γ ≥ 1/(8p^2)`. A defect of exactly `1/(16p^2)`
+then leaves gap exactly `1/(16p^2)`, and a defect of `1/(8p^2)` leaves gap 0.
+Alias mass or a deleted tail makes the final gap strictly larger, so those two
+operations cannot be what forces the factor one half. The Gaussian value of
+`S` may be strictly smaller than `1 - 1/(8p^2)`; that extra slack is not used.
+
+**Row norm and principal sections.** Diagonal 1 and off-sum at most
+`1 - 1/(16p^2)` give absolute row sum `2 - 1/(16p^2) < 2`. A principal
+subrow keeps a subset of the off-diagonal entries, so its absolute off-sum
+is no larger and its gap is no smaller.
+
+**What the factor one half is not.** It is half of the published certificate
+`1/(8p^2)`, not necessarily half of the true `γ`. The `x/2` branch is at least
+`2/p^2` before the tiny tail, sixteen times `1/(8p^2)`. Extra slack is real
+and unused. Charging each of `2p - 1` band entries with mass `1/(16p)`, the
+old margin copied once per entry, produces a row change larger than
+`1/(8p^2)` for every `p ≥ 2`. The budget has to be a total row sum.
+
+## What this does not prove
+
+LOG-A §3 already shows that one elimination step on a strictly row-diagonally
+dominant matrix does not decrease the minimum absolute row gap. The identity
+does not use the numerical size of the gap, so it applies to a matrix whose
+gap is `1/(16p^2)`. This package does not re-prove that identity, and it does
+not rerun the Gaussian circuit.
+
+The column statement in `research/gaussian-gauge-column` is a different
+mechanism: a relative weight error inside one cell, with the explicit warning
+that a row-sum bound does not replace it. #4402 and #4437 bound ideal column
+sums. #4481 keeps a Schur margin of `1/(10p^2)` once that larger gap is
+already known. None of those is the alias, truncation and rounding budget for
+the row.
+
+The Neumann bound `‖H^{-1}‖_∞ ≤ 1/δ` applies after this lemma with
+`δ = 1/(16p^2)`, because `H = I - E` with `‖E‖_∞ ≤ 1 - δ`. The `p^{10}` norm,
+the chirp origin, across-cell columns and the unnamed setup constant remain
+open. This is not an admission of #4100 and not a change to the selected
+frontier.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/narrow-row-half-gap --check-only
+python3 -B scripts/research_package.py --package research/narrow-row-half-gap
+```
+
+`verify.py` pins the five source sentences, checks the series comparisons, the
+uniform integer certificate, the three operations for `p = 1..200`, the `C = 5`
+and `C = 4` entry rules, the polynomial thresholds, and the singular control.
+It does not evaluate a Gaussian matrix and does not replay #4100.
+
+## Task and overlap
+
+- Card `uniform-transfer-audit`, scope refined to this one precision sentence.
+- Base: canonical main `fbc9ea0249746acca4f504d4fda2b84e0e36cf0d`, priority
+  revision 7. #4100 remains pinned by the family record at
+  `337d04939571a637aeab54a0f58f54fde811663a`.
+- The coverage map's still-open column, after dropping merged closures
+  including #4356, #4371, #4373, #4376 and #4377, puts this sentence at the
+  ninth remaining obligation. #4217 open question 1 and #4371 open question 2
+  ask for the same explicit budget.
+- #4438 records that its column gauge is not a row argument. This package is
+  that missing row argument.
+
+## Open next questions
+
+1. Does the stored narrow band have at most `2p` off-diagonal entries in every
+   row, and does the note's rounding meet absolute error `2^{-5p}`? The total
+   budget above is proved either way. The first step is the definition of `W`
+   in `GAUSSIAN.md` together with one rounding mode for a kernel entry. It is
+   blocked until that mode is pinned; the name `C` in the setup formula is not
+   yet a number.
+2. Which chirp origin does the interior caller use? The coverage map lists
+   this beside the half-gap sentence, and #4304 shows that a centred chirp can
+   push one `p = 19` entry above 1. The first step is to name the origin in
+   the interior kernel and compare that one entry. This row budget does not
+   choose the origin.
+
+## Credit
+
+The ideal bound `‖N-I‖_∞ ≤ exp(-2aθ) + 5 exp(-2a)` is LOG-A §1 from PR1673.
+PR1786, and #4100's byte-identical `vendor/FINE-PRIME.md`, state the half-gap
+sentence. The `1/(8p^2)` certificate for every `p ≥ 1` is the merged
+`pr1786-fine-prime-transfer-audit`. #4217 asked the question. #4438
+(James Reed) separated the within-cell column gauge from any row-sum charge.
+#4402, #4437 and #4481 are the neighbouring column and Schur results cited
+above and not reused as a row proof.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or formal-kernel review is claimed.

research/narrow-row-half-gap/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "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": "docs/research/pr4100-audit-coverage-map.md",
+      "usage": "input",
+      "git_blob": "8bcf878042c15f9f45652664999058b38c944030",
+      "sha256": "b9b45dbc288d5da63a8d0cb31cbaca83e7ff200f692dc481ff5b9a2616569203"
+    },
+    {
+      "path": "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+      "usage": "input",
+      "git_blob": "3bcf490a8c164d44aff5b7e2ec2e0f4bf07d7a73",
+      "sha256": "e05d6b8596c80b6e8676569a0ff464a29fa704c3304143f58914f47cdf38b272"
+    },
+    {
+      "path": "research/gaussian-gauge-column/README.md",
+      "usage": "input",
+      "git_blob": "7926f38cfcb0bbf0a47517ed5aa40e7f5a80dc5e",
+      "sha256": "82101b0310ea5f7b1c273a11fd1cd72185f025a158023379d976e747cb329c9b"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/FINE-PRIME.md",
+      "usage": "input",
+      "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3",
+      "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce"
+    }
+  ]
+}

research/narrow-row-half-gap/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "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": "Does alias removal, band truncation and a row-sum rounding defect of 1/(16p^2) leave the #4100 narrow reference row a gap of at least 1/(16p^2)?",
+  "scope_change_reason": "The card asks for one quantified #4100 implication at its caller. This package takes only the narrow-row half-gap sentence that FINE-PRIME.md asserts in one line and that the coverage map still lists as open after the ideal 1/(8p^2) certificate. It does not audit CRT repair, the free-algebra lift, the column gauge or the chirp origin.",
+  "bottleneck_link": "#4100 proposes an unconditional exponent above the selected kappa. GAUSSIAN.md's inverse bounds use row gap delta >= 1/(16p^2). The half-gap sentence is the step from the proved ideal certificate 1/(8p^2) to that rounded gap. A missing budget there blocks treating the proposed inverse norm as proved. This audit does not change the selected frontier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the ideal certificate, the three row operations and the explicit rounding budget. Do not identify the unnamed setup constant, execute the Gaussian circuit, or choose the chirp origin.",
+  "outcome": "completed",
+  "evidence": "verify.py pins the five source sentences and checks the series comparisons, the uniform integer certificate, the three operations for every p from 1 through 200, the C=5 and C=4 entry rules, the polynomial thresholds through degree 8, and the singular control.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok 4.7",
+  "open_questions": [
+    {
+      "question": "Does the stored narrow band have at most 2p off-diagonal entries per row, and does #4100's rounding meet absolute error 2^{-5p}?",
+      "why_it_matters": "The total row-sum budget tau <= 1/(16p^2) is proved. The per-entry rule is only a sufficient special case, and the note's unnamed C is not shown to be at least 5.",
+      "first_step": "Pin the definition of W in GAUSSIAN.md and one rounding mode for a kernel entry, then compare 2 W eta with 1/(16p^2).",
+      "blocked_by": "The pinned sentences name W only as O(sqrt(p) polylog(p)) and do not fix the rounding mode."
+    },
+    {
+      "question": "Which chirp origin does the interior caller use?",
+      "why_it_matters": "The coverage map lists this beside the half-gap sentence. A centred chirp can push one p=19 shifted-kernel entry above 1, so the row budget does not choose the matrix.",
+      "first_step": "Name the origin in the interior kernel and compare that one p=19 entry with the centred witness.",
+      "blocked_by": "The origin is a different hypothesis from the rounding budget."
+    }
+  ]
+}

research/narrow-row-half-gap/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "docs/research/pr4100-audit-coverage-map.md",
+    "research/capped-phase-fusion/LOG-A-PHASE-SCHUR-AUDIT.md",
+    "research/gaussian-gauge-column/README.md",
+    "research/unconditional-batched-crt/GAUSSIAN.md",
+    "research/unconditional-batched-crt/vendor/FINE-PRIME.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source-sentence pins, ideal-gap series comparisons, three row operations for p=1..200, C=5 and C=4 entry rules, polynomial thresholds, and the singular control."
+    }
+  ]
+}