From 754e8c6849a152b4a7531ee7f2e8d8cee2d69b5a Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 13:48:28 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4554's=20native=20stab?= =?UTF-8?q?ility=20lowering:=20exact=20gate=20norms,=20roundoff=20formulas?= =?UTF-8?q?,=20#956=20moment=20and=20depth,=20shear=20bounds=20(no=20new?= =?UTF-8?q?=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../.gitattributes | 2 + .../PR4554-NATIVE-STABILITY.md | 118 ++++++++++ .../PR956-PROFILE.json | 100 ++++++++ .../pr4554-native-stability-check/README.md | 55 +++++ .../SOURCES.json | 18 ++ .../pr4554-native-stability-check/TASK.json | 100 ++++++++ .../pr4554-native-stability-check/VERIFY.json | 18 ++ .../pr4554-native-stability-check/verify.py | 218 ++++++++++++++++++ 8 files changed, 629 insertions(+) create mode 100644 research/pr4554-native-stability-check/.gitattributes create mode 100644 research/pr4554-native-stability-check/PR4554-NATIVE-STABILITY.md create mode 100644 research/pr4554-native-stability-check/PR956-PROFILE.json create mode 100644 research/pr4554-native-stability-check/README.md create mode 100644 research/pr4554-native-stability-check/SOURCES.json create mode 100644 research/pr4554-native-stability-check/TASK.json create mode 100644 research/pr4554-native-stability-check/VERIFY.json create mode 100644 research/pr4554-native-stability-check/verify.py diff --git a/research/pr4554-native-stability-check/.gitattributes b/research/pr4554-native-stability-check/.gitattributes new file mode 100644 index 0000000000..497266d1c2 --- /dev/null +++ b/research/pr4554-native-stability-check/.gitattributes @@ -0,0 +1,2 @@ +PR4554-NATIVE-STABILITY.md -text +PR956-PROFILE.json -text diff --git a/research/pr4554-native-stability-check/PR4554-NATIVE-STABILITY.md b/research/pr4554-native-stability-check/PR4554-NATIVE-STABILITY.md new file mode 100644 index 0000000000..86f984363c --- /dev/null +++ b/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=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=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. diff --git a/research/pr4554-native-stability-check/PR956-PROFILE.json b/research/pr4554-native-stability-check/PR956-PROFILE.json new file mode 100644 index 0000000000..3bb4409c33 --- /dev/null +++ b/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 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. diff --git a/research/pr4554-native-stability-check/SOURCES.json b/research/pr4554-native-stability-check/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/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" + } + ] +} diff --git a/research/pr4554-native-stability-check/TASK.json b/research/pr4554-native-stability-check/TASK.json new file mode 100644 index 0000000000..e697fdc2ff --- /dev/null +++ b/research/pr4554-native-stability-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent coverage of the bounded-word lowering that turns #956's exact-scalar Gaussian provider into a native finite-word kernel.", + "budget_minutes": 45, + "stop_rule": "Stop at NATIVE-STABILITY.md.", + "outcome": "completed", + "evidence": "Exact gate-norm bounds (3,000 a); 40 fixed-point programs within the transported local-error bound (worst 0.035); 3,321 precision/width formula cases; Walsh rescaling; #956 m/W/rank-48 bound to its PROFILE.json, integer-root certificate and moment < 1 recomputed, depth bound; shear identities and perturbation bounds (9,003 cases); 6 statements bound.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Explicit prefix-norm constant K for #956's literal provider template.", + "why_it_matters": "#4554 states it is computable but prints no value.", + "first_step": "Multiply elementary gate bounds over #956's nonchild pass list.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4554-native-stability-check/VERIFY.json b/research/pr4554-native-stability-check/VERIFY.json new file mode 100644 index 0000000000..9ca09a6681 --- /dev/null +++ b/research/pr4554-native-stability-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact gate norms; fixed-point program roundoff vs transported bound; precision and width formulas; #956 profile binding, root certificate, moment and depth; shear-division bounds; binding to vendored texts (sha256)." + } + ] +} diff --git a/research/pr4554-native-stability-check/verify.py b/research/pr4554-native-stability-check/verify.py new file mode 100644 index 0000000000..91ebbd9544 --- /dev/null +++ b/research/pr4554-native-stability-check/verify.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Independent check of PR #4554 (Dugongue) NATIVE-STABILITY.md, from the vendored text and #956's vendored PROFILE.json. + +Nothing is imported from #4554 or #956 code. + 1. Gate norms, exactly over rational complex a with the bound abar = |Re a| + |Im a| >= |a|: the 2x2 block of + x <- x + a y has largest squared singular value <= (1 + abar)^2 (rational eigenvalue test), scaling <= max(1, abar)^2, + COPY = 2 (norm sqrt 2), CLEAR <= 1. + 2. Roundoff: a fixed-point lowering (round toward zero at P bits) of random rational ADD/SCALE programs with + denominators 2 and 3 has error at most sum_k sqrt(2) 2^-P * prod(suffix gate bounds); the precision formula P gives + sqrt(2) A 2^e (e+1)^theta K^(D+1) 2^-P <= 2^-(B+2); the integral width I covers K^(D+1) sqrt(Z 2^e) 2^b with three + bits to spare; |(1-i)^e|^2 = 2^e exactly and the Walsh rescaling keeps error <= 2^-B. + 3. #956 instantiation: m = 73, W = 58,899 and largest child rank 48 bound to #956's PROFILE.json (head fa4df77c, + vendored, sha256-pinned); the integer-root certificate r u_r^1024 >= m 2^32768 > r (u_r - 1)^1024 and the moment + mu = sum h_r r u_r / (W m 2^32) < 1 behind theta = 1023/1024 are recomputed; the depth bound + D(e) <= 1 + ceil(log(e+1)/log(73/48)) holds for the worst-case contraction e -> 48e/73, e < 10^6. + 4. Shear divisions: t1 = 1 + |mu|^2 >= 1 and Re t2 = -[(a - 1/2)^2 + b^2 + 3/4] exactly; |1/t1| <= 1, |1/t2| <= 4/3; + perturbations |dt1| <= (2U+1) delta, |dt2| <= (2U+2) delta and, when |dt2| <= 3/8, |d(1/t2)| <= (32/9)|dt2|, + on random and extremal mu (a = 1/2, b = 0). + 5. Polyloglog absorption: max_x x^C e^(-(k-k')x) = (C/(e(k-k')))^C is finite. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as Fr +import hashlib +import json +import math +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +SPEC = HERE / "PR4554-NATIVE-STABILITY.md" # #4554 head 4f46c6a9, research/native-word-fft/NATIVE-STABILITY.md, blob 86f98436 +SPEC_SHA256 = "260e78bf8f88667a637b804d013d1e7c6dfdf1e23ae35ffdc64a4366c7321221" +PROFILE = HERE / "PR956-PROFILE.json" # #956 head fa4df77c, research/pr390-heterogeneous-provider-closure/PROFILE.json, blob 3bb4409c +PROFILE_SHA256 = "ded51df11009cfd26bf1bbe5108603f89b1dea8d3dd52c9865ef4034d517f68b" + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +def abar(a): + return abs(a[0]) + abs(a[1]) + + +def lam_max_le(X, s): + """Largest eigenvalue of [[1, a],[conj a, 1+s]] (s = |a|^2) is <= X, decided in rationals.""" + tr, det = 2 + s, Fr(1) + # lam_max = (tr + sqrt(tr^2 - 4 det))/2 <= X <=> 2X - tr >= 0 and (2X - tr)^2 >= tr^2 - 4 det + return 2 * X - tr >= 0 and (2 * X - tr) ** 2 >= tr * tr - 4 * det + + +def check_gate_norms(rng): + cases = 0 + for _ in range(3000): + a = (Fr(rng.randint(-60, 60), rng.choice((1, 2, 3, 4, 6, 9))), Fr(rng.randint(-60, 60), rng.choice((1, 2, 3, 6)))) + s = a[0] ** 2 + a[1] ** 2 + need(abar(a) ** 2 >= s, "abar >= |a|") + need(lam_max_le((1 + abar(a)) ** 2, s), "||x += a y|| <= 1 + abar") + need(max(s, 1) <= max(abar(a) ** 2, 1), "||scale|| <= max(1, abar)") + cases += 1 + # COPY (x, y) -> (x, x): M^T M = [[2, 0], [0, 0]], norm^2 = 2. + need([[1 * 1 + 1 * 1, 0], [0, 0]] == [[2, 0], [0, 0]], "COPY norm sqrt 2") + return cases + + +def tz(v, P): + """Round a rational toward zero to the 2^-P grid.""" + S = 1 << P + n = v * S + q = n.numerator // n.denominator if n >= 0 else -((-n.numerator) // n.denominator) + return Fr(q, S) + + +def check_roundoff(rng): + runs, worst = 0, 0.0 + for _ in range(40): + Z, G, P = rng.randint(2, 6), rng.randint(5, 40), rng.choice((12, 20, 30)) + x = [(Fr(rng.randint(-8, 8), 4), Fr(rng.randint(-8, 8), 4)) for _ in range(Z)] + xe, xa = list(x), list(x) + gates = [] + for _ in range(G): + a = (Fr(rng.randint(-3, 3), rng.choice((1, 2, 3, 6))), Fr(rng.randint(-3, 3), rng.choice((1, 2, 3)))) + if rng.random() < 0.6: + i, j = rng.sample(range(Z), 2) + gates.append(("ADD", i, j, a, 1 + float(abar(a)))) + else: + gates.append(("SCALE", rng.randrange(Z), None, a, max(1.0, float(abar(a))))) + for op, i, j, a, _ in gates: + for vec, rounded in ((xe, False), (xa, True)): + src = vec[j] if op == "ADD" else vec[i] + prod = (a[0] * src[0] - a[1] * src[1], a[0] * src[1] + a[1] * src[0]) + new = (vec[i][0] + prod[0], vec[i][1] + prod[1]) if op == "ADD" else prod + vec[i] = (tz(new[0], P), tz(new[1], P)) if rounded else new + err = math.sqrt(sum(float((p[0] - q[0]) ** 2 + (p[1] - q[1]) ** 2) for p, q in zip(xa, xe))) + bound = 0.0 + for k in range(G): + suffix = math.prod(g[4] for g in gates[k + 1:]) + bound += math.sqrt(2) * 2.0 ** (-P) * suffix + need(err <= bound, "sum of transported local errors") + worst = max(worst, err / bound if bound else 0) + runs += 1 + # The precision formula and integral width. + formulas = 0 + for e in range(0, 201, 5): + for A in (1, 5, 1000): + for theta in (Fr(1, 2), Fr(1023, 1024), Fr(1)): + for K in (2, 3, 17): + D = 1 + math.ceil(math.log(e + 1) / math.log(73 / 48)) + for B in (0, 10, 100): + P = (B + e + math.ceil(math.log2(A)) + math.ceil(float(theta) * math.log2(e + 1)) + + (D + 1) * math.ceil(math.log2(K)) + 3) + lhs = 0.5 + math.log2(A) + e + float(theta) * math.log2(e + 1) + (D + 1) * math.log2(K) - P + need(lhs <= -B - 2, "precision formula") + formulas += 1 + for Zb in (1, 4, 30): + for b in (0, 8, 64): + I = b + math.ceil(e / 2) + (D + 1) * math.ceil(math.log2(K)) + math.ceil(math.log2(Zb + 1)) + 3 + mag = (D + 1) * math.log2(K) + 0.5 * (math.log2(Zb) + e) + b + need(mag <= I - 3, "integral width") + for e in range(0, 200): + g = (1, 0) + for _ in range(e): + g = (g[0] + g[1], g[1] - g[0]) # multiply by (1 - i) + need(g[0] ** 2 + g[1] ** 2 == 2 ** e, "|(1-i)^e|^2 = 2^e") + for B in (0, 20): + need(Fr(2 ** e) * Fr(1, 2 ** (2 * (B + math.ceil(e / 2) + 1))) <= Fr(1, 2 ** (2 * B + 2)), "Walsh rescale") + return runs, worst, formulas + + +def check_956(): + raw = PROFILE.read_bytes() + need(hashlib.sha256(raw).hexdigest() == PROFILE_SHA256, "vendored #956 PROFILE.json") + p = json.loads(raw) + h = {int(r): n for r, n in p["global"]["histogram"].items()} + u = {int(r): n for r, n in p["global"]["integer_root_upper"].items()} + m, W = p["physical"]["m"], p["global"]["live"] + need(m == 73 and W == 58899 and max(h) == 48, "m = 73, W = 58,899, largest child rank 48") + target = m << 32768 + for r in h: + need(r * u[r] ** 1024 >= target > r * (u[r] - 1) ** 1024, "integer-root certificate") + mu = Fr(sum(h[r] * r * u[r] for r in h), W * m * (1 << 32)) + need(mu < 1, "moment below 1 (theta = 1023/1024 funded)") + need(sum(r * n for r, n in h.items()) <= m * W, "rank mass within the stock") + worst_depth = 0 + for e in list(range(1, 2000)) + [10 ** k for k in range(4, 7)]: + x, levels = Fr(e), 1 + while x >= 1: + x = x * 48 / 73 + levels += 1 + bound = 1 + math.ceil(math.log(e + 1) / math.log(73 / 48)) + need(levels <= bound, "depth bound, counting the leaf call as a level") + worst_depth = max(worst_depth, levels - bound) + return float(1 - mu), worst_depth + + +def check_shear(rng): + cases = 0 + mus = [(Fr(1, 2), Fr(0))] + [(Fr(rng.randint(-400, 400), 37), Fr(rng.randint(-400, 400), 41)) for _ in range(3000)] + for a, b in mus: + t1 = 1 + a * a + b * b + t2 = (a - t1, b) + need(t1 >= 1, "t1 >= 1") + need(t2[0] == -((a - Fr(1, 2)) ** 2 + b * b + Fr(3, 4)), "Re t2 identity") + need(t2[0] <= Fr(-3, 4) and t2[0] ** 2 + t2[1] ** 2 >= Fr(9, 16), "|t2| >= 3/4") + U2 = a * a + b * b + U = math.sqrt(float(U2)) + for _ in range(3): + dl = Fr(rng.randint(1, 1000), 1000) + ang = rng.uniform(0, 2 * math.pi) + d = (Fr(math.cos(ang)).limit_denominator(10 ** 6) * dl, Fr(math.sin(ang)).limit_denominator(10 ** 6) * dl) + dd = math.hypot(float(d[0]), float(d[1])) + a2, b2 = a + d[0], b + d[1] + t1p = 1 + a2 * a2 + b2 * b2 + t2p = (a2 - t1p, b2) + need(abs(float(t1p - t1)) <= (2 * U + 1) * dd + 1e-12, "t1 perturbation") + dt2 = math.hypot(float(t2p[0] - t2[0]), float(t2p[1] - t2[1])) + need(dt2 <= (2 * U + 2) * dd + 1e-12, "t2 perturbation") + if dt2 <= 3 / 8: + z, zp = complex(float(t2[0]), float(t2[1])), complex(float(t2p[0]), float(t2p[1])) + need(abs(1 / z - 1 / zp) <= 32 / 9 * dt2 + 1e-12, "reciprocal perturbation") + cases += 1 + return cases + + +def check_polyloglog(): + for C in (1, 3, 10): + for gap in (0.01, 0.1, 0.5): + peak = (C / (math.e * gap)) ** C + xs = [C / gap * f for f in (0.5, 0.9, 1.0, 1.1, 2.0)] + need(all(x ** C * math.exp(-gap * x) <= peak * (1 + 1e-12) for x in xs), "bounded absorption factor") + return 9 + + +def check_binding(): + raw = SPEC.read_bytes() + need(hashlib.sha256(raw).hexdigest() == SPEC_SHA256, "vendored NATIVE-STABILITY.md") + text = raw.decode("utf-8") + for s in ("For one scalar gate x<-x+a*y, the Euclidean operator norm is at most 1+|a|.", "COPY has norm at most sqrt(2)", + "uses m=73, largest child rank 48, productive stock W=58,899", "theta=1023/1024", + "\\operatorname{Re}(t_2)=-[(a-1/2)^2+b^2+3/4]\\le-3/4.", "(32/9)"): + need(s in text, f"spec states: {s}") + return 6 + + +def main(): + rng = random.Random(45545) + runs, worst, formulas = check_roundoff(rng) + gap, depth = check_956() + report = {"status": "PASS_PR4554_NATIVE_STABILITY_CHECK", "gate_norm_cases": check_gate_norms(rng), + "fixed_point_programs": runs, "worst_error_over_transport_bound": worst, "formula_cases": formulas, + "pr956_moment_gap": gap, "depth_excess_over_bound": depth, "shear_cases": check_shear(rng), + "absorption_cases": check_polyloglog(), "spec_statements_bound": check_binding(), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())