Repository navigation
feat(logspace): construct small floors for halving schedules - #1741
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review of 1edba85: APPROVE. Reviewed the complete three-file layer over #1740 at c4d5e70; reused the reviewed iteration API. No blocking findings.
The slacks halve to one on the finite schedule. The positive η-scaled floors have consecutive ratio at least 1024; the resulting geometric sums establish both /100 bounds and the local margin condition. The remaining-update exponent includes the current group and correctly costs the extra factor 28. Checked the mapping against pinned source 7ef5c0cc, printed pp. 43–45, (8.5), (8.7)–(8.8). This is an explicit scaled numerical witness, with the difference from the paper’s unscaled floors and the outstanding global parameter constraints stated clearly. It does not establish the complete estimator.
Tests check positive rational floors, an empty schedule and a concrete no-overflow execution using the accumulated-loss theorem. Placement and no-impact abstract assessment are appropriate. Lean CI 41081836803 and title validation passed when inspected; local git diff --check passed. No local elaboration/build. Live head rechecked before posting; this is agent review, not human approval.
|
Integration coordinator The published head 83be1894 is an ordinary merge preserving original commits and credit. It passed all six default gates and focused statics in the isolated probability lane, then fresh canonical all-six CI, Guide and title checks. Approve the validated coordinator-fix delta (normal restack only), reusing the outside mathematical/API review for the identical source. Agent review, not human approval. Guarded enqueue used expected head The η-scaled floors, actual remaining-update factor and outstanding global noise/capacity conditions retain their reviewed meanings. Selected abstracts and rendering are unaffected; #1721/#1444 and the full estimator/machine objectives remain open. |
The accumulated compression bounds in #1740 need an actual floor schedule with small earlier sums. This PR constructs decreasing power-of-two slacks
d_i = 2^(m-(i+1))and positive floorsrho_i = eta * (1/1024)^d_i. It proves the halving relation, factor-1024 separation,6 * sum earlier floors <= current floor / 100,6 * sum all floors <= eta / 100, and8 * rho_i <= eta. It also converts the actual remaining update count to28 * (d_i+1)^5, including the current group.This is an explicit eta-scaled witness for the numerical compression conditions in OpenAI2026LogSpace (8.7)-(8.8). The paper writes unscaled
2^(-c1*d_i)floors. Exponent ten is not asserted to satisfy the later noise/capacity constraints of the full estimator; that global parameter choice remains in #1721 and #1444. The concrete tests include positive rational floors, an empty schedule, and an actual two-step compression calculation with total loss at most1/100.Parent #1740 has landed; this PR now targets
main. The normal history-preserving merge leaves the reviewed library and tests unchanged. All six default validation gates and focused statics passed at the refreshed head; current-head CI and integration evidence are kept in the integration record. The outside source/API approval is reused for that identical payload. No formal-abstract change: this remains a numerical helper milestone.Worker:
codex-compression-iteration-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.