twoEdgeFibre
plain-language theorem explainer
The named fibre of the two-edge witness (two disjoint directed edges) inside the equal-census (4,2,0) sector: all ordered edge-endpoint assignments on four vertices that are ordered relabelings of that witness. Gravity auditors cite it for the stationary class-mass ratio and the coarea identity at these witnesses. It is a plain filter of the universe of incidence maps by the ordered-relabeling predicate.
Claim. The fibre of the two-edge witness is the finite set of all maps $ev:\{0,1\}\to\{0,1,2,3\}^2$ for which there exist permutations $\sigma_v$ of the four vertices and $\sigma_e$ of the two edges carrying the fixed incidence $0\mapsto(0,1),\,1\mapsto(2,3)$ onto $ev$.
background
Gap 2 / A20 studies a raw LIFO Poissonized post/unpost process on serially named tet-free bounded complexes. Legal moves (append vertex, unpost max unused vertex, append edge, unpost max edge) each have rate 1, so the rate matrix is symmetric and the unique stationary law on each finite cap is uniform. Flag 8 is unmoved; Aut, orbit, and gauge language appear only on the conclusion side.
The equal-census pair at $(4,2,0)$ is the two-edge complex versus path-plus-isolated. The two-edge witness is the incidence sending edge 0 to endpoints $(0,1)$ and edge 1 to $(2,3)$. An incidence lies in a fibre when some ordered vertex-and-edge relabeling carries the target onto it (the Boolean predicate inFibre).
The factorial $nV!,nE!,nT!$ counts sort-respecting arrival orders; fibre cardinality equals that count divided by directed Aut order (orbit-stabilizer, conclusion only).
proof idea
Definition by filter: take the universe of all maps $\mathrm{Fin},2\to\mathrm{Fin},4\times\mathrm{Fin},4$ and retain those for which the ordered-relabeling predicate holds against the fixed two-edge incidence. No proof obligations; the body is a one-line Finset filter.
why it matters
This fibre is the left-hand witness in the scoped coarea and class-mass ratio package. Downstream, its cardinality is measured as 24, the fibre-card ratio against the path-plus fibre (48) is exactly $1/2$, and under the uniformity premise the $\pi$-weighted class-mass ratio equals that fibre ratio. The coarea identity then reads: arrival-order factorial times inverse fibre card equals inverse directed Aut order at the two-edge witness.
In the Recognition gravity lane this supplies the concrete Aut-corrected stationary mass comparison at equal census without importing FullTheoryLedger or moving Flag 8. It is the named set that makes the ratio test and the factorial-emergence claim checkable by native decision and exact rational arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.