Point4
plain-language theorem explainer
Four-dimensional Euclidean space over the reals, written as the type of points with four real coordinates and the standard inner product. It is the ambient carrier for the Lenz-style fixed-cross-distance construction that contrasts with planar bipartite spectra. Anyone citing the four-space collapse for Erdős #661 uses this abbreviation. The body is a one-line type synonym for Mathlib's EuclideanSpace.
Claim. Write $\mathrm{Point}_4$ for the Euclidean space $\mathbb{R}^4$ (real four-space with the standard inner-product metric).
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: finite planar point sets $P$ and $Q$ are coupled by Euclidean distances, and the classical distinct-distance count is the size of the cross-coupling alphabet. In a single positive-definite planar carrier, true two-sector orthogonality is unavailable, so the square-grid $n/\sqrt{\log n}$ scale is expected to be rigid.
To exhibit the contrasting mechanism, the same language is lifted to a richer carrier. Four-space supplies enough orthogonal room for two finite channels to sit so that every cross-distance is identical. The abbreviation simply names that ambient space: Mathlib's EuclideanSpace over $\mathbb{R}$ indexed by Fin 4.
Upstream dependencies are only the ambient Recognition scaffolding (ratio orbit two, empty channel list); they do not constrain the geometry of this type.
proof idea
Pure definitional abbreviation: Point4 is identified with EuclideanSpace ℝ (Fin 4). No proof obligations, no lemmas applied.
why it matters
Feeds the downstream predicate FixedCrossDistanceInFourSpace, which asserts existence of a single $r$ such that every cross-distance between two finite subsets of four-space equals $r$. That predicate's doc-comment states the contrast explicitly: "Lenz-style collapse in a richer carrier... Erdős #661 is hard because this orthogonal two-sector mechanism is not available in one planar carrier."
In the Recognition reading, the planar rigidity target (true two-sector orthogonality unavailable in one positive-definite plane) is the physical reason the $n/\sqrt{\log n}$ scale should not improve. Four-space is the minimal ambient dimension in which the orthogonal counter-example lives, so the abbreviation is the type-level hook for that comparison. It does not itself invoke T8 ($D=3$) or the eight-tick octave; those constrain the physical carrier, while this object is a mathematical foil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.