baryFn_apply
plain-language theorem explainer
The barycentric apex map on the standard $d$-simplex is definitionally the barycenter of its vertex tuple. Anyone simplifying singular-subdivision operators or support estimates will fire this simp lemma. The proof is pure reflexivity: the apex function is defined as that barycenter.
Claim. For every $m\in\mathbb{N}$ and every tuple $w:\mathrm{Fin}(m+1)\to\Delta^d$ of vertices in the standard $d$-simplex over $\mathbb{R}$, the barycentric apex function at $w$ equals the barycenter of $w$.
background
This module builds affine singular subdivision on standard simplices, the combinatorial engine behind prism operators and support-diameter estimates. The ambient object is the standard simplex $\Delta^d\subset\mathbb{R}^{d+1}$ of nonnegative coordinates summing to one.
The barycenter of a finite vertex tuple $w$ is the equal-weight average $\mathrm{sbary}(w)=\frac{1}{m+1}\sum_i w_i$, still a point of $\Delta^d$. The barycentric apex function is the same map, re-packaged with the arity expected by the subdivision and tee operators: it sends a vertex tuple to that barycenter so cones and subdivisions can attach an apex without a separate averaging step.
Upstream, the apex function is defined by direct application of the barycenter; this lemma simply exposes that equality for rewriting.
proof idea
Term-mode reflexivity. The apex function is defined as $\mathrm{fun},w\mapsto\mathrm{sbary},w$, so the stated equality is definitional and closes by rfl. Marked @[simp] so later estimates reduce apex applications automatically.
why it matters
Feeds the Stage 6 main estimate on barycentric subdivision: every piece of the subdivided affine simplex has vertices in the original hull, with pairwise distances contracted by the factor $n/(n+1)$. That bound rewrites apex evaluations through this simp lemma before comparing distances and hull membership.
In the broader foundation stack, singular subdivision underpins prism operators and homology comparisons used when Recognition Science forces discrete geometric structure (eight-tick octave, $D=3$) from the forcing chain. The lemma itself is bookkeeping, but without it the support-contraction argument cannot simplify the apex term cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.