coe_predAbove
plain-language theorem explainer
The underlying natural number of the predecessor-above index map equals i−1 when p < i and equals i otherwise. Anyone tracking barycentric coordinates through a prism map on standard simplices cites this identity. The proof is a two-branch case split on p < i, rewriting with the two characterizing lemmas for that index map.
Claim. For $n\in\mathbb{N}$, $p\in\mathrm{Fin}\,n$ and $i\in\mathrm{Fin}\,(n+1)$, the natural-number value of the predecessor-above map applied to $p$ and $i$ is $i-1$ if $(p:\mathbb{N})<(i:\mathbb{N})$, and equals $i$ otherwise.
background
The module builds the classical prism operator on singular simplices: continuous maps $\Delta^{n+1}\to\Delta^n\times I$ that decompose the product of a simplex with the unit interval. The first factor of the $i$-th prism map is the affine simplex map induced by the predecessor-above index function on $\mathrm{Fin}$.
That index function, written $p.\mathrm{predAbove},i$ in Mathlib, collapses $\mathrm{Fin},(n+1)$ onto $\mathrm{Fin},n$ by skipping or decrementing according to the cut at $p$. Coercing the result to $\mathbb{N}$ is the concrete arithmetic needed when comparing faces and when proving that prism maps compose correctly with face inclusions.
Upstream, the comparison side-conditions are discharged via the standard $\mathrm{Fin}$ order characterizations (less-than and less-or-equal on underlying naturals). The prism definition itself packages this index map with a second barycentric-sum coordinate valued in the unit interval $I$.
proof idea
Case-split on whether $(p:\mathbb{N})<(i:\mathbb{N})$.
If yes, rewrite by the Mathlib lemma that characterizes predecessor-above under a strict cast-successor inequality, discharging the side condition by simpa with the $\mathrm{Fin}$ less-than definition; then simp closes the goal with the hypothesis.
If no, rewrite by the complementary lemma (predecessor-above under a less-or-equal cast-successor hypothesis), again discharging via simpa with the $\mathrm{Fin}$ order definition and the negation of less-than; simp finishes.
why it matters
This arithmetic identity is the bookkeeping step behind every prism–face commutation in the module. It is used by the five composition theorems: top and bottom of the prism (constant height $1$ and $0$), the adjacent-face cancellation that kills interior terms of $\partial P$, and the high-face / low-face factorizations that match the remaining $(i,j)$ terms of $\partial P$ against $P\partial$.
Those identities are exactly the geometric content of the prism operator in singular homology: they make the prism a chain homotopy between the two endpoint inclusions of $\Delta^n\times I$. In the Recognition foundation stack this sits in Stage 1 of the singular-prism development, supplying the continuous maps later fed into homology and forcing-chain arguments. It does not itself touch T5–T8 or the J-cost; it is pure simplex combinatorics supporting that later layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.