stdSimplex_dist_le_one
plain-language theorem explainer
Any two points of the standard simplex lie at supremum distance at most 1. Diameter control for affine simplices and barycentric subdivision cites this bound. The proof is coordinatewise: each barycentric weight lives in [0,1], so absolute differences are at most 1, and the product metric reduces to that.
Claim. For all $x,y$ in the standard simplex $\Delta^d\subset\mathbb{R}^{d+1}$ (nonnegative coordinates summing to $1$), $\mathrm{dist}_{\infty}(x,y)\le 1$.
background
The ambient object is the standard geometric $d$-simplex: points of $\mathbb{R}^{d+1}$ with nonnegative coordinates summing to one. Mathlib equips it with the subspace metric induced by the product ($\ell^\infty$) metric on coordinate space, so distance is the max absolute difference of barycentric weights.
This module develops singular and affine subdivision machinery (barycentric iteration, support of subdivided simplices) used to make mesh size arbitrarily small. The local payoff is Stage 6 of the pre-temporal forcing chain: iterated barycentric pieces of any affine simplex inside $\Delta^d$ become uniformly small in diameter.
Membership in the simplex forces each coordinate into the unit interval $[0,1]$. That elementary bound is all that is needed for a uniform diameter estimate independent of $d$ and of the particular pair of points.
proof idea
Rewrite subtype distance as ambient product distance, then apply the product-metric criterion dist_pi_le_iff at threshold $1$. For each coordinate $j$, expand real distance as an absolute value and split into the two one-sided inequalities. From simplex membership, both $x_j$ and $y_j$ lie in $[0,1]$ (mem_Icc_of_mem_stdSimplex). Two short linarith steps close $x_j-y_j\le 1$ and $y_j-x_j\le 1$.
why it matters
Feeds the Stage 6 payoff theorem exists_asubIter_small: after enough barycentric iterations, every pair of vertices in every support simplex of an affine simplex in $\Delta^d$ has distance less than any prescribed $\varepsilon>0$. The contraction factor $(n/(n+1))^k$ only drives diameters to zero if the initial diameter is finite; this lemma supplies the uniform seed bound $\mathrm{diam}(\Delta^d)\le 1$.
In the Recognition foundation stack, controlled mesh refinement under subdivision is the geometric engine behind singular-homology and prism arguments that rigidify discrete recognition structure before temporal forcing. Without a $d$-independent diameter cap, the iteration estimate would not be uniform across ambient dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.