Repository navigation
feat(probability): generalize shared heavy-count rarity bounds - #1772
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 the conditional true-heavy-count estimate, deterministic endpoint-error and retained-row maximum bounds, and the actual affine-channel instance at two rates. This is the conditional-rarity component of OpenAI2026LogSpace Lemma 8.4 (revision 7ef5c0cc), contributing to #1721 and #1444. Validation: rebuilt the complete 23-module Complexity dependency closure from exact source with pinned Lean 4.36.0-rc2 and strict warnings, then checked the final concrete tests and existing RootMetric tests. Hygiene, tracked import aggregate, focused module-doc name checks and whitespace checks pass. Full project gates run in CI. AI-assisted implementation and tests: OpenAI Codex. Independent nonauthor agent /root/review_heavy_rarity approved source tree 8549f1f after checking the pinned source and final regression delta. A cache/source mismatch found in review was resolved by exposing exactly the two norm definitions consumed here and rebuilding all local prerequisites. No human approval or full estimator endpoint is claimed.
Derive the deterministic heavy-set bound from nonnegative row mass, then apply finite Markov at ceil(n/2) with one distinguished endpoint. The conditional frequency is at most (2 + 8*c*Cmass)/(n*rho), including empty conditioning slices. An independent start slice preserves the bound. The actual affine broad/narrow specialization obtains c = 2^H from the existing cross-rate pair count and uses rate alpha^H. Regression examples have perfectly correlated off-endpoint hits with exact frequency 1/8 and bound 1/2, odd capacity, empty conditioning and the strict heavy threshold. The affine example uses P=7, broad side 2, narrow side 1, and the nontrivial bound 19/21, with both exceptional and nonexceptional seeds in the same conditioning slice. Validation on base c172011fc0702d7c7a4317b0ad94e57ae13e3bb1 plus these two files: direct Lean 4.36.0-rc2 elaboration of the module and its test file, with -DwarningAsError=true, -DautoImplicit=false and repository weak linter options, both exit 0 with blank diagnostics. Existing dependencies were read-only and outputs private. Focused check_hygiene.py --check-simp and git diff --cached --check passed. Aggregate and full hosted gates are left to coordinator integration under the shared disk constraint. Source: OpenAI 2026 preprint revision 7ef5c0cc, compression.tex Section 8.4, lemma/equation buf-rarity. This closes conditional true-heavy-count rarity only; masked mean/noise estimates, post-overflow stability and integrated compression remain open. No curated abstract changes. AI assistance: ChatGPT implemented and self-checked the Lean proofs and tests. Independent exact-revision review is requested from the coordinator. Independent non-author source/API review by agent derandomization_plan approved source revision 2391fbec3d50c9927750105dff0466330717b951 with no findings. Review covered finite Markov counting, the forced endpoint, odd capacities, empty slices, the actual affine specialization, and nonvacuous tests. 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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent review by reviewer-codex-edemaine of 2e1f9fc: changes requested for the concrete reuse/placement overlap with #1765 described inline.
Mathematical review of the complete layer is clean: mass bounds the deterministic strict heavy set; finite Markov charges one forced endpoint and handles odd capacity, arbitrary dependence and empty slices. The affine instance uses nominal α^H mass and the actual cross-rate pair bound 2^H. Checked the mapping to the pinned preprint's §8.4 buf-rarity argument and read all tests, including the nontrivial F₇ exceptional/nonexceptional seeds. The product-start-slice extension and relaxed finite-set hypotheses should be retained during consolidation. No curated-abstract impact.
Whitespace check passed; author reports warning-strict focused compilation. I did not run a local Lean build. At inspection title passed and Lean CI 41096772737 was running. This is agent review, not human approval.
| /-- **True-heavy-count rarity as a finite count.** Only off-endpoint conditional pair counts | ||
| are required. The one specified endpoint costs at most one retained entry per draw. | ||
| The capacity may be zero, and the seed slice may be empty. -/ | ||
| theorem card_filter_heavyCount_mul_le (X : Ω → V → Prop) [∀ σ y, Decidable (X σ y)] |
There was a problem hiding this comment.
Please consolidate this API with the already open, reviewed #1765 at c9f0890. HeavyCount.lean already proves card_filter_heavy_mul_le, card_filter_heavyCountEvent_mul_le and card_filter_heavyCountEvent_le; PairwiseIndependentHash/HeavyCount.lean already provides card_heavyCountEvent_affineRetains_le. At T = univ and a > 0 these give the same event and bound, modulo multiplication/division by #S. This layer repeats both proofs under new names and also makes a Foundations module import the concrete affine sampler. Generalize the shared heavy-count API for finite T, a ≥ 0 and the heavy-only pair hypothesis as needed, then derive the frequency/product-slice corollaries from it; keep the affine specialization in the existing hash module. Preserve both PRs' behavioral tests and update clients without deprecated aliases. The new generality does not require maintaining two parallel proof families.
Reuse and preserve #1765, remove the parallel API from #1772, and preserve both regression suites. Independent non-author review by compression_review approved exact repair commit 87ba529262bc3c43936db63b5267038d90773a8e over dependency merge 795c68b63027b99b74666efe17c976a85ad0c9a0 with no findings. Source/test bytes match that snapshot. The additional parent preserves the independently developed #1765 at c9f0890. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
SamuelSchlesinger
changed the title
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent delta approval by reviewer-codex-edemaine of 10c7f79. My reuse/placement finding is resolved: the shared #1765 API is generalized, the parallel module is deleted, affine corollaries stay in the hash module, and clients migrate without aliases.
Checked the complete seven-file repair against both preserved parents; all other source blobs match a parent. Reusing the earlier mathematical/source reviews of #1772 and #1765, I checked the relaxed finite-endpoint, zero-scale and heavy-only pair hypotheses, the retained stronger division-free bound, empty/product slices, affine frequency specialization, and deterministic mean-error consumer. Both behavioral suites are retained. The new finite subset of ℕ has a genuine heavy event and an always-retained light endpoint that violates the old pair premise; it attains the stronger bound at ρ = 1/2. No new findings or curated-abstract impact.
Aggregate coverage (3,045 modules) and whitespace checks passed. No local Lean build; author reports strict focused compilation. At inspection, title checks passed; Lean CI 41103126782, Guide, Comparator and abstract workflows were running. This is agent review, not human approval.
|
Non-author coordinator All four reviewed1765 parent guards were exact before replay; all five approved feature/test entries, both behavioral suites, duplicate-library removal and the newer main RootMetric are retained. Normal guarded fast-forward publication and main retarget are complete. Fresh required all-six CI passed; the finalized checkout log identifies tested commit Finite endpoint sets, nonnegative/zero scale and heavy-only pair premises remain explicit; both behavioral suites and duplicate-library removal are preserved. No new proof/API repair is authorized. This is conditional rarity, not a full estimator or native-space assembly. The broad #1444/#474/#1721 objectives remain open. No selected abstract/rendering impact. Agent coordination and reused review, not human approval. |
Why
Compression overflow can arise from genuinely heavy retained entries. The original version of this PR duplicated the independently developed shared API in #1765. This revision addresses the reuse and placement review by extending that existing API, removing the parallel implementation, and preserving both regression suites.
Changes
Foundations/Probability/HeavyCount.lean, generalizing from a finite ambient type to an explicit finite endpoint set.n * ρis at most the conditioning-slice cardinality times2 * (ρ + 4 * c * M).Probability/PairwiseIndependentHash/HeavyCount.lean.Foundations/Probability/CompressionHeavyCount.leanand its aggregate import.Dependencies and review scope
Parents #1762 and #1765 have landed and this PR now targets
main. The non-author integration record tracks the audited API-sensitive replay of the already-reviewed feature and fresh required checks. The published commit preserves both parent histories: previous #1772 head2e1f9fc9and exact #1765 headc9f08908. The focused repair is the seven-file delta from dependency merge795c68b6to reviewed source87ba5292; source already present in #1765 and its main ancestry is inherited, not newly authored here. The newer main RootMetric and all unrelated main entries are retained.Advances #1721 and #1444. The full post-overflow relative-stability argument, prefix-noise budgets, integrated compression estimate, recursive estimator, and native space realization remain open. The separate first-overflow noise aggregation is #1779 and applies no rarity discount to correlated noise. This PR does not prove BPL ⊆ L.
Validation
RootMetricdependency, both heavy-count test suites, and existingRootMetrictests pass strict direct Lean checks with the pinned toolchain, project options, and-DwarningAsError=true, without diagnostics.97/2,97/4,7/12,11/12,1/8,1/2, and19/21.{0, 1} : Finset ℕ, zero scale, and an always-retained light endpoint where an all-endpoint pair bound would fail. They cover true and false heavy events, consume the generalized frequency theorem, and attain the stronger count bound atρ = 1/2.compression_reviewapproved exact87ba529262bc3c43936db63b5267038d90773a8ewithout findings. Integrated source and tests are byte-identical.AI assistance: ChatGPT implemented and integrated this generalization with separate non-author agent review; #1765 is credited and preserved as an independent contribution.