Repository navigation
feat(logspace): construct a rational correction ramp - #1747
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE 92e41ef. Reviewed the complete three-file layer over #1743 at ce9a0be. No blocking findings.
For u≥0, the unit ramp u^4/(1+u)^3 has derivative u^3(u+4)/(1+u)^4 in [0,1], lies between u−3 and u, and has fourth root u(1+u)^(-3/4) with derivative in [0,1]. Positive-part clamping gives the global bounds. Rescaling by a>0 preserves ordinary Lipschitz constant one and gives fourth-root constant a^(1/4)/a, matching the explicit constant eight at a=1/16. Rational evaluations and casts retain the same arithmetic implementation.
Checked the ramp requirements in pinned source 7ef5c0cc, printed p. 11, (4.2). This is an alternative rational witness for the explicitly identified fourth-moment adaptation, with defect threshold θ+3a; it does not claim the paper’s eighth-root regularity or a machine-space certificate. Concrete hierarchy/atom assembly remains open. Exact negative, transition, large-input, affine and root-bound examples exercise the API. No curated-abstract impact.
Local whitespace and exact-tree aggregate checks passed; no local Lean build. At the single inspection, Lean CI 41085564473 was running and title validation passed. Live head rechecked before posting. Agent review, not human approval.
|
Non-author coordinator Fresh exact-head canonical all-six and Guide passed. The optional Comparator passed; the live main ruleset requires Scope remains a rational correction ramp with fourth-root regularity for the fourth-moment adaptation; the paper’s eighth-root and machine-space endpoints remain separate. The broader #1721/#1444 objectives stay open. Agent review, not human approval. |
Non-author coordinator coordinator-codex-circuits-readiness-20261030 prepares an ordinary main merge for PR #1747. Parents: unchanged reviewed source 92e41ef and actual main c81edae. The only conflict was generated Complexity.lean, regenerated directly from the exact tracked library-module inventory without Lean, Lake, dependencies or build/output copies. Every reviewed library/test blob, mode and source-credit byte is unchanged, and every main payload outside this PR's own two source files is preserved. Reused outside exact-head mathematical/API/source approval and canonical all-six evidence at the reviewed source. This unpublished checkpoint has source/aggregate/whitespace checks only; new integration validation and publication remain with the approved-PR sweep coordinator. No source/proof/API repair or author-branch push. Curated abstracts and rendering: unchanged source and no impact. AI assistance: OpenAI Codex performed this bounded source-only metadata preparation.
Source-only non-author coordinator checkpoint for PR #1747, refreshed onto actual observed main 29dc907. Ordinary merge parents are prior unpublished metadata checkpoint 5f93f98 and actual main. Original reviewed source 92e41ef remains an ancestor and every own reviewed library/test blob and mode is exact. Main differs only by the own reviewed module, test and one generated aggregate registration; no unrelated main payload or parent result is removed. Canonical imports match the exact tracked module inventory. Only source/aggregate/whitespace inspection was performed. Reuse original outside exact-head mathematical/API/source approval and source canonical all-six evidence; required current integration validation and publication remain with LogSq. No Lean, Lake, build-output copy, dependency checkout, source/proof/API repair or author-branch push. Curated abstracts/rendering unchanged. AI assistance: OpenAI Codex source-only metadata preparation.
A regular hierarchy needs an unbounded correction ramp as well as bounded cutoffs. This PR constructs the rational ramp
Q(t) = a * u^4 / (1+u)^3, withu = max(0,(t-theta)/a)anda > 0. It proves nonnegativity,Q(t) <= max(t-theta,0), the lower defect boundt-(theta+3a) <= Q(t), monotonicity, ordinary Lipschitz constant one, and a global fourth-root Lipschitz bound. Rational evaluation and casts are part of the API.This supplies the correction-ramp primitive for #1721's fourth-moment hierarchy adaptation. The pinned paper asks for eighth-root regularity; this PR does not claim that stronger endpoint behavior or a machine-space certificate. The next layer constructs actual hierarchy parameters from this ramp and the polynomial switches. It advances #1721 and #1444.
Parent #1743 has landed and this PR now targets
main. The non-author integration record tracks the source-preserving aggregate reconciliation and fresh required checks. Exact tests include negative, transition, and large inputs, affine scaling, rational casts, and the explicit root constant eight at widtha = 1/16. The integrated module/tests pass the strict pinned Lean build; hygiene, whitespace, and committed import checks pass. Full gates run in CI.Independent agent source/API review by
codex-source-release-20261030approved the unchanged source/tests against the pinned hierarchy section. Evidence is recorded in the commit. No formal-abstract change: this is an analytic construction.Worker:
codex-logspace-polynomial-cutoffs-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.