proper_contradiction_from_separated_diameter
plain-language theorem explainer
From the unified separated-diameter contradiction one obtains the proper-case bridge: two diameter segments that are properly separated cannot have all four cross-distances bounded by the diameter. Anyone discharging the Hopf–Pannwitz four-point core in the Erdős #132 shell-multiplicity setting cites this. The proof is a one-line specialization that feeds the proper-separation hypothesis into the left disjunct of the unified statement.
Claim. Assume that for all points $a,b,c,d\in\mathbb{R}^2$ and all $\Delta\in\mathbb{R}$, the equalities $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$ together with the four cross-bounds $\mathrm{dist}(a,c),\mathrm{dist}(a,d),\mathrm{dist}(b,c),\mathrm{dist}(b,d)\le\Delta$ and the distinctness side-conditions forbid both proper and collinear segment separation. Then the same data already forbid proper segment separation alone.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean simplicity, so the classical multiplicity threshold $\le n$ becomes $\le 2n$.
Two abstract bridge propositions sit above the geometry. The proper bridge asserts that no four points with two diameter segments of common length $\Delta$ and all four cross-distances $\le\Delta$ can satisfy proper segment separation; the doc-comment identifies this as the positive-$\Delta$ orientation-sign core of four-point Hopf–Pannwitz geometry. The unified bridge strengthens the conclusion to rule out either proper or collinear segment separation under the same metric hypotheses.
The present declaration is the forgetful implication from the unified bridge down to the proper bridge.
proof idea
One-line specialization. Introduce the four points, the common diameter $\Delta$, the four distinctness hypotheses, the two diameter equalities, the four cross-distance upper bounds, and the proper-separation certificate. Apply the unified contradiction hypothesis to the same data, packaging the proper certificate as the left disjunct Or.inl of the separation alternative. No further geometric work is required.
why it matters
Inside the Distance Shell Multiplicity development this is the proper-case projection of the unified separated-diameter contradiction. The proper bridge is the orientation-sign core of the four-point Hopf–Pannwitz configuration that underpins diameter-shell uniqueness and sparse-shell control for the RS reading of Erdős #132. The companion declaration (noted in the next doc-comment) supplies the collinear case the same way; together they let any proof that already holds the unified contradiction discharge either specialized bridge without reopening the geometry. No downstream consumers are recorded yet; the lemma is infrastructure for later shell-multiplicity and diameter-shell uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.