Repository navigation
feat(logspace): bound coupled correction-dense product errors - #1752
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE cfa2bc7. Reviewed the complete four-file layer over #1749 at b986884, the actual root/loss definitions and atom support/value APIs. No blocking findings.
The scalar split through F′B weights left error by B and right error by F′. Homogeneous-loss contraction over midpoints gives the explicit constant 2^(2(s−1))s^s for every nonzero natural exponent. Summing endpoints uses B’s row cap; summing old sources uses F′’s incoming cap and the exact f/u normalization. No independence or old-source-dependent right-error contract is introduced. The atom corollary derives its caps from the actual gates and bounds from clipped denominators; only the versions needed by that split carry value bounds. Checked the scoped mapping against pinned source 7ef5c0cc, pp. 36–37, proof of Lemma 7.3. Terminal scale/conditional-mean comparisons and complete estimator assembly remain separate.
The regression uses perfectly correlated masks, independently evaluates positive product and factor root errors (81/2, 1/2, 1/6), and instantiates the atom theorem with release factor three. Exposing rootDistPow leaves its body unchanged; no selected-abstract impact. Local whitespace and exact-tree aggregate checks passed; no local Lean build. At the single inspection, Lean CI 41088660811 was running and title validation passed. Live head rechecked immediately before posting. Agent review, not human approval.
|
Non-author coordinator The single verified descendant publication provides covering native all-six checks, exact-main all-six success, validated merge-group restoration and the usable public cache. Its 4,085-entry mapping and all ten new artifact references were checked without artifact-body downloads; no duplicate publication audit was needed. The coupled-product source error uses the actual joint slice and reviewed normalization; masks and factors may be dependent. Full recursive/native estimator assembly remains open in #1721/#1444. No selected-abstract impact. Agent coordination, not human approval. |
The recursive estimator needs a product-error bound that permits the left factor, right factor and usage masks to share an environment. This PR proves that bound for actual finite matrix products, then specializes it to the existing correction and dense atoms.
Splitting through the estimated-left/true-right product charges the left error to the right row cap and the right error to the estimated left incoming cap. The latter gives the exact source normalization factor
f / u. The moment constant is explicit:2 ^ (2 * (s - 1)) * s ^ s, equal to 16384 for exponent four. The atom corollary derives its support caps and value bounds from the actual gates and clipped denominators. The only existing API change exposes the unchanged definition ofrootDistPowfor these consumers.The regression uses perfectly correlated Boolean masks, factor weights one versus sixteen, and unequal normalizations. It independently evaluates nonzero product and factor errors before applying the atom theorem. Strict integrated source/tests and the existing RootMetric tests pass; aggregate, import, hygiene and whitespace checks pass. An independent AI review approved source revision
fcbb5797a9c8b5c9bde9fd80de74ed84ec2c1e90; this published revision retains those exact files. Full project gates run in CI.Based on #1749, following #1742. Part of #1721 and #1444. This proves the coupled product/source-domain portion of Lemma 7.3 in the pinned OpenAI2026LogSpace source. Conditional means, terminal scale changes, normalizer/detector errors and the complete recursive estimator remain open. AI-assisted implementation and review; no human approval or full equality is claimed.