fst_mem_edgeVerts
plain-language theorem explainer
If an ordered pair belongs to an edge set, its first endpoint lies among the vertices that appear in that set. Cosmology proofs that quantify over realised vertices of E cite this. The argument is a one-line Finset membership wrapper: image of fst, then left disjunct of the union.
Claim. Let $E$ be a finite set of ordered pairs on a type $V$ with decidable equality, and let $p\in E$. Then the first component $p_1$ belongs to the vertex support of $E$, defined as the union of the images of the two projections of $E$.
background
Phase 59 of the Recognition cosmology stack studies integer-rung descent on a graded field $k:V\to\mathbb{Z}$ over a finite edge set $E\subseteq V\times V$. The cost law from Phase 56 requires the unit-step invariant: every adjacency changes the rung by at most one. The positive results here show that descending the top rung preserves that invariant.
The support of an edge set is the finite set of vertices that actually appear as endpoints: $$\mathrm{edgeVerts}(E) := \pi_1(E)\cup\pi_2(E).$$ Downstream existence statements need this support to be nonempty whenever $E$ is, and to contain every endpoint of every edge. The present lemma is the first-projection half of that membership fact.
The same edgeVerts pattern appears in lattice-ball and Freudenthal geometry modules as the set of vertices incident to a concrete adjacency list; here it is the abstract Finset version used by the rung-descent theorems.
proof idea
One-line wrapper. Unfold edgeVerts as the union of the two projection images. Apply Finset.mem_union.mpr on the left disjunct, then Finset.mem_image.mpr with witness $p$, the hypothesis $p\in E$, and reflexivity on the first projection.
why it matters
Feeds exists_top_descent_unitStep, the Phase-59 existence theorem: for any nonempty edge set carrying a unit-step rung field there is a realised maximum rung $M$, and descending the top cells preserves UnitStep. That proof first obtains a nonempty support from a nonempty $E$, which needs both endpoints of some edge to land in edgeVerts; this lemma supplies the first-component direction (its twin handles the second).
In the module narrative this closes the positive half of the unit-step story: generic real-valued moves need not preserve the invariant (Phase 58), but forced top-rung integer descent does, so the Phase-56 graded cost law remains theorem-backed cycle to cycle along the engine's natural relaxation move. No new axioms; pure Finset bookkeeping under the Recognition rung ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.