Repository navigation
feat(logspace): preserve stationary outputs under compression - #1746
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE 13625a7. Reviewed the complete three-file layer over #1745 at 90e85db; reused the unchanged compression/iteration APIs. No blocking findings.
The coordinate bounds, floor ≤ η and positive K ≤ n imply threshold/default/new padded rank ≤ max(η,q). Above η, either the new default equals q or the old rank witnesses lie in the identity region, preserving q. Below η, both ranks remain in the explicitly flat region. For gated outputs, closed gates stay closed; open gates leave supported entries unchanged and cannot move small entries into support. Induction preserves these facts with zero increments and fixed K. Checked the stationary-reference argument against pinned source 7ef5c0cc, printed p. 46, Lemma 8.2. Construction of the initial reference and its discrepancy from truth remain separate obligations, as stated.
Tests demonstrate moving defaults/entries with nonzero preserved outputs, both fixed high rank and changing low rank, and arbitrary iteration counts. The padded-rank definition and structural output hypotheses are inspectable; no whole-row equality or completed-estimator claim. No curated-abstract impact. Local whitespace and exact-tree aggregate checks passed; no local Lean build. Lean CI 41084973492 and title validation passed at the single inspection. Live head rechecked before posting. Agent review, not human approval.
|
Non-author coordinator Fresh exact-head canonical all-six and Guide passed. The optional Comparator passed; the live main ruleset requires Scope remains stationary gated outputs under zero-increment compression; initial reference construction, root discrepancy and the full estimator remain separate. The broader #1721/#1444 objectives stay open. Agent review, not human approval. |
Non-author coordinator coordinator-codex-circuits-readiness-20261030 prepares an ordinary main merge for PR #1746. Parents: unchanged reviewed source 13625a7 and actual main c81edae. The only conflict was generated Complexity.lean, regenerated directly from the exact tracked library-module inventory without Lean, Lake, dependencies or build/output copies. Every reviewed library/test blob, mode and source-credit byte is unchanged, and every main payload outside this PR's own two source files is preserved. Reused outside exact-head mathematical/API/source approval and canonical all-six evidence at the reviewed source. This unpublished checkpoint has source/aggregate/whitespace checks only; new integration validation and publication remain with the approved-PR sweep coordinator. No source/proof/API repair or author-branch push. Curated abstracts and rendering: unchanged source and no impact. AI assistance: OpenAI Codex performed this bounded source-only metadata preparation.
Source-only non-author coordinator checkpoint for PR #1746, refreshed onto actual observed main 29dc907. Ordinary merge parents are prior unpublished metadata checkpoint 3388755 and actual main. Original reviewed source 13625a7 remains an ancestor and every own reviewed library/test blob and mode is exact. Main differs only by the own reviewed module, test and one generated aggregate registration; no unrelated main payload or parent result is removed. Canonical imports match the exact tracked module inventory. Only source/aggregate/whitespace inspection was performed. Reuse original outside exact-head mathematical/API/source approval and source canonical all-six evidence; required current integration validation and publication remain with LogSq. No Lean, Lake, build-output copy, dependency checkout, source/proof/API repair or author-branch push. Curated abstracts/rendering unchanged. AI assistance: OpenAI Codex source-only metadata preparation.
The stationary-reference comparison needs compression to preserve the relevant gated outputs even when it changes row entries. This PR proves that property for the concrete update and its zero-increment iteration. It bounds the thresholds by
max eta oldRank, preserves the padded first-coordinate rank aboveeta, keeps low ranks in the flat region, and proves output preservation from explicit entry-support, gate-closing, and flat-rank hypotheses.This is the stationary-output-preservation portion of OpenAI2026LogSpace Lemma 8.2. It handles positive default padding and the capacity condition
n >= K. It does not claim whole-row equality, the construction of the initial reference from actual preloss, its root discrepancy from truth, or post-overflow stability; those remain in #1721 and #1444. The following layer will connect this theorem to the actual preloss state.Parent #1745 has landed and this PR now targets
main. The non-author integration record tracks the source-preserving aggregate reconciliation and fresh required checks. Tests exhibit actual movement of entries/defaults while a nonzero output remains fixed, covering both a preserved high rank and a changing low rank, including arbitrary stationary iteration counts. The integrated module/tests pass the strict pinned Lean build; hygiene, whitespace, and committed import checks pass. Full gates run in CI.Independent agent source/API review by
codex-logspace-polynomial-cutoffs-20261030approved the unchanged library/tests. Evidence is recorded in the commit. No formal-abstract change: this completes one comparison argument, not the full estimator.Worker:
codex-compression-iteration-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.