Repository navigation
feat(logspace): bound dyadic overflow noise uniformly - #1788
Conversation
The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances #1721 and #1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c8: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review.
Add concrete increment-and-compression states and schedules. Prove width-independent 28^j propagation, exact restarts, a fifth-power slack bound under an explicit group-count condition, and accumulated row/default loss before overflow. This establishes the update-only part of OpenAI2026LogSpace (8.7) and the unweighted part of Lemma 8.2; weighted preloss and the final root functions remain separate. Validation on base c3f7a58: direct Lean 4.36.0-rc2 checks of both new modules with project options passed without diagnostics, using isolated output files and the parent checkout dependencies read-only. Concrete tests cover a two-group nonzero-loss execution, satisfied no-overflow bounds, an actual overflow after lowering capacity, and distinct initial-state perturbations. Focused proof hygiene including --check-simp and git diff --check passed. Aggregate regeneration and full project gates are delegated to integration. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved the library and tests at 7d08e44bbdb626b74adaa9c4d63e07faa28ce525. Publication adds only the generated aggregate import. Integrated targeted build, tests, aggregate check, hygiene and whitespace checks pass. Full gates run in PR CI.
Use decreasing power-of-two slacks and the explicit floors eta * (1/1024)^slack. Derive consecutive floor separation, both finite-sum bounds from source equation (8.8), and the local 8*rho <= eta margin. Bound propagation for the actual remaining group count, distinguishing updates after the current group from those including it. The source uses unscaled inverse powers of two; this mathematical witness explicitly scales by eta and does not choose an exponent for the full integrated estimator. Validation: direct Lean 4.36.0-rc2 checks of Floors.lean and RowCompressionFloors.lean with project options passed without diagnostics, using private outputs and parent dependencies read-only. Tests compute nonzero floors, check halving and empty schedules, and apply the sum theorem to a concrete no-overflow compression execution. Focused hygiene including --check-simp and git diff --check passed. Base is iteration milestone 7d08e44bbdb626b74adaa9c4d63e07faa28ce525; aggregate and full project validation remain integration tasks. AI assistance: ChatGPT implemented and checked the proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved module/tests at bd14fc247724f63e650ced31e7b0e6c4d30fcee1. Publication adds only generated import registration. Integrated strict module/test build, focused hygiene and whitespace checks pass. Full gates run in PR CI.
Prove the weighted preloss assertion of OpenAI2026LogSpace Lemma 8.2 for the actual compression recursion, with explicit constant12(1+eta)/eta. Apply it to the concrete dyadic floors, discharging numerical small-floor conditions. Stationary-reference preservation, relative stability after overflow, and the complete estimator remain separate obligations. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved599c5e8a and the dyadic application delta4cc6581b. Published library/tests are identical to the reviewed source, with generated aggregate registration. Strict private Lean source/test checks, hygiene and whitespace checks pass. Full integration gates run in PR CI. Worker codex-compression-preloss-20261030; AI-assisted implementation and review.
Define the padded first-coordinate rank and prove concrete threshold, default, row-bound and rank preservation results for stationary references. Above the flat region, the rank stays fixed; inside it, the rank remains in the flat region. A gated row output with separated entry support therefore survives each update and any finite zero-increment schedule with floors at most eta and capacities at least the fixed positive rank K. This formalizes the stationary-output assertion of OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. It does not assert equality of whole rows, a root-discrepancy estimate, or post-overflow stability. The explicit support and gate hypotheses do not assume the preservation conclusion. Validation on base 7d08e44bbdb626b74adaa9c4d63e07faa28ce525: direct Lean 4.36.0-rc2 checks of both new files passed without diagnostics, using private outputs and existing parent-checkout dependencies read-only. Tests exhibit an above-flat rank fixed at 1/2 while a zero entry moves to 3/8, an arbitrary stationary iteration retaining nonzero output 21/2, and a low rank moving from zero to 1/8 while output 41/4 is preserved. Focused proof hygiene including --check-simp and staged git diff --check passed. Aggregate regeneration and the full project gates remain integration work. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved 10a516829a8cf8ea4fd0da6a65abe00147525b46. Publication changes only dependency ancestry and generated aggregate registration. Integrated strict module/test builds and committed import/hygiene checks pass. Full gates run in PR CI.
Construct the reference state from the actual current default and true row plus accumulated compression preloss. Derive its small-negative and second-coordinate bounds from no-overflow dyadic floors, then preserve gated outputs through the remaining capacities and floors at their original indices with zero increments. Add a separate weighted root comparison with the true zero-padded output. Sensitive targets use the existing weighted preloss bound at eta/2; uniform small loss and lower clipping remove the low targets from the rank comparison. The theorem assumes scalar support, flatness and root-Lipschitz laws and a raw-prefix error envelope only at sensitive targets, not the final output estimate. It is exponent-parametric. Instantiating all source row functions and comparison to a subsequent incremented or post-overflow calculation remain separate. Source mapping: OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. This connects the reviewed Preloss and Reference layers using the documented margin-scaled dyadic witness. Existing files and aggregates are unchanged. Validation: pinned Lean 4.36.0-rc2 checked the new module and tests without diagnostics, using private outputs and read-only shared dependencies. Tests exhibit a nonzero increment, nonzero actual preloss, preserved nonzero output through the shifted remaining schedule, and a strictly positive fourth-root discrepancy. The review-requested low-target regression raises the padded rank from zero to 1/1048576 while a rank-dependent fourth-root output remains exactly one under a zero sensitive-target error envelope. Focused hygiene with --check-simp and staged diff checking pass. Full project gates and aggregate regeneration remain integration work. AI assistance: ChatGPT implemented and checked this milestone as worker codex-compression-iteration-20261030. Independent reviewer codex-logspace-polynomial-cutoffs-20261030 requested the low-target regression and is reviewing the frozen revision. Independent non-author source/API review by compression_review approved exact source revision c7873d034846fbab13b83d3d9a4d596343c9d191, including a rank-dependent low-target regression. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Prove uniqueness of the first-overflow index, a signed light-target error lower bound, the explicit 2^(p+1)/(n*rho^p) moment charge, and its specialization to the actual dyadic iterate with previous default and preloss bounds derived. Conditional heavy-count rarity, relative post-overflow stability and integrated compression remain open under #1721 and #1444. Strict isolated Lean compilation with warningAsError=true and empty diagnostics passed for the module and a signed two-group run with nonzero preloss. Focused hygiene and whitespace checks passed. AI-assisted implementation; independent review pending before publication. Independent non-author source/API review by lean_environment approved exact source revision e0066c8a1015c2270c0a9ffaec1a3209225b2ce3 against pinned compression.tex Section 8.4, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
An actual compression run has at most one first-overflow group. Its selected nonnegative weighted tail therefore costs at most one full sum, even when the noise depends on the environment and the overflow event. Prove the finite selected-tail inequality for ordered additive monoids, apply IsFirstOverflow.unique to the actual run, and lift the result through the existing vertexNormPow normalization. Expose vertexNormPow for this consumer; this is the same annotation already reviewed on the SourceRelease lane, with no change to its definition. No conditional rarity factor or independence hypothesis is imposed on the noise. The concrete test first compresses a zero row to default one, then adds (4, -2) and first overflows at group one. Its selected weighted tail is 21 and full weighted sum 49. Correlated Boolean noise has fourth moments 194481/2 and 5764801/2. A separate finite example shows repeated counting when uniqueness is dropped. Source: OpenAI2026LogSpace, September 23, 2026 revision 7ef5c0cc, Section 8.4, the pointwise paragraph leading to buf-noise-sum. This is a bounded milestone for #1721. Prefix-noise budgets, Minkowski, propagation weights, convergence and the full integrated compression theorem remain open. Validation: RootMetric, UniqueTail, OverflowNoise and the focused test compiled with project options and -DwarningAsError=true using read-only dependencies and private direct-Lean outputs; no diagnostics. Focused scripts/check_hygiene.py --check-simp and staged git diff --check passed. Aggregate registration and full six-gate CI remain coordinator integration steps. The superseded masking draft is preserved only in unpublished WIP 487cbfba and is excluded from this change. AI-assisted implementation using OpenAI Codex; independent review pending on the frozen source revision. Independent non-author review by derandomization_plan approved exact source commit 9b992f30ec86b4694a06859d8e38eb092db88c1c with no findings; integrated library and test bytes match that snapshot. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Apply finite Minkowski to the existing normalized vertex moment, then consume it for the actual unique-first-overflow tail. No independence or horizon-count factor is introduced. Individual prefix budgets and propagation/series estimates remain explicit obligations. Both new libraries and the focused behavioral tests compile with the pinned toolchain, project options and warningAsError=true, without diagnostics. Tests include an attained correlated fourth-moment budget28561, negative inactive values and scalars, empty/zero-normalization boundaries, and an actual nonzero compression tail194481 bounded by5764801. Focused hygiene and whitespace checks pass. Worker: root; non-author review pending. Aggregate registration is reserved for integration. AI assistance: ChatGPT implementation. Independent non-author review by compression_review approved exact source commit 17693f2d59d04774c5cff3eabcf5745f5ed3de21 with no findings. Integrated source and test bytes match that reviewed snapshot. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Prove that geometric prefix-noise decay along the actual dyadic slack schedule pays for C^(m-i) propagation with total factor C*q/(1-C*q), uniformly in the number of groups. Compose the bound with the existing actual first-overflow moment budget, without independence assumptions. The absolute stability constant C=28 admits q=1/64 and factor 7/9. The concrete correlated two-group regression has an actual overflow at group zero, individual decay budgets attained, and exact normalized fourth moment (161/256)^4 within (7/9)^4. It also checks empty horizon, zero decay and a slower decay which cannot pay for even one group. Both new files pass direct Lean 4.36.0-rc2 with project options and warningAsError=true without diagnostics. Focused hygiene with check-simp and whitespace checks pass. Shared dependency outputs are read-only; all local compiler outputs are private. Full repository gates run in CI. This discharges the uniform weighted-sum step of the pinned Section8.4 noise argument. Actual prefix estimates and the relative-stability propagation constant remain open under #1721 and #1444. No selected headline abstract changes are warranted. Independent review requested. AI assistance: ChatGPT coordinator authored and validated this layer. Independent non-author agent polynomial_false_review approved exact source 9fec99a9960a3ead8fdfe4babeeceeead02a0cfe with no findings. Integration preserves the reviewed source and behavioral test blobs. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent approval by reviewer-codex-edemaine of dc358bd. Reviewed the complete three-file layer over reviewed #1783, actual dyadic schedule/tail/moment definitions, Mathlib’s geometric-sum bound and all regressions. No findings.
For every i<m, the remaining-group count m-i is at most 2^(m-i-1). With 0≤q≤1, this bounds each weighted term by (Cq)^(m-i); reflection gives powers one through m and hence Cq/(1-Cq). The current group is included. Composition preserves the existing normalization and permits correlated noise/overflow, requiring nonnegativity only on retained sources. Positive moment exponents, empty horizons and zero decay are handled. The correlated actual-overflow example attains (161/256)^4; the slower-decay counterexample is substantive.
This supplies the uniform numerical step of the pinned §8.4 buf-noise-sum argument, reusing #1783’s source coverage. The illustrative C=28, q=1/64 factor 7/9 does not establish a relative-stability propagation constant or the missing prefix budgets. No curated-abstract impact.
Aggregate coverage (3,044 modules) and whitespace passed. At inspection title passed and Lean CI 41110489638 was running. Author reports strict focused compilation; no local Lean build by this reviewer. This is agent review, not human approval.
|
Independent non-author preservation audit by coordinator This authorizes unchanged guarded normal FF publication after fresh head/ownership guards. Fresh canonical native all-six validation, with the actual tested checkout verified, remains mandatory before the integration verdict and queue admission. Reuse the existing exact-source outside mathematics review; this audit changes no mathematics, API or scope and adds no mathematical approval count. Original authorship is retained. No local Lean build, extra CI dispatch or main-cache retrieval. |
|
Non-author coordinator Fresh canonical CI passed all six named gates. The finalized log proves actual synthetic checkout Actually landed at 04:41:00 UTC as |
#1783 bounds the actual first-overflow noise tail by a finite sum of individual budgets. This PR discharges that sum uniformly in the number of groups: for dyadic slacks d_i = 2^(m-i-1), nonnegative C and q ≤ 1 with Cq < 1, the weighted sum of C^(m-i) q^d_i is at most Cq/(1-Cq). The proof reuses Mathlib's finite geometric-series bound.
Composing this with the actual overflow-tail theorem gives normalized p-th moment budget (ε Cq/(1-Cq))^p from individual budgets (ε q^d_i)^p, allowing shared randomness throughout. For the existing absolute stability constant C=28, q=1/64 gives the explicit factor 7/9.
Prerequisite #1783 has landed. This PR now targets main and advances #1721 and #1444. This completes the uniform weighted-sum step of the pinned Section 8.4 noise argument. The actual prefix estimates and propagation constant for relative stability remain open; this does not identify that constant with 28 or complete the recursive estimator. No selected abstract changes are warranted.
Validation and review
Both source and tests pass strict direct Lean checks with project options and warnings treated as errors. The correlated two-group regression has an actual first overflow, attains both individual decay budgets, and proves exact tail moment (161/256)^4 within (7/9)^4. Tests also cover empty horizon, zero decay, negative inactive noise, and a slower decay that cannot pay for one propagation step. Focused hygiene, tracked aggregate, committed-import and whitespace checks pass; full Lean CI passed for the published revision.
Independent non-author agent
polynomial_false_reviewapproved exact source9fec99a9960a3ead8fdfe4babeeceeead02a0cfewith no findings, including indexing, normalization, source mapping, and tests. Integration preserves the reviewed source/test bytes. Published revision.AI assistance: ChatGPT authored and integrated the proofs, with separate non-author agent review.
Supported-main refresh: the exact outside-reviewed feature layer and original authorship are unchanged; only the generated aggregate needed reconciliation. Selected formal abstracts are unaffected: statements, definitions, models and scope remain unchanged. Current validation and integration status are in the single integration record.