module module moderate

`IndisputableMonolith.Mathematics.DistanceShellMultiplicity`

Defines ordered non-diagonal pair events on a finite planar point set and the multiplicity of each Euclidean distance shell. Introduces sparse shells, the unique diameter shell, and ordered forms of classical distance-counting statements (including an ordered Erdős-type claim). A pure mathematics module that packages combinatorial geometry for later Recognition-spectrum use; proofs are elementary counting and uniqueness arguments on finite sets.

claimFor a finite planar set $S\subset\mathbb{R}^2$, the ordered non-diagonal pair events are the ordered pairs $(p,q)\in S\times S$ with $p\neq q$. The ordered distance spectrum is the multiset of Euclidean lengths $\|p-q\|$, and the ordered shell multiplicity of a length $r$ is the number of such pairs at distance $r$. A shell is sparse when its multiplicity is small relative to $|S|$; the diameter shell is the (unique) shell at maximal distance.

background

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

This module treats the one-set (non-bipartite) ordered analogue. Points are planar pairs; events are ordered off-diagonal pairs. Distances form shells whose multiplicities are counted without identifying $(p,q)$ with $(q,p)$. Sparse shells and the diameter shell are singled out as extremal combinatorial objects.

Notation stays elementary: Euclidean norm on $\mathbb{R}^2$, finite cardinality, and multiplicity functions on the positive reals. No Recognition constants appear yet; the layer is pure discrete geometry feeding later spectrum bridges.

proof idea

Definition-heavy module. Core objects (ordered pair events, ordered distance spectrum, ordered shell multiplicity, SparseShell, IsDiameterShell) are introduced as defs. Supporting lemmas establish nonnegativity of the diameter value, uniqueness of the diameter shell, and the comparison that every realized distance is at most the diameter. Named theorems (ordered Erdős-type statement, divergence of sparse shells, second-sparse-shell flux bridge) are combinatorial counting or uniqueness arguments on those defs, not deep analytic machinery.

why it matters in Recognition Science

Supplies the ordered, one-channel distance-shell language that sits beside the bipartite spectrum of Erdős #661. Downstream Recognition work can treat shell multiplicities as discrete flux or alphabet sizes when coupling planar configurations to propagation delay. The sparse-shell and diameter-shell predicates isolate extremal geometric regimes that later flux-bridge lemmas (named in-module) can convert into spectral constraints. No forcing-chain landmark (T5–T8) is proved here; the module is infrastructure for distance-spectrum counting inside the mathematics layer.

scope and limits

Does not prove the classical distinct-distances conjecture or any asymptotic Erdős bound.
Does not treat bipartite $P$–$Q$ spectra; that lives in the imported module.
Does not introduce RS constants, $J$-cost, or phi-ladder mass formulae.
Does not claim infinitary or continuous limits beyond finite planar sets.
Does not assert physical units or experimental falsifiers.

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