Add physical Gaussian row norm transfer audit

research/physical-gaussian-row-norm-transfer/PROOF.md

@@ -0,0 +1,101 @@
+# All-center contraction and unit-ball preservation for PR #3878
+
+## Quantified interface
+
+PR #3878, exact head `1a86a8fb73bb7a0982fff99852a031832c191902`, states the
+physical tile contract for integer `p > 100`, integer
+`2 <= alpha < sqrt(p)`, `u = alpha^2`, `1 < t/s < 2`, and its production-halo
+hypotheses. Its exact normalized map is
+
+```text
+(A x)_v = (1/(2 alpha)) sum_(j in Z)
+            exp(-pi (j - c_v)^2/alpha^2) x_j,
+c_v = (s/t)v.
+```
+
+The `x_j` are periodic source labels and may be any complex values with
+`||x||_infinity <= 1`. PR #3878 proves a uniform per-output error
+
+```text
+||T(x) - A(x)||_infinity < C 2^-p,
+C = sqrt(2) + 2^-11.
+```
+
+This note independently proves the exact all-center row bound
+
+```text
+for every real c and every alpha >= 2:
+  sum_(j in Z) exp(-pi (j-c)^2/alpha^2) <= 1 + alpha,
+  ||A||_(infinity -> infinity) <= 1/2 + 1/(2 alpha) <= 3/4.
+```
+
+It then derives the local domain-preservation implication. For every `p >= 3`
+and every unit-ball tile input,
+
+```text
+||T(x)||_infinity <= ||A(x)||_infinity + C 2^-p
+                  < 3/4 + 1/4 = 1.
+```
+
+Thus PR #3878's stated `p > 100` is more than enough for the output of one
+tile to satisfy the next tile's unit-ball numerical domain, if the caller
+passes the values directly on a compatible grid. This is a local implication
+only; it does not prove a full tensor schedule or any inter-axis precision
+conversion.
+
+## Proof of the row bound
+
+Fix `c` and `alpha >= 2`, and put
+`f(z)=exp(-pi (z-c)^2/alpha^2)`. Its values lie in `[0,1]`, and every strict
+level set `{z : f(z) > h}`, `0 < h < 1`, is an interval. Any interval of
+length `ell` contains at most `ell+1` integers. The layer-cake identity gives
+
+```text
+sum_(j in Z) f(j)
+  = integral_(h=0..1) #({j in Z : f(j)>h}) dh
+ <= integral_(h=0..1) (length({z : f(z)>h}) + 1) dh
+  = integral_R f(z) dz + 1
+  = alpha + 1.
+```
+
+The bound is uniform in the center `c`; no alignment of `(s/t)v` with the
+source lattice is needed. With periodic labels, multiple terms can name the
+same source coordinate, but all Gaussian weights are nonnegative. For any
+input with `||x||_infinity <= 1`, the absolute output is at most the sum of
+all those weights. Therefore the induced sup-norm bound for the periodic map
+is the same row-sum bound. Dividing by `2 alpha` yields
+
+```text
+||A||_(infinity -> infinity) <= (alpha+1)/(2 alpha)
+                              = 1/2 + 1/(2 alpha) <= 3/4.
+```
+
+For the error constant, `sqrt(2) < 10/7`, so
+`C < 10/7 + 1/2048 < 3/2`. If `p >= 3`, then
+`C 2^-p < (3/2)/8 = 3/16 < 1/4`. Combining this with the row bound proves
+`||T(x)||_infinity < 1` for every unit-ball input. The deduction uses only
+PR #3878's pointwise error premise and the exact row bound; it does not use
+the implementation's separate output-norm assertion.
+
+## Boundary controls and scope
+
+The bound `alpha >= 2` makes the sufficient contraction estimate at most
+`3/4`. At `alpha=1` the same estimate gives only `1`, so this proof route does
+not establish a `3/4` contraction. This is a limitation of the estimate, not
+a counterexample to the actual Gaussian row sum at `alpha=1`.
+
+The error precision guard in the domain-preservation deduction also matters.
+At `p=2`, the source constant obeys `C/4 > 1/4`; the abstract maps
+`A(z)=3z/4` and `T(z)=3z/4+1/4` have error at most `C/4` on the unit disk but
+`T(1)=1`. Thus a `<1` output bound does not follow from the row and error
+bounds at that precision. For `p>=3`, the exact rational upper bound above
+does imply it.
+
+The live handoff at discussion #1166 comment `19010279` claims the larger
+physical Gaussian tensor join. This result stops at the local all-center norm
+and domain-preservation implication. It does not prove tensor-error
+recurrences, tile routing, disjoint output coverage, coordinate moves,
+precision conversion, tape/hosting costs, chirp composition, CRT or integer
+recovery. PR #3877 already states a separate all-dimension recurrence for its
+positive coefficient-rounded operator; that recurrence is outside this
+audit.

research/physical-gaussian-row-norm-transfer/README.md

@@ -0,0 +1,52 @@
+# Physical Gaussian row-norm transfer
+
+**Status: independently proved the all-center local contraction and its
+unit-ball consequence; no tensor theorem claimed.**
+
+## Question and result
+
+At the exact normalized Gaussian interface used by PR #3878, does the row-sum
+bound hold uniformly over every center and periodic source labeling, and does
+the local tile error then keep its output inside the next tile's unit-ball
+domain? Yes. For every real center `c` and `alpha >= 2`,
+
+```text
+sum_j exp(-pi (j-c)^2/alpha^2) <= 1 + alpha,
+||S/2||_(infinity -> infinity) <= 1/2 + 1/(2 alpha) <= 3/4.
+```
+
+With PR #3878's per-output error `C 2^-p`, `C=sqrt(2)+2^-11`, this alone
+implies `||tile(x)||_infinity < 1` for every unit-ball input whenever `p>=3`.
+The cited PR uses `p>100`, so its local precision is sufficient. The
+all-center proof and exact guards are in [PROOF.md](PROOF.md).
+
+The result is a local independent check of a premise in PR #3878. It does not
+replay the tile implementation or establish that a full caller applies the
+tile to every source interval. The live handoff at #1166 comment `19010279`
+claims the larger tensor join; this pass deliberately stops at the local
+row-norm/domain implication and does not prove its error recurrence.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+python3 -B research/physical-gaussian-row-norm-transfer/verify.py
+```
+
+The verifier checks exact rational endpoint constants and the retained PR
+proof snapshot hash. The all-center result follows from the layer-cake proof
+in `PROOF.md`, not a finite Gaussian sum search. See
+[SOURCES.md](SOURCES.md) for source heads and digests.
+
+## Open next questions
+
+The active full tensor-join handoff at discussion #1166 comment `19010279`
+owns the next larger question. No distinct local follow-up is justified until
+that caller is published; its per-axis source and grid contracts can then be
+checked against this lemma.
+
+Credit: Jose Manuel (`jmbarrancoml`), PR #3878, for the physical tile and local
+error theorem. The row-sum proof and exact precision implication here are
+separate work by OpenAI Codex (`macbook-11`). No independent human or formal
+kernel review is claimed.

research/physical-gaussian-row-norm-transfer/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/physical-gaussian-row-norm-transfer/SOURCES.md

@@ -0,0 +1,16 @@
+# Source records
+
+Base repository and task-card provenance are in `SOURCES.json`.
+
+| Source | Exact commit | File | SHA256 |
+|---|---|---|---|
+| [PR #3878: physical Gaussian expansion tile](https://github.com/CrocSwap/integer-mult-bounds/pull/3878) | `1a86a8fb73bb7a0982fff99852a031832c191902` | `research/physical-gaussian-expansion/PROOF.md` | `5452f3e2191824b4a8451c83fbdf58b3b2228f4e1966a6f22c3e60bd152e56b0` |
+
+The exact PR #3878 proof bytes are retained in `inputs/`; the local verifier
+checks their hash. Its local tile error estimate is used as a conditional
+premise. This package does not independently replay the source construction
+or certify its analytic error estimate. PR #3877, head
+`5e7bdfa3c53bbb5a8d6e81f0efe7005c89184e6a`, was read as live overlap: its
+Theorem 2 already gives an all-dimension recurrence for a different
+coefficient-rounded operator. That recurrence and the active full tensor join
+are explicitly outside this package's result.

research/physical-gaussian-row-norm-transfer/TASK.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "docs/audit.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 the selected review scope and choose one exact all-size or precision implication.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "Choose one tape, precision, hosting or restoration lemma."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision"
+    ]
+  },
+  "scope_status": "refined",
+  "scope_change_reason": "After the required source-bound baseline and live overlap check, I selected PR #3878's normalized Gaussian tile boundary. A live #1166 handoff (comment 19010279) claims the full PR #3877/#3878 tensor join and its error recurrence, so I narrowed this pass to the independent local all-center row-norm and unit-ball-preservation implication.",
+  "actual_scope": "Prove that the exact normalized Gaussian row mass at PR #3878's tile boundary is at most 1+alpha for every real center and alpha>=2, then derive the exact p threshold at which the tile's local error implies unit-ball output preservation.",
+  "bottleneck_link": "The exact row contraction plus the tile's uniform local error gives the numerical domain guarantee needed before another tile may consume the output. The active full tensor caller remains a separate obligation.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the all-center row bound and exact unit-ball implication are proved with their parameter guards. Do not implement a tensor caller, derive its error recurrence, or run the PR's full replay.",
+  "outcome": "completed",
+  "evidence": "PROOF.md independently proves the all-center Gaussian row-mass bound by layer cake, transfers it to the periodic sup-norm operator, and derives that the local error C*2^-p preserves the unit ball for p>=3. verify.py checks exact rational endpoint and precision constants and the pinned PR #3878 proof snapshot. PR #3878's local numerical theorem remains a conditional premise; its implementation was not replayed.",
+  "author": "OpenAI Codex (macbook-11)",
+  "ai_assistance": "This proof, verifier and prose were prepared by OpenAI Codex. No independent human or formal-kernel review is claimed.",
+  "open_questions": [],
+  "no_open_questions_reason": "The larger full tensor-join question is already claimed in live discussion #1166 comment 19010279. This pass has no separate continuation that avoids that scope."
+}

research/physical-gaussian-row-norm-transfer/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/physical-gaussian-row-norm-transfer/inputs/PR3878-PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Checks the retained PR #3878 proof snapshot by SHA256; exact rational alpha=2 contraction endpoint, alpha=1 boundary of the sufficient estimate, C upper bound, p=3 minimum precision control, and p=2 counterexample to deriving strict output preservation from the error estimate. The all-center row bound is the layer-cake proof in PROOF.md, not a finite sum search."
+    }
+  ]
+}