Repository navigation
feat(logspace): derive sentinel coupling from clipped prefix budgets - #1790
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.
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.
Prove Finset.kthLargest_eq_of_eq_or_gt in the existing order-statistic module, preserving Christian Reitwiessner's credit. Values may change arbitrarily when both versions remain strictly above a nonnegative ceiling; if one positive-order rank is at most that ceiling, the actual ranks agree. The boundary rank = ceiling and zero padding are included. Define actual first-coordinate sentinel replacement, leaving every second coordinate unchanged. Derive equality of padded first ranks, size thresholds, and new defaults. The bounded modified rank implies marked cardinality < K. Under the explicit 3R separation, both channels of marked entries are in the compression identity region, and replacement commutes with the concrete update at every retained endpoint. No output equality is assumed. Source mapping for issue #1721: OpenAI2026LogSpace revision 7ef5c0cc, compression.tex Section 8.3, proof of Lemma 8.3, sentinel replacement and removal in the fewer-than-K large-entry case. This is the exact local rank/update argument, independent of the root exponent. Relative-error control through later increments, the iterated coupling, scalar upper saturation, heavy-count closure, and full post-overflow stability remain open. Sentinels are proof devices, not an algorithmic enumeration claim. No curated abstract or catalogue impact; no aggregate changes. Tests use [1000000,4,2,-1] with sentinel 100, K=n=3, positive old default 1/2, and floor 1. Rank and threshold equal the ceiling 2; smaller signed entries actually compress, while a marked second coordinate of -17 is preserved. Further cases exercise K above the retained cardinality and demonstrate why changing a value exactly at the ceiling can change the rank. Validation: KthLargest, Sentinel, and RowCompressionSentinel tests compile without diagnostics under Lean 4.36.0-rc2, warningAsError=true and project linter options, using isolated private outputs and shared dependencies read-only. Focused hygiene --check-simp and staged git diff --check pass. Full integration gates and independent exact-revision review are left to the coordinator. Base is reviewed Reference 10a5168; only these three files belong to this milestone. AI assistance: ChatGPT worker codex-logspace-polynomial-cutoffs-20261030 authored and validated the change. Independent non-author source/API review by agent derandomization_plan approved source revision 68a162675ea79cd7e6e29b0831c725d0dca9bbb2 with no findings. Integrated source and tests are byte-identical to that reviewed revision. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
For issue #1721, construct the modified initial state and increments: retain the common default, replace marked first entries by L, clear only marked first-channel increments, and retain all second-channel increments. Prove coupling of the actual original and modified iterates at every prefix. Their defaults agree, the modified full row is exactly the sentinel replacement of the original row, and both original marked coordinates equal their actual raw prefixes. The large-input condition is derived from cumulative raw absolute variation: 3R plus the full first-channel variation is below each marked initial first coordinate. Only the actual modified input ranks and step thresholds are assumed bounded by R. A post-update rank bound is used by the main result to prove exact padded-rank equality and the same ceiling after every positive prefix. No original compressed-input or final-output contract is assumed, and no bound depends on the largest original first coordinate. Source mapping: OpenAI2026LogSpace revision 7ef5c0cc, compression.tex Section 8.3, proof of Lemma 8.3, the induction removing the sentinel modification. Deriving the ceilings and variation bounds from clipped errors, scalar upper saturation, the heavy-count case, and the complete post-overflow estimate remain separate. Sentinels are analytical devices; this adds no enumeration or machine-resource certificate. No curated abstract impact and no aggregate changes. The test runs two actual groups with marked first increments -5,+7 and second increments +2,-3. It computes the modified intermediate states and both ceiling bounds, then applies the theorem to recover the original marked raw prefix (1000002,-18), common increased default 2, and final padded-rank equality. An unmarked raw first prefix -2 becomes compressed value 2, so the test exercises real compression as well as nonzero signed increments in both channels. Validation: both new files compile without diagnostics under Lean 4.36.0-rc2, warningAsError=true, and all project linter options, with private outputs and shared dependencies read-only. Focused hygiene --check-simp and staged git diff --check pass. Full integration gates and independent exact-revision review remain coordinator-owned. This commit adds only SentinelIteration and its tests atop reviewed Sentinel 68a16267, which is unchanged and preserved on its original branch. AI assistance: ChatGPT worker codex-logspace-polynomial-cutoffs-20261030 authored and validated the change. Independent non-author source/API review by agent lean_environment approved source revision 6626a870805138484aed78a8c97c1218e3c89899 with no findings. Review covered the actual-run induction, original total variation, modified-only ceilings, full-function equality, both signed coordinates, post-update ranks, and the nontrivial two-step test. Integrated source and tests are byte-identical to that reviewed revision. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Compare actual compression schedules with different increments using the exact 28-weighted propagation sum. Prove that stationary references preserve initial rank ceilings and bound their actual input thresholds. For fewer than K true first entries above a fixed level L0, derive every input rank, threshold and total-variation hypothesis of the existing sentinel-removal induction from clipped raw-prefix errors. The fixed sentinel is 16*(L0+1), the rank ceiling is 2*L0+1, and the small weighted budget is at most 1/8 after scaling by 1+16*(L0+1). No bound on the largest true entry, original compressed inputs, or final output discrepancy is assumed. Both marked original channels follow their actual raw prefixes, with exact default and padded-rank agreement. The 202-line signed behavioral suite exercises a genuine first overflow, default change and erasure of a negative low second channel, nonconstant raw evolution of a true first entry 1000, exact coupling to sentinel 32, and weighted budget 9933/125000. Its zero-initial global run verifies the local indexing: start from the already-added overflow input and use a zero first local increment. The preceding global raw prefix has large error and is not a required premise. It also checks failure of the heavy-count branch and of unclipping at error 1. Both libraries and the behavioral suite pass strict isolated direct Lean checks with warningAsError=true and no diagnostics. Focused hygiene with check-simp and whitespace checks pass. Full integration gates remain for hosted CI. This is the small-heavy-set sentinel coupling step of the relative-stability proof, not the full output comparison. Upper saturation, the at-least-K large entry branch, and integrated compression remain open under #1721 and #1444. AI-assisted implementation by ChatGPT agent polynomial_false_finish; exact revision independent review pending before publication. Independent non-author agent polynomial_false_review approved exact source fd5e03c3ea1a7eb550f0d731bc4548a9da535bd3 with no remaining findings. The only review correction normalized three module-comment headings; final integration strictly rechecked all source and tests and preserves reviewed bytes. 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.
Independent agent review by reviewer-codex-edemaine of f9e5a7c, covering this layer over #1776. No blocking findings.
The 28-weighted recurrence charges each increment at its actual update. With fewer than K true entries above L₀, common small preloss and the explicit scaled budget ≤ 1/8, the proof derives modified rank/threshold ceilings and marked-coordinate variation, then reuses the existing exact coupling induction. Both marked channels follow their raw prefixes; no bound on the largest true first entry is assumed. I checked the mapping against pinned source 7ef5c0cc, §8.3, Lemma 8.3, p. 47. The stated exclusions—upper saturation, final output comparison and the other heavy-count branch—are accurate; curated abstracts are unaffected.
The signed two-group regression supplies the hypotheses with budget 9933/125000, a genuine overflow/default change, and evolving marked coordinates. Its global/local comparison correctly avoids assuming small error before the overflow input. Aggregate and whitespace checks pass. At the single CI inspection, PR title passed and Lean Action CI was running (run 41111874808). I did not run local Lean; author-reported strict source/test checks do not replace the remaining CI gates. Live head and review history were rechecked before posting. This is agent approval, not human approval.
This was referenced Oct 30, 2026
Collaborator
Author
|
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. |
SamuelSchlesinger
changed the base branch from
feat/logspace-compression-sentinel-iteration
to
main
October 31, 2026 04:25
Collaborator
Author
|
Non-author coordinator Fresh canonical CI passed all six named gates. The finalized log proves actual synthetic checkout Actually landed at 04:40:44 UTC as |
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.
#1776 proves exact sentinel coupling under bounds on modified ranks/thresholds and marked-coordinate variation. This PR derives both requirements from actual clipped raw-prefix errors, a strict true-heavy-count bound, common initial preloss, and an explicit small weighted error budget.
The reusable perturbation API compares actual compression schedules with different increments, with weights 28^m for initial error and 28^(m-i) for increment errors. A stationary reference gives rank ceiling 2L₀; the clipped-prefix budget gives modified input rank/threshold ceiling 2L₀+1 and keeps the marked original first coordinates in the identity region. The existing coupling induction then supplies exact states, defaults, positive-prefix ranks, and raw evolution of both original marked channels. No upper bound on the largest true entry or final output error is assumed.
Prerequisite #1776 has landed. This PR now targets main and advances #1721 and #1444. This completes the sentinel-coupling step in the branch with fewer than K true entries above L₀. Upper saturation, final row-output comparison, the at-least-K branch, and the full relative-stability theorem remain open. No selected abstract changes are warranted.
Validation and review
All three source/test files pass strict direct Lean with project options and warnings treated as errors, without diagnostics. The signed two-group regression has actual threshold 10^-7 exceeding floor 10^-9, a changed default, an erased low negative second channel, an evolving first entry initially 1000, and a preserved marked signed second channel. Its exact scaled budget is 9933/125000 < 1/8. A zero-initial global run equals the local run starting from the already-added overflow input; the preceding global prefix deliberately has large error, so that unwanted premise is not introduced.
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 sourcefd5e03c3ea1a7eb550f0d731bc4548a9da535bd3. The only review correction repaired module-comment headings; integration rechecked the final source and preserves its bytes. Published revision.AI assistance: ChatGPT worker
polynomial_false_finishimplemented and validated the proofs; separate agents reviewed and integrated them.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.