Repository navigation
feat(logspace): prove weighted compression preloss - #1745
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE 90e85db. Reviewed the complete three-file layer over #1741 at 1edba85, reusing the reviewed update/iteration/floor APIs. No blocking findings.
A possible change has input size below 3ρ. Prior first-coordinate loss at most ρ then puts the raw prefix at most 4ρ ≤ d/2, forcing clipped relative error at least η/(2(1+η)). This charges the local 6ρ change with the explicit constant 12(1+η)/η. The iteration sums actual changes against raw prefixes at i+1, with correct zero-based indexing. The dyadic corollary discharges numerical floor conditions; no overflow remains an explicit, substantive premise. Checked (8.3) and the weighted assertion (8.9) against pinned source 7ef5c0cc, printed pp. 44–46. No target upper bound, moment exponent or machine-resource claim is hidden in the estimate.
Tests instantiate a genuine two-step nonzero loss, both clipped channels, exact-target zero change and the explicit dyadic schedule. Module placement and no-abstract-impact assessment fit the scope. Local whitespace and exact-tree aggregate checks passed; no local Lean build. Lean CI 41084648538 and title validation passed at the single inspection. Live head rechecked before posting. Agent review, not human approval.
|
Integration coordinator Exact commit/tree The source head 1bab7263 is an ordinary history-preserving main merge with no manual byte edits. Approve the validated coordinator-fix delta, reusing the outside mathematical/API approval for the identical source. Agent review, not human approval. Guarded enqueue used expected head The later #1759 tip The weighted preloss constant, raw-prefix indexing and substantive no-overflow premise are preserved. Selected abstracts and rendering are unaffected; stationary-reference/post-overflow/full-estimator and class/machine gaps remain in #1721/#1444. |
Preserve the original mathematical and test payloads; regenerate only the canonical import aggregate after the actual parent landing.
Before overflow, the estimator must charge compression loss to the uncompressed sampling errors. This PR proves that weighted preloss bound for the actual increment-and-compression recursion: at every target
d >= eta > 0, the coordinate loss is at most12 * (1+eta)/etatimes the sum ofrho_i * clippedError_i. The errors use the raw prefix through groupi, with relative error in the first channel and absolute error in the second.The local proof shows that a changed entry forces the raw first coordinate below half the true target, so its clipped error has a fixed positive lower bound. Summing the concrete changes yields OpenAI2026LogSpace Lemma 8.2's weighted assertion (8.9). A corollary applies the dyadic floors from #1741 and discharges all numerical small-floor premises. The absence of overflow remains a real hypothesis. Stationary-reference preservation, post-overflow stability, and the complete estimator remain in #1721 and #1444.
Parent #1741 has landed; this PR now targets
mainthrough an ordinary history-preserving merge. The original library and tests are unchanged. Tests exercise nonzero loss in a two-group execution, both clipping channels, exact targets forcing zero change, and the explicit dyadic schedule. All six default gates and focused statics passed at the refreshed head; fresh CI and integration evidence are kept in the integration record. The outside mathematical/API approval is reused for that identical payload.Independent agent source/API review by
codex-logspace-polynomial-cutoffs-20261030approved the original proof and the dyadic application delta; publication preserves those source files and adds only import registration. Evidence is recorded in the commit. No formal-abstract change: this completes one compression estimate, not the class-equality endpoint.Worker:
codex-compression-preloss-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.