edgeVerts
plain-language theorem explainer
Given a finite set of ordered edges on a vertex type, form the finite set of all endpoints that actually appear. Cosmology and geometry modules cite it whenever a rung field or triangulation must be restricted to the support of the adjacency. The body is the two-sided image of the edge set under the product projections, united.
Claim. For a decidable vertex type $V$ and a finite set $E$ of ordered pairs in $V \times V$, write $\mathrm{edgeVerts}(E)$ for the finite set of all first and second components of pairs in $E$: $\mathrm{edgeVerts}(E) = \{ u \mid \exists v.\ (u,v)\in E \} \cup \{ v \mid \exists u.\ (u,v)\in E \}$.
background
Phase 59 of the cosmology stack studies integer-rung descent on a graph whose edges carry the minimal-distinction invariant UnitStep: every adjacency changes the integer rung field $k : V \to \mathbb{Z}$ by at most one. The cost law from GradedRungCost is charged only on those adjacencies, so proofs need the actual support of the edge set rather than an ambient vertex universe.
This definition packages that support: the vertices that occur as either endpoint of some pair in $E$. Upstream geometry modules use the same name for concrete edge tables (Freudenthal cube edges, two-cube strip edges); here the object is the generic Finset projection, independent of any particular lattice. LatticeBallEdges supplies one concrete $E$ (ordered diamond adjacencies) that can be fed in.
The module's positive claim is that descending the top rung preserves UnitStep unconditionally. To state existence of such a descent without an external bound $M$, one must know the realised maximum is attained on a vertex that actually sits in $E$; that is exactly membership in this support set.
proof idea
One-line definitional body: take the Finset image of $E$ under the first projection, the image under the second projection, and form their union. No lemmas are applied; decidable equality on $V$ is required only so that Finset image and union are well-typed.
why it matters
The definition is the support carrier for the Phase-59 existence theorem exists_top_descent_unitStep: a preserving top-rung descent always exists for nonempty unit-step edge sets, with $M$ read off as the realised maximum on edgeVerts $E$, and with nontriviality witnessed by a vertex in that set. The companion lemmas fst_mem_edgeVerts and snd_mem_edgeVerts are the immediate membership facts used in that proof.
Downstream geometry reuses the same name for concrete Freudenthal edge tables (cube triangulation, two-cube strip) and for edgeInTet_vertices, which matches triangulation edges to tetrahedron edge vertices. In the Recognition framework this sits under the graded-rung cost path opened by T5–T7 (J-cost, phi self-similarity, eight-tick structure): UnitStep is the discrete adjacency bound the cost meter assumes, and top-rung descent is the parameter-free move shown to keep that bound cycle to cycle. The definition itself is pure bookkeeping; the theorem content lives in the descent lemmas that quantify over it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.