module module moderate

`IndisputableMonolith.Mathematics.DistanceShellMultiplicity`

Module on ordered non-diagonal pair events and distance-shell multiplicities for a finite planar point set. Discrete geometers and RS workers physicalizing Erdős distinct-distance questions cite it for sparse shells, the unique diameter shell, and ordered multiplicity counts. Structure is definitional setup plus short uniqueness and comparison lemmas, then named bridges toward sparse-shell divergence.

claimFor a finite planar set $P$, ordered non-diagonal pair events are pairs $(p,q)\in P\times P$ with $p\neq q$. The ordered distance spectrum and ordered shell multiplicity record Euclidean distances and their multiplicities. A shell is sparse when multiplicity is controlled; the diameter shell is the unique outermost shell, and distances are at most that diameter.

background

The parent import physicalizes Erdős problem #661 as a two-channel range spectrum: finite planar channels $P$ and $Q$ coupled by Euclidean delay, with classical distinct distances as the alphabet size of the cross-coupling spectrum.

This module specializes to ordered non-diagonal pairs inside one finite planar set. It introduces planar points, the set of ordered pair events, the ordered distance spectrum, and ordered shell multiplicity (how many ordered pairs realize each distance). Sparse shells are those with controlled multiplicity; a diameter shell is characterized as the outermost distance class.

Local lemmas pin nonnegativity and uniqueness of the diameter shell and the comparison that every realized distance is at most the diameter. Named targets include an ordered form of an Erdős-type sparse-shell statement and a second-sparse-shell flux bridge.

proof idea

Definition-heavy module, not a single theorem. It declares planar points, ordered pair events, ordered distance spectrum, and ordered shell multiplicity, then the predicates SparseShell and IsDiameterShell. Short lemmas prove the diameter shell is nonnegative and unique, and that every distance is at most the diameter once a diameter shell is fixed. The remaining names (Erdos132Ordered, SparseShellsDiverge, SecondSparseShellFluxBridge) package the ordered sparse-shell divergence claim and a flux-style bridge; proofs are local algebraic or counting arguments on the ordered multiplicity data.

why it matters in Recognition Science

Places ordered shell multiplicity and sparse/diameter shell language in the RS mathematics layer so distinct-distance and range-spectrum questions can be stated in the same vocabulary as the bipartite distance spectrum (Erdős #661 physicalization). Downstream use list is empty at the graph edge, so the module is a leaf setup: its named objects (especially SparseShellsDiverge and SecondSparseShellFluxBridge) are the intended hooks for later flux or forcing arguments rather than inputs to an already-wired parent theorem. It does not itself touch T0–T8, RCL, or the phi ladder; it supplies discrete-geometry scaffolding those continuum claims may later cite.

scope and limits

Does not prove the classical Erdős distinct distances conjecture.
Does not treat bipartite (two-channel) spectra; that lives in the imported module.
Does not force physical constants, phi, or D = 3.
Does not assert infinitary limits without the named sparse-shell hypotheses.
Does not supply numerical distance tables or computational enumeration.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum module_import

declarations in this module (337)

abbrev Point2 L26
def orderedPairEvents L29
def orderedDistanceSpectrum L34
def orderedShellMultiplicity L39
def SparseShell L46
def IsDiameterShell L50
theorem diameter_shell_nonneg L56
theorem isDiameterShell_unique L66
theorem dist_le_of_diameter_shell L74
def Erdos132Ordered L95
def SparseShellsDiverge L104
def SecondSparseShellFluxBridge L118
def HopfPannwitzOrderedDiameterBound L129
def DiameterShellExistsEventually L139
def DiameterShellSparseBound L147
def diameterOrderedEdges L154
theorem orderedShellMultiplicity_eq_diameterOrderedEdges_card L161
theorem diameter_ordered_edge_data L168
theorem diameter_ordered_edges_cross_distances_le L181
def DiameterShellOrderedMultiplicityBound L201
theorem diameter_shell_sparse_from_ordered_bound L210
def OnClosedSegment L218
theorem left_endpoint_on_segment L222
theorem right_endpoint_on_segment L228
theorem on_closed_segment_symm L234
theorem on_closed_segment_comm L243
theorem midpoint_on_closed_segment L248
theorem on_closed_segment_convex L255
theorem on_closed_segment_self_eq L269
theorem dist_add_on_closed_segment L278
theorem dist_left_le_of_on_closed_segment L290
theorem dist_right_le_of_on_closed_segment L298
theorem eq_right_of_on_closed_segment_of_dist_left_eq L306
theorem eq_left_of_on_closed_segment_of_dist_right_eq L315
theorem onClosedSegment_iff_mem_segment L325
theorem on_closed_segment_strict L340
def OrderedEdgesMeetGeometrically L361
def OrderedEdgesGeometricallyDisjoint L369
theorem ordered_edges_meet_symm L374
theorem ordered_edges_meet_comm L381
theorem ordered_edges_meet_swap_left L387
theorem ordered_edges_meet_swap_right L395
theorem ordered_edges_meet_of_fst_on_segment L404
theorem ordered_edges_meet_of_snd_on_segment L411
theorem ordered_edges_meet_of_fst_on_segment_symm L418
theorem ordered_edges_meet_of_snd_on_segment_symm L425
def OrderedEdgesShareEndpoint L432
theorem ordered_edges_meet_of_share_endpoint L437
def NoDisjointDiameterEdges L457
def DiameterSegmentsMeetLocally L470
def EndpointDisjointDiameterSegmentsMeetLocally L482
theorem diameter_segments_meet_from_endpoint_disjoint_core L495
def FourPointDiameterCrossing L508
theorem four_point_diameter_crossing_zero_case L521
def orient2 L536
theorem orient2_swap L540
theorem orient2_cyclic L558
theorem orient2_cyclic' L564
theorem orient2_plucker L570
theorem orient2_bcd_decomposition L576
theorem orient2_alternating_sum_eq_zero L583
theorem orient2_zero_transitive L592
theorem orient2_zero_transitive_swap L627
theorem orient2_zero_of_two_points_on_line_and_point_on_join L635
theorem orient2_left_self L663
theorem orient2_right_self L669
theorem orient2_eq_zero_of_on_closed_segment L676
theorem orient2_affine_third L686
theorem orient2_of_on_closed_segment L696
theorem exists_scalar_of_orient2_zero L708
theorem dist_from_diff_eq_smul L738
theorem affine_zero_of_nonpos_nonneg L764
theorem exists_orient2_zero_on_segment_of_nonpos_nonneg L790
theorem exists_orient2_zero_on_segment_of_nonneg_nonpos L802
theorem same_strict_sign_of_pos_mul L812
theorem convex_combo_ne_zero_of_same_strict_sign L837
theorem same_side_segments_disjoint L882
def ProperSegmentSeparation L901
theorem proper_segment_separation_signs L907
theorem proper_segment_separation_geometrically_disjoint L919

… and 257 more