chore: commit open changes [lean-runtime-analysis]#22
Conversation
|
Warning You have reached your daily quota limit. Please wait up to 24 hours and I will start processing your requests again! |
|
Note Reviews pausedIt looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Run ID: 📒 Files selected for processing (1)
📝 WalkthroughWalkthroughThis PR replaces the placeholder selection kernel with a Hamming-weight CDF-based best-of-λ selection measure and completes the sel_amplification_bound proof; it also updates ChangesSelection Amplification Kernel Improvements
Project Infrastructure and Rebranding
Estimated Code Review Effort🎯 4 (Complex) | ⏱️ ~45 minutes Possibly related PRs
Poem
🚥 Pre-merge checks | ✅ 4 | ❌ 1❌ Failed checks (1 inconclusive)
✅ Passed checks (4 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 4
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@blueprint/src/web.tex`:
- Around line 17-19: Update the broken URLs used for site metadata: locate the
LaTeX/macros entries \home, \github, and \dochome in the file (currently
pointing to https://Jonathangadeaharder.github.io/drift-lean and
https://github.com/Jonathangadeaharder/drift-lean) and either rename them to
match an existing repository (rename repository to drift-lean) or revert the
URLs to the correct repository name (replace "drift-lean" with
"lean-runtime-analysis") so the three commands \home, \github, and \dochome
point to valid, non-404 destinations.
In `@LBTCoupling.lean`:
- Around line 586-603: The three lemmas coea_sel_measure_prob,
coea_sel_measure_cdf, and coea_measure_ge_from_count are left as sorry; either
prove them or explicitly mark them as trusted assumptions. To fix: implement
proofs for coea_sel_measure_prob by unfolding coea_sel_measure, handling the
degenerate dirac case (use Measure.dirac_apply_of_mem) then group the sum by
Hamming weight and telescope the sum ∑_w C(n,w)·(cdf(w+1)-cdf(w))/C(n,w) to get
1; implement coea_sel_measure_cdf by unfolding coea_sel_measure and coea_measure
on the A_ge (A_lvl n) k sets and showing the CDF identity 1 - (1 - μ)^λ from the
independent best-of-λ selection definition; and prove coea_measure_ge_from_count
similarly by relating counts to μ(A_ge(k)). If you intend these as axioms,
replace each sorry with a clear trusted axiom/lemma and document it, otherwise
complete the formal proofs in the lemmas named above.
- Around line 567-582: The coea_sel_measure currently spreads mass uniformly
across bitstrings of equal Hamming weight, which breaks the semantics for
lambda_pop = 1 because coea_sel_measure 1 P must equal coea_measure; fix by
replacing the uniform-within-weight construction with the true argmax selection
distribution (i.e. define a sel_argmax_dist lambda_pop P that assigns to each x
the probability that x is the argmax offspring under P, resolving ties uniformly
among equally-fit offspring), then use sel_argmax_dist in place of the current
uniform decomposition inside coea_sel_measure (and update any uses in
expected_generations to use this argmax distribution); alternatively, if you
intend to keep the level-uniform measure, move the related theorem to a
weight-quotiented state space and rename coea_sel_measure to reflect that it is
the level-uniform measure to avoid changing the original process (refer to
coea_sel_measure, coea_measure, sel_cdf, expected_generations, Population, and
BitString in your edits).
In `@LBTCoupling.lean.bak`:
- Around line 1-6: LBTCoupling.lean.bak is a leftover backup that interferes
with the Lake build; remove the file or move it out of the source tree (e.g., to
docs/ or archive/) so Lake doesn’t try to compile it; ensure only
LBTCoupling.lean remains in the repository and verify lakefile.lean still
references the intended source file.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: c777c59e-c888-48c6-8528-7a312d05d226
📒 Files selected for processing (9)
.github/workflows/blueprint.yml.github/workflows/ci.yml.gitignoreLBTCoupling.leanLBTCoupling.lean.bakblueprint/src/web.texdeep_think_rlocal.mdlake-manifest.jsonlakefile.lean
| /-- Selection measure via weight-level CDF decomposition. | ||
| The mass at bitstring x is: | ||
| (sel_cdf(hamming_weight(x) + 1) - sel_cdf(hamming_weight(x))) / C(n, hw(x)) | ||
| This distributes the probability that the best offspring has weight = w | ||
| uniformly over the C(n,w) bitstrings at that weight level. | ||
|
|
||
| Key property: μ_sel(A_ge(k)) = 1 - (1 - μ(A_ge(k)))^λ = 1 - sel_cdf(k). -/ | ||
| noncomputable def coea_sel_measure {n : ℕ} (lambda_pop : ℕ) | ||
| (P : Population (BitString n) lambda_pop) : Measure (BitString n) := | ||
| if lambda_pop = 0 then Measure.dirac (fun _ => false) | ||
| else coea_measure lambda_pop P | ||
|
|
||
| else | ||
| ∑ x : BitString n, | ||
| let w := hamming_weight x | ||
| let weight := (sel_cdf lambda_pop P (w + 1) - sel_cdf lambda_pop P w) / | ||
| ↑(Nat.choose n w) | ||
| weight • Measure.dirac x |
There was a problem hiding this comment.
This changes the Markov process instead of just encoding best-of-λ.
For lambda_pop = 1, best-of-1 should reduce to coea_measure, but this construction redistributes each weight level uniformly over all bitstrings with that Hamming weight. Unless coea_measure is already uniform within every level, coea_sel_measure 1 P is a different distribution. Since expected_generations evolves the full Population (BitString n) lambda_pop, this changes the process being bounded rather than merely quotienting the proof to level events. Please either construct the actual argmax distribution or move the theorem to an explicit weight-quotiented state space.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@LBTCoupling.lean` around lines 567 - 582, The coea_sel_measure currently
spreads mass uniformly across bitstrings of equal Hamming weight, which breaks
the semantics for lambda_pop = 1 because coea_sel_measure 1 P must equal
coea_measure; fix by replacing the uniform-within-weight construction with the
true argmax selection distribution (i.e. define a sel_argmax_dist lambda_pop P
that assigns to each x the probability that x is the argmax offspring under P,
resolving ties uniformly among equally-fit offspring), then use sel_argmax_dist
in place of the current uniform decomposition inside coea_sel_measure (and
update any uses in expected_generations to use this argmax distribution);
alternatively, if you intend to keep the level-uniform measure, move the related
theorem to a weight-quotiented state space and rename coea_sel_measure to
reflect that it is the level-uniform measure to avoid changing the original
process (refer to coea_sel_measure, coea_measure, sel_cdf, expected_generations,
Population, and BitString in your edits).
| lemma coea_sel_measure_prob {n : ℕ} (lambda_pop : ℕ) | ||
| (P : Population (BitString n) lambda_pop) : | ||
| coea_sel_measure lambda_pop P Set.univ = 1 := by | ||
| dsimp [coea_sel_measure] | ||
| split_ifs with h | ||
| · simp [Measure.dirac_apply_of_mem (Set.mem_univ _)] | ||
| · exact coea_measure_univ lambda_pop P | ||
| · -- Group the sum by weight level, then telescope | ||
| -- ∑_x weight(x) = ∑_w C(n,w) · (cdf(w+1) - cdf(w)) / C(n,w) | ||
| -- = ∑_w (cdf(w+1) - cdf(w)) = cdf(n+1) - cdf(0) = 1 | ||
| sorry | ||
|
|
||
| /-- Key CDF property: μ_sel(A_ge(k)) = 1 - (1 - μ(A_ge(k)))^λ. | ||
| This is the defining property of the best-of-λ selection measure. -/ | ||
| lemma coea_sel_measure_cdf {n : ℕ} (lambda_pop : ℕ) | ||
| (P : Population (BitString n) lambda_pop) (k : ℕ) : | ||
| coea_sel_measure lambda_pop P (A_ge (A_lvl n) k) = | ||
| 1 - (1 - coea_measure lambda_pop P (A_ge (A_lvl n) k)) ^ lambda_pop := by | ||
| sorry |
There was a problem hiding this comment.
Core selection guarantees are still unresolved on the proof path to the runtime bound.
coea_sel_measure_prob, coea_sel_measure_cdf, and coea_measure_ge_from_count are still sorry, but they are immediately used to manufacture IsMarkovKernel and to close sel_amplification_bound, which then feeds G1 and the final theorem. So the new selection kernel and amplification result are still resting on unverified obligations. If this is intentionally outside the mechanized boundary, please surface it explicitly as trusted assumptions; otherwise the core result here is still incomplete.
Also applies to: 611-614, 643-649, 814-830
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@LBTCoupling.lean` around lines 586 - 603, The three lemmas
coea_sel_measure_prob, coea_sel_measure_cdf, and coea_measure_ge_from_count are
left as sorry; either prove them or explicitly mark them as trusted assumptions.
To fix: implement proofs for coea_sel_measure_prob by unfolding
coea_sel_measure, handling the degenerate dirac case (use
Measure.dirac_apply_of_mem) then group the sum by Hamming weight and telescope
the sum ∑_w C(n,w)·(cdf(w+1)-cdf(w))/C(n,w) to get 1; implement
coea_sel_measure_cdf by unfolding coea_sel_measure and coea_measure on the A_ge
(A_lvl n) k sets and showing the CDF identity 1 - (1 - μ)^λ from the independent
best-of-λ selection definition; and prove coea_measure_ge_from_count similarly
by relating counts to μ(A_ge(k)). If you intend these as axioms, replace each
sorry with a clear trusted axiom/lemma and document it, otherwise complete the
formal proofs in the lemmas named above.
| import LintOptions | ||
| import Hoeffding | ||
| import Mathlib.Probability.Kernel.Basic | ||
| import Mathlib.MeasureTheory.Integral.Bochner.Basic | ||
| import Mathlib.MeasureTheory.MeasurableSpace.Instances | ||
| import Mathlib.Analysis.SpecialFunctions.Log.Basic |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Check if there's already a LBTCoupling.lean file that this is backing up
fd -e lean -g '*LBTCoupling*'
# Check lakefile to see what files are expected to be built
cat lakefile.lean 2>/dev/null | head -50Repository: Jonathangadeaharder/lean-runtime-analysis
Length of output: 1288
Remove or relocate the .bak backup file.
This is a backup file. The actual source file LBTCoupling.lean already exists and is included in the build system (see lakefile.lean). Since the .bak extension prevents compilation by Lake, either delete it if no longer needed or move it to a docs/, archive/, or similar non-source directory to avoid confusion.
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@LBTCoupling.lean.bak` around lines 1 - 6, LBTCoupling.lean.bak is a leftover
backup that interferes with the Lake build; remove the file or move it out of
the source tree (e.g., to docs/ or archive/) so Lake doesn’t try to compile it;
ensure only LBTCoupling.lean remains in the repository and verify lakefile.lean
still references the intended source file.
Agent-Logs-Url: https://github.com/Jonathangadeaharder/lean-runtime-analysis/sessions/6ab1f9fa-876f-4b8e-afb9-2926c50bd100 Co-authored-by: Jonathangadeaharder <44533402+Jonathangadeaharder@users.noreply.github.com>
Jonathangadeaharder
force-pushed
the
chore/pr-open-changes
branch
from
522ff85 to
209fac9
Compare
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@lakefile.lean`:
- Around line 26-30: Remove the unresolved merge-conflict markers (<<<<<<< HEAD,
=======, >>>>>>>) and the duplicated lean_exe «drift_lean» declaration so only a
single, valid lean_exe «drift_lean» where block remains; locate the conflicting
lines containing the symbols <<<<<<< HEAD, =======, >>>>>>> and the two
occurrences of lean_exe «drift_lean» and delete the conflict markers and the
extra duplicate declaration, preserving the intended configuration from one of
the blocks.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: defaults
Review profile: CHILL
Plan: Pro
Run ID: 27b9e031-9d12-4f07-b109-08a8a8450907
📒 Files selected for processing (4)
.gitignoreLBTCoupling.leanblueprint/src/web.texlakefile.lean
✅ Files skipped from review due to trivial changes (2)
- blueprint/src/web.tex
- .gitignore
Added 7 private helper lemmas translating Corus et al. 2018 Lemma 18: - one_sub_pow_le_exp_neg_mul: (1-p)^n ≤ exp(-pn) - exp_neg_le_sub_ratio: exp(-x) ≤ (n-1)/n when x ≥ log(n/(n-1)) - log_ratio_le_two_div: log(n/(n-1)) ≤ 2/n for n ≥ 2 - exp_eight_le_3072, log_3072_ge_eight: exp(8) ≤ 3072 - key_bound: 4n·log(128(n+1)n³)/e ≥ 2/n - one_sub_pow_le_ratio: (1-p)^λ ≤ (n-1)/n Also: replaced axiomatized coea_sel_measure with real CDF-based definition (sel_cdf + weight-level decomposition), added coea_sel_measure_cdf lemma (sorry), added ExponentialBounds import. Sorry count: 8 → 7 (sel_exp_inequality closed).
Jonathangadeaharder
force-pushed
the
chore/pr-open-changes
branch
from
209fac9 to
012d046
Compare
Open changes from working tree
.lake/config/to .gitignore (untracked build artifacts).lake/config/files from indexSummary by CodeRabbit
New Features
Documentation
Chores