Repository navigation
feat(probability): construct polynomial atom cutoffs and row laws - #1757
Conversation
Supply a computable rational degree-seven transition and its rescaling, with real endpoint, monotonicity, and value/complement fourth-root Lipschitz laws. Exact rational cast lemmas connect the arithmetic definitions to the real analysis. Concrete tests cover interior values, affine rescaling, clamping, equal endpoints, and root perturbations across both transition boundaries. This advances issue #1721's fourth-moment route. The pinned primary source OpenAI2026LogSpace, atoms.tex Section 5.1 at revision 7ef5c0cc, uses the same normalized-integral construction with s = 8. This implementation specializes it to s = 4 and does not claim eighth-root regularity, complete hierarchy admissibility, or machine resource bounds. No OpenAI Lean was consulted. Validation on base 2d1638c with the two added files: both modules compile under the repository's Lean options with warnings as errors using isolated temporary outputs and read-only existing dependencies; focused check_hygiene.py --check-simp and git diff --cached --check pass. The final documentation-only wording change was inspected after those builds. Full repository integration gates and independent review remain for coordinator integration; no aggregate file has been edited. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved source a6967d13aafee47ae16b61ac2b12f533426f9971 and freshly compiled both files. Publication adds only the generated aggregate import. Integrated strict module/test builds, hygiene and whitespace checks pass. Full gates run in PR CI.
Remove three aggregate imports that came from untracked source copies during integration. The polynomial switch module and tests are unchanged. Validate import targets against the committed Git tree before publication.
Use Q(t) = a*u^4/(1+u)^3 with u = max(0,(t-theta)/a). For a>0, prove nonnegativity, the upper ramp bound, lower defect theta+3*a, monotonicity, and global Lipschitz constant one. The fourth root is globally Lipschitz with explicit constant |a^(1/4)|*|a^-1|; the proof also bounds its derivative at arbitrarily large positive inputs. Definitions use exact rational arithmetic and have real cast lemmas. This is an alternative rational witness for the correction-ramp conditions of OpenAI2026LogSpace Section 4.1 at revision 7ef5c0cc, adapted to issue #1721's fourth-moment route. The primary source uses eighth roots. Full hierarchy threshold/cutoff instantiation is a separate next component; no machine resource bound is asserted and no OpenAI Lean was consulted. Validation atop a6967d13: the module and focused tests compile with the repository Lean options and warnings as errors, using private temporary outputs and read-only existing dependencies. Tests cover exact rational values, negative and large inputs, real cast compatibility, uniform ramp bounds, ordinary perturbation, and the explicit fourth-root Lipschitz constant 8 when a=1/16. Focused hygiene --check-simp and diffcheck pass. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-source-release-20261030 approved d3d62d9ff7fe1e54fabbf8b3ce779f929736f6ba. Publication preserves source/tests and adds generated import registration. Integrated strict module/test builds and hygiene/committed import checks pass. Full gates run in PR CI.
Extend HierarchyParams with the strict core threshold ladder, a positive iteration count, strict copy-count inequality, monotone bounded cutoffs, row-gate closure, and root/complement regularity. Prove the strengthened bundle nonempty using an actual rational ramp and polynomial cutoffs. The construction chooses theta = 1/(128q), width 1/(384q), theta2 = 1/(64q), copy thresholds 1/(8q) and 1/(4q), then the factorial-tail iteration count, copies, and detector ranks in the primary source's dependency order. This advances #1721's fourth-moment hierarchy gap. It is an explicit s=4 adaptation of OpenAI2026LogSpace Sections 4.1-4.4 and Remark 4.6 at pinned revision 7ef5c0cc; the source uses s=8. It does not prove eighth-root regularity, every later atom/access-score margin, a recursive estimator, or a machine-space bound. Existing HierarchyParams APIs are unchanged. Validation atop d3d62d9f: new module and focused tests compile with pinned Lean and repository options, warnings as errors, using private outputs and read-only dependencies. Tests extract actual witnesses at q=2, prove nonzero ramp and exact plateau values, use row-root perturbation at its closed endpoint, and feed the underlying parameters into the existing stage API for a nonzero two-vertex matrix. Focused hygiene --check-simp and diffcheck pass. No aggregate or existing source file was modified. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved c7ac6dea11574e721ded46aeb0f76c2ccaf79df9 and independently compiled both files. 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.
Define actual rational polynomial preparation, row-gate, auxiliary-score and broad-witness functions. Prove their range and closed threshold laws, flat rank regions, incoming-score compatibility, joint Lipschitz fourth roots, and exact rational-cast identities. Preserve the existing exponential AtomCutoffs API and Christian Reitwiessner's source credit. This is the fourth-moment adaptation for #1721 of the threshold template in OpenAI2026LogSpace (5.5), and the witness in the support-margin proof and compression-threshold table of Section 5.5, revision 7ef5c0cc. The source uses eighth roots; these degree-seven cutoffs only establish fourth-root regularity. The actual functions are proved regular, rather than an assumed regularity bundle. Normalized main outputs, access enumeration and machine-resource bounds remain separate. Validation: the new module and full focused test file compile without diagnostics with Lean 4.36.0-rc2 and repository strict options, using private outputs and read-only dependencies. Executable rational tests evaluate all three row functions to 1/4 with both switches in their transition regions. Further tests check signed inputs, closed endpoints and the witness's strict 82 > 3*27 margin, real/rational agreement, nonzero existing atomPrep and auxScore expressions on a concrete matrix, and nonconstant fourth-root variation. Focused --check-simp hygiene and staged diff checking pass. Independent review and full integration gates remain pending; aggregate regeneration belongs to the coordinator. AI assistance: implemented by worker /root/compression_review on feat/logspace-polynomial-atom-cutoffs, based on the reviewed hierarchy lane. The Stationary specialization will be a separate cross-lane change. Independent non-author source/API review by lean_environment approved exact source revision a4eae07bdd9993e038a83aea84cc3c4b31c794d9 against pinned atoms.tex, 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 d885c30, reviewing this layer over #1748.
The preparation, row, auxiliary and witness thresholds match (5.5) and Lemma 5.5 of the pinned preprint (pp. 21, 25). The proofs establish the claimed ranges, support/plateau laws and joint fourth-root Lipschitz bounds; the narrow witness retains 82 > 3·27. Checked the rational interior values, signed/boundary cases and nonzero atomPrep/auxScore clients. Existing all-positive-power cutoffs remain distinct. No mathematical/API findings; no curated-abstract impact. Stationary specialization and estimator assembly remain open.
Read the complete layer and relevant definitions/proofs/tests. Aggregate imports exactly match the tree and diff whitespace checks pass. CI inspected once: Lean run 41090505211 was running; title check passed. Author reports strict module/test validation; I did not run a local Lean build. This is agent approval, not human review.
|
Landed and usable descendant cache verified. #1757 landed at 01:15:10 UTC as 94ab5c74, with exact neutral tree Non-author coordinator The exact reviewed payloads are retained in fixed descendant The finite scalar/fourth-moment scope, support margins and root-Lipschitz laws are unchanged. Stationary specialization is the separate #1766 layer; normalized atoms and the full estimator/machine objectives in #1721/#1444 remain open. Selected abstracts/rendering are unaffected. This adds agent integration evidence, not a new mathematical or human review. |
The fourth-moment estimator needs concrete preparation, auxiliary-score and broad-witness functions with support margins and jointly Lipschitz fourth roots. This PR builds all three from the proved polynomial switch, including the source's narrow witness margin, and proves their range, threshold, rank-flatness and rational-cast laws. It also proves that the auxiliary score is one throughout the open preparation support.
The tests evaluate all three rational interior cases, signed and closed-boundary inputs, and nonzero existing atomPrep/auxScore expressions with the new cutoffs. A root-variation example forces a positive Lipschitz constant. Strict integrated module/tests, tracked aggregate, committed-import, hygiene and whitespace checks pass. Independent AI review approved source revision
a4eae07bdd9993e038a83aea84cc3c4b31c794d9against the pinned primary source; this published revision retains its exact files. Full project gates run in CI.#1748 has landed; this PR now targets
main, following #1743 → #1747 → #1748. Part of #1721 and #1444. The existing exponential cutoff API is preserved because it promises regularity for every positive root power. These new functions establish the fourth-moment route's concrete scalar cases; Stationary specialization, normalized atom families, access enumeration and the full estimator remain separate. AI-assisted implementation and review; no human approval or full equality is claimed.Integration refresh by Codex coordinator
codex-atoms-compression-integrator-20261031: ordinary merge of actual main40476ad8, preserving the original source commits, both reviewed library/test blobs and the exact feature patch. Only the generated aggregate conflict was resolved. The integration record tracks fresh current-head validation and the reused outside source approval. Selected abstracts and rendering are unaffected.