refactor: extract shared definitions into HuangzhongLaw72.Shared#3
Open
devin-ai-integration[bot] wants to merge 1 commit into
Open
refactor: extract shared definitions into HuangzhongLaw72.Shared#3devin-ai-integration[bot] wants to merge 1 commit into
devin-ai-integration[bot] wants to merge 1 commit into
Conversation
Extract 13 duplicated definitions and theorems from HuangzhongLaw72.lean and HuangzhongLaw72_core.lean into a new shared module: - doubleFactOdd (definition + succ/pos/odd/ge_pow3/strictMono) - piE_term, piE_term_norm_le, piE_series_summable - piE_norm_summable, piE_tail_summable, piE_tail_norm_summable - geom_tail_summable, partialSum_piE_real, piE_limit Rename HuangzhongLaw72_core.lean -> HuangzhongLaw72/Core.lean to fit the module hierarchy. Both files now import from Shared instead of re-declaring the same code. Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
Author
🤖 Devin AI EngineerI'll be helping with this pull request! Here's what you should know: ✅ I will automatically:
Note: I can only respond to comments from users who have write access to this repository. ⚙️ Control Options:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Eliminates ~100 lines of duplicated code between
HuangzhongLaw72.leanandHuangzhongLaw72_core.leanby extracting 13 shared definitions/theorems into a newHuangzhongLaw72/Shared.leanmodule.What moved to
Shared.lean:doubleFactOdd+ properties (_succ,_pos,_odd,_ge_pow3,_strictMono,_cast_pos)pow3_cast_pos,piE_term,piE_term_norm_lepiE_series_summable,piE_norm_summablegeom_tail_summable,piE_tail_summable,piE_tail_norm_summablepartialSum_piE_real,piE_limit,piE_limit_eq_tsumStructural change:
HuangzhongLaw72_core.lean→HuangzhongLaw72/Core.lean(fits module hierarchy). Both consumer files nowimport HuangzhongLaw72.Sharedand retain only their unique content:SunYi,huangzhong, category-theory framework)truncation_6_approx(6-term error bound)Proofs adapted to Mathlib4 v4.30 API changes (
Summable.sum_add_tsum_nat_add,Summable.tsum_le_tsum,div_le_div_of_nonneg_left). Fulllake buildpasses.Link to Devin session: https://app.devin.ai/sessions/7d7bee1bfe334766b67ff4802561f331
Requested by: @jackyfan01