snd_mem_edgeVerts
plain-language theorem explainer
If an ordered pair lies in a finite edge set, its second endpoint belongs to the vertex support of that set (the union of first- and second-component images). Cosmology arguments that read off realised rung values on the support of E cite this membership fact. The proof is a one-line Finset image-and-union term.
Claim. Let $E$ be a finite set of ordered pairs on a type $V$ with decidable equality, and let $p\in E$. Then the second component $p_2$ lies in the vertex support of $E$, i.e. in $\{\,q_1:\,q\in E\,\}\cup\{\,q_2:\,q\in E\,\}$.
background
Phase 59 of the cosmology stack studies integer-rung fields $k:V\to\mathbb{Z}$ on a finite edge set $E\subseteq V\times V$. The forced minimal-distinction invariant UnitStep requires that every adjacency changes the rung by at most one: $k(p_1)-k(p_2)\in{0,+1,-1}$. The live engine descends top-rung cells by exactly one step; the module proves that this parameter-free move preserves UnitStep.
The auxiliary set of edge vertices is the Finset support of $E$: the union of the first-component image and the second-component image. Downstream existence of a realised maximum rung is stated over this support, not over all of $V$, so membership of both endpoints of each edge must be recorded.
The sibling first-component lemma is the left half of the same support fact; together they feed the nonempty-support step in the top-descent existence theorem.
proof idea
Term-mode proof. Unfold the support as $\mathrm{image},\pi_1\cup\mathrm{image},\pi_2$. Apply the right-hand disjunct of Finset membership in a union, then exhibit $p$ itself as the image witness for $\pi_2$ via Finset.mem_image with the given hypothesis $p\in E$ and reflexivity on the second projection.
why it matters
Feeds exists_top_descent_unitStep, the module's main existence theorem: for any nonempty edge set carrying a unit-step rung field there is a realised maximum $M$ on the edge support such that descending the top-rung cells preserves UnitStep. That theorem needs the support to be nonempty whenever $E$ is; extracting either endpoint of a witness edge uses this lemma (or its first-component twin).
In the broader Recognition stack this closes the positive half of Phase 59: the cost meter of Phase 56/57 is theorem-backed along the forced top-rung descent (T-3 style, one rung at a time), complementary to Phase 58's negative result that a blind real-valued mean move need not preserve unit-step. No new axioms; pure Finset bookkeeping on the support that the existence argument quantifies over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.