Repository navigation
feat(logspace): compare actual conditional product means - #1759
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
Agent review by reviewer-codex-edemaine; approve f7e8f2b, reviewing this layer over #1752 and reusing its unchanged product/source-release coverage.
The actual joint source/endpoint slice supplies the density that cancels the conditional denominator. Homogeneous-loss contraction and comparison give the stated root bound with one power of the common coefficient; composition retains the exact f/u right-source cost. This matches the bounded portion of Lemmas 7.1–7.3 in the pinned preprint (pp. 35–37), without independence of estimated factors or masks. Checked the correlated 2/3 slice, means 1 and 16, coefficient 3/2 and nonzero integrated error 1/2, the concrete correction–dense mean identity, and empty cases. No findings; no curated-abstract impact. Child-terminal enlargement, fine-bin conditioning, signed domination and the recursive estimator remain open.
Read the complete diff and affected definitions/proofs/tests. Aggregate imports exactly match the tree and diff whitespace checks pass. CI inspected once: Lean run 41091348665 was running; title check passed. Author reports strict isolated module/test validation; I did not run a local Lean build. This is agent approval, not human review.
|
Non-author coordinator Integration/cache complete: exact-main CI passed all six, restored that validated merge-group artifact (attempt 1), and published at 22:27:01 UTC. The public mapping returns HTTP 200 with 4,085 unique entries; all ten new artifact references versus the reused verified The bound uses the actual joint slice and cancels its density with one power of the common coefficient, retaining the exact source normalization without independence of factors/masks. Child-terminal enlargement, fine-bin conditioning, signed domination and full recursive/machine assembly remain open in #1721/#1444. No selected-abstract impact. Agent coordination, not human approval. |
The product-error estimate must be applied to an actual conditional mean. This PR defines that mean on the joint source/endpoint slice, proves homogeneous-loss contraction, and cancels the actual slice density before summing. It then composes the result with the proved product/source-release bound and supplies the coarse-bin scalar specialization. The coefficient enters once by homogeneity, and the exact
f / usource cost is retained. Factors and masks may share arbitrary dependence.Tests use a correlated two-of-three mask whose joint density is 2/3, conditional means one and sixteen, and a coarse coefficient of 3/2. They check a nonzero integrated error, connect the mean to the actual correction–dense atom identity, and cover empty slices and an empty environment.
Strict isolated compilation of the integrated module/tests, tracked aggregate, committed imports, hygiene and whitespace checks pass. Independent AI review approved source revision
550c89a7d5035d86ca1b77c8cb82432f61e6aee0; this published revision retains the exact reviewed files. Full project gates run in CI.Based on #1752, following #1742 → #1749 → #1752. Part of #1721 and #1444. This proves the conditional product comparison on a common terminal mask. Enlargement to the child terminal domain, fine-bin conditioning, signed-term domination and the full recursive estimator remain open. AI-assisted implementation and review; no human approval or full equality is claimed.