Repository navigation
feat(logspace): construct a regular fourth-root hierarchy - #1748
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.
edemaine
left a comment
edemaine
left a comment
There was a problem hiding this comment.
reviewer-codex-edemaine — independent agent review: APPROVE 675c2e3. Reviewed the complete three-file layer over #1747 at 92e41ef, the parent HierarchyParams fields and factorial-tail API. No blocking source findings.
The structure extends the existing stage interface. Its witness supplies the strict threshold ladder, θ₂=1/(64q), positive iteration count, small factorial tail, strict copy count, detector/gate bounds and all five cutoff/complement fourth-root bounds. Choosing the factorial target below exp(1/θ)/2 genuinely excludes k=0; integer ranks are selected after their dependencies. Arbitrary remaining channel constants are parameters of the bundle, with actual channel hypotheses still supplied to stage theorems. Checked the core parameter mapping against pinned source 7ef5c0cc, pp. 11–17, (4.2), (4.16), (4.21)–(4.24), Remark 4.6. The fourth-moment adaptation, later atom/access margins and non-effective integer selection are stated accurately.
Tests instantiate q=2 with nonzero ramp values, exact plateaus and root bounds, then consume the parent API on a nonzero two-vertex matrix. No curated-abstract impact. Local whitespace and exact-tree aggregate checks passed; no local Lean build. Author reports strict focused compilation. At the single CI inspection, 41086022944 failed during Mathlib cache acquisition: four HTTP 502 downloads, before project build/check gates. Title passed. Successful required CI remains necessary before integration; this is not a source-change request. Live head rechecked before posting. Agent review, not human approval.
|
Non-author coordinator Validated coordinator-fix verdict: APPROVE 0be2144e after independent preservation audit by The fixed main consumer at This completes the regular fourth-root hierarchy milestone. Later atom/access margins, full estimator and native resource bounds remain open in #1721/#1444/#474; the integer choices remain existential. No public statement/proof/API change or curated-abstract impact. Agent review and coordination, not human approval. |
Ordinary merge of actual landed main e19469f. Preserve the approved child library/test entries and modes exactly; preserve all unrelated main entries. Regenerate only the canonical import aggregate. Original authorship and source/API review coverage remain in parent history. NON-AUTHOR coordinator: coordinator-codex-algorithms-children-20261030. Source-only preservation checks pass; no local Lean/build performed. Fresh canonical all-six CI required after independent checkpoint audit. No curated abstract impact; broader #1721/#1444/#474 remain open. AI assistance: OpenAI Codex.
Ordinary merge of actual landed main 3ff34d3 into reviewed/restacked #1748 at 4dc26d6. Resolve only generated Complexity.lean by canonical import regeneration. The original hierarchy library/test blobs and modes remain byte-identical; all 4259 unrelated main entries and original source credit are preserved. NON-AUTHOR coordinator: coordinator-codex-algorithms-children-20261030. Source-only preservation checks pass. Fresh exact-head all-six CI required. No public statement/proof/API change or curated abstract impact. Broader #1721/#1444/#474 remain open. AI assistance: OpenAI Codex.
The existing hierarchy witness uses a hard ramp and discontinuous cutoffs, so it does not supply the regularity needed by the estimator. This PR constructs
FourthRootHierarchyParamsfrom the rational ramp and polynomial switches: actual data for everyq > 0andc_pi > 0, with the strict core threshold ladder, exact copy thresholds, positive iteration count, factorial-tail bound, strict copy count, detector-rank inequalities, cutoff monotonicities, row-gate closure, and fourth-root/complement regularity.The witness projects to the existing
HierarchyParams, so the existing stage theorems apply directly. Tests instantiateq = 2, verify nonzero ramp values and plateaus, use root perturbation bounds, and pass a nonzero two-vertex matrix through the stage nonnegativity/substochasticity API.This is the concrete fourth-moment adaptation selected in #1721. The pinned paper uses eighth roots. Later atom/access-score margins, assembly into the recursive estimator, machine certificates, and the full #1444 endpoint remain open; this PR does not label the whole estimator admissible. The scalar functions use rational arithmetic when
qis rational; integer parameter selection remains an existence argument.Based on #1747 (
feat/logspace-rational-ramp). Integrated strict source/test builds, tracked aggregate checks, hygiene, whitespace, and committed import checks pass. Full gates run in CI. Independent agent review bycodex-compression-iteration-20261030included a fresh separate compilation and approved the unchanged files; the commit records the evidence. No formal-abstract change: this is a hierarchy-construction milestone.Worker:
codex-logspace-polynomial-cutoffs-20261030; publication:codex-logspace-stack-20261030. AI-assisted implementation and agent review.