5.1 The data🔗

• A coarse subdivision. Let T_0 be any subdivision of P (Theorem 7.1). (In the bi-Lipschitz case, Step 9, we will instead take T_0 of mesh \le \delta, using Theorem 8.5; nothing else changes.)

• Thresholds. Enumerate the N active indices as \alpha_0, \dots, \alpha_{N-1} and set t_{\alpha_j} := (j+1)/(N+1). Then each t_\alpha \in (0,1) and distinct active thresholds differ by at least \mathrm{gap} := 1/(N+1) > 0.

• Barycentric coordinate functionals. For each face \sigma of T_0 (an affinely independent finite set), choose affine functionals W_{\sigma,u} : \mathbb R^k \to \mathbb R, one per vertex u \in \sigma, whose restrictions to \operatorname{conv}(\sigma) are the barycentric coordinates: for q \in \operatorname{conv}(\sigma), all W_{\sigma,u}(q) \ge 0, \sum_{u\in\sigma} W_{\sigma,u}(q) = 1, and \sum_{u\in\sigma} W_{\sigma,u}(q)\,u = q. (Existence: prescribe the values \delta_{u,v} on the affinely independent set \sigma, as in Proposition 4.2. On \operatorname{conv}(\sigma), these values are the barycentric coordinates because an affine functional applied to a convex combination is the corresponding combination of its vertex values.) By affine independence, barycentric weights are unique: two weight systems on \sigma with equal (unit) total mass representing the same point agree.

• A global vertex order. Fix the lexicographic order \preceq on \mathbb R^k (any linear order would do). For a face \sigma, weights w, and a vertex v \in \sigma, the cumulative weight is \mathrm{cum}_\sigma(w, v) \;:=\; \sum_{u \in \sigma,\; u \preceq v} w(u).

In Lean, the barycentric coordinate functionals are constructed from prescribed-value affine maps and packaged, with their uniqueness, as follows (the thresholds appear further down, as exists_thresholds):

The Lipschitz bound on the cumulative-weight functionals, uniform over the finitely many faces of the coarse subdivision (used for the fineness choice in Section 5.4):