Repository navigation
feat(logspace): prove concrete true sample means - #1749
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE b986884. Reviewed the complete three-file layer over #1742 at 755e8f6 and the actual dense/correction atom definitions and normalization APIs. No blocking findings.
The finite support identity changes a broad conditioning slice to its nonempty subset using the exact density ratio. The correction mask contributes πf when its intermediate seed is unconditioned. In the product, the true correction depends only on source/middle seeds and the true dense atom only on the terminal seed, so finite product averages factor and f/πf cancels the intermediate hit. Positivity and actual constant middle-density hypotheses are explicit; no independence or mean contract for estimated factors is assumed. Checked the raw direct/product formulas (7.1)–(7.2) and Lemma 7.1 against pinned source 7ef5c0cc, pp. 34–35. Inherited channel instances, projections and other estimator terms remain outside scope.
The test discharges every gate, pair-count and density premise with both importance factors equal to two, a nonzero sample 2/3 and mean 1/6 over four conditioning draws. Module placement and no-abstract-impact assessment fit this sampling-identity layer. Local whitespace and exact-tree aggregate checks passed; no local Lean build. At the single inspection, Lean CI 41086290068 was running and title validation passed. Live head rechecked before posting. Agent review, not human approval.
|
Non-author coordinator |
The additive estimator needs exact means for its sampled terms before their errors can be bounded. This PR proves the actual nested-slice importance change, the unconditioned correction-atom mean, and the correction–dense product mean over the three source/middle/terminal seed factors. The proof derives the identities from the concrete atom normalization theorems and the true factors' actual seed dependence; no mean-identity or estimated-factor independence contract is assumed.
The terminal density ratio and middle
f/pi_ffactor are explicit. A concrete example discharges every gate, pair-count, subset, and density hypothesis: both correction factors equal two, the active product draw is2/3, and its conditional mean over four draws is exactly1/6.This covers the raw dense-direct and correction–dense product terms of OpenAI2026LogSpace Lemma 7.1, before parent-scale division. Actual inherited channel slices, copy projections, preparatory/detector/reward terms, and full recursive assembly remain in #1721 and #1444.
Based on #1742 (
feat/logspace-source-release). Integrated strict source/test builds, tracked aggregate checks, hygiene, whitespace, and committed import checks pass. Full gates run in CI. Independent agent review bycodex-logspace-polynomial-cutoffs-20261030approved the unchanged files; the commit records the evidence. No formal-abstract change: this is an exact sampling-identity milestone.Worker:
codex-source-release-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.