Repository navigation
feat(logspace): construct and compare stationary compression references - #1750
Merged
Merged
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.
edemaine
approved these changes
Oct 30, 2026
edemaine
left a comment
edemaine
left a comment
Collaborator
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE 62a7cba. Reviewed the complete three-file layer over #1746 at 13625a7, reusing the reviewed preloss, floor and stationary-output APIs. No blocking findings.
The reference uses the actual current default and truth plus actual compressed-minus-raw prefix loss. Dyadic small sums derive its coordinate/default bounds; continuation shifts the original schedule by j and adds no increments. The discrepancy proof charges sensitive targets at η/2, clips first entries and padded ranks below η, and proves rank stability after that clipping. Low targets remain below support using the independent η/100 uniform-loss bound, so their larger raw errors need not enter the envelope. The scalar Lipschitz law then costs three coordinate bounds, yielding 3CB. Checked this mapping against pinned source 7ef5c0cc, p. 46, Lemma 8.2. Actual atom-family scalar laws and comparison with the incremented/post-overflow calculation remain explicit open obligations; the exponent-parametric statement does not assert the eighth-moment endpoint.
Tests exhibit nonzero increment/preloss, shifted continuation, positive root discrepancy and a rank-dependent output with a changing low-target entry and padded rank but zero sensitive-target budget. No curated-abstract impact. Local whitespace and exact-tree aggregate checks passed; no local Lean build. At the single inspection, Lean CI 41087891979 was running and title validation passed. Live head rechecked before posting. Agent review, not human approval.
This was referenced Oct 30, 2026
Collaborator
Author
|
Non-author coordinator Validated coordinator-fix verdict: APPROVE 27be7bdf, carrying forward the outside source/API approval after independent preservation audit. Exact-head source CI, actual queue CI and exact landed-main CI passed all six gates. Shared cache publication audit passed; I independently checked the saved map digest/header, unique pairs, all 16 new-ref availability receipts and exact retained source/modes, with no duplicate log/map GET or artifact-body download. This completes the stationary-reference milestone. Actual scalar-law instantiation, incremented/post-overflow comparison and the full estimator/native-space endpoint remain open in #1721/#1444/#474. No public statement/proof/API change, new mathematical approval count or curated-abstract impact. Agent review and coordination, not human approval. |
Ordinary merge of actual landed main e19469f. Preserve the approved child library/test entries and modes exactly; preserve all unrelated main entries. Regenerate only the canonical import aggregate. Original authorship and source/API review coverage remain in parent history. NON-AUTHOR coordinator: coordinator-codex-algorithms-children-20261030. Source-only preservation checks pass; no local Lean/build performed. Fresh canonical all-six CI required after independent checkpoint audit. No curated abstract impact; broader #1721/#1444/#474 remain open. AI assistance: OpenAI Codex.
SamuelSchlesinger
changed the base branch from
feat/logspace-compression-reference
to
main
October 31, 2026 00:12
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
The local compression lemmas and stationary output law did not yet construct the comparison state used in Section 8.3. The comparison must use the actual current default and the actual accumulated preloss, and its rank bound must remain valid for small targets, signed entries and zero padding.
Changes
Stack and scope
Based on #1746, continuing #1736 → #1740 → #1741 → #1745 → #1746. Part of #1721 and #1444.
This is the stationary-reference portion of Lemma 8.2 from the pinned OpenAI2026LogSpace preprint, revision
7ef5c0cc. It assumes explicit scalar support, flatness and root-Lipschitz laws. Actual atom-family instantiation, the comparison with an incremented or post-overflow run, and integrated estimator bounds remain open. The theorem is exponent-parametric; the fourth-root examples do not claim the paper's eighth-moment endpoint.Validation and review
Strict builds of the module and tests passed on the integrated source; tracked aggregate, committed imports, hygiene and whitespace checks passed. The source/test files at this revision are identical to independently reviewed local revision
c7873d034846fbab13b83d3d9a4d596343c9d191. A separate AI review checked the pinned source, padded-rank argument and concrete low-target regression, with no remaining findings. Full project gates run in CI.AI-assisted implementation and review; no human approval or full-project completion is claimed.