pathPlusEV
plain-language theorem explainer
Defines the two-edge directed path witness on four vertices: edges map to ordered pairs (0,1) and (1,2), leaving one isolated vertex. Gravity Gap-2 probes cite it as the fixed edge-valuation for automorphism and fibre counts. The body is a one-line piecewise assignment on Fin 2.
Claim. The path-plus-isolated edge map $e \mapsto (v_{\mathrm{src}}, v_{\mathrm{tgt}})$ sends the first directed edge to $(0,1)$ and the second to $(1,2)$ as an element of $\mathrm{Fin}\,2 \to \mathrm{Fin}\,4 \times \mathrm{Fin}\,4$.
background
This module is an uncommitted adversarial probe of Gap-2 label-erasure claims (G1 dependency, directed Aut recomputation, fibre counts). The ambient objects are finite directed edge valuations: maps from a two-edge index set into ordered pairs of four vertex labels.
The same assignment appears in the Poisson-coarea Gap-2 development as the path-plus-isolated witness. Downstream counts filter permutations of vertices and edges that commute with this valuation (ordered incidence preservation), and build the fibre of all valuations in the same orbit class.
In short: fix a concrete two-step directed path on four labels, then enumerate Aut candidates and fibre size against that fixed map.
proof idea
Pure definitional assignment, not a proof. On input edge index $e \in {0,1}$, return $(0,1)$ when $e=0$ and $(1,2)$ otherwise. No lemmas are applied; the term is the piecewise function itself.
why it matters
Supplies the fixed edge valuation that pathPlusAutCount filters against when counting directed Aut candidates for the path-plus-isolated witness, and that pathPlusFibre uses when collecting the fibre of namings. Those counts feed the hostile-probe checks on Gap-2 label erasure (kernel enumeration of directed Aut, fibre cardinality claims such as the measured 24 namings for two disjoint directed edges).
Within the Seven Gaps gravity stack this is scaffolding data, not a physics theorem: it pins a concrete combinatorial witness so Aut and fibre statements can be recomputed or attacked without definitional collapse. It does not itself invoke J-cost, the forcing chain, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.