pathPlusEV
plain-language theorem explainer
Defines the edge-to-endpoint map for the path-plus-isolated witness at census (4,2,0): two edges form the path 0—1—2 on four named vertices. Downstream Aut-count and fibre enumerations cite this fixed incidence. The body is a two-branch constant function on Fin 2.
Claim. The path-plus-isolated edge-endpoint assignment is the map $e \mapsto (u_e,v_e)$ on two edges and four vertices given by $0 \mapsto (0,1)$ and $1 \mapsto (1,2)$ (a path of length two, one vertex unused).
background
Module Gap2PoissonCoarea treats Gap 2 / A20 (lane C16): a LIFO Poissonized post/unpost process on tet-free bounded complexes. At equal census $(nV,nE,nT)=(4,2,0)$ one compares two Aut-distinct complexes; the stationary class-mass ratio under uniform $\pi$ is exactly $1/2$ after the directed Aut correction. Process language is firewalled from Aut/orbit vocabulary except in conclusions.
The path-plus-isolated witness is one side of that pair: four vertices, two edges arranged as a path, one isolated vertex. Its companion is the two-edge (disjoint edges) complex. Edge data are maps $\mathrm{Fin}, nE \to \mathrm{Fin}, nV \times \mathrm{Fin}, nV$. Related gluing primitives include the single-edge complex (two vertices, one joining edge) used elsewhere in the SevenGaps stack.
Fibre size equals the sort-respecting arrival count $nV!, nE!, nT!$ divided by directed Aut order (orbit-stabilizer on the conclusion side only). This incidence map is the seed for those counts.
proof idea
Pure definition: a lambda on $\mathrm{Fin}, 2$ with a single if-then-else. Edge index $0$ is sent to the ordered pair $(0,1)$; every other index (necessarily $1$) is sent to $(1,2)$. No lemmas, no tactics.
why it matters
Seeds the path-plus-isolated side of the Gap 2 ratio test. Immediate consumers are pathPlusAutCount (cardinality of directed Aut candidates commuting with this incidence) and pathPlusFibre (named fibre of this incidence under the in-fibre relation). Those feed the measured/theorem claim that the path-plus fibre has 24 namings, versus 48 on the two-edge side, giving the exact $\pi$-weighted class-mass ratio $1/2$ under uniformity at $(4,2,0)$.
The module headline keeps Flag 8 unmoved and does not import FullTheoryLedger. The definition is the concrete geometric input that lets the Aut-correction and fibre enumerations stay inside exact rational arithmetic on finite Fin types, without invoking continuous gravity or continuum Poissonization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.