sphere_fin_one_finite

This module is a Mathlib-only leaf that restates the content-typed linking object and detector from the public spine, then shows the detector fails in dimensions 0 and 1. In dimension 0 the argument begins with the geometry of the unit sphere in $\mathbb{R}^{1}$: with a single coordinate, the Euclidean norm condition collapses to a quadratic equation on that coordinate.

The ambient space is EuclideanSpace ℝ (Fin 1), so points are functions Fin 1 → ℝ. The standard basis vector $e_{0}$ is the single with value $1$ at index $0$. The metric sphere of radius $1$ about the origin is exactly the classical $S^{0}$. Downstream, finiteness of this set is used to conclude that every subspace of $S^{0}$ is totally disconnected, hence has vanishing first singular homology via Mathlib’s vanishing theorem for totally disconnected spaces.

First prove the sphere is a subset of the two-point set ${e_{0}, -e_{0}}$. For $x$ on the sphere, rewrite via the zero-centered sphere characterization and Fin.sum_univ_one to get $(x_{0})^{2} = 1$, hence $(x_{0}-1)(x_{0}+1)=0$ by nlinarith. Split on the product-zero alternative: each branch forces $x = e_{0}$ or $x = -e_{0}$ by Subsingleton.elim on Fin 1 and evaluation of single. Conclude finiteness by subset of the finite set obtained by inserting one singleton into another.

This is the geometric seed for not_detects_zero in the same module: once $S^{0}$ is finite, every subspace is totally disconnected and $H_{1}$ vanishes, so no embedded circle can produce nontrivial linking homology in dimension 0. The module’s purpose is to discharge the low-dimensional cases of the linking detector before the framework forces $D = 3$ (forcing-chain step T8). Without a clean $S^{0}$ finiteness lemma, the $D=0$ half of “linking vanishes in low dimension” would not glue by exact into the public spine. No downstream edges are recorded yet; the immediate consumer is the sibling non-detection theorem and the Finite instance on the subtype.