SharedEndpointDiameterRepresentativesMeetSimply
plain-language theorem explainer
Defines the endpoint-sharing half of the local diameter-representative condition for finite point sets in the plane: distinct ordered diameter edges that share a vertex must meet simply. Cited by the case-split that builds the full ordered-representative certificate, and discharged by the shared-endpoint diameter theorem. Pure Prop packaging; no proof body.
Claim. For every finite $A \subset \mathbb{R}^2$ and every real $\Delta$ that is a diameter shell of $A$, if $e,f$ are ordered pairs in $A$ at distance $\Delta$ whose underlying unordered edges are distinct and that share an endpoint, then $e$ and $f$ meet simply.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance shell becomes a two-body recognition-energy shell, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
Points live in $\mathbb{R}^2$ (Point2). A value $\Delta$ is a diameter shell of a finite set $A$ when it is realized as a pairwise distance and is maximal among distances in $A$. The ordered diameter-edge set collects ordered pairs from $A$ at exact distance $\Delta$. Two ordered edges share an endpoint when they have a common vertex; they meet simply when their geometric incidence is the elementary (non-crossing, non-overlapping) local configuration required by the diameter-support Conway condition.
This declaration isolates only the shared-endpoint branch of that local condition. The complementary endpoint-disjoint branch is a sibling Prop; together they feed the full ordered-representative certificate.
proof idea
No proof: the declaration is a bare Prop abbreviation whose body is the universal statement above. Downstream, shared_endpoint_diameter_representatives_meet_simply proves the Prop by case analysis on the ordered pairs and local Euclidean geometry of shared vertices. The combiner distinct_diameter_representatives_meet_simply_from_cases takes this Prop (and the endpoint-disjoint sibling) as hypotheses and splits on whether two representatives share an endpoint.
why it matters
This is the endpoint-sharing half of the local diameter representative theorem for the RS reading of Erdős #132. Downstream, shared_endpoint_diameter_representatives_meet_simply discharges it, and distinct_diameter_representatives_meet_simply_from_cases merges it with the endpoint-disjoint half into the full ordered-representative certificate used for diameter-support Conway conditions.
In the module's physical picture, diameter shells are the extremal two-body recognition-energy shells; controlling how distinct diameter representatives meet at a shared vertex keeps shell occupancy and sparse-shell flux arguments geometrically honest. It does not itself invoke the forcing chain (T5–T8) or the mass ladder, but it sits in the combinatorial substrate those continuum claims rely on when distances are realized by point configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.