Repository navigation
feat(logspace): prove fine-bin conditional product comparison - #1771
Conversation
Prove the finite double-counting inequality in the source-domain part of OpenAI2026LogSpace Lemma 7.3 and its exact K * (f / u) cost in integrated table and vector norms. Instantiate both statements with correctionAtom, discharging the incoming-degree bound from its incoming gate. Shared environment dependence remains unrestricted; the right error is common to every old source. Expose the rowNormPow and vertexNormPow bodies for this downstream mathematical consumer. No definitions or theorem statements change. Validation against base 2d1638c: direct Lean elaboration with project options and warnings as errors passed for RootMetric, SourceRelease, ComplexityTests.SourceRelease and the existing ComplexityTests.RootMetric (covering AtomCutoffs and RootError). Outputs were private; dependencies were read-only. Hygiene with --check-simp and git diff --check passed. The changed-file lint requires the absent ComplexityAbstracts.ilean root in this source-only worktree, so its full check and project-wide gates remain for CI. Aggregate imports are left to the integrating coordinator. Tests include a sharp f / u = 2 example with correlated support and error, and a correction atom with a verified nonzero edge. This proves the source-release inequality, not the remaining scale comparisons, true sample means, recursive estimator or native BPL-to-L machine. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved final43118874cf98b42ae1ed3bc776a6c7e6fd9f4d6d. Publication adds only the generated aggregate import. Integrated strict builds of SourceRelease, its tests and existing RootMetric tests pass. Full gates run in PR CI.
Remove three stray aggregate imports introduced during local integration. Source-release proofs, APIs and tests remain unchanged. The committed import graph is now checked before publication.
Prove the direct dense and correction-dense mean identities from the actual atom definitions on their finite conditioning slices. The exact terminal density ratio changes to the nested usage slice, and f / pi_f cancels the intermediate retention density. Finite product averages factorize because the true right dense atom uses only the terminal seed. Both atom normalizations are derived from the existing gate and pair-count hypotheses, rather than assumed as mean contracts. This implements the direct/product part of OpenAI2026LogSpace Lemma 7.1 at pinned source revision 7ef5c0cc, before division by the parent scale. Copy, detector, reward and conditional-walk assembly remain separate. It makes no estimator-error or machine-space claim. Validation against source-release 43118874: TrueSampleMeans and ComplexityTests.TrueSampleMeans elaborate with project options and warnings as errors, using private outputs and read-only dependencies. Hygiene with --check-simp and git diff --check passed. Full project gates and import aggregate registration remain for the integrating coordinator and CI. The concrete example has middle hit probability 1/2, terminal broad density 1/2 and usage density 1/4. Both correction factors equal two; the active sample is 2/3 and the conditional product mean is 1/6. All gate, pair-count, subset and density hypotheses are discharged. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved 9c1014a804ed32d06ba499196f460987b6a3d87d against the pinned Lemma7.1. Publication preserves the reviewed source/tests and adds only generated import registration. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI.
Independent non-author source/API review by compression_review approved exact source revision fcbb5797a9c8b5c9bde9fd80de74ed84ec2c1e90 against the pinned Lemma 7.3, 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.
Independent non-author source/API review by compression_review approved exact source revision 550c89a7d5035d86ca1b77c8cb82432f61e6aee0 against pinned estimation.tex Sections 7.2-7.3, 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.
Independent non-author source/API review by agent lean_environment approved final source revision ae8af63254c804422dedbd1a61a1ed1a4dcb1a8b after the duplicate expectation proofs were replaced by reuse of documented existing lemmas. 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 ef9700e: approve. Reviewed the complete layer over #1759, reusing its conditional-mean and #1752's coupled-product coverage.
Checked the mapping against the pinned September 23 source, §7.2 (7.2), p.34, and Lemma 7.3's fine-bin argument, p.37. Restricting to the supported narrower terminal slice before Jensen leaves exactly (b/a)^s·πa/πb; the stated density comparisons give (b/a)^(s−1). Both left row caps establish the product bound, and the existing pointwise incoming-cap argument retains f/u. Source and terminal masks use separate product coordinates; factor values and errors can share both coordinates. Positive terminal densities and exponent, bounded nonnegative factors, and nested terminal masks are explicit; empty source slices are allowed.
The checked-example proofs include the sharp 1/96 versus false 1/192 bound, anticorrelated estimated factors, and a full theorem instance discharging the caps and support hypotheses. Copy/detector/reward estimates and recursive estimation remain open; curated abstracts are unaffected. Aggregate coverage and whitespace checks passed. Author reports strict focused source/test compilation; I did not run a local build. At inspection, title passed and Lean CI 41096605245 was running. This is agent review, not human approval.
|
Non-author integration coordinator The ordinary merge of landed main preserves the complete approved nonaggregate feature patch byte-for-byte, including the public expectation helpers; every unrelated main entry is preserved. The shared main file matched the reviewed parent before the post-squash resolution. Coordinator Fresh canonical CI 41146004007 completed successfully: build, tests, lint, aggregate, style and Init imports all passed. The job started before retargeting and checked synthetic merge Landed at 2026-10-31 00:28:02 UTC as The fixed covering main consumer and completed public-cache closeout are recorded once in the shared publication record. |
Merge actual landed main d6c3de5 into approved feature ef9700e. Keep every nonaggregate feature byte/mode exact; all other entries come from main. Regenerate the aggregate from the full sorted source inventory. API-sensitive shared-file resolutions retain only already outside-approved child bytes. Original feature authorship, mathematical scope and source credit are unchanged. Source-only checkpoint: no Lean build or final integration approval. Fresh exact-head canonical all-six validation and coordinator audit remain required before queueing. Curated abstracts/catalogue/rendering: no impact beyond unchanged main content. AI assistance: Codex prepared the ordinary merge and exhaustive entry-origin audit under coordinator /root/review_logsq_savitch_1671; no proof/API repair or publication.
Fine-bin comparison must change the conditioning slice before taking the root-metric power. This proves the comparison for actual conditional product means, retaining the exact marginal-density factor and allowing arbitrary coupling of the factor errors. Both left-row caps derive the product bound; actual retention-rate assumptions yield the (b/a)^(s−1) cost, together with the existing f/u source-release factor.
Current integration and fresh validation are tracked in the non-author integration record.
Builds on landed #1759; advances #1721 and #1444. The sharp example has cost 1/96 = (1/8)·(1/12) and demonstrates that dropping the inverse-density factor would falsely require 1/192. Tests also cover the full product theorem and empty source conditioning. Two existing expectation lemmas are documented and reused. This supplies the fine-bin product comparison; copy/detector/reward estimates and the recursive estimator remain open.
Validation and independent agent review are recorded in this revision. Strict direct Lean checks passed for both affected probability modules and their behavioral tests, with warningAsError=true and project linters; tracked aggregate, committed imports, and whitespace checks passed. Lean CI passed for this published revision. AI assistance: ChatGPT authored the proofs and tests, performed independent agent review, and integrated the change.