Audit the exact one-dimensional Erdős 1084 value

[DomTheDeveloper]

Green result

The complete proof of the exact one-dimensional value

f 1 n = n - 1

now replays successfully against the current catalog definition and pinned Lean toolchain.

The proof is mathematically faithful:

• upper bound: inject each unit-distance pair into its larger endpoint, excluding the minimum point;
• lower bound: use the integer-line witness {0,1,…,n-1}.

Immutable provenance

Historical source blob:

771c6c62762fa9e970dd3d3c52e984d18db216d5

Audit branch head:

8bd9c48b60533cfbeb50c60d28e893a6c7ef3a9d

Focused run 30213292071 passed:

• exact source-blob verification;
• current catalog-module build;
• proof-only source generation;
• no-hole/no-trust scan;
• complete Lean compilation;
• exact theorem axiom audit.

Axiom footprint:

[propext, Classical.choice, Quot.sound]

No sorryAx or compiler-trust dependency appears.

Status

Green proof recovery. The canonical admitted declaration still needs a focused restoration patch before promotion to _PRs/ready/. This audit-only PR should not merge.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.