The multiplicity diagram is finite at every bar: mult(rankFn)(p) ≠ ⊤

Let ι be a type, stage : ℝ → Set ι a stage family and J : ℝ → ι → ι → Prop a relation family satisfying the filtration law hLaw and the tameness module axioms hTame. Then for every point p of the extended-real plane with second coordinate equal to ⊥ (a birth-only bar) or strictly below the first coordinate (a genuine bar d < b), the multiplicity is finite: mult (rankFn stage J) p ≠ ⊤. Proof: a general exclusion principle says that any extended natural bounded by a finite one is finite (x ≤ y, y ≠ ⊤ ⟹ x ≠ ⊤). If p.1 is a real coercion and p.2 = ⊥, the multiplicity unfolds to an infimum over ε > 0 and t ≤ b − ε of rank differences; evaluating at ε = 1 and t = b − 1 bounds it by rankFn (b − 1) (b − 1) − rankFn (b + 1) (b − 1) ≤ rankFn (b − 1) (b − 1), which is finite by q-tameness (every rank is finite: the t-classes of points alive at s form a finite set). If p.2 < p.1, both coordinates are real coercions, and evaluating the infimum at ε = (b − d)/4 bounds the multiplicity by a finite rank, again finite by q-tameness. If p.1 is not a real coercion (⊥ or ⊤), the multiplicity is 0 by the unfolding's if-branch, and 0 ≠ ⊤.