From 30ce22be2dd737791d40318bd90928042db40ee3 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 13:45:10 +0700 Subject: [PATCH] =?UTF-8?q?Independently=20check=20#4554's=20native=20oute?= =?UTF-8?q?r=20assembly=20and=20Gaussian=20recount:=20exact=20tolerance,?= =?UTF-8?q?=20perturbed=20assemblies,=20lattice=20tail,=20exponents=20(no?= =?UTF-8?q?=20new=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 --- .../pr4554-outer-recount-check/.gitattributes | 2 + .../PR4554-NATIVE-OUTER-ASSEMBLY.md | 59 ++++ .../PR4554-NATIVE-RECOUNT.md | 87 ++++++ research/pr4554-outer-recount-check/README.md | 56 ++++ .../pr4554-outer-recount-check/SOURCES.json | 18 ++ research/pr4554-outer-recount-check/TASK.json | 100 +++++++ .../pr4554-outer-recount-check/VERIFY.json | 18 ++ research/pr4554-outer-recount-check/verify.py | 251 ++++++++++++++++++ 8 files changed, 591 insertions(+) create mode 100644 research/pr4554-outer-recount-check/.gitattributes create mode 100644 research/pr4554-outer-recount-check/PR4554-NATIVE-OUTER-ASSEMBLY.md create mode 100644 research/pr4554-outer-recount-check/PR4554-NATIVE-RECOUNT.md create mode 100644 research/pr4554-outer-recount-check/README.md create mode 100644 research/pr4554-outer-recount-check/SOURCES.json create mode 100644 research/pr4554-outer-recount-check/TASK.json create mode 100644 research/pr4554-outer-recount-check/VERIFY.json create mode 100644 research/pr4554-outer-recount-check/verify.py diff --git a/research/pr4554-outer-recount-check/.gitattributes b/research/pr4554-outer-recount-check/.gitattributes new file mode 100644 index 0000000000..9cea1b295d --- /dev/null +++ b/research/pr4554-outer-recount-check/.gitattributes @@ -0,0 +1,2 @@ +PR4554-NATIVE-OUTER-ASSEMBLY.md -text +PR4554-NATIVE-RECOUNT.md -text diff --git a/research/pr4554-outer-recount-check/PR4554-NATIVE-OUTER-ASSEMBLY.md b/research/pr4554-outer-recount-check/PR4554-NATIVE-OUTER-ASSEMBLY.md new file mode 100644 index 0000000000..b9c5496896 --- /dev/null +++ b/research/pr4554-outer-recount-check/PR4554-NATIVE-OUTER-ASSEMBLY.md @@ -0,0 +1,59 @@ +# A direct native Fourier-to-integer assembly + +This is a sufficient assembly theorem with an explicit caller and an explicit missing transform hypothesis. Its multiplication construction uses no Turing-machine algorithm. The independently proved closed Gaussian kernel in NATIVE-STABILITY.md does not, by itself, meet the cyclic Fourier hypothesis below. + +## Input and arithmetic + +Fix a standard random-access machine with word width w=c_w ceil(log2(n+2)), for a sufficiently large fixed c_w, and add/subtract, Boolean operations, shifts, comparison, indexed memory and word multiplication/division. The input consists of two n-bit nonnegative integers in packed words. Output is their ordinary packed product. Input conversion and output packing operate on O(n/w) words, with a constant number of shifts and masks per digit. A product of two fixed-size multiword scalars costs O(1) instructions: split into half-word digits and use a fixed number of word products and carry updates. No full-input unit-cost product is used. + +Choose b=floor(log2(n+2)/8), after a fixed small-input cutoff, and let B=ceil(n/b). Write both inputs in radix 2^b with B digits. Let L be the smallest power of two at least 2B. Thus 2B<=L<4B, and L=Theta(n/log n). All digits and all exact convolution coefficients have O(log n) bits. + +## The explicit transform hypothesis + +Assume an actual uniform native cyclic Fourier program on L complex entries provides the following contract. For arbitrary complex inputs with real and imaginary parts of magnitude at most L^4 2^(4b), it computes either the unnormalized forward transform or the normalized inverse transform, with absolute output error at most delta, where + + delta = 1/(128 L 2^b), + +using O(log n)-bit fixed-point words and total work F(L,n). Its full root construction, address generation, table construction, precision operations and scratch clearing are included in F. A program proof must establish this hypothesis for the full arbitrary-input domain; a kernel identity or nonzero denominator check does not establish it. + +## Constructive assembly and proof + +Pad the digit arrays by zeros to length L. Apply the forward program to each, multiply corresponding approximate outputs using bounded-word complex arithmetic, and apply the normalized inverse program. Round every final real output to the nearest integer. Compute each pointwise product with absolute error at most delta. This is feasible using O(log n) fractional and integral bits. + +The exact forward outputs have modulus at most L 2^b. The difference between an exact product AB and the computed product is at most + + 2 L 2^b delta + delta^2 + delta < 1/16. + +The normalized inverse Fourier operator has infinity-to-infinity norm at most 1: each row has L entries of modulus 1/L. Thus its exact application to the product errors contributes less than 1/16 per output. The inverse program adds at most delta<1/16. The final real error is therefore less than 1/8, so nearest-integer rounding recovers every exact convolution coefficient. The imaginary part is discarded. The forward approximants, product approximants and inverse inputs all lie within the stated magnitude domain, including fixed rounding margins. + +There is no cyclic aliasing because L>=2B. Each coefficient is at most B(2^b-1)^2. A left-to-right radix carry pass uses the recurrence + + s_j = c_j + carry_j, + digit_j = s_j mod 2^b, + carry_(j+1) = floor(s_j/2^b). + +The carry is at most B 2^b by induction, up to a fixed harmless endpoint constant. Each s_j has O(log n) bits, and shifting/masking and O(1) word additions implement each step. Remaining carries terminate in O(1) additional digits because their size is O(log n). The carry and output packing cost O(L), including zero padding. + +Hence the complete native multiplication algorithm has cost + + O(F(L,n) + L), L=Theta(n/log n). + +The input-dependent word width is determined from n; the program and every fixed constant are independent of n. Fixed finitely many small inputs can use grade-school digit multiplication. + +## Native saving corollary and its exact scope + +If a concrete transform satisfies + + F(L,n) = O(L (log L)^(1-kappa) (loglog(L+4))^C) + +for fixed kappa>0 and fixed C, the multiplication cost is + + O(n/(log n)^kappa * (loglog(n+4))^C + n/log n). + +For every fixed 0=2 and alpha= P ln 2 + ln(32(X+1)), + a(2R-1) >= ln 2. + +These conditions can be selected by rationally certified squared comparisons and a doubling loop; no exact square-root instruction is needed. For any real center z, splitting the shifted lattice by its two sides and comparing successive terms gives + + sum_(|j-z|>R) exp[-a(j-z)^2] + <= 4 exp[-a(R-1)^2] / (1-exp[-a(2R-1)]). + +Consequently the periodic omitted tail, including the 1/alpha prefactor, is below 2^(-P-1), after the displayed fixed guard. This bound covers the infinite lattice; a finite s-times-largest-entry bound alone would not establish it. + +Take a power-of-two block width q=Theta(R). Partition output k and the extended source indices j into q-blocks. Retain a whole source/output rectangle whenever some pair lies within the radius R; each output block meets O(1) source blocks because both slopes are constant. The centered exponent on every retained rectangle is O(p). The exact diagonal-Hankel-diagonal identity in GAUSSIAN-CHIRP.md reduces each rectangle to one paid linear convolution of length O(q), with O(p) magnitude/accuracy guards and O(q log q) native word work. It is essential to evaluate the whole rectangle, rather than reintroduce an entrywise truncation mask. + +For the actual asymptotic line lengths, s is superpolynomial in p and hence s>2R. Centers lie in [0,s), so only the three source-period copies in [-s,2s) are needed for retained blocks. Access u_j by j mod s, using bounded-word arithmetic; this adds a constant number of boundary blocks. No scan of infinitely many copies is performed. The tail estimate above accounts for all omitted copies. + +There are O(t/q) rectangles. With O(log p) coefficient/precision guards and the ordinary paid exp/root preparation, the complete forward map costs + + O(t log p + n^eta polylog n) + +for any fixed small eta>0. Its working words have a sufficiently large fixed constant times log n bits. Prefactor multiplication, root generation, FFT kernel transforms, gathering, summation and periodic boundaries are included. This replaces the literal window-product count O(t alpha sqrt(p)), not merely its tape movement. + +## Actual inverse: O(s(1+p/alpha^2)) + +The source defines N=C T D, with q_i=floor((t/s)i+1/2), beta_i=(t/s)i-q_i and |beta_i|<=1/2. Its actual entries and the explicit tail proof are given in NATIVE-BANDED-INVERSE.md. Truncating to periodic distance h=O(1+sqrt(p)/alpha) gives row-sum error as small as 2^-P, because the tail is bounded by + + 4 exp[-pi alpha^2 h(h+1)]. + +The predecessor bound ||N-I||<2^(-alpha^2 theta) is eventually at most 1/8. Form the positive truncated coefficients using the paid exp table. The ordinary-band part is strictly row diagonally dominant; its factors have pivots uniformly bounded away from zero and no unbounded element growth. The periodic corner entries are a literal rank-at-most-2h update. The Woodbury Schur matrix has norm-distance at most 1/3 from identity, so its small inverse is itself computed by the same proved elimination, rather than supplied by an oracle. + +Band factorization, 2h right-hand solves, the small Schur factorization, matrix formation and final recovery together cost + + O(s(1+h)^2) = O(s(1+p/alpha^2)). + +The storage is O(s(1+h)). Accuracy P+O(log s+log h) bits suffices by the explicit rounding/residual proof. This remains O(log n). The external diagonal D and selector C cost O(t) extra work with the paid coefficient table. Shared exp/root preparation adds n^eta polylog n, once for the complete family. + +## Sum over the actual tensor axes + +Let T be the padded array size, d=Theta(p^epsilon), and alpha^2=Theta(d sqrt(p)), as in the source. There are T/t_i disjoint forward lines along axis i, and comparable source/target axis lengths. The sum of the forward costs is O(T d log p). The sum of the inverse costs is + + O(T[d + d p/alpha^2]) = O(T[d+sqrt(p)]). + +Including diagonal maps, selectors and setup, the complete Gaussian axis adapters therefore cost + + O(T[p^epsilon log p + sqrt(p)] + n^eta polylog n). + +A stronger actual reuse bound is available because all parallel fibers of one axis share the same s_i,t_i,alpha and hence the same matrix N. Factor the ordinary band part and prepare X=A0^-1 U and the small Schur factors once per axis. A new right-hand side then uses only two band triangular solves, a small Schur solve and Xz recovery, for O(s_i(1+h)) work. The Schur O(h^2) solve is covered because s_i>h. Across all fibers, the inverse contribution is O(T d(1+h)); the one-time factor work is O(d r(1+h)^2), where r=max(t_i)=2^{Theta(p/d)}=n^{o(1)}. With h=O(1+p^(1/4)/sqrt(d)), the complete stronger adapter bound is + + O(T[p^epsilon log p + p^(1/4+epsilon/2)] + + n^eta polylog n + n^{o(1)}). + +Numerical factor errors do not accumulate across independent right-hand sides; each satisfies the same explicit operator/residual error bound. All stored factors and Woodbury columns are paid for in O(d r(1+h)) preparation space. This is direct factor reuse of an explicitly stored input-independent map, not an oracle or an uncharged matrix inverse. + +This is a strict asymptotic native improvement over direct dense-window evaluation. The direct forward loops alone cost O(T d alpha sqrt(p))=O(T p^(3/4+3epsilon/2)); the new forward contribution is O(T p^epsilon log p). The inverse uses direct band elimination instead of repeated Neumann window applications. These are changes to concrete arithmetic algorithms, not a division of a TM-time estimate by word width. + +## Positive O(1)-amortized selected-bit metadata lemma + +Suppose a simultaneous layer selects d of the L address bits, with d=(log n)^epsilon for a fixed epsilon<1 and L=O(log n). For each of its O(log n) levels, prepare an array deposit[j], 0<=j<2^d, mapping a compressed selected-bit index to its physical-bit submask. Explicit construction costs O(2^d poly(d,log n)) per level, and total preparation is n^o(1). Any fixed rational-kernel template's permutation and quarter-phase tables on these d bits can be prepared with the same type of paid bound. + +Let M be the complementary-address mask. Its submasks can be enumerated in increasing order using + + next = (current-M) & M + +in modular word arithmetic, stopping on return to zero. For each complementary base and each j, base OR deposit[j] is its physical address. Every input point belongs to exactly one such pair, and all T gathers/scatters take O(T) word instructions. No PEXT, PDEP, popcount oracle or d-step extraction is required per point. + +For a separately applied tensor twiddle diagonal, scan coordinates in natural mixed-radix odometer order. Maintain the sum of the per-axis exponent contributions; only changed axes are updated. Since every radix is at least 2, the total number of axis changes is O(T+d), so the metadata work is O(T+d), with bounded-word arithmetic and the paid root-power queries. This lemma applies when the phase is the actual separated sum of per-axis contributions, as in the common tensor level; it does not assert the same cost for an arbitrary nonseparable phase function. + +## Verification scope and next assembly + +The real ordinary-band bounded-word reference implementation band_solve.py was independently rerun: 20 systems, 208 rows, maximum raw arithmetic width 193 bits under a 256-bit budget; singular and overflow controls passed. Fraction is confined to its external exact residual oracle. The implementation uses exact product accumulation in substitution and fixed-grid elimination. Its operation counter is an instrumented model, not an emitted RamStd instruction certificate. The periodic real Woodbury implementation periodic_solve.py was also independently reviewed and rerun: 3 periodic systems, 9 right-hand sides reusing the same prepared factors, 123 rows, maximum raw width 192 bits. Its preparation constructs the ordinary factors, the 2h inverse-update columns and small Schur factors exactly once; each new right-hand side performs O(s h) reuse work with no refactor. These periodic fixtures evaluate exact residuals with an external Fraction oracle. The actual Gaussian N is real, so a complex input is handled by separate real and imaginary right-hand solves, doubling only the constant. The general complex-matrix elimination proof remains informal; it is not an executable path covered by these real fixtures. + +The rational closed Gaussian/Walsh kernel from #956 also has the positive native precision lowering proved in NATIVE-STABILITY.md. Choosing epsilon=1/8 suggests a conservative full native saved-exponent assembly once its tensor caller, arbitrary twiddles, record products, cyclic embedding, precision and recovery are all connected and replayed. That complete assembler is not emitted here. In particular these component results are not a new best kappa and are not a completed proof of a faster full cyclic transform. + +Credit: upstream Gaussian resampling and inverse estimates are predecessor results with their Harvey-Hoeven references; the rational kernel is #956 with its stated lineage; chirp convolution, FFT, diagonal dominance and Woodbury have classical precedents. The contribution here is the explicit native finite-word construction, quantitative conditioning, paid preparation and actual Gaussian caller recount. Prepared for Dugongue with substantial OpenAI Codex assistance. + +Additional root integration: periodic_solve.py now replays real Woodbury systems with reusable factors. gaussian_inverse.py constructs the actual positive Gaussian N entries using a paid Machin pi series and signed exp tables, then solves three periodic systems (55 rows), with reference residual below 2^-100. gaussian_block.py evaluates 12 concrete Gaussian rectangles (45 outputs), checked below 2^-60. These are finite operational-model fixtures, not a full cyclic-transform replay; finite Decimal sums are independent validation only. diff --git a/research/pr4554-outer-recount-check/README.md b/research/pr4554-outer-recount-check/README.md new file mode 100644 index 0000000000..0793e112ed --- /dev/null +++ b/research/pr4554-outer-recount-check/README.md @@ -0,0 +1,56 @@ +# Independent check of #4554: native outer assembly and Gaussian-map recount + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** + +This package checks two documents from Dugongue's #4554 (head `4f46c6a9`): +- `NATIVE-OUTER-ASSEMBLY.md`, the caller-tolerance theorem. A native cyclic transform with output error `δ = 1/(128L2^b)` gives exact multiplication in `O(F(L,n) + L)`. +- `NATIVE-RECOUNT.md`, the recount of the Gaussian maps, with its lattice tail, cost exponents and metadata lemma. + +The texts are vendored as `PR4554-NATIVE-OUTER-ASSEMBLY.md` (blob `b9c54968`) and `PR4554-NATIVE-RECOUNT.md` (blob `300188c8`), with their SHA256 pinned. Nothing is imported from #4554's code. With #4556–#4560, this covers every constructive component of #4554 except `NATIVE-STABILITY.md` and `PHASE-TABLES.md` §2. + +## Results + +All checked claims are confirmed. + +**Outer assembly.** +- **Exact inequalities.** For `L = 2^k` (`k ≤ 64`) and `b ≤ 16`, with `δ = 1/(128L2^b)`, three facts hold exactly (1,024 cases): + - the product error `2L2^bδ + δ² + δ < 1/16`; + - inverse inputs stay inside the domain, `(L2^b+δ)² + δ ≤ L^4 2^(4b)`; + - the final budget `1/16 + 1/16 = 1/8`. +- **Assembly runs.** My own assembly uses a transform that satisfies the contract with deliberate perturbations: every forward output, pointwise product and inverse output is moved by modulus `δ(1−10⁻⁶)`, in coherent or random directions. It ran 16 times, for `n` from 254 to 65,534 bits on all-ones and random operands. + - Every product is exact, with `2B ≤ L < 4B` and carries `≤ B2^b`. + - The worst final real error is 6.2·10⁻⁵. These perturbations do not reach the analytic worst case; the guarantee rests on the exact inequalities above. +- **Corollary.** The exponent bookkeeping `L(log L)^(1−κ) ≤ n/(log n)^κ` for `L = n/log n` holds. + +**Recount.** +- **Lattice tail.** `Σ_{|j−z|>R} e^(−a(j−z)²) ≤ 4e^(−a(R−1)²)/(1 − e^(−a(2R−1)))` holds for 4,000 random real centres, `a` and `R`. It is checked in ratio form, and the worst ratio is 0.26. The periodic budget derived from it falls below `2^(−P−1)`. +- **Radius selection.** Selecting `R` by doubling with rational squared comparisons meets both stated conditions in 36 cases (`π > 333/106`, `ln 2 < 0.6932`). The result stays within a factor 2 of the least admissible radius. + + **Note.** The second condition, `a(2R−1) ≥ ln 2`, gives `R = Θ(α²)` and binds only when `α` exceeds about `√P`. That is outside the source regime `α < √p`, so `R = Θ(α√p)` stands as stated. +- **Cost exponents.** With `d = p^ε` and `α² = d√p`, exact exponent arithmetic gives: + - `h ~ p^(1/4−ε/2)`; + - `dh ~ p^(1/4+ε/2)`, the stated adapter term; + - `dp/α² ~ p^(1/2)`; + - direct forward `~ p^(3/4+3ε/2)`. +- **Metadata lemma.** `next = (current−M) & M` enumerates every submask in increasing order, checked for all `M < 2^11`. A mixed-radix odometer with radices `≥ 2` makes at most `2T + d` digit changes (200 random cases). +- **Binding.** 9 statements are bound verbatim to the vendored texts. + +## Verify + +```text +python3 -B research/pr4554-outer-recount-check/verify.py +``` + +This runs in about 5 s with the standard library only. The assembly simulation uses double-precision FFTs, whose rounding is far below `δ`. + +## Limitations + +- **Not established here:** the transform hypothesis itself, a native cyclic program with `F = O(L(log L)^(1−κ)…)`. #4554 states that it is not supplied, and this package does not supply it either. +- **Assembly runs.** The perturbations are contract-satisfying samples, not a proof of the worst case. +- **Out of scope:** `NATIVE-STABILITY.md` and `PHASE-TABLES.md` §2. + +## Open next questions + +- An independent check of `NATIVE-STABILITY.md`, the rational Gaussian kernel and safe shear divisions. That is the last unchecked constructive component of #4554. First step: replay its stated recurrence on the #956 rational kernel in exact rationals. + +Credit: Dugongue (#4554); the Harvey–van der Hoeven sources and #956's rational kernel lineage. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4554-outer-recount-check/SOURCES.json b/research/pr4554-outer-recount-check/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4554-outer-recount-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-outer-recount-check/TASK.json b/research/pr4554-outer-recount-check/TASK.json new file mode 100644 index 0000000000..3480df812b --- /dev/null +++ b/research/pr4554-outer-recount-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 caller theorem that would carry any faster native cyclic transform to a Word RAM multiplication bound, and of the Gaussian-map recount.", + "budget_minutes": 45, + "stop_rule": "Stop at NATIVE-OUTER-ASSEMBLY.md and NATIVE-RECOUNT.md.", + "outcome": "completed", + "evidence": "Exact tolerance inequalities (1,024 cases); 16 contract-satisfying perturbed assemblies up to 65,534 bits, all exact; lattice tail on 4,000 random centres (worst ratio 0.26); radius selection by rational squared comparisons (36 cases); cost exponents exactly; submask enumeration for all M < 2^11; odometer change count; 9 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": "Independent check of #4554 NATIVE-STABILITY.md.", + "why_it_matters": "Last unchecked constructive component of #4554.", + "first_step": "Replay its recurrence on the #956 rational kernel in exact rationals.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4554-outer-recount-check/VERIFY.json b/research/pr4554-outer-recount-check/VERIFY.json new file mode 100644 index 0000000000..5165bda0d2 --- /dev/null +++ b/research/pr4554-outer-recount-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": 300, + "checks": "Exact caller-tolerance inequalities; perturbed-transform assemblies with exact recovery; lattice tail; rational radius selection; cost exponents; submask and odometer lemmas; binding to vendored texts (sha256)." + } + ] +} diff --git a/research/pr4554-outer-recount-check/verify.py b/research/pr4554-outer-recount-check/verify.py new file mode 100644 index 0000000000..b30c8fd77f --- /dev/null +++ b/research/pr4554-outer-recount-check/verify.py @@ -0,0 +1,251 @@ +#!/usr/bin/env python3 +"""Independent check of PR #4554 (Dugongue) NATIVE-OUTER-ASSEMBLY.md and NATIVE-RECOUNT.md, from vendored text only. + +Nothing is imported from #4554's code. + Outer assembly. + * Exactly, for L = 2^k (k <= 64) and b <= 16, with delta = 1/(128 L 2^b): 2L2^b delta + delta^2 + delta < 1/16, the + inverse-input modulus (L2^b + delta)^2 + delta <= L^4 2^(4b), and the final budget 1/16 + 1/16 = 1/8. + * My own assembly with a contract-satisfying adversarial transform: every forward output, pointwise product and + inverse output is perturbed by modulus delta*(1 - 1e-6), coherently (worst sign) or in random directions; digits + are radix 2^b with b = floor(log2(n+2)/8), L the least power of two >= 2B. Recovery must be exact, with final + real error < 1/8 and every carry <= B 2^b, for n up to 65534 bits (all-ones and random operands). + * The corollary: L(log L)^(1-kappa) = O(n/(log n)^kappa) for L = n/log n, by exact exponent bookkeeping. + Recount. + * The two-sided lattice tail sum_{|j-z|>R} e^(-a(j-z)^2) <= 4 e^(-a(R-1)^2)/(1 - e^(-a(2R-1))) for 4,000 random + real centres, a and R (ratio form, no underflow), and the derived periodic budget below 2^(-P-1). + * Selecting R by doubling and rational squared comparisons (pi and ln 2 by rational bounds) meets both stated + conditions and stays within a factor 2 of the least admissible radius. + * Cost exponents with d = p^eps, alpha^2 = d sqrt(p): h ~ p^(1/4 - eps/2), d h ~ p^(1/4 + eps/2), + d p/alpha^2 ~ p^(1/2), d alpha sqrt(p) ~ p^(3/4 + 3eps/2), in exact rational exponent arithmetic. + * Metadata lemma: next = (current - M) & M enumerates every submask of M in increasing order (all M < 2^11), and + a mixed-radix odometer with radices >= 2 changes at most 2T + d axis digits in total (exhaustive small cases). +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import cmath +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 +SPECS = {"PR4554-NATIVE-OUTER-ASSEMBLY.md": "f1e194c01fc1ba4e33c698dbc287aeca8ff0efe822b195c50c95b619242cf9dc", "PR4554-NATIVE-RECOUNT.md": "fc14d31113ef3abd597e654e0aec35ef7972d014268e4b8b7624f202f9ff79db"} # #4554 head 4f46c6a9; blobs b9c54968 (outer), 300188c8 (recount) + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +# ---------------------------------------------------------------- outer assembly +def check_tolerance_exact(): + cases = 0 + for k in range(1, 65): + L = 1 << k + for b in range(1, 17): + d = Fr(1, 128 * L * 2 ** b) + need(2 * L * 2 ** b * d + d * d + d < Fr(1, 16), "product error < 1/16") + need((L * 2 ** b + d) ** 2 + d <= L ** 4 * 2 ** (4 * b), "inverse inputs inside the domain") + need(Fr(1, 16) + d < Fr(1, 8) - Fr(1, 16) + Fr(1, 16), "final budget") + cases += 1 + return cases + + +def fft(a, invert): + n = len(a) + if n == 1: + return list(a) + even, odd = fft(a[0::2], invert), fft(a[1::2], invert) + sign = 1 if invert else -1 + out = [0j] * n + for k in range(n // 2): + t = cmath.exp(sign * 2j * math.pi * k / n) * odd[k] + out[k], out[k + n // 2] = even[k] + t, even[k] - t + return out + + +def perturb(vals, delta, mode, rng, ref=None): + out = [] + for i, v in enumerate(vals): + if mode == "coherent": + direction = ref[i] / abs(ref[i]) if ref is not None and abs(ref[i]) > 0 else 1 + else: + direction = cmath.exp(2j * math.pi * rng.random()) + out.append(v + delta * (1 - 1e-6) * direction) + return out + + +def assemble(x, y, n, mode, rng): + b = max(1, int(math.log2(n + 2)) // 8) + B = -(-n // b) + L = 1 + while L < 2 * B: + L *= 2 + need(2 * B <= L < 4 * B, "2B <= L < 4B") + delta = 1 / (128 * L * 2 ** b) + dx = [(x >> (b * i)) & ((1 << b) - 1) for i in range(B)] + [0] * (L - B) + dy = [(y >> (b * i)) & ((1 << b) - 1) for i in range(B)] + [0] * (L - B) + X = fft([complex(v) for v in dx], False) + Y = fft([complex(v) for v in dy], False) + Xp = perturb(X, delta, mode, rng, ref=X) + Yp = perturb(Y, delta, mode, rng, ref=Y) + prod = [p * q for p, q in zip(Xp, Yp)] + prod = perturb(prod, delta, mode, rng, ref=prod) + need(max(abs(v) for v in prod) <= L ** 4 * 2 ** (4 * b), "inverse input domain") + inv = [v / L for v in fft(prod, True)] + inv = perturb(inv, delta, mode, rng, ref=[complex(1, 0)] * L) + coeffs = [round(v.real) for v in inv] + worst = max(abs(v.real - c) for v, c in zip(inv, coeffs)) + need(worst < 1 / 8, "final real error < 1/8") + carry, out = 0, 0 + for j in range(L + 4): + s = (coeffs[j] if j < L else 0) + carry + out |= (s & ((1 << b) - 1)) << (b * j) + carry = s >> b + need(carry <= B * 2 ** b, "carry <= B 2^b") + need(carry == 0, "carries terminate") + return out, worst + + +def check_assembly(): + rng = random.Random(45544) + runs, worst = 0, 0.0 + for n in (254, 1000, 5000, 65534): + for kind in ("ones", "random"): + x = (1 << n) - 1 if kind == "ones" else rng.getrandbits(n) + y = (1 << n) - 1 if kind == "ones" else rng.getrandbits(n) + for mode in ("coherent", "random"): + out, w = assemble(x, y, n, mode, rng) + need(out == x * y, "exact product") + worst = max(worst, w) + runs += 1 + # Corollary exponent bookkeeping: with L = n/log n, log L = log n - loglog n <= log n, so + # L (log L)^(1-kappa) <= n (log n)^(-kappa); the n/log n output term is dominated when kappa <= 1. + for kappa in (Fr(1, 1000), Fr(1, 3), Fr(1)): + need(-kappa >= -1, "n/(log n)^kappa dominates n/log n for kappa <= 1") + return runs, worst + + +# ---------------------------------------------------------------- recount +def check_lattice_tail(): + rng = random.Random(9) + worst = 0.0 + for _ in range(4000): + a = rng.uniform(0.02, 3.0) + R = rng.uniform(1.2, 12.0) + z = rng.uniform(-50, 50) + denom = 1 - math.exp(-a * (2 * R - 1)) + lo, hi = math.floor(z - R - 80), math.ceil(z + R + 80) + ratio = sum(math.exp(-a * ((j - z) ** 2 - (R - 1) ** 2)) for j in range(lo, hi + 1) if abs(j - z) > R) + ratio = ratio * denom / 4 + need(ratio <= 1 + 1e-12, "two-sided lattice tail") + worst = max(worst, ratio) + # Derived budget: a(R-1)^2 >= P ln2 + ln(32(X+1)) and a(2R-1) >= ln 2 give X/alpha * tail < 2^(-P-1) (alpha >= 2). + for P in (10, 64, 300): + for X in (0, 1, 10 ** 6): + tail_bound = 4 * 2.0 ** (-P) / (32 * (X + 1)) / (1 - 0.5) + need(X / 2 * tail_bound < 2.0 ** (-P - 1), "periodic budget") + return 4000, worst + + +def select_radius(alpha, P, X): + """Doubling loop with rational squared comparisons: pi > 333/106, ln 2 < 6932/10000, ln y < 0.6932 * bitlength(y).""" + a_lo = Fr(333, 106) / Fr(alpha) ** 2 + rhs = Fr(6932, 10000) * (P + (32 * (X + 1)).bit_length()) + R = 2 + while not (a_lo * (R - 1) ** 2 >= rhs and a_lo * (2 * R - 1) >= Fr(6932, 10000)): + R *= 2 + return R, a_lo, rhs + + +def check_radius(): + cases = 0 + for alpha in (2, 3, 8, 50): + for P in (16, 64, 512): + for X in (0, 1, 2 ** 40): + R, a_lo, rhs = select_radius(alpha, P, X) + a_true = math.pi / alpha ** 2 + need(a_true * (R - 1) ** 2 >= P * math.log(2) + math.log(32 * (X + 1)), "first condition") + need(a_true * (2 * R - 1) >= math.log(2), "second condition") + # Least real radius meeting both rational conditions; the second, R >= (ln2/a + 1)/2 = Theta(alpha^2), + # binds only when alpha exceeds about sqrt(P), outside the source regime alpha < sqrt(p). + Rmin = max(1 + math.sqrt(float(rhs / a_lo)), (float(Fr(6932, 10000) / a_lo) + 1) / 2) + need(R <= 2 * Rmin + 2, "within a factor 2 of the least admissible radius") + cases += 1 + return cases + + +def check_exponents(): + eps = [Fr(1, 8), Fr(1, 4), Fr(1, 3)] + for e in eps: + d, alpha = e, e / 2 + Fr(1, 4) # log_p d, log_p alpha (alpha^2 = d sqrt p) + h = Fr(1, 2) - alpha # h = O(sqrt(p)/alpha) for large p + need(h == Fr(1, 4) - e / 2, "h exponent") + need(d + h == Fr(1, 4) + e / 2, "d h exponent") + need(d + 1 - 2 * alpha == Fr(1, 2), "d p / alpha^2 exponent") + need(d + alpha + Fr(1, 2) == Fr(3, 4) + 3 * e / 2, "direct forward exponent") + return len(eps) + + +def check_metadata(): + w = 16 + mask = (1 << w) - 1 + for M in range(1 << 11): + seq, cur = [0], 0 + while True: + cur = (cur - M) & M & mask + if cur == 0: + break + seq.append(cur) + need(seq == [s for s in range(M + 1) if s & ~M == 0], "submask enumeration") + rng = random.Random(3) + for _ in range(200): + d = rng.randint(1, 6) + radices = [rng.randint(2, 5) for _ in range(d)] + T = math.prod(radices) + digits, changes = [0] * d, d + for _ in range(T - 1): + i = 0 + while True: + digits[i] += 1 + changes += 1 + if digits[i] < radices[i]: + break + digits[i] = 0 + i += 1 + need(changes <= 2 * T + d, "odometer changes <= 2T + d") + return 1 << 11 + + +def check_binding(): + n = 0 + for name, sha in SPECS.items(): + need(hashlib.sha256((HERE / name).read_bytes()).hexdigest() == sha, f"vendored {name}") + n += 1 + outer = (HERE / "PR4554-NATIVE-OUTER-ASSEMBLY.md").read_text(encoding="utf-8") + for s in ("delta = 1/(128 L 2^b),", "2 L 2^b delta + delta^2 + delta < 1/16.", "L^4 2^(4b)"): + need(s in outer, f"OUTER states: {s}") + n += 1 + rec = (HERE / "PR4554-NATIVE-RECOUNT.md").read_text(encoding="utf-8") + for s in ("<= 4 exp[-a(R-1)^2] / (1-exp[-a(2R-1)]).", "next = (current-M) & M", "O(T[p^epsilon log p + p^(1/4+epsilon/2)]", + "O(T p^(3/4+3epsilon/2))"): + need(s in rec, f"RECOUNT states: {s}") + n += 1 + return n + + +def main(): + runs, worst = check_assembly() + tails, tail_ratio = check_lattice_tail() + report = {"status": "PASS_PR4554_OUTER_RECOUNT_CHECK", "tolerance_cases": check_tolerance_exact(), + "adversarial_assemblies": runs, "assembly_worst_final_error": worst, + "lattice_tail_cases": tails, "lattice_tail_worst_ratio": tail_ratio, "radius_cases": check_radius(), + "exponent_cases": check_exponents(), "submask_masks": check_metadata(), + "spec_statements_bound": check_binding(), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main())