lensora · Oct 22, 2026
diff --git a/research/triangular-parity-uniform-prefix/README.md b/research/triangular-parity-uniform-prefix/README.md
@@ -0,0 +1,183 @@
+# A sharp uniform bound for all triangular parity macro cuts
+
+**Scoped theorem:** every prefix, suffix, inverse prefix and inverse suffix
+of the exact lower-triangular parity compiler, at complete-shear boundaries,
+has infinity norm at most `1/(1−η)` when the symbol's tail `l1` is at most
+`η < 1`. Thus **2 suffices at `η ≤ 1/2`, independently of depth**, and no
+smaller constant bounds all four kinds of cuts uniformly in dyadic dimension.
+No new κ, full gate-level stability theorem or supplier admission is claimed.
+
+The source [SHALLOW-TOEPLITZ.md §3 and §6](../unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md)
+already gives polynomial circuit bounds. This result sharpens the *composed
+macro-cut* bound to a constant: it controls an unfinished child multiplied by
+its ancestor shear, not just each descendant matrix separately. It covers the
+source's parallel child execution and every order-preserving interleaving of
+the disjoint child macros. Serial even-first execution is only one such order.
+
+The actual caller is [GAUSSIAN.md's triangular compiler](../unconditional-batched-crt/GAUSSIAN.md),
+which supplies part of the conditional error ledger in
+[one-factor-of-t](../one-factor-of-t/README.md). Internal dirty-shear gates,
+generator normalization and the completed Gaussian stage remain separate.
+
+## Statement and proof
+
+Let `N=2^h`, `f(0)=1`, and `Σ_{j=1}^{N−1}|f_j| ≤ η < 1`, with real or
+complex coefficients. Write `T=T_N(f)` for multiplication by `f` modulo `z^N`.
+At each node write `f(z)=e(z²)+z o(z²)` and, modulo `z^(N/2)`, set
+
+```text
+k = o/e,       s = e − z o²/e,
+U = [I, T(zk); 0, I],       L = [I, 0; T(k), I],
+T = L diag(E,S) U,           E=T(e), S=T(s).
+```
+
+The matrices in this identity use the even/odd coordinate order. Simultaneous
+row/column permutation preserves the infinity norm. Execute `U`, the two
+recursive child programs on disjoint coordinates, then `L`. A macro is a
+whole such shear, not one gate of its FFT implementation. Reordering coordinates
+also has norm one and does not change the argument.
+
+For any cut, including either endpoint, let `P` be the executed prefix and
+`Q` the remaining suffix, so `T=QP`. We prove simultaneously
+
+```text
+max(‖P‖∞, ‖P⁻¹‖∞, ‖Q‖∞, ‖Q⁻¹‖∞) ≤ 1/(1−η).
+```
+
+The one-dimensional leaf is the identity. For the induction step, put
+
+```text
+a = ‖e−1‖₁,  b = ‖o‖₁,  c = 1−a,  d = c²−b².
+```
+
+Here coefficient `l1` is submultiplicative, truncation cannot increase it,
+and `a+b ≤ η < 1`, hence `c>b≥0` and `d>0`. Neumann expansion gives
+
+```text
+‖k‖₁ ≤ b/c,
+‖s−1‖₁ ≤ a+b²/c ≤ a+b ≤ η.
+```
+
+These shared-budget estimates are the one-level mechanism of James Reed's
+[#4699](https://github.com/CrocSwap/integer-mult-bounds/pull/4699); they are
+rederived here so the proof does not depend on unmerged executable code.
+The induction hypothesis bounds **each of the four child cut operators** by
+
+```text
+X = 1/c      for E,         Y = c/d      for S,
+```
+
+since `1−(a+b²/c)=d/c`. During the child phase, an arbitrary interleaving
+is some pair of legal child cuts. If their prefixes are `P_e,P_s` and
+suffixes are `Q_e,Q_s`, then exactly
+
+```text
+P    = diag(P_e,P_s) U,         P⁻¹ = U⁻¹ diag(P_e⁻¹,P_s⁻¹),
+Q    = L diag(Q_e,Q_s),         Q⁻¹ = diag(Q_e⁻¹,Q_s⁻¹) L⁻¹.
+```
+
+For a block row, add its block norms. The nontrivial block-row bounds and
+their nonnegative gaps below `B=1/(c−b)` are:
+
+| Operator | Block-row upper bound | `B` minus that upper bound |
+|---|---|---|
+| `P` | `(c+b)/c²` | `b²/[c²(c−b)]` |
+| `P⁻¹` | `1/c+b/d` | `b²/(c d)` |
+| `Q` | `b/c²+c/d` | `b³/(c² d)` |
+| `Q⁻¹` | `(c+b)/d` | `0` |
+
+Every other block row is bounded by `X` or `Y`, both at most `B`.
+Thus all four norms are at most `B=1/(1−a−b) ≤ 1/(1−η)`.
+The cuts just after `U` and just before `L` are included by taking identity
+or completed child cuts. At the two outer endpoints use
+`‖T‖∞ ≤ 1+η ≤ 1/(1−η)` and the Neumann bound
+`‖T⁻¹‖∞ ≤ 1/(1−η)`. This completes induction for every dyadic `N` and every
+legal child interleaving, including simultaneous layers of disjoint macros.
+
+## Sharpness and the remaining three-halves question
+
+For `f(z)=1−ηz`, the last row of `T_N(f)⁻¹` has absolute sum
+
+```text
+1+η+⋯+η^(N−1) = (1−η^N)/(1−η).
+```
+
+As dyadic `N` grows this tends to `1/(1−η)`. This inverse is an inverse
+prefix at the final cut (and an inverse suffix at the initial cut).
+Consequently the common four-operator constant is optimal. This is not a
+claim that every one of the four kinds individually needs that constant.
+
+Even a **forward suffix** can exceed `3/2`: take `N=4` and
+`f=(1,1/2,0,0)`. Immediately after the root right shear `U`, the suffix is
+`L diag(I,I−Z/4)`. In original coordinate order its last row is
+`(0,−1/4,1/2,1)`, of absolute sum **7/4**. Thus a one-level factor cap of
+`3/2` cannot be assigned to all composed cuts.
+
+Whether **forward prefixes alone** always satisfy `1+η` remains open here.
+This refines the initial investigation rather than claiming its sharp
+forward-prefix question was solved. #4701, #4702, #4704, #4705 and #4706 give
+individual `N=8` forward-prefix examples; none is used as a universal proof.
+
+## Exact controls and reproduction
+
+```sh
+python3 -B scripts/research_package.py --package research/triangular-parity-uniform-prefix --check-only
+python3.12 -B scripts/research_package.py --package research/triangular-parity-uniform-prefix
+python3.12 -O -B research/triangular-parity-uniform-prefix/verify.py
+```
+
+The standard-library checker independently builds the literal parity matrices,
+checks their endpoint identity, enumerates **every pair of child cut matrices**
+for seven rational fixtures at `N=1,2,4,8,16`, and checks all four operators at
+116 distinct fixture cuts. Signed dense tails, the zero tail, `η=3/4`, and the
+half-budget pure-odd family are included. It checks the exact `7/4` suffix row
+and geometric inverse formula. Wrong Schur sign, missing left shear and
+reversed macro order must change the endpoint; a tail outside the hypothesis
+exceeds 2. Runtime is a few seconds. Explicit failures remain active under `-O`.
+These finite controls test implementation and failure modes; the induction above,
+not the finite fixtures, supplies the universal claim.
+
+The proof was separately reviewed by a second Codex agent, which also used an
+independent sparse row-action checker for three child interleaving schedules.
+This is additional AI checking, not independent human or maintainer acceptance.
+Source blobs and SHA256 hashes are in [SOURCES.json](SOURCES.json); replay inputs
+are in [VERIFY.json](VERIFY.json). No external PR checkout is needed.
+
+## Open next questions
+
+1. **Is `1+η` the sharp forward-prefix bound?** It would improve the one-sided
+   macro error budget. First derive a row-level invariant retaining correlation
+   between `P_e` and `P_e E⁻¹`; the norm-product induction above loses that
+   correlation. No exact forward counterexample or proof is supplied here.
+2. **What happens inside one actual dirty-shear circuit?** The Gaussian caller
+   needs gate-level precision, not just macro boundaries. Bind the §2 FFT/twist
+   implementation and its inverse to the four macro envelopes, then account for
+   gate rounding. The local coefficient norms, generator compiler, row gap and
+   `p^100` normalization must still be justified; this package does not price them.
+
+## Provenance and credit
+
+Base: canonical main `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7,
+selected conditional κ=`60403/20000000`. Canonical investigation:
+[Discussion #4715](https://github.com/CrocSwap/integer-mult-bounds/discussions/4715).
+At entry, overlap coverage comprised 480 open PRs (2026-10-22T17:40:03Z),
+3632 Discussion records (17:41:08Z), and all 5860 local notes. Coverage omits
+arbitrary diffs and is not proof of novelty. Submission freshness is in TASK.json.
+
+- Vlado Vojdanovski/#1673 supplies the shallow Toeplitz compiler; Cinna Davis's
+  #4100 retains it at the later Gaussian caller, preserving its source lineage.
+- Ryanson Jonathan's `one-factor-of-t` identifies the error-ledger obligation;
+  it credits unpaidmoon's #4371 and the earlier #4320/#4311 audits.
+- Jose Manuel (`jmbarrancoml`), #4198 at
+  `e457d5e912a27307d725827aeca7198169320b84`, supplies exact rational Stein
+  generators and a separate polynomial generator-macro bound; its triangular
+  child execution is explicitly outside that result. This is complementary.
+- James Reed's one-level result is #4699 at
+  `67c70cc7d190fc4f728292d8f384c13f26f90385`; the finite series is #4701 at
+  `f6769f4542584057423935e7070ccf3c71d954e9`, #4702 at
+  `1767e47008695dd05ec16d67e3dfe8ceb25afcf3`, #4704 at
+  `93d3b4416a2be3bdfc684481e4e3d01670c3a534`, #4705 at
+  `3b71da338aeae3008244a132fc7dccf52800cbd8`, and #4706 at
+  `adb541f871698ed45d9d36d02617b6b9760f2b3e`.
+
+Prepared for Brian with substantial OpenAI Codex assistance. Apache-2.0.
diff --git a/research/triangular-parity-uniform-prefix/SOURCES.json b/research/triangular-parity-uniform-prefix/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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": "research/one-factor-of-t/README.md",
+      "usage": "input",
+      "git_blob": "4f907fcc3f217fe8450268dfa647180ab011834c",
+      "sha256": "c4c56df1ec816d357a23067e45aeb311ae62778a286acaf9aed4cc200e66d0d8"
+    },
+    {
+      "path": "research/unconditional-batched-crt/GAUSSIAN.md",
+      "usage": "input",
+      "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b",
+      "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242"
+    },
+    {
+      "path": "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md",
+      "usage": "input",
+      "git_blob": "bc4349b2daea548ffa09e1f38a31f1df86b0b7be",
+      "sha256": "b384b93f3fb4a8c97da2e617ebc14d55cebb0a739070e7f8dbb66f63e24e9310"
+    }
+  ]
+}
diff --git a/research/triangular-parity-uniform-prefix/TASK.json b/research/triangular-parity-uniform-prefix/TASK.json
@@ -0,0 +1,108 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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": "Prove the all-depth bound 1/(1-eta) for all four macro-cut operators of the lower-triangular parity compiler, at every dyadic size and every legal child interleaving, with eta<1.",
+  "scope_change_reason": "The initial sharper forward-prefix 3/2 question remains open; the completed result is a sharp common bound of 2 for forward/inverse prefixes/suffixes at eta<=1/2, including the actual parallel schedule, plus a 7/4 forward-suffix witness. This is a quantified partial stability theorem, not another single-symbol pass.",
+  "bottleneck_link": "SHALLOW-TOEPLITZ section 3 is cited by GAUSSIAN; controlling composed macro cuts independently of depth strengthens one boundary of the Gaussian precision ledger while leaving dirty-shear gates and completed normalization open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after a general macro-bound proof and exact failure controls; do not expand into full Gaussian, native, Lean or selected construction replay.",
+  "outcome": "completed",
+  "evidence": "README.md induction and sharpness proof; verify.py exact endpoint, all-interleaving cut matrices and four failure controls.",
+  "author": "Brian, with substantial OpenAI Codex assistance",
+  "ai_assistance": "OpenAI Codex derived and implemented the result; a separate Codex subagent reviewed the proof and ran independent sparse row-action controls. No human or maintainer review claimed.",
+  "open_questions": [
+    {
+      "question": "Do forward prefixes alone satisfy 1+eta at every depth?",
+      "why_it_matters": "Would sharpen the one-sided macro amplification bound beyond the common four-operator constant.",
+      "first_step": "Find a row-level invariant retaining correlation between P_e and P_e E inverse.",
+      "blocked_by": "No general proof or exact forward-prefix counterexample is supplied."
+    },
+    {
+      "question": "Can the actual dirty-shear FFT/twist circuit be bounded between these macro cuts?",
+      "why_it_matters": "The Gaussian caller needs gate-level precision, not merely macro-boundary conditioning.",
+      "first_step": "Bind one literal section-2 shear circuit and its inverse to the macro envelopes and account for rounding.",
+      "blocked_by": "Internal shear, generator, row-gap and completed-normalizer obligations remain outside this result."
+    }
+  ],
+  "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4715",
+  "submission_checkpoint": {
+    "checked_at": "2026-10-22T17:50:15.142755+00:00",
+    "canonical_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+    "priority_revision": 7,
+    "guidance_and_source_changes": "none",
+    "coverage": {
+      "local": {
+        "head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+        "records": 5862,
+        "head_records": 5860,
+        "complete_head_inventory": true,
+        "unsearched_head_paths": []
+      },
+      "open_prs": {
+        "fetched_at": "2026-10-22T17:49:23.029725+00:00",
+        "complete_pagination": true,
+        "records": 484
+      },
+      "discussions": {
+        "fetched_at": "2026-10-22T17:50:14.963355+00:00",
+        "complete_pagination": true,
+        "records": 3636
+      }
+    },
+    "warnings": [],
+    "overlap_decision": "The live #4699/#4701/#4702/#4704/#4705/#4706 heads are unchanged. #4198 concerns rational Stein generators and explicitly leaves parity-child execution separate; this package proves the all-depth triangular child macro-cut bound. No competing general four-cut bound found in searched coverage."
+  }
+}
diff --git a/research/triangular-parity-uniform-prefix/VERIFY.json b/research/triangular-parity-uniform-prefix/VERIFY.json
@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/one-factor-of-t/README.md",
+    "research/unconditional-batched-crt/GAUSSIAN.md",
+    "research/unconditional-batched-crt/vendor/SHALLOW-TOEPLITZ.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact parity identity, all child-interleaving cuts of seven fixtures, four cut-operator norms, sharpness and four failure controls"
+    }
+  ]
+}