Repository navigation
feat(probability): bound computable hierarchy stage parameters - #1751
Conversation
Replace the arbitrary prime witness in stageModulus with computable least-prime search. Expose primality, both lower bounds and minimality; derive the factor-of-two Bertrand bound and explicit log2 and Nat.size bounds. Compute stageSide by natural ceiling division and prove equality with its former real-ceiling specification. Preserve the channel and hierarchy theorem statements and Christian Reitwiessner's source credit. This advances #1721's concrete hierarchy parameter work. The arithmetic refinement is separate from the paper's estimator and supplies no machine space certificate. The existing source mapping to OpenAI2026LogSpace Sections 2-3 and 4.5 is unchanged; the new prime bound uses Mathlib's Bertrand theorem rather than importing an OpenAI Lean implementation. Validation: the changed library module and complete hierarchy-channel test module compile with the pinned Lean 4.36.0-rc2 toolchain and strict repository options, using shared dependencies read-only and private outputs. Executable checks return [2, 11, 17, 2, 2] for boundary, composite-bound, prime-bound and ceiling-division cases. Formal tests check prime minimality, a linear bit-length specialization, the exact ceil(5/4) side and the actual retention interface at rate 1/4 with density 2/5. All previous three-layer hierarchy tests are retained and pass. Focused proof hygiene with --check-simp and git diff --check pass. Full six-gate integration validation and independent review are pending. Implemented with AI assistance by worker /root/compression_review on feat/logspace-bounded-stage-primes; coordinator /root owns integration. Independent non-author source/API review by lean_environment approved exact source revision f7400570ede09f783a5c24ecc7d13e9d9fe5c51c and independently compiled the full affected module/test. Reviewed source files are unchanged after integration. 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 22c8398. Reviewed the complete two-file change, the actual stage channel definitions and affected hierarchy clients. No blocking findings.
Nat.find selects the least prime satisfying max(2^l,M l) ≤ P. That lower bound is always positive, so Mathlib’s Bertrand theorem supplies P ≤ 2 max(2^l,M l), including l=0/M=0. Monotonicity and the power/shift identities give the stated log2 and binary-length bounds. Natural ceiling division has positive denominator 2^l and is proved exactly equal to the former real-ceiling side specification; the retention proof transports through that identity. The modulus now has the intentionally stronger least-prime meaning; existing channel/hierarchy theorem statements, rates and identifier conditions are preserved. These are executable arithmetic/value bounds, not time or independent-space certificates.
The tests retain the three-layer hierarchy and add executable boundary/composite/prime cases, minimality, nonintegral ceil(5/4), a linear bit-length specialization and actual retention rate 1/4 with density 2/5. Existing source credit is retained. No selected-abstract statement or rendering impact. Local git diff --check passed; no local Lean build. At the single inspection, Lean CI 41088348960, Guide and Comparator were running; title passed. Live head rechecked before posting. Agent review, not human approval.
|
Non-author coordinator |
The hierarchy stage parameters previously selected an arbitrary prime and used a real ceiling. This change makes the prime the least qualifying prime found by a natural-number search and computes the side length by natural ceiling division. It proves minimality, the factor-of-two Bertrand bound, explicit logarithmic and binary-length bounds, and exact equality with the former real-ceiling specification. Existing channel and hierarchy theorem statements are preserved.
The tests retain the existing three-layer hierarchy and add executable prime/side examples, the exact ceiling bridge, and the retention calculation. Strict integrated module and full test builds, tracked aggregate, hygiene and whitespace checks passed. An independent AI source/API review approved local revision
f7400570ede09f783a5c24ecc7d13e9d9fe5c51c, independently compiled both changed files, and found no issues. The published revision retains those exact files; full project gates run in CI.Part of #1444 and the hierarchy/estimator resource work. This establishes executable arithmetic and bounds on parameter values; a machine-space certificate for the search and division remains separate. Based on current main. Christian Reitwiessner's existing authorship is retained. AI-assisted implementation and review; no human approval or full derandomization endpoint is claimed.