feat(ForMathlib): single-chart boundary-cell count (3/4) - #15
Merged
Conversation
This was referenced Jun 19, 2026
Stacked on 2/4. Adds the `1/n`-closeness helper `abs_sub_le_one_div_of_ceil_natCast_mul_eq` (introduced here, next to its first use) and `ncard_index_image_chart_le`: one `M`-Lipschitz chart of `[0,1]ᵈ⁻¹` meets `O(nᵈ⁻¹)` grid cells. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…iew) Per riccardobrasca's review on PR #15: - `abs_sub_le_one_div_of_ceil_natCast_mul_eq` now takes the natural `(hn : 0 < n)` (ℕ) rather than `0 < (n : ℝ)`, casting once internally. - `ncard_index_image_chart_le` is shortened by extracting two reusable sub-results: `diam_Icc_inter_ceil_preimage_le` (the grid-fibre diameter bound) and `ncard_index_image_le_of_diam_le_lipschitz` (the per-cell count for a Lipschitz image of a small-diameter set). No statement content changes to the public chart bound. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CBirkbeck
added a commit
that referenced
this pull request
Jul 9, 2026
…o [Finite ι] Per @xroblot's review (PR #13): put each private helper next to its first use, and weaken `setFinite`'s hypothesis. - `setFinite_index_image_of_isBounded` now takes `[Finite ι]`, recovering `Fintype` via `Fintype.ofFinite` inside the proof — dropping the `set_option linter.unusedFintypeInType false` workaround (the conclusion never mentions `Fintype.card`). - `ceil_natCast_mul_le_ceil_natCast_mul_add` moved next to its only consumer `ncard_index_image_le_of_diam_le`; `abs_sub_le_one_div_of_ceil_natCast_mul_eq` next to `ncard_index_image_chart_le`. This re-slices the stack so each helper lands in the PR that first uses it (#14, #15) instead of #13. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Collaborator
|
This now needs a merge master. |
…nature
- ncard_index_image_le_of_diam_le_lipschitz and ncard_index_image_chart_le
take an explicit [Fintype i] (master merge generalised the section
variable to {i : Type*})
- the _lipschitz helper drops the 0 <= r argument removed from
ncard_index_image_le_of_diam_le in 14
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Owner
Author
|
Done — merged master in and retargeted the base:
|
…omain - ncard_index_image_chart_le now takes phi : (kappa -> R) -> (iota -> R) for any [Fintype kappa], with the boundary factor (n+1) ^ Fintype.card kappa in place of the hardcoded Fin (Fintype.card iota - 1); the proof only ever used finiteness of the domain (riccardobrasca review) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
3 participants
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.
Adds the
1/n-closeness helperabs_sub_le_one_div_of_ceil_natCast_mul_eq(introduced here, next to its first use per @xroblot's review) andncard_index_image_chart_le: a singleM-Lipschitz chart of[0,1]ᵈ⁻¹meetsO(nᵈ⁻¹)grid cells.Builds green on the
v4.31.0-rc1/ mathlib-master pin.🤖 Generated with Claude Code