From afb777550eb620b8eda3ea7e7804ebea23bfce3b Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Sat, 24 Oct 2026 21:48:38 -0700
Subject: [PATCH 1/3] Audit uniform encoded Gaussian coefficient bounds and
 freeze independent interval oracle

---
 .../ORACLE-FREEZE.json                        |   6 +
 .../PROOF.md                                  | 183 ++++++++++++++++++
 .../README.md                                 |  54 ++++++
 .../SOURCES.json                              |  96 +++++++++
 .../TASK.json                                 |  74 +++++++
 .../oracle.py                                 |  72 +++++++
 6 files changed, 485 insertions(+)
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/ORACLE-FREEZE.json
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/PROOF.md
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/README.md
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/SOURCES.json
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/TASK.json
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/oracle.py

diff --git a/research/encoded-gaussian-directed-coefficient-audit/ORACLE-FREEZE.json b/research/encoded-gaussian-directed-coefficient-audit/ORACLE-FREEZE.json
new file mode 100644
index 0000000000..5b77df9f0d
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/ORACLE-FREEZE.json
@@ -0,0 +1,6 @@
+{
+  "stage": "before any source output capture",
+  "oracle_sha256": "87dd13add789995c763ff1f4f059ac23d1b221fff2699daaa38566510f3d1022",
+  "self_tests": "60 interval cases passed, plus zero/scaling/pi controls",
+  "independence": "distinct algorithm, same AI-assisted contributor; no independent authorship claim"
+}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/PROOF.md b/research/encoded-gaussian-directed-coefficient-audit/PROOF.md
new file mode 100644
index 0000000000..ad6a4df7bb
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/PROOF.md
@@ -0,0 +1,183 @@
+# Audit of the actual encoded Gaussian coefficient contract
+
+JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0.
+This is a source-relative written proof plus independent-algorithm finite
+checks, not formal-kernel or independent human acceptance. It audits PR3851's
+encoded producer, not the different host Gaussian.exponential audited in
+`gaussian-scalar-backend-audit`.
+
+## Quantified statement
+
+For integers P,F>=1, a rational 0<=f<=F, a Boolean growth flag and integer
+sigma>=0 (None means zero), the pinned Exponentials.grid_interval returns
+integers l<=u such that, with eta=2^-P,
+
+    l eta <= 2^-sigma exp((+1 if growth else -1) pi f) <= u eta,
+    u-l <= 2.
+
+Consequently coefficient, which returns l, has downward error <2eta. All
+constructor, Taylor-range, interval-width and final-width checks succeed
+mathematically. Termination is for every finite represented input, with the
+encoded Count/Rational operations and ownership semantics retained. There
+is no assertion that arbitrary non-admitted input succeeds. In particular
+negative f and f>F must be rejected. No global H row-gap theorem follows.
+
+## Directed primitives and Machin interval
+
+`quotient(a,b,True)` is ceil(a/b), because it increments precisely for a
+nonzero remainder; the ordinary branch is floor. `ceil_shift` performs the
+right shift and increments precisely when a discarded bit is one. Reading
+beyond the number's right marker does not add a discarded bit. Both preserve
+the input head by rewinding. Thus nested downward divisions and nested
+upward divisions preserve the corresponding exact rational bounds.
+
+Write X=4F, k=ceil(log2(8(X+1))), H0=P+X+k+16, c=ceil(log2 H0),
+R=P+4X+4k+2c+64, h=2^-R, J=ceil(R/4)+8, N=ceil(R/3)+8.
+All are the actual Count computations, including remainder-based ceilings.
+For this domain H0>=27, R>=115, R<5H0, N<=R/2, and R>=4k.
+For the R<5H0 bound use c<=H0/2, valid for integral H0>=4:
+R<=P+4X+4k+H0+64<5(P+X+k+16), since P>=1.
+
+The actual nested archive's twiddle_setup.arctangent encloses each of J
+alternating terms using [floor(term/h),floor(term/h)+1]h. The signs reverse
+the endpoint order for negative terms. The next omitted arctangent term
+has magnitude at most 1/5^(2J+1)<h because 25^J>16^J>2^R;
+the 239 tail is smaller. Its symmetric one-unit padding is sufficient.
+Machin's identity pi=16 atan(1/5)-4 atan(1/239) then encloses pi with width
+(20J+40)h<=7Rh. The exact signs and nested source bytes are authenticated.
+The classical bounds 3<pi<16/5, together with this tiny width, also give
+the constructor's strict 3<pi_lower<=pi_upper<4 checks. For example pi>25/8
+and pi<22/7 follow from elementary rational series enclosures; the independent
+arcsine oracle checks stronger rational bounds without using Machin.
+
+Multiplication by f and outward quotient yield width at most (7RF+2)h.
+The upper x endpoint is <X: pi<16/5 and (7R+1)h<4/5 for R>=115.
+After division by 2^k and outward rounding, the y interval obeys
+
+    Delta_y <= (7R+65)h/32 <= Rh/4,
+    0 <= y_lower <= y_upper <= 1/8.
+
+Indeed 2^k>=32F+8 and the extra shift adds less than 2h. For the range,
+X/2^k<=X/(8(X+1)); the missing margin is at least 2^-k>=h.
+This derives the actual range check, not just an assumption about exp inputs.
+
+## Taylor termination, early exit and squaring
+
+The true positive Taylor terms for every y in the interval are enclosed by
+the actual lower/upper recurrence. In real R-grid units, each nested rounding
+adds at most 2h per endpoint. Upper terms stay <=1 by induction, since their
+next value is <= previous/8+2h<1. For term-width d_j,
+
+    d_j <= d_(j-1)/8 + Delta_y + 4h <= 2Delta_y+5h.
+
+At early exit the added upper term is <=h; all following exact term ratios
+are <=1/8, so the omitted positive tail is <=h/7. At fixed exit after N
+updates the tail is <(8/7)2^(-3(N+1))<h. The extra upper unit therefore
+suffices in both branches. Closing the encoded iterator on early exit is
+part of the unchanged source's scratch-release path.
+
+The accumulated interval has lower endpoint >=1 and width
+E0<=N(2Delta_y+5h)+h<=R^2 h. Comparing upper terms with the exact series
+at y_upper gives rounding excess <=(16/7)Nh+h<=3Nh. Thus its upper endpoint
+u0 satisfies log(u0)<=y_upper+3Nh.
+
+Let li,ui denote the endpoints after i outward squarings. They remain >=1,
+and log(u_(i+1))<=2log(ui)+h. Consequently
+
+    sum_(i=0)^(k-1) log(ui)
+      <= (2^k-1)y_upper + 2^k(3N+1)h < X+1.
+
+The last inequality follows from 2^k y_upper <= x_upper+2^k h and
+2^k(3N+2)h<1. To see the latter uniformly, use k<=R/4,
+3N+2<=2R<=2^(R/2), so the product is <=2^(-R/4)<1.
+Widths satisfy E_(i+1)<=2ui Ei+2h. Since each factor 2ui>=2,
+unrolling the recurrence and summing the reciprocal geometric majorant gives
+
+    Ek <= 2^k exp(X+1)(R^2+2)2^-R
+       < 2^(-P-2X-3k-57) <= 2^(-P-83).
+
+Here R^2+2<=32H0^2, H0<=2^c and exp(X+1)<2^(2X+2).
+This proves the positive_interval strict width check (<eta).
+No finite sweep in P,F replaces these inequalities.
+
+## Reciprocal and final normalization
+
+For decay, reciprocation reverses endpoint order. On [1,infinity) it cannot
+increase width; the two outward R-grid quotients add less than 2h. Growth
+keeps the original enclosure. Both branches therefore have width <eta/2.
+Scaling by 2^-sigma does not increase it. Final outward P-grid rounding adds
+less than 2eta to width. The endpoint difference is an integer number of
+eta units and is strictly below 5eta/2, hence at most 2eta. The actual source
+accepts difference<=3; the proved tighter bound implies that check. The
+lower coefficient is an approximation, not necessarily the exact irrational
+floor. Changing this contract to exact-floor equality would be unjustified.
+
+## Binding every Axis argument family
+
+The actual Axis requires s<t<2s and 2w<s, all positive integers. Put
+rho=t/s, theta=(t-s)/s. It computes q_j=floor(rho*j+1/2), beta_j=rho*j-q_j,
+so -1/2<=beta_j<1/2, including half-up ties. Its declared F is the maximum
+of ceil(u/(4theta)) and ceil(u(rho*w+1/2)^2).
+
+The weight argument u(1/4-beta_j^2)/theta is in [0,u/(4theta)]. The
+normalized growth diagonal uses u beta_j^2<=u/4 with sigma=2u. For reflected
+rows, beta_(s-j)^2=beta_j^2: ordinary ties change the sign, while half ties
+remain -1/2 on both sides. This justifies the source's squared-offset check
+and reuse; it is not an unproved identity of signed beta values.
+
+The nonzero kernel argument u rho d^2, d<=w, is <=u(rho*w+1/2)^2.
+For a cross-cell entry let delta be the chosen signed cyclic distance,
+|delta|<=w. Since rho*s=t is integer,
+
+    rho*delta+beta_i = beta_j + m,  m an integer.
+
+The nearest-integer property gives |beta_j+m|>=|beta_j|, including ties.
+Thus f=u[(rho*delta+beta_i)^2-beta_j^2]>=0, while
+f<=u(rho*w+1/2)^2. Direct and wrapped branches both satisfy the prepared
+domain. Zero kernel/diagonal entries bypass the backend exactly as in source.
+This proves the coefficient-call domain for every admitted Axis tuple. It
+does not prove nonzero rounded weights for arbitrary P: positive exact
+weights may truncate to zero. That is a separate Axis admission check and
+production precision obligation, expressly retained.
+
+## Independent checks and costs
+
+The oracle uses pi=6 asin(1/2), a positive series whose consecutive-term
+ratio is <1/4, so eight times the next term bounds the pi tail. It computes
+exp(-x) by alternating even/odd rational sums at x<=1/4, applies outward
+dyadic squaring, and obtains growth by reciprocal. Thus the source positive
+Taylor/Machin paths are not their own numerical oracle. Every source output
+must contain the entire finer oracle interval; mere overlap is insufficient.
+Oracle source/self-tests are frozen before source-output capture. This is
+algorithmic separation within one AI-assisted contribution, not a claim of
+independent authorship or human verification.
+
+The adapter executes unchanged encoded Axis construction and isolated boundary
+calls with no_decode active. It records raw arguments, endpoints, setup grid
+and branch counters; decodes only after protected execution returns. It also
+checks the actual argument multiset against the rational formulas above,
+including reflection, wrapped differences, growth and normalization. It
+supplies no approximation or host arithmetic to the source producer.
+
+The retained ordinary-arithmetic bound per coefficient preparation/application
+is O(R^3+(R+B_f)^2), plus O(sigma+R) for the explicit final shift scan and
+storage for its encoded extent. Machin and O(R) Taylor iterations operate on
+O(R+X+B_f)-bit carriers, X<=R; k squarings and reciprocal divisions fit that
+coarse bound. It is not a bit-length-only tariff for enormous sigma. Actual
+Axis repeats coefficients and pays matrix setup/storage; the audit does not
+claim a free cache, a new machine-step leading constant or faster setup.
+Independent-oracle memory and observer snapshots are verification overhead.
+
+## Open next questions
+
+Compose these directed scalar errors with the actual weight ratios and
+cross-cell entries to obtain the production old-H perturbation bound, then
+bind the ideal matrix row gap. Preserve the separate positive rounded-weight
+admission and exact arithmetic/movement contracts. The present theorem does
+not install global row dominance, LU caps, online Core error, tensor/CRT
+admission or a multiplication theorem, and changes no selected frontier.
+
+Credit Jose Manuel/jmbarrancoml PR3851 for the physical encoded producer and
+its original precision proof, the retained physical-ring Machin runtime and
+Gaussian lineage, and the distinct prior scalar-backend audit. Frozen inputs
+and source-specific notices remain unchanged.
diff --git a/research/encoded-gaussian-directed-coefficient-audit/README.md b/research/encoded-gaussian-directed-coefficient-audit/README.md
new file mode 100644
index 0000000000..43fe61bffb
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/README.md
@@ -0,0 +1,54 @@
+# Actual encoded Gaussian coefficient audit
+
+This scoped source-relative proof establishes directed growth/decay enclosures
+and a two-target-ulp endpoint bound for the actual encoded Exponentials routine,
+for every P,F>=1, rational 0<=f<=F and nonnegative binary scale. It derives
+Taylor early/fixed tails, repeated-squaring width, reciprocal direction and
+final rounding from the actual policy. [PROOF.md](PROOF.md) also proves the
+actual Axis weight, kernel, wrapped cross-cell and normalized diagonal arguments
+fit the prepared bound. Positive rounded weights and global rowgap remain
+separate obligations.
+
+An oracle using positive arcsine for pi and alternating decay series was frozen
+before observing source outputs. The adapter runs unchanged encoded Axis and
+isolated boundary calls, recording raw data under no_decode and decoding only
+after execution. Each source interval must contain the entire finer oracle
+interval; simple overlap is insufficient. This is independent-algorithm
+checking by the same AI-assisted contributor, not independent human review.
+
+## Reproduce
+
+Python3.12, standard library only, from repository root:
+
+```sh
+python3.12 scripts/research_package.py --package research/encoded-gaussian-directed-coefficient-audit --check-only
+python3.12 -I -B research/encoded-gaussian-directed-coefficient-audit/verify.py --oracle-only
+python3.12 scripts/research_package.py --package research/encoded-gaussian-directed-coefficient-audit
+```
+
+The two actual source commands have 240-second bounds. Source inputs and the
+frozen oracle are authenticated before imports. RESULT.json is mandatory and
+compared as complete typed JSON. The original source and nested archives remain
+unchanged; source-history and export checks use explicit input base32890bc.
+
+## Limits
+
+This audits the encoded physical backend, distinct from the normalized host
+Gaussian.exponential scalar audit. No global old-H coefficient composition,
+ideal gap, LU, online solve, Core headroom, tensor/CRT or new kappa is claimed.
+Original setup, rational arithmetic, scans and storage remain paid; a final
+shift by huge sigma costs its scan, not just log(sigma). Oracle and observer
+memory are verification overhead.
+
+## Open next questions
+
+Compose actual weight-ratio/cross-cell errors into the production original-H
+perturbation bound, retaining positive rounded-weight admission, and bind the
+ideal matrix rowgap. This scalar enclosure result alone does not establish it.
+
+## Credit
+
+JoyboyBrian with substantial OpenAI Codex assistance, Apache-2.0. Credit Jose
+Manuel/jmbarrancoml PR3851 for the physical producer and original precision
+proof, the retained physical-ring Machin runtime and Gaussian lineage, and
+the distinct prior normalized scalar-backend audit. Frozen notices remain.
diff --git a/research/encoded-gaussian-directed-coefficient-audit/SOURCES.json b/research/encoded-gaussian-directed-coefficient-audit/SOURCES.json
new file mode 100644
index 0000000000..fde1908edb
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/SOURCES.json
@@ -0,0 +1,96 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/LICENSE",
+      "usage": "input",
+      "git_blob": "0e259d42c996742e9e3cba14c677129b2c1b6311",
+      "sha256": "a2010f343487d3f7618affe54f789f5487602331c0a8d03f49e9a7c547cf0499"
+    },
+    {
+      "path": "references/semantic-bulk/rad20/NOTICE",
+      "usage": "input",
+      "git_blob": "544634f5f3001c50330413f22dc0070e07c46738",
+      "sha256": "82fc72aff49769ae82a8ce886846d9bd0601827a09c955042d26a61177d14369"
+    },
+    {
+      "path": "research/gaussian-scalar-backend-audit/README.md",
+      "usage": "input",
+      "git_blob": "35d8acdec29207a95dca69f1403c70acd9a307fc",
+      "sha256": "c8afcb07053ee3ca797ee5d65084a6e047fd046efb4e9591154c30a0c194a710"
+    },
+    {
+      "path": "research/physical-gaussian-core/PROOF.md",
+      "usage": "input",
+      "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889",
+      "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a"
+    },
+    {
+      "path": "research/physical-gaussian-core/README.md",
+      "usage": "input",
+      "git_blob": "94caa778ca1eedcbbb3953db5cb215d3206ec0b6",
+      "sha256": "ce063e3796bdcea206959918915826ae75c1bcbd74736913e5b330aa04fb5791"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_exponentials.py",
+      "usage": "input",
+      "git_blob": "8f0f32d7090554b47c112142e300c88fb8e5db4d",
+      "sha256": "f7a27cacbb27c0cfa4a63054e83feba2beae91b3fa9d3c37f903620b3899e67b"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_matrix.py",
+      "usage": "input",
+      "git_blob": "fc41183a42f5e1af5ea2294c295a0519abbcdb6c",
+      "sha256": "5bb982c6f36083b646bd5a5ab2ea4059c203fa0cc824e9f28132c0f323824bac"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rationals.py",
+      "usage": "input",
+      "git_blob": "053404d91c1bef0d4bb0f6647491847bf5879aaf",
+      "sha256": "6f9a380c8c7b4233c3bc338a6206d65cc85bee2e4f5625c2a212065f04f4b73d"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_sources.py",
+      "usage": "input",
+      "git_blob": "ce521f91997775e189f984ba7dd68a15bf9ecd9b",
+      "sha256": "c5889a97a11a9c6c6c44deb8a2042498ddc3f55703de15269132b8f198e24b15"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/branchfree-source.tar",
+      "usage": "input",
+      "git_blob": "48dc77f5145d649bfed6745e38ab18b11772d597",
+      "sha256": "e6cdacd59a067189a99bfe03f4448913bb8d518ed4a9b1d981a68c5c666529c7"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/word-export.tar",
+      "usage": "input",
+      "git_blob": "885794cf3328941209034ee2d946ed76dbea8ce3",
+      "sha256": "d428e8b6aef4d348fa2e922ca64c4cfd634bbb2f0c150033273e65fcf4600b49"
+    },
+    {
+      "path": "research/schur-boundary-residual/fixture.py",
+      "usage": "input",
+      "git_blob": "69a50b6471c170097d6b97e2e2bfc66faefd30aa",
+      "sha256": "3d59d56c088e989819fc48d348b0969a6c38dd37cb0d14660abeb14e34ce5130"
+    }
+  ]
+}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/TASK.json b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
new file mode 100644
index 0000000000..e4ad3272bb
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "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": "Independent encoded Machin/Taylor growth and decay coefficient contract at actual Axis arguments.",
+  "scope_change_reason": "Released production coefficient question; distinct encoded backend and growth/shift domain from prior normalized host decay audit.",
+  "bottleneck_link": "Discharges actual scalar coefficient enclosure premise upstream of old-H perturbation and rowgap.",
+  "budget_minutes": 60,
+  "stop_rule": "TODO",
+  "outcome": "completed",
+  "evidence": "Quantified PROOF.md, frozen independent oracle, actual encoded Axis and boundary-call receipts.",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Can actual weighted ratios and cross-cell coefficient errors be composed into the production original-H perturbation bound?",
+      "why_it_matters": "Scalar enclosures alone do not prove the matrix rowgap.",
+      "first_step": "Bind positive rounded weights and every actual ratio to ideal coefficient intervals.",
+      "blocked_by": "Global matrix ideal gap and full production composition remain separate."
+    }
+  ]
+}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/oracle.py b/research/encoded-gaussian-directed-coefficient-audit/oracle.py
new file mode 100644
index 0000000000..99d6064240
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/oracle.py
@@ -0,0 +1,72 @@
+"""Independent rational arcsine / alternating-decay oracle. Apache-2.0.
+JoyboyBrian with substantial OpenAI Codex assistance. No source imports.
+"""
+from fractions import Fraction as Q
+from functools import lru_cache
+
+
+def need(ok,why):
+    if not ok:raise ValueError(why)
+
+
+def down(x,T):return Q((x*(1<<T)).__floor__(),1<<T)
+def up(x,T):return Q((x*(1<<T)).__ceil__(),1<<T)
+
+
+@lru_cache(None)
+def pi_box(T):
+    # pi=6 asin(1/2). Positive successive-term ratio is <1/4.
+    term=Q(1,2);total=Q();n=0
+    while True:
+        total+=term
+        term*=Q((2*n+1)**2,8*(n+1)*(2*n+3));n+=1
+        if 8*term<Q(1,1<<(T+4)):break
+    return down(6*total,T),up(6*total+8*term,T)
+
+
+def decay_point(x,T):
+    need(0<=x<=Q(1,4),'independent alternating range')
+    # Even/odd partial sums straddle exp(-x); no source positive series.
+    term=Q(1);total=Q(1);n=0
+    while True:
+        n+=1;term*=x/n
+        total+=term if n%2==0 else -term
+        following=term*x/(n+1)
+        other=total-following if n%2==0 else total+following
+        if following<Q(1,1<<(T+4)):
+            return down(min(total,other),T),up(max(total,other),T)
+
+
+def interval(f,P,growth=False,sigma=0):
+    need(f>=0 and type(P) is int and P>=1 and type(sigma) is int and sigma>=0,'oracle domain')
+    if f==0:return Q(1,1<<sigma),Q(1,1<<sigma)
+    F=max(1,f.__ceil__());T=P+16*F+48
+    lo,hi=pi_box(T);xlo=f*lo;xhi=f*hi;k=0
+    while xhi>Q(1,4):xlo/=2;xhi/=2;k+=1
+    lower=decay_point(xhi,T)[0];upper=decay_point(xlo,T)[1]
+    for _ in range(k):lower=down(lower*lower,T);upper=up(upper*upper,T)
+    need(lower>0,'oracle reciprocal denominator')
+    if growth:lower,upper=1/upper,1/lower
+    lower/=1<<sigma;upper/=1<<sigma
+    need(upper-lower<Q(1,1<<(P+10)),'independent oracle resolution')
+    return lower,upper
+
+
+def self_tests():
+    lo,hi=pi_box(80)
+    need(Q(314159,100000)<lo<hi<Q(314160,100000),'independent pi familiar rational bounds')
+    cases=0
+    for f in (Q(0),Q(1,1000),Q(1,4),Q(1),Q(4)):
+        for P in (1,8,24):
+            for sigma in (0,3):
+                dec=interval(f,P,False,sigma);grow=interval(f,P,True,sigma)
+                need(dec[0]<=dec[1] and grow[0]<=grow[1],'ordered independent intervals')
+                need(dec[0]*grow[0]<=Q(1,1<<(2*sigma))<=dec[1]*grow[1],'growth decay reciprocal identity')
+                cases+=2
+    # Exact alternating tail sign and scaling controls.
+    l,u=decay_point(Q(0),32);need(l==u==1,'zero alternating series')
+    need(interval(Q(0),4,True,7)==(Q(1,128),Q(1,128)),'binary normalization exact')
+    return {'intervals':cases,'pi_method':'positive arcsine with geometric tail','exp_method':'alternating decay with rational endpoint evaluation and outward squaring'}
+
+
+if __name__=='__main__':print(self_tests())

From 9fb51bc0e3c30f650ea2a44acc820731f677e9c8 Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Sat, 24 Oct 2026 21:52:41 -0700
Subject: [PATCH 2/3] Verify actual encoded coefficient calls against frozen
 oracle and rejection controls

---
 .../PROOF.md                                  |   9 +-
 .../README.md                                 |   4 +
 .../RESULT.json                               | 890 ++++++++++++++++++
 .../TASK.json                                 |   2 +-
 .../VERIFY.json                               |  54 ++
 .../producer.py                               | 117 +++
 .../test_package.py                           |  29 +
 .../verify.py                                 |  42 +
 8 files changed, 1143 insertions(+), 4 deletions(-)
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/RESULT.json
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/VERIFY.json
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/producer.py
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/test_package.py
 create mode 100644 research/encoded-gaussian-directed-coefficient-audit/verify.py

diff --git a/research/encoded-gaussian-directed-coefficient-audit/PROOF.md b/research/encoded-gaussian-directed-coefficient-audit/PROOF.md
index ad6a4df7bb..fd7f576039 100644
--- a/research/encoded-gaussian-directed-coefficient-audit/PROOF.md
+++ b/research/encoded-gaussian-directed-coefficient-audit/PROOF.md
@@ -16,7 +16,7 @@ integers l<=u such that, with eta=2^-P,
     u-l <= 2.
 
 Consequently coefficient, which returns l, has downward error <2eta. All
-constructor, Taylor-range, interval-width and final-width checks succeed
+Exponentials constructor, Taylor-range, interval-width and final-width checks succeed
 mathematically. Termination is for every finite represented input, with the
 encoded Count/Rational operations and ownership semantics retained. There
 is no assertion that arbitrary non-admitted input succeeds. In particular
@@ -108,7 +108,8 @@ keeps the original enclosure. Both branches therefore have width <eta/2.
 Scaling by 2^-sigma does not increase it. Final outward P-grid rounding adds
 less than 2eta to width. The endpoint difference is an integer number of
 eta units and is strictly below 5eta/2, hence at most 2eta. The actual source
-accepts difference<=3; the proved tighter bound implies that check. The
+accepts difference<=3; the proved tighter bound implies that check. The pre-final normalized interval has width <eta/2 and the final
+lower floor loses <eta, so coefficient error is <3eta/2<2eta. The
 lower coefficient is an approximation, not necessarily the exact irrational
 floor. Changing this contract to exact-floor equality would be unjustified.
 
@@ -134,7 +135,9 @@ For a cross-cell entry let delta be the chosen signed cyclic distance,
 The nearest-integer property gives |beta_j+m|>=|beta_j|, including ties.
 Thus f=u[(rho*delta+beta_i)^2-beta_j^2]>=0, while
 f<=u(rho*w+1/2)^2. Direct and wrapped branches both satisfy the prepared
-domain. Zero kernel/diagonal entries bypass the backend exactly as in source.
+domain. The zero-distance kernel and the H matrix diagonal bypass the backend
+by returning exactly one. The normalized diagonal still invokes growth,
+including at beta=0.
 This proves the coefficient-call domain for every admitted Axis tuple. It
 does not prove nonzero rounded weights for arbitrary P: positive exact
 weights may truncate to zero. That is a separate Axis admission check and
diff --git a/research/encoded-gaussian-directed-coefficient-audit/README.md b/research/encoded-gaussian-directed-coefficient-audit/README.md
index 43fe61bffb..5bc6441a3a 100644
--- a/research/encoded-gaussian-directed-coefficient-audit/README.md
+++ b/research/encoded-gaussian-directed-coefficient-audit/README.md
@@ -31,6 +31,10 @@ frozen oracle are authenticated before imports. RESULT.json is mandatory and
 compared as complete typed JSON. The original source and nested archives remain
 unchanged; source-history and export checks use explicit input base32890bc.
 
+Actual finite replay passed with 19 Axis calls and 10 isolated calls,
+including P=1, growth/decay, scale513 and four domain rejections. All
+source intervals contain the independent finer intervals.
+
 ## Limits
 
 This audits the encoded physical backend, distinct from the normalized host
diff --git a/research/encoded-gaussian-directed-coefficient-audit/RESULT.json b/research/encoded-gaussian-directed-coefficient-audit/RESULT.json
new file mode 100644
index 0000000000..f9dc2511ea
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/RESULT.json
@@ -0,0 +1,890 @@
+{
+  "oracle_self_tests": {
+    "intervals": 60,
+    "pi_method": "positive arcsine with geometric tail",
+    "exp_method": "alternating decay with rational endpoint evaluation and outward squaring"
+  },
+  "producer": {
+    "axis": {
+      "s": 13,
+      "t": 14,
+      "u": 1,
+      "w": 1,
+      "P": 24,
+      "F": 4,
+      "calls": 19
+    },
+    "rows": [
+      {
+        "lower": 617,
+        "upper": 618,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          13,
+          4
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 25,
+        "early": 1,
+        "oracle": [
+          [
+            1602604155993210011089819128841869261,
+            43556142965880123323311949751266331066368
+          ],
+          [
+            3205208311986420022179638257683738523,
+            87112285931760246646623899502532662132736
+          ]
+        ]
+      },
+      {
+        "lower": 4194304,
+        "upper": 4194305,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          0,
+          1
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 1,
+        "early": 1,
+        "oracle": [
+          [
+            1,
+            4
+          ],
+          [
+            1,
+            4
+          ]
+        ]
+      },
+      {
+        "lower": 786,
+        "upper": 787,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          165,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 25,
+        "early": 1,
+        "oracle": [
+          [
+            2040695899707853805037621937286267621,
+            43556142965880123323311949751266331066368
+          ],
+          [
+            4081391799415707610075243874572535243,
+            87112285931760246646623899502532662132736
+          ]
+        ]
+      },
+      {
+        "lower": 4273002,
+        "upper": 4273003,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          1,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 13,
+        "early": 1,
+        "oracle": [
+          [
+            77371252455336267181195264,
+            303785041746558429756943661
+          ],
+          [
+            19342813113834066795298816,
+            75946260436639607439235915
+          ]
+        ]
+      },
+      {
+        "lower": 1622,
+        "upper": 1623,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          153,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 25,
+        "early": 1,
+        "oracle": [
+          [
+            64291630923230896112000039534763,
+            664613997892457936451903530140172288
+          ],
+          [
+            128583261846461792224000079069527,
+            1329227995784915872903807060280344576
+          ]
+        ]
+      },
+      {
+        "lower": 4518068,
+        "upper": 4518069,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          4,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 14,
+        "early": 1,
+        "oracle": [
+          [
+            77371252455336267181195264,
+            287307317297427559100691053
+          ],
+          [
+            19342813113834066795298816,
+            71826829324356889775172763
+          ]
+        ]
+      },
+      {
+        "lower": 5433,
+        "upper": 5434,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          133,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 24,
+        "early": 1,
+        "oracle": [
+          [
+            430471669518440063184353707360909,
+            1329227995784915872903807060280344576
+          ],
+          [
+            215235834759220031592176853680455,
+            664613997892457936451903530140172288
+          ]
+        ]
+      },
+      {
+        "lower": 4958142,
+        "upper": 4958143,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          9,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 15,
+        "early": 1,
+        "oracle": [
+          [
+            19342813113834066795298816,
+            65451639749823288281681351
+          ],
+          [
+            77371252455336267181195264,
+            261806558999293153126725403
+          ]
+        ]
+      },
+      {
+        "lower": 29493,
+        "upper": 29494,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          105,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 23,
+        "early": 1,
+        "oracle": [
+          [
+            1168365621247937250586281603477003,
+            664613997892457936451903530140172288
+          ],
+          [
+            2336731242495874501172563206954007,
+            1329227995784915872903807060280344576
+          ]
+        ]
+      },
+      {
+        "lower": 5647179,
+        "upper": 5647180,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          16,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 16,
+        "early": 1,
+        "oracle": [
+          [
+            77371252455336267181195264,
+            229862376580059566971409395
+          ],
+          [
+            4835703278458516698824704,
+            14366398536253722935713087
+          ]
+        ]
+      },
+      {
+        "lower": 259595,
+        "upper": 259596,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          69,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 22,
+        "early": 1,
+        "oracle": [
+          [
+            39228986904352558088715936081,
+            2535301200456458802993406410752
+          ],
+          [
+            313831895234820464709727488651,
+            20282409603651670423947251286016
+          ]
+        ]
+      },
+      {
+        "lower": 6675606,
+        "upper": 6675607,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          25,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 17,
+        "early": 1,
+        "oracle": [
+          [
+            4835703278458516698824704,
+            12153148768530951036601943
+          ],
+          [
+            77371252455336267181195264,
+            194450380296495216585631085
+          ]
+        ]
+      },
+      {
+        "lower": 3704842,
+        "upper": 3704843,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          25,
+          52
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 19,
+        "early": 1,
+        "oracle": [
+          [
+            68342277623879883645296687,
+            309485009821345068724781056
+          ],
+          [
+            68342277623879883645296695,
+            309485009821345068724781056
+          ]
+        ]
+      },
+      {
+        "lower": 8190233,
+        "upper": 8190234,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "weight_pair",
+        "argument": [
+          36,
+          169
+        ],
+        "growth": true,
+        "sigma": 2,
+        "steps": 18,
+        "early": 1,
+        "oracle": [
+          [
+            77371252455336267181195264,
+            158490499948333292985037105
+          ],
+          [
+            19342813113834066795298816,
+            39622624987083323246259275
+          ]
+        ]
+      },
+      {
+        "lower": 569365,
+        "upper": 569366,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "kernel_entry",
+        "argument": [
+          14,
+          13
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 21,
+        "early": 1,
+        "oracle": [
+          [
+            172080308775958645006079541799,
+            5070602400912917605986812821504
+          ],
+          [
+            688321235103834580024318167199,
+            20282409603651670423947251286016
+          ]
+        ]
+      },
+      {
+        "lower": 447135,
+        "upper": 447136,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "matrix_entry",
+        "argument": [
+          15,
+          13
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 22,
+        "early": 1,
+        "oracle": [
+          [
+            270277034464984594309179375403,
+            10141204801825835211973625643008
+          ],
+          [
+            540554068929969188618358750809,
+            20282409603651670423947251286016
+          ]
+        ]
+      },
+      {
+        "lower": 19322,
+        "upper": 19323,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "matrix_entry",
+        "argument": [
+          28,
+          13
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 24,
+        "early": 1,
+        "oracle": [
+          [
+            1530885528085410555222684048705437,
+            1329227995784915872903807060280344576
+          ],
+          [
+            1530885528085410555222684048705439,
+            1329227995784915872903807060280344576
+          ]
+        ]
+      },
+      {
+        "lower": 19322,
+        "upper": 19323,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "matrix_entry",
+        "argument": [
+          28,
+          13
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 24,
+        "early": 1,
+        "oracle": [
+          [
+            1530885528085410555222684048705437,
+            1329227995784915872903807060280344576
+          ],
+          [
+            1530885528085410555222684048705439,
+            1329227995784915872903807060280344576
+          ]
+        ]
+      },
+      {
+        "lower": 725009,
+        "upper": 725010,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "matrix_entry",
+        "argument": [
+          1,
+          1
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 21,
+        "early": 1,
+        "oracle": [
+          [
+            6687029959141178880805505,
+            154742504910672534362390528
+          ],
+          [
+            13374059918282357761611013,
+            309485009821345068724781056
+          ]
+        ]
+      },
+      {
+        "lower": 16777215,
+        "upper": 16777216,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "isolated",
+        "argument": [
+          0,
+          1
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 1,
+        "early": 1,
+        "oracle": [
+          [
+            1,
+            1
+          ],
+          [
+            1,
+            1
+          ]
+        ]
+      },
+      {
+        "lower": 5887457,
+        "upper": 5887458,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "isolated",
+        "argument": [
+          1,
+          3
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 19,
+        "early": 1,
+        "oracle": [
+          [
+            108604419971115036046619605,
+            309485009821345068724781056
+          ],
+          [
+            108604419971115036046619613,
+            309485009821345068724781056
+          ]
+        ]
+      },
+      {
+        "lower": 4810888718777,
+        "upper": 4810888718778,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "isolated",
+        "argument": [
+          4,
+          1
+        ],
+        "growth": true,
+        "sigma": 0,
+        "steps": 26,
+        "early": 1,
+        "oracle": [
+          [
+            43556142965880123323311949751266331066368,
+            151895182238008254402877165473660023
+          ],
+          [
+            87112285931760246646623899502532662132736,
+            303790364476016508805754330947320045
+          ]
+        ]
+      },
+      {
+        "lower": 58,
+        "upper": 59,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "isolated",
+        "argument": [
+          4,
+          1
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 26,
+        "early": 1,
+        "oracle": [
+          [
+            303790364476016508805754330947320045,
+            87112285931760246646623899502532662132736
+          ],
+          [
+            151895182238008254402877165473660023,
+            43556142965880123323311949751266331066368
+          ]
+        ]
+      },
+      {
+        "lower": 0,
+        "upper": 1,
+        "P": 24,
+        "F": 4,
+        "R": 196,
+        "k": 8,
+        "N": 74,
+        "J": 57,
+        "tag": "isolated",
+        "argument": [
+          1,
+          3
+        ],
+        "growth": true,
+        "sigma": 513,
+        "steps": 19,
+        "early": 1,
+        "oracle": [
+          [
+            1,
+            9410130746921251361955786132368313054228091382293749338846689196342624762453630507826643424445295405189997323678824015961287019010457557181497471523618816
+          ],
+          [
+            1,
+            9410130746921251361955785439200889524024376487690203303075763337233355918499486715206748270789968453783591563685222489926392494662654816830604514280079360
+          ]
+        ]
+      },
+      {
+        "lower": 1,
+        "upper": 2,
+        "P": 1,
+        "F": 1,
+        "R": 115,
+        "k": 6,
+        "N": 47,
+        "J": 37,
+        "tag": "isolated",
+        "argument": [
+          0,
+          1
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 1,
+        "early": 1,
+        "oracle": [
+          [
+            1,
+            1
+          ],
+          [
+            1,
+            1
+          ]
+        ]
+      },
+      {
+        "lower": 0,
+        "upper": 1,
+        "P": 1,
+        "F": 1,
+        "R": 115,
+        "k": 6,
+        "N": 47,
+        "J": 37,
+        "tag": "isolated",
+        "argument": [
+          1,
+          3
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 14,
+        "early": 1,
+        "oracle": [
+          [
+            1618331968353912771,
+            4611686018427387904
+          ],
+          [
+            404582992088478193,
+            1152921504606846976
+          ]
+        ]
+      },
+      {
+        "lower": 46,
+        "upper": 47,
+        "P": 1,
+        "F": 1,
+        "R": 115,
+        "k": 6,
+        "N": 47,
+        "J": 37,
+        "tag": "isolated",
+        "argument": [
+          1,
+          1
+        ],
+        "growth": true,
+        "sigma": 0,
+        "steps": 17,
+        "early": 1,
+        "oracle": [
+          [
+            36893488147419103232,
+            1594312181268019411
+          ],
+          [
+            2305843009213693952,
+            99644511329251213
+          ]
+        ]
+      },
+      {
+        "lower": 0,
+        "upper": 1,
+        "P": 1,
+        "F": 1,
+        "R": 115,
+        "k": 6,
+        "N": 47,
+        "J": 37,
+        "tag": "isolated",
+        "argument": [
+          1,
+          1
+        ],
+        "growth": false,
+        "sigma": 0,
+        "steps": 17,
+        "early": 1,
+        "oracle": [
+          [
+            99644511329251213,
+            2305843009213693952
+          ],
+          [
+            1594312181268019411,
+            36893488147419103232
+          ]
+        ]
+      },
+      {
+        "lower": 0,
+        "upper": 1,
+        "P": 1,
+        "F": 1,
+        "R": 115,
+        "k": 6,
+        "N": 47,
+        "J": 37,
+        "tag": "isolated",
+        "argument": [
+          1,
+          3
+        ],
+        "growth": true,
+        "sigma": 513,
+        "steps": 14,
+        "early": 1,
+        "oracle": [
+          [
+            1,
+            9410130746921251365195598249162080745989529452071773691135897823780810106508211580895257427432068245602771817695395706579190245216275391827373883398291456
+          ],
+          [
+            1,
+            9410130746921251359380888454797225621594938988967737416306766938282265624256289987450143122524884858993243411985287182093090072366145968359097070369374208
+          ]
+        ]
+      }
+    ],
+    "domain_rejections": [
+      [
+        24,
+        4,
+        -1
+      ],
+      [
+        24,
+        4,
+        5
+      ],
+      [
+        1,
+        1,
+        -1
+      ],
+      [
+        1,
+        1,
+        2
+      ]
+    ],
+    "controls": [
+      "growth-sign",
+      "binary-normalization",
+      "collapsed-upper-endpoint",
+      "actual-cross-cell-calls"
+    ],
+    "cleanup": "owned scratch blank, markers erased, heads restored"
+  }
+}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/TASK.json b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
index e4ad3272bb..4667120c6d 100644
--- a/research/encoded-gaussian-directed-coefficient-audit/TASK.json
+++ b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
@@ -58,7 +58,7 @@
   "scope_change_reason": "Released production coefficient question; distinct encoded backend and growth/shift domain from prior normalized host decay audit.",
   "bottleneck_link": "Discharges actual scalar coefficient enclosure premise upstream of old-H perturbation and rowgap.",
   "budget_minutes": 60,
-  "stop_rule": "TODO",
+  "stop_rule": "20-minute proof/source feasibility gate; never infer uniform enclosure or global rowgap from finite checks.",
   "outcome": "completed",
   "evidence": "Quantified PROOF.md, frozen independent oracle, actual encoded Axis and boundary-call receipts.",
   "author": "JoyboyBrian",
diff --git a/research/encoded-gaussian-directed-coefficient-audit/VERIFY.json b/research/encoded-gaussian-directed-coefficient-audit/VERIFY.json
new file mode 100644
index 0000000000..05e7e4a294
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/VERIFY.json
@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "references/semantic-bulk/rad20/LICENSE",
+    "references/semantic-bulk/rad20/NOTICE",
+    "research/gaussian-scalar-backend-audit/README.md",
+    "research/physical-gaussian-core/PROOF.md",
+    "research/physical-gaussian-core/README.md",
+    "research/physical-gaussian-core/gaussian_axis.py",
+    "research/physical-gaussian-core/gaussian_exponentials.py",
+    "research/physical-gaussian-core/gaussian_matrix.py",
+    "research/physical-gaussian-core/gaussian_rationals.py",
+    "research/physical-gaussian-core/gaussian_sources.py",
+    "research/physical-gaussian-core/inputs/branchfree-source.tar",
+    "research/physical-gaussian-core/inputs/word-export.tar",
+    "research/schur-boundary-residual/fixture.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Actual encoded Axis coefficient calls plus boundary cases and independent interval containment."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Identical source and oracle receipt with assertions disabled."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 30,
+      "checks": "Missing/typed-mutated receipt, source corruption and frozen-oracle corruption; normal/O and empty PATH, no physical rerun."
+    }
+  ]
+}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/producer.py b/research/encoded-gaussian-directed-coefficient-audit/producer.py
new file mode 100644
index 0000000000..342df9162e
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/producer.py
@@ -0,0 +1,117 @@
+"""Observer-only actual Axis/Exponentials execution; no oracle values supplied."""
+from collections import Counter
+from fractions import Fraction as Q
+import oracle
+
+
+def arguments(s,t,u,w):
+    rho=Q(t,s);theta=rho-1;beta=[rho*j-(rho*j+Q(1,2)).__floor__() for j in range(s)]
+    phase=[(rho*j+Q(1,2)).__floor__()-j for j in range(s)]
+    F=max((u/(4*theta)).__ceil__(),(u*(rho*w+Q(1,2))**2).__ceil__())
+    out=[]
+    for j,b in enumerate(beta):
+        if s-j<j:continue
+        out.extend([('weight_pair',u*(Q(1,4)-b*b)/theta,False,0),('weight_pair',u*b*b,True,2*u)])
+    for d in range(1,w+1):out.append(('kernel_entry',u*rho*d*d,False,0))
+    for i in range(s):
+        for j in range(s):
+            if i==j:continue
+            delta=j-i;direct=abs(delta)<=w
+            if not direct:
+                if s-abs(delta)>w:continue
+                delta=delta-s if delta>0 else delta+s
+            if direct and phase[i]==phase[j]:continue
+            f=u*((rho*delta+beta[i])**2-beta[j]**2)
+            oracle.need(0<=f<=F,'rational Axis argument domain')
+            out.append(('matrix_entry',f,False,0))
+    return F,out
+
+
+def run(helper):
+    from cardinal_counts import Count
+    from check_support import no_decode
+    from gaussian_axis import Axis
+    from gaussian_exponentials import Exponentials
+    from gaussian_rationals import Rational
+    from ring_words import Signed
+    from router_metadata import owned
+    from scratch_pool import ScratchPool
+    from session import OuterScope,erase_marker,sealed_constructors
+    raw=[];tag=['isolated'];saved=Exponentials.grid_interval
+    def snap(v):return helper.tape_bytes(v.tape)
+    def wrapped(self,f,growth=False,binary_scale=None):
+        argument=(f.numerator.negative,snap(f.numerator.magnitude),snap(f.denominator))
+        scale=None if binary_scale is None else snap(binary_scale)
+        steps,early=self.taylor_steps,self.early_stops
+        result=saved(self,f,growth,binary_scale)
+        raw.append({'tag':tag[0],'argument':argument,'growth':growth,'scale':scale,
+                    'lower':snap(result[0]),'upper':snap(result[1]),
+                    'P':snap(self.precision),'F':snap(self.argument_bound),
+                    'R':snap(self.R),'k':snap(self.k),'N':snap(self.terms),'J':snap(self.J),
+                    'steps':self.taylor_steps-steps,'early':self.early_stops-early})
+        return result
+    saved_methods={name:getattr(Axis,name) for name in ('weight_pair','kernel_entry','matrix_entry')}
+    def label(name,method):
+        def call(self,*args):
+            old=tag[0];tag[0]=name
+            try:return method(self,*args)
+            finally:tag[0]=old
+        return call
+    Exponentials.grid_interval=wrapped
+    for name,method in saved_methods.items():setattr(Axis,name,label(name,method))
+    pool=ScratchPool(512);scope=OuterScope(pool);axis=None;failures=[]
+    try:
+        with owned(*(Count.literal(v)for v in (13,14,1,1,24))) as params:
+            with sealed_constructors(),scope.installed():
+                try:
+                    with no_decode():axis=Axis(*params,pool)
+                    for P,F in ((24,4),(1,1)):
+                        with owned(Count.literal(P),Count.literal(F)) as (precision,bound):
+                            exp=None
+                            try:
+                                with no_decode():exp=Exponentials(precision,bound)
+                                for numerator,denominator,growth,sigma in ((0,1,False,0),(1,3,False,0),(F,1,True,0),(F,1,False,0),(1,3,True,513)):
+                                    with owned(Rational(Signed(Count.literal(numerator)),Count.literal(denominator)),Count.literal(sigma)) as (f,scale):
+                                        with no_decode():lo,hi=exp.grid_interval(f,growth,scale)
+                                        lo.close();hi.close()
+                                for fval in (-1,F+1):
+                                    with owned(Rational.literal(fval)) as (f,):
+                                        try:
+                                            with no_decode():exp.positive_interval(f)
+                                        except ValueError:failures.append((P,F,fval))
+                                        else:raise ValueError('invalid source argument accepted')
+                            finally:
+                                if exp is not None:exp.close()
+                finally:
+                    if axis is not None:axis.close()
+                    pool.empty()
+    finally:
+        Exponentials.grid_interval=saved
+        for name,method in saved_methods.items():setattr(Axis,name,method)
+    for tape in pool.tapes:erase_marker(tape)
+    oracle.need(not pool.live and all(t.head==1 and all(x==4 for x in t.cells)for t in pool.tapes),'all source scratch restored')
+    rows=[]
+    for record in raw:
+        sign,n,d=record['argument'];f=Q((-1 if sign else 1)*helper.count(n),helper.count(d))
+        row={key:helper.count(record[key])for key in ('lower','upper','P','F','R','k','N','J')}
+        row.update(tag=record['tag'],argument=[f.numerator,f.denominator],growth=record['growth'],sigma=0 if record['scale'] is None else helper.count(record['scale']),steps=record['steps'],early=record['early'])
+        oracle.need(0<=f<=row['F'],'actual argument admitted')
+        lo,hi=oracle.interval(f,row['P'],row['growth'],row['sigma'])
+        oracle.need(Q(row['lower'],1<<row['P'])<=lo<=hi<=Q(row['upper'],1<<row['P']),'entire independent oracle enclosed')
+        oracle.need(0<=row['upper']-row['lower']<=2,'proved two-target-ulp width')
+        X=4*row['F'];k=(8*(X+1)-1).bit_length();H=row['P']+X+k+16;c=(H-1).bit_length();R=row['P']+4*X+4*k+2*c+64
+        oracle.need((row['R'],row['k'],row['N'],row['J'])==(R,k,(R+2)//3+8,(R+3)//4+8),'actual precision and ceiling policy')
+        row['oracle']=[[x.numerator,x.denominator]for x in (lo,hi)];rows.append(row)
+    F,expected=arguments(13,14,1,1)
+    actual=[(r['tag'],Q(*r['argument']),r['growth'],r['sigma'])for r in rows if r['tag']!='isolated']
+    oracle.need(Counter(actual)==Counter(expected),'actual Axis argument multiset including reflected reuse and wrap')
+    oracle.need(len(failures)==4,'source domain rejection count')
+    growth=next(r for r in rows if r['tag']=='isolated' and r['P']==24 and r['growth'] and r['argument']==[4,1])
+    decay=oracle.interval(Q(4),24,False)
+    oracle.need(decay[1]<Q(growth['lower'],1<<24),'wrong growth sign rejected')
+    scaled=next(r for r in rows if r['P']==24 and r['sigma']==513)
+    unscaled=oracle.interval(Q(*scaled['argument']),24,True)
+    oracle.need(unscaled[0]>Q(scaled['upper'],1<<24),'omitted binary normalization rejected')
+    oracle.need(any(Q(*r['oracle'][0])>Q(r['lower'],1<<r['P']) for r in rows),'collapsed upper endpoint rejected')
+    oracle.need(any(r['tag']=='matrix_entry' for r in rows),'cross-cell backend actually exercised')
+    return {'axis':{'s':13,'t':14,'u':1,'w':1,'P':24,'F':F,'calls':len(actual)},'rows':rows,'domain_rejections':failures,'controls':['growth-sign','binary-normalization','collapsed-upper-endpoint','actual-cross-cell-calls'],'cleanup':'owned scratch blank, markers erased, heads restored'}
diff --git a/research/encoded-gaussian-directed-coefficient-audit/test_package.py b/research/encoded-gaussian-directed-coefficient-audit/test_package.py
new file mode 100644
index 0000000000..5b549a353a
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/test_package.py
@@ -0,0 +1,29 @@
+"""Cheap source/receipt controls; no actual coefficient replay."""
+import json,os,shutil,subprocess,sys,tempfile
+from pathlib import Path
+HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1]
+def need(ok,why):
+    if not ok:raise ValueError(why)
+def main():
+    count=0
+    with tempfile.TemporaryDirectory(prefix='coefficient-controls-') as directory:
+        root=Path(directory);p=root/'research'/HERE.name
+        shutil.copytree(HERE,p,ignore=shutil.ignore_patterns('__pycache__'))
+        for r in json.loads((HERE/'SOURCES.json').read_text())['files']:
+            if r['usage']=='input':
+                target=root/r['path'];target.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(ROOT/r['path'],target)
+        receipt=(p/'RESULT.json').read_bytes();source=root/'research/physical-gaussian-core/gaussian_exponentials.py';original=source.read_bytes();oracle=p/'oracle.py';frozen=oracle.read_bytes()
+        for opt in ([],['-O']):
+            command=[sys.executable,'-I','-B',*opt,str(p/'verify.py'),'--oracle-only']
+            def run(ok,phrase):
+                r=subprocess.run(command,cwd=root,env={**os.environ,'PATH':''},text=True,capture_output=True,timeout=10)
+                need((r.returncode==0)==ok and phrase in r.stdout+r.stderr,phrase+' '+r.stdout+r.stderr)
+            run(True,'PASS_ENCODED_GAUSSIAN_COEFFICIENT_AUDIT_ORACLE');count+=1
+            (p/'RESULT.json').unlink();run(False,'FileNotFoundError');count+=1
+            (p/'RESULT.json').write_bytes(receipt)
+            d=json.loads(receipt);d['oracle_self_tests']['intervals']=float(d['oracle_self_tests']['intervals']);(p/'RESULT.json').write_text(json.dumps(d));run(False,'complete typed receipt mismatch');count+=1
+            (p/'RESULT.json').write_bytes(receipt)
+            source.write_bytes(original+b'\nraise RuntimeError("UNAUTHENTICATED_SOURCE_EXECUTED")\n');run(False,'source hash research/physical-gaussian-core/gaussian_exponentials.py');count+=1;source.write_bytes(original)
+            oracle.write_bytes(frozen+b'\nraise RuntimeError("ALTERED_ORACLE_EXECUTED")\n');run(False,'frozen independent oracle');count+=1;oracle.write_bytes(frozen)
+    print('PASS_COEFFICIENT_PACKAGE_CONTROLS '+str(count))
+if __name__=='__main__':main()
diff --git a/research/encoded-gaussian-directed-coefficient-audit/verify.py b/research/encoded-gaussian-directed-coefficient-audit/verify.py
new file mode 100644
index 0000000000..d0aa89d928
--- /dev/null
+++ b/research/encoded-gaussian-directed-coefficient-audit/verify.py
@@ -0,0 +1,42 @@
+"""Authenticate before importing source; compare the full typed receipt."""
+import argparse,hashlib,importlib.util,json,sys,tempfile
+from pathlib import Path
+HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1]
+def need(ok,why):
+    if not ok:raise ValueError(why)
+def canonical(v):return json.dumps(v,sort_keys=True,separators=(',',':'),allow_nan=False)
+def sources():
+    for row in json.loads((HERE/'SOURCES.json').read_text())['files']:
+        if row['usage']=='input':
+            p=ROOT/row['path'];need(p.is_file() and not p.is_symlink() and hashlib.sha256(p.read_bytes()).hexdigest()==row['sha256'],'source hash '+row['path'])
+    frozen=json.loads((HERE/'ORACLE-FREEZE.json').read_text())
+    need(hashlib.sha256((HERE/'oracle.py').read_bytes()).hexdigest()==frozen['oracle_sha256'],'frozen independent oracle')
+def run(physical=True):
+    sources()
+    with tempfile.TemporaryDirectory(prefix='coefficient-pycache-') as temp:
+        old=sys.pycache_prefix;sys.pycache_prefix=temp
+        try:
+            sys.path.insert(0,str(HERE));import oracle
+            out={'oracle_self_tests':oracle.self_tests()}
+            if physical:
+                sys.path.insert(0,str(ROOT/'research/physical-gaussian-core'))
+                spec=importlib.util.spec_from_file_location('raw_snapshot_helper',ROOT/'research/schur-boundary-residual/fixture.py')
+                helper=importlib.util.module_from_spec(spec);spec.loader.exec_module(helper)
+                from gaussian_sources import opened
+                import producer
+                with opened():out['producer']=producer.run(helper)
+            return out
+        finally:sys.pycache_prefix=old
+
+def main():
+    p=argparse.ArgumentParser();p.add_argument('--record',type=Path);p.add_argument('--oracle-only',action='store_true');a=p.parse_args()
+    if a.record:need(not a.record.exists(),'record refuses overwrite')
+    else:expected=json.loads((HERE/'RESULT.json').read_text())
+    result=run(not a.oracle_only)
+    if a.record:a.record.write_text(json.dumps(result,indent=2)+'\n')
+    else:
+        if a.oracle_only:expected={'oracle_self_tests':expected['oracle_self_tests']}
+        need(canonical(result)==canonical(expected),'complete typed receipt mismatch')
+    print('PASS_ENCODED_GAUSSIAN_COEFFICIENT_AUDIT'+('_ORACLE'if a.oracle_only else''))
+    print(hashlib.sha256(canonical(result).encode()).hexdigest())
+if __name__=='__main__':main()

From 9fc80f1db55d4939c7b53c0799e6840cce35fbf8 Mon Sep 17 00:00:00 2001
From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com>
Date: Tue, 27 Oct 2026 22:05:37 -0700
Subject: [PATCH 3/3] Record resumed encoded coefficient proof review and exact
 source continuity

---
 .../README.md                                 | 19 +++++++++++++++++
 .../TASK.json                                 | 21 ++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/research/encoded-gaussian-directed-coefficient-audit/README.md b/research/encoded-gaussian-directed-coefficient-audit/README.md
index 5bc6441a3a..ee7d0056f2 100644
--- a/research/encoded-gaussian-directed-coefficient-audit/README.md
+++ b/research/encoded-gaussian-directed-coefficient-audit/README.md
@@ -35,6 +35,25 @@ Actual finite replay passed with 19 Axis calls and 10 isolated calls,
 including P=1, growth/decay, scale513 and four domain rejections. All
 source intervals contain the independent finer intervals.
 
+## Resumed source review
+
+The unpublished two-commit result was resumed on canonical main
+`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8, after
+[reclaiming its released discussion](https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19233742).
+All thirteen scientific inputs still match their frozen blobs; the original
+revision-7 card and selected-record pins remain historical provenance.
+A source review rechecked the encoded Machin signs and tail, Taylor early/fixed
+exit, squaring/reciprocal rounding and Axis half-tie/wrapped argument domains.
+It found no required scientific change. This is same-contributor review.
+The publication still requires both registered actual-source replay modes;
+metadata or oracle-only checks do not establish their success.
+
+The overlap refresh covered 341 open PRs, 5,722 discussion records and 8,348
+local notes. The normalized host scalar audit uses a different backend;
+PR4449's across-cell repair assumes an exponential contract. Neither is repeated
+here. The Tensor accuracy package's production-page admission remains separate.
+These coverage figures are a snapshot, not a novelty certificate.
+
 ## Limits
 
 This audits the encoded physical backend, distinct from the normalized host
diff --git a/research/encoded-gaussian-directed-coefficient-audit/TASK.json b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
index 4667120c6d..b8ef74479a 100644
--- a/research/encoded-gaussian-directed-coefficient-audit/TASK.json
+++ b/research/encoded-gaussian-directed-coefficient-audit/TASK.json
@@ -70,5 +70,24 @@
       "first_step": "Bind positive rounded weights and every actual ratio to ideal coefficient intervals.",
       "blocked_by": "Global matrix ideal gap and full production composition remain separate."
     }
-  ]
+  ],
+  "resumption": {
+    "upstream_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+    "priority_revision": 8,
+    "selected_record_pr": 6030,
+    "checked_at": "2026-10-28T05:05:36.727564+00:00",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3664#discussioncomment-19233742",
+    "previous_local_head": "b4596aa6d30f70ed160bf7f39b9f7ac7d62e2249",
+    "decision": "Complete and validate preserved result; all thirteen scientific input blobs unchanged. Keep frozen provenance and oracle.",
+    "review_scope": "Rechecked source-directed Machin signs/tail, positive Taylor early/fixed tails, squaring width, reciprocal direction, final rounding, Axis half ties and wrapped cross-cell domain; no scientific change required. Same-contributor review.",
+    "validation_obligation": "Both normal and optimized actual-source cold Git-free replays; oracle-only and source-binding checks are not substitutes.",
+    "overlap_coverage": {
+      "open_prs": 341,
+      "open_prs_fetched_at": "2026-10-28T04:53:27.931656+00:00",
+      "discussion_records": 5722,
+      "discussions_fetched_at": "2026-10-28T04:54:38.413598+00:00",
+      "local_notes": 8348,
+      "limits": "No exact duplicate found; no remote closed-PR body or arbitrary code-diff scan; not a novelty certificate."
+    }
+  }
 }