Independently check #4554's native stability lowering: exact gate norms, roundoff formulas, #956 moment and depth, shear bounds (no new κ)

research/pr4554-native-stability-check/.gitattributes

@@ -0,0 +1,2 @@
+PR4554-NATIVE-STABILITY.md -text
+PR956-PROFILE.json -text

research/pr4554-native-stability-check/PR4554-NATIVE-STABILITY.md

@@ -0,0 +1,118 @@
+# Direct bounded-word lowering of the closed rational Gaussian kernel
+
+This is a native arithmetic construction. It neither calls a Turing machine nor imports a TM simulation or multiplication routine. Its purpose is to turn an existing exact-scalar Gaussian/Walsh provider into a bounded-word algorithm with an explicit accuracy guarantee.
+
+## A literal sufficient class
+
+Consider a fixed finite provider template with:
+- arbitrary independent live arrays and explicitly cleared owned scratch;
+- fixed rational complex scalar ADD/SCALE operations, COPY, CLEAR, and exact monomial coordinate/quarter-phase operations;
+- recursive children that are exact unitary Gaussian kernels, possibly on disjoint fibers and conjugated by monomial operators;
+- a complete exact endpoint equal to the desired unitary kernel on every live input, with owned scratch erased.
+
+Read every coefficient from the literal finite template. Replace each rational scalar operation by its signed integer numerator/denominator calculation followed by rounding to a fixed binary grid. Multiplication/division here is on a fixed number of O(log n)-bit words, not on the full input. Nonzero fixed denominators are explicit integers. Metadata, address calculations and phase choices are integer computations.
+
+This class includes the rational Gaussian kernel in PR #956, whose nonchild coefficients are fixed with denominators supported on 2 and 3 and whose monomial phases are fourth roots of unity. It does not automatically include that PR's separate all-length cyclic Fourier compiler, which prepares additional input-length-dependent scalars through Newton/Toeplitz constructions.
+
+## Prefix norms are derived, not assumed
+
+For one scalar gate x<-x+a*y, the Euclidean operator norm is at most 1+|a|. For x<-a*x it is at most max(1,|a|), including the untouched coordinates. COPY has norm at most sqrt(2), CLEAR has norm 1, and coordinate/quarter-phase monomials have norm 1. These statements hold on all arbitrary inputs, not only on a chosen test vector.
+
+Replace |a| by the explicit rational upper bound |Re(a)|+|Im(a)|. Multiply these elementary bounds over the finite template; enlarge the result to an integer K>=2. This is an effective finite calculation from actual coefficient bytes. It bounds every prefix and suffix of that template when recursive children are treated as their exact unitary operators.
+
+A coefficientwise pass acts as a direct sum of the same fixed bank operation, so its norm bound does not grow with array length. Disjoint completed fiber calls form a direct sum of unitary maps. Completed owned-scratch macros have the extended map U_live direct-sum 0_owned after their initial clearing, hence norm at most 1. A primitive prefix inside one such macro is covered by the same fixed template bound.
+
+Classical base butterflies are grouped into completed unitary two-point kernels. Thus an arbitrarily long sequence of completed classical rounds does not multiply their prefix bounds: a partial primitive prefix lies inside only one current butterfly, while all completed rounds are unitary.
+
+Let D(e) be the maximum recursive call depth at rank e. An expanded prefix or suffix is inside at most one unfinished child at each depth. All its other completed children are unitary. Induction therefore gives the actual bound
+$$
+\|\text{expanded prefix}\|_2,\;\|\text{expanded suffix}\|_2
+\le K^{D(e)+1}.
+$$
+The exponent is depth, not total work. It does not hide an unproved stability oracle.
+
+## Explicit roundoff theorem
+
+Suppose the exact scalar count is at most
+$$
+M(e)\le A\,2^e(e+1)^\theta
+$$
+for fixed A>=1 and 0<theta<=1, and the input entries have absolute value at most 2^b. Use enough integral bits to cover the bound below. At each scalar update, compute the exact rational value from the stored approximants and round its two components toward zero at P fractional bits. Its local complex error is at most sqrt(2)*2^-P.
+
+By linearity, the total output error is the sum of these local errors transported through the exact remaining suffixes. Hence
+$$
+\|\widehat y-y\|_\infty
+\le \|\widehat y-y\|_2
+\le \sqrt2\,A\,2^e(e+1)^\theta K^{D(e)+1}\,2^{-P}.
+$$
+For requested error 2^-B it suffices to choose
+$$
+P=B+e+\lceil\log_2 A\rceil+
+  \lceil\theta\log_2(e+1)\rceil+
+  (D(e)+1)\lceil\log_2 K\rceil+3.
+$$
+
+Exact prefixes have magnitude at most K^(D+1)*sqrt(Z*2^e)*2^b, where fixed Z counts the simultaneously live array banks in the template. The same sum-of-local-errors argument bounds the approximate prefixes by this quantity plus the displayed error envelope. Thus an explicit integral width is
+$$
+I=b+\lceil e/2\rceil+
+ (D(e)+1)\lceil\log_2K\rceil+
+ \lceil\log_2(Z+1)\rceil+3.
+$$
+Increase it by a constant if output accuracy B is allowed to be negative; the intended use has B>=0. Every stored signed fixed-point numerator uses at most I+P+O(1) bits. Fixed rational numerators/denominators add only a template-dependent constant. Choose the physical word-width coefficient large enough for the exact intermediate numerator products, sums and divisions, or use a fixed number of limbs. This yields O(1) word instructions per scalar update.
+
+When e,b,B=O(log n), D(e)=O(log(e+2)), and A,K,Z are fixed before n, I+P=O(log n). Thus the finite-word program has the same asymptotic arithmetic operation count as the exact-scalar provider, with a computable constant and no TM or bit-cost-machine call. The cutoff can be enlarged until fixed template constants fit; below it the program uses direct unitary butterflies.
+
+## Instantiation of the actual closed provider
+
+PR #956 is pinned at fa4df77c9dfdbac93368d95dcb361e69b3b65464. Its optimized source uses m=73, largest child rank 48, productive stock W=58,899, and a complete exact profile. Its own all-input recurrence is
+$$
+t(e)\le\sum_r(H_r/W)t(rf(e))
++A\,[a+m+2\lceil\log_2(e+2)\rceil+1],
+$$
+where t(e)=T(e)/2^e, f(e)<=e/73 and the explicit integer-root certificate funds theta=1023/1024.
+
+The actual contraction gives
+$$
+D(e)\le 1+
+\left\lceil \frac{\log(e+1)}{\log(73/48)}\right\rceil.
+$$
+All source bank/owner constants are fixed before e. The elementary template bill supplies a finite upper bound for the number and coefficient sizes of its nonchild passes, from which K above is computable. In particular this does not replace a varying exact scalar of unknown condition by a word operation.
+
+Therefore this pinned rational native Gaussian/Walsh provider admits a bounded-word approximation program of work
+$$
+O\bigl(2^e(e+1)^{1023/1024}\bigr)
+$$
+and arbitrary requested error 2^-B with the explicit precision formula above. For the unnormalized Walsh conversion H_e=(1-i)^e D_e C_e D_e, first request kernel error 2^{-(B+ceil(e/2)+1)} and add ceil(e/2)+1 integral bits for the final scaling. Since |(1-i)^e|=2^{e/2}, the final error is at most 2^-B. These additions remain O(e). Quarter-phase D_e is exact. The power (1-i)^e is an exactly representable Gaussian integer and can be prepared by O(e) bounded-word updates, absorbed by the displayed work bound. No integer-multiplication theorem follows merely from this kernel statement.
+
+The same argument applies to a different *actually constructed* fixed rational provider and its proved recurrence; it does not assert a better profile or select unknown scalar coefficients. In particular, a critical-root compiler word must first have an actual admitted algebraic finite-word construction. Removing tape tariffs alone is not that construction.
+
+## Boundary for cyclic transforms and multiplication
+
+A separate cyclic transform requires explicit algorithms for roots, scalar preparation, conditioning, numerical errors, and convolution/recovery. Nonzero prepared denominators alone do not imply polynomially bounded inverse magnitudes. The exact-scalar PR #956 cyclic section does not supply the quantitative bounds needed here merely by proving nonzeroness.
+
+Root/phase tables and ordinary bounded-word FFT base multiplication can instead be constructed directly, but their complete caller and accuracy costs must be provided. No base multiplication TM is permitted in such an assembly. The nine/54-row TM outer ledger cannot simply have all costs divided by word width: each retained operation must be rebuilt as array/word arithmetic and re-invoiced.
+
+This is a positive finite-word native kernel theorem and a concrete assembly interface. It does not establish a new integer-multiplication exponent or worldwide priority for standard roundoff analysis.
+
+
+## A quantitative bound for the actual shear preparation
+
+One denominator family in the actual cyclic compiler is already quantitatively safe. Write mu=a+ib with a,b real, and put t1=1+mu*conjugate(mu), t2=mu-t1. Then
+$$
+t_1=1+a^2+b^2\ge1,\qquad
+\operatorname{Re}(t_2)=-[(a-1/2)^2+b^2+3/4]\le-3/4.
+$$
+Consequently |1/t1|<=1 and |1/t2|<=4/3, uniformly in mu. This is stronger than nonzeroness and is a direct sufficient stability bound for these two divisions. If mu is approximated within delta<=1 and |mu|<=U, then the induced t1 perturbation is at most (2U+1)delta; t2 adds another delta. Provided the t2 perturbation is at most 3/8, its reciprocal perturbation is at most (32/9) times that perturbation, by the identity 1/z-1/z'=(z'-z)/(zz'). Thus this shear preparation is polynomially conditioned whenever U is polynomially bounded. The Newton c-inverses and complete cyclic circuit still require their own quantitative analysis. Credit: ram_cost identified the completion-of-squares argument during this session.
+
+## Polyloglog overhead still retains a strict saving
+
+For completeness, a direct finite-word compiler need not retain a constant number of words to preserve an exponent saving. Suppose an actually constructed native transform on N data words has exact arithmetic work O(N (log N)^{1-kappa}) with fixed kappa>0, and an explicit numerical analysis and implementation bound every scalar update, preparation and packing overhead together by (loglog(N+4))^C for a fixed C. Then the finite-word cost is
+$$
+O\bigl(N(\log N)^{1-\kappa}(\log\log(N+4))^C\bigr)
+=O\bigl(N(\log N)^{1-\kappa'}\bigr)
+$$
+for every fixed 0<kappa'<kappa. Indeed, setting x=loglog(N+4), the ratio is at most a constant times x^C exp(-(kappa-kappa')x), which is bounded for x>=0. This is a positive absorption theorem; it does not assert that the unresolved Newton/Toeplitz preparation meets its explicit hypothesis. It is useful when a separately derived precision budget is O(log N (loglog N)^c): elementary schoolbook limb multiplication and long division on (loglog N)^c limbs have polynomially many limb operations, and therefore satisfy this overhead condition. No unbounded exact-scalar instruction or TM multiplication routine is invoked.
+
+## Credit and evidence
+
+The closed exact provider, arbitrary-input identity, ownership, recurrence, finite-profile certificate and explicit pass constants are predecessor results from #956 and its #390/Sussman/P193, native, frame/bank, bridge and normalization lineage. Prepared for Dugongue with substantial OpenAI Codex assistance. The roundoff proof above is informal; no new Lean or GPU process was run. Source inspection is not independent acceptance of the predecessor's complete theorem.

research/pr4554-native-stability-check/PR956-PROFILE.json

@@ -0,0 +1,100 @@
+{
+  "literal_source_head": "0e790f2dfb64e17bdee154aee151bb0c1dddb28e",
+  "local": {
+    "children": {
+      "1": 2090,
+      "2": 601,
+      "3": 524,
+      "4": 109,
+      "5": 215,
+      "6": 332,
+      "7": 58,
+      "8": 24,
+      "9": 8
+    },
+    "frame_occurrences": 3953,
+    "centres": 8,
+    "scalar_adds": 14940,
+    "scalar_clears": 16,
+    "real_primitive_upper": 165748,
+    "checked_live_columns": 1023,
+    "checked_dirty_helper_columns": 783,
+    "checked_initial_active_scratch_columns": 8,
+    "complete_column_operator_sha256": "d676b1445729d675e4f7d8f6b2ad9f846328d91df479a5bd51e77c23e279e9e2"
+  },
+  "global": {
+    "histogram": {
+      "1": 630027,
+      "2": 173088,
+      "3": 150912,
+      "4": 31392,
+      "5": 61920,
+      "6": 95616,
+      "7": 16704,
+      "8": 29952,
+      "9": 2304,
+      "16": 15360,
+      "32": 15360,
+      "48": 15360
+    },
+    "children": 1237995,
+    "rank_mass": 4289643,
+    "live": 58899,
+    "deficit": 9984,
+    "integer_root_upper": {
+      "1": 4313000540,
+      "2": 4310082051,
+      "3": 4308375760,
+      "4": 4307165537,
+      "5": 4306227049,
+      "6": 4305460401,
+      "7": 4304812315,
+      "8": 4304250997,
+      "9": 4303755940,
+      "16": 4301338429,
+      "32": 4298427831,
+      "48": 4296726154
+    },
+    "moment_upper": [
+      1538808304431335,
+      1538896445833216
+    ],
+    "moment_gap": [
+      88141401881,
+      1538896445833216
+    ],
+    "a": 2644,
+    "B0": 118984464,
+    "A_bits": 5387
+  },
+  "physical": {
+    "K": 4,
+    "m": 73,
+    "replicas": 32,
+    "private_families": 793,
+    "banks_per_stage": 3131,
+    "local_calls": 288,
+    "forward_calls": 160,
+    "backward_calls": 128,
+    "paid_padding_calls": 28107
+  },
+  "scope": {
+    "native_saving": "1/1024",
+    "cyclic_saving": "7474546/10000000000",
+    "cyclic_exponent_inherited": true,
+    "cyclic_root": "supplied exp(2*pi*i/D(N)), 0<D(N)<8N^3, one root primitive charged",
+    "closed_Lean_program_checked": false,
+    "bit_tape_multiplication_admitted": false
+  },
+  "completed_evidence_reused": {
+    "local_scalar_columns_each_orientation": 1031,
+    "data_adapters": 240,
+    "sink_adapters": 2,
+    "all_size_basis": "universal proofs, separate from finite evidence",
+    "unpublished_replays_offered_as_evidence": false,
+    "local_scalar_columns_fresh_replay_each_orientation": 1031,
+    "unique_actual_frame_edges": 3135
+  },
+  "publication_preparation_did_not_rerun_completed_math_checks": true,
+  "correction_revision_fresh_finite_validation": "FINITE-VALIDATION.json"
+}

research/pr4554-native-stability-check/README.md

@@ -0,0 +1,55 @@
+# Independent check of #4554: native lowering of the closed rational Gaussian kernel
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+This is the last constructive component of Dugongue's #4554 (head `4f46c6a9`) that I had not yet checked, after #4556–#4561. `NATIVE-STABILITY.md` makes four claims:
+- a fixed rational ADD/SCALE provider template has derived prefix norms;
+- its fixed-point lowering has the stated roundoff and precision formulas;
+- it instantiates to #956's closed Gaussian/Walsh provider (`m = 73`, `W = 58,899`, `θ = 1023/1024`);
+- the two shear divisions of the cyclic compiler are quantitatively safe.
+
+The text is vendored as `PR4554-NATIVE-STABILITY.md` (blob `86f98436`). #956's `PROFILE.json` at #956 head `fa4df77c` is vendored as `PR956-PROFILE.json` (blob `3bb4409c`). Both have their SHA256 pinned. Nothing is imported from either PR's code.
+
+## Results
+
+All checked claims are confirmed.
+
+1. **Gate norms, exactly.** With `ā = |Re a| + |Im a| ≥ |a|`, over 3,000 rational complex `a` with denominators from {1,2,3,4,6,9}:
+   - the 2×2 block of `x ← x + a·y` has largest squared singular value `≤ (1+ā)²`, decided by a rational eigenvalue test;
+   - scaling is `≤ max(1, ā)`;
+   - COPY has norm `√2`, and CLEAR `≤ 1`.
+2. **Roundoff.**
+   - **Programs.** 40 random rational ADD/SCALE programs (up to 40 gates, denominators 2 and 3), lowered with truncation toward zero at `P ∈ {12, 20, 30}` bits. Every one has error within the sum of local errors `√2·2^−P` transported through the product of suffix gate bounds; the worst ratio is 0.035.
+   - **Formulas.** In 3,321 parameter cases, the precision formula `P` gives `√2A2^e(e+1)^θK^(D+1)2^−P ≤ 2^(−B−2)`, and the integral width `I` covers `K^(D+1)√(Z2^e)2^b` with three bits to spare.
+   - **Walsh rescaling.** `|(1−i)^e|² = 2^e` exactly for `e < 200`, and the rescaling keeps the error `≤ 2^−B`.
+3. **#956 instantiation.**
+   - `m = 73`, `W = 58,899` and largest child rank 48 match #956's `PROFILE.json` as stated.
+   - The integer-root certificate `r·u_r^1024 ≥ m·2^32768 > r·(u_r−1)^1024` holds at all 12 ranks.
+   - The moment `μ = Σh_r·r·u_r/(W·m·2^32)` is `< 1` (gap 5.7·10⁻⁵), so `θ = 1023/1024` is funded.
+   - The depth bound `D(e) ≤ 1 + ⌈log(e+1)/log(73/48)⌉` holds for the worst-case contraction `e → 48e/73` for all `e < 2000` and at `10^4…10^6`, even counting the leaf call as a level.
+4. **Shear divisions.** Over 3,001 rational `μ` (including the extremal `μ = 1/2`) and 9,003 perturbations:
+   - `t1 = 1+|μ|² ≥ 1` and `Re t2 = −[(a−1/2)² + b² + 3/4] ≤ −3/4` hold exactly;
+   - `|t1' − t1| ≤ (2U+1)δ` and `|t2' − t2| ≤ (2U+2)δ`;
+   - whenever `|Δt2| ≤ 3/8`, `|Δ(1/t2)| ≤ (32/9)|Δt2|`.
+5. **Polyloglog absorption.** `max_x x^C e^(−(κ−κ')x) = (C/(e(κ−κ')))^C` is finite.
+6. **Binding.** 6 statements are bound verbatim to the vendored text.
+
+## Verify
+
+```text
+python3 -B research/pr4554-native-stability-check/verify.py
+```
+
+This runs in about 1 s with the standard library only.
+
+## Limitations
+
+- **Template constant `K`.** `K` is not computed from #956's literal template bytes. #4554 says it is computable but does not print a value, so the formulas are checked for `K ∈ {2, 3, 17}`.
+- **#956's own theorem.** It is not re-proved. Only the profile constants and the moment certificate are recomputed.
+- **Newton/Toeplitz preparation.** #4554 states that the cyclic compiler's Newton/Toeplitz preparation is not covered, and it is not checked here.
+
+## Open next questions
+
+- Compute the explicit prefix-norm constant `K` for #956's literal provider template, from its coefficient bytes. First step: read its fixed nonchild pass list and multiply the elementary gate bounds.
+
+Credit: Dugongue (#4554); the #956 provider and its #390/Sussman/P193 lineage; ram_cost for the completion-of-squares shear argument, as credited in #4554. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4554-native-stability-check/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}