fix(ForMathlib): exclude the base point in distinctDistancesFrom - #5065
Open
theebayuser wants to merge 1 commit into
Open
fix(ForMathlib): exclude the base point in distinctDistancesFrom#5065theebayuser wants to merge 1 commit into
theebayuser wants to merge 1 commit into
Conversation
github-actions
Bot
added
erdos-problems
The docstring says "distances between a given point and all other points",
and both consumers state R(x_i) = #{|x_j - x_i| : j ≠ i}, but the definition
took the image over all of `points`, so whenever `pt ∈ points` the self-distance
0 was counted too. Erase `pt` first.
Both consuming statements are unchanged as propositions:
- `erdos_1082.parts.ii` compensated with a `- 1`; since `dist x pt = 0` iff
`x = pt`, the old count is exactly the new count plus one, so dropping the
`- 1` yields a propositionally equal statement and the linked `formal_proof`
permalink still establishes it.
- `maximalDistinctDistancesFrom` (and hence `erdos_653`) is value-invariant:
every R(x_i) shifts by exactly 1, and the number of distinct values of a
(+1)-shifted family is unchanged.
theebayuser
force-pushed
the
fix/distinct-distances-from-self
branch
from
August 20, 2026 04:55
749b9dc to
27a7a71
Compare
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.
Closes #5064. Stacked on #5063 (the diff shows both commits until that one merges; only the last commit is this PR).
distinctDistancesFromnow erasesptbefore taking the image, matching its docstring and theerdos_1082.parts.iidrops its compensating- 1: sincedist x pt = 0 ↔ x = pt, the old count is exactly the new count plus one, so the statement is propositionally equal and the linkedformal_proofpermalink (0aca4d7) still establishes it. The docstring's "each point only determines 3 distances" now also matches the definition's value.maximalDistinctDistancesFrom/erdos_653are value-invariant: everylake --wfail build FormalConjecturesForMathlib FormalConjectures.ErdosProblems.«1082» FormalConjectures.ErdosProblems.«653»python3 scripts/check_category_warnings.pyon the elaborated 1082: clean