Claim

superseded

theoretical Claim

Vela Mathematics Programrecorded Aug 17, 2026, 6:40 PM

Source: source:formal-conjectures
Source record: Erdos94.erdos_94.variants.sum_multiplicity
Published at: github.com

Canonical assertion

At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0. For occurrence resolution only, the exact occurrence Erdos94.erdos_94.variants.sum_multiplicity is associated with problem:erdos:94 under resolver entity root sha256:32f6e98a826da23c12c7cfcb8853e4712de130136c59f0454bd115c3fdb1e6b1. That occurrence is one of four Erdős 94 declarations Formal Conjectures publishes, and this identity does not establish the cubic distance-multiplicity conjecture.

Local Standing

Local Standing

Replayed at commit 36c6d0fef71a.

superseded

Evidence

3 retained spans.

3

Assurance

2 scoped checks, each answering a different question. They do not combine into a single verdict, and none of them is the Claim's Standing.

corrected_record_scope_fidelity

Declares 4 limits on what it establishes.

pass

occurrence_mapping_fidelity

Declares 4 limits on what it establishes.

pass

Evidence and Decision

Exact retained path.

Exact relationships

Typed edges retained by this projection.

6 relationships

corrects

1

claimstanding · supersededclaim_record edge

At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0.

No edge evidence text is retained.

sha256:aedff5078a30bea1f8a51c1188f2f0aa9bc43da06c894706297d8bd7a4830767

Supports

3

artifactrecordedcontent_addressed edge

119e4d22c1e8e5f2931f576e6e1af92f906f7bd49d7f4de28b22cb92955600ad

No edge evidence text is retained.

sha256:119e4d22c1e8e5f2931f576e6e1af92f906f7bd49d7f4de28b22cb92955600ad

artifactrecordedcontent_addressed edge

2db17099b421eff43d4892ddedcdd7b1bfecfbc6cca013447b3b94a81c3cd0f8

No edge evidence text is retained.

sha256:2db17099b421eff43d4892ddedcdd7b1bfecfbc6cca013447b3b94a81c3cd0f8

artifactrecordedcontent_addressed edge

e2054e7d5d57d1d1f4fd311d26dba65afb90ef873e7f04cb7bb5e431e43148eb

No edge evidence text is retained.

sha256:e2054e7d5d57d1d1f4fd311d26dba65afb90ef873e7f04cb7bb5e431e43148eb

corrects from

1

claimstanding · acceptedclaim_record edge

At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0. For occurrence resolution only, the exact occurrence Erdos94.erdos_94.variants.sum_multiplicity is associated with problem:erdos:94 under resolver entity root sha256:32f6e98a826da23c12c7cfcb8853e4712de130136c59f0454bd115c3fdb1e6b1. That occurrence is one of four Erdős 94 declarations Formal Conjectures publishes, and this identity does not establish the cubic distance-multiplicity conjecture.

No edge evidence text is retained.

sha256:aaaf6ebbf510ad08e6376c5958d23f4eb7704944f7d37916eee4ae253e809b3b

proposes from

1

proposalproposal · acceptedsigned_record edge

At lean-proofs commit 423344341fbfdf4f8f684a302c5d05379125e7dc, Erdos94.variants.sum_multiplicity proves that for every finite planar point set P, the sum over its distinct determined distances of the unordered-pair distance multiplicities equals P.card.choose 2, matching Formal Conjectures commit 94a278e06a8bcbc2e4f2935e491c0c115ec832e0. For occurrence resolution only, the exact occurrence Erdos94.erdos_94.variants.sum_multiplicity is associated with problem:erdos:94 under resolver entity root sha256:32f6e98a826da23c12c7cfcb8853e4712de130136c59f0454bd115c3fdb1e6b1. That occurrence is one of four Erdős 94 declarations Formal Conjectures publishes, and this identity does not establish the cubic distance-multiplicity conjecture.

No edge evidence text is retained.

sha256:aedff5078a30bea1f8a51c1188f2f0aa9bc43da06c894706297d8bd7a4830767

Not recorded for this Claim

No correction supersedes, succeeds, or depends on it.

Scope and conditions

An exact evidence file is bound to this Result; its recorded path remains in the technical record.
Occurrence association with problem:erdos:94 is navigation-only and establishes no statement identity or semantic equivalence.
Caveat: This proves only the elementary sum_multiplicity identity, not the cubic Erdős 94 theorem or either other variant.
Caveat: The Formal Conjectures build needs the mechanical Sym2.mk.uncurry to Sym2.mk API spelling change between its pinned Mathlib and lean-proofs.
Caveat: No external source-owner review, human review, upstream acceptance, or external adoption occurred.
Caveat: Producer checks are not Verification, Decision, or Standing.
Caveat: The predecessor's distance_multiplicity_double_counting Verification remains recoverable at rollback/submission-v2-coh-00 (508b39a) and is not re-attested over the compact v3 bytes.

Reproduce the source snapshot

Replay establishes the exact record and checks. It does not add scientific authority.

Inspect graph neighborhood

Cite this Result

Identifies these exact bytes. A correction or supersession produces a different record.

Vela Mathematics Program. Claim vcl_4cae0d412a95d1965b927e1f7dbaa4245f5b9c3f84c5913e1d6a7880d6349165. sha256:aedff5078a30bea1f8a51c1188f2f0aa9bc43da06c894706297d8bd7a4830767. https://problems.science/repositories/math/claims/vcl_4cae0d412a95d1965b927e1f7dbaa4245f5b9c3f84c5913e1d6a7880d6349165