twoPointOneEdge
plain-language theorem explainer
The minimal two-vertex complex with a single directed edge from 0 to 1 (no tetrahedra). It is the oriented witness in the Gap-2 ledger site-symmetry no-go: gauge counting wants mass 1 on this complex, while the edgeless pair wants 1/2. Pure data abbreviation packing vertex/edge/tet counts and the endpoint map; cited by the Aut-cardinality, measure, and headline obstruction theorems in the same module.
Claim. For any bound $B\ge 2$, the bounded complex with $n_V=2$ vertices, $n_E=1$ edge, $n_T=0$ tetrahedra, whose unique edge joins ordered endpoints $(0,1)$, and whose tetrahedron map is empty.
background
Gap 2 (R2) asks whether the recognition ledger's site symmetry can supply the gauge-counting measure on triangulation classes. The natural first move is orbit-stabilizer: read mass off how many site relabelings leave ledger cost fixed, yielding factors $1/|\mathrm{Aut}|$.
A BoundedComplex B is a finite complex whose vertex, edge, and tetrahedron counts are bounded by $B$, together with maps naming the endpoints of each edge and the four vertices of each tet. Automorphisms are relabelings that preserve those incidence data; crucially, edge comparison uses ordered endpoint pairs, so orientation is visible to the complex but not to a symmetric ledger cost.
The module pairs this directed-edge complex with the edgeless two-point complex. On a two-element site type every recognition ledger is a symmetric zero-diagonal matrix, hence fixed by the transposition, so both complexes share site-symmetry count 2 while their geometric automorphism counts differ (2 vs 1).
proof idea
Definitional abbreviation, not a proof. It fills the BoundedComplex record: two vertices, one edge, zero tets; the bound hypotheses discharge the size inequalities (2 ≤ B, 1 ≤ B, and 0 ≤ B); edgeVerts is the constant map to the ordered pair (0,1); the tet map is the empty elimination on Fin 0.
why it matters
This is one of the two concrete witnesses that kill ledger-site-symmetry as a route to gauge counting. Downstream, the automorphism group is shown to be a subsingleton, so its cardinality is 1 and the symmetry-factor measure equals 1. The companion edgeless pair has measure 1/2. The headline theorem then: any candidate measure that factors, on two-vertex complexes, through the site-symmetry count of an encoded ledger cannot satisfy gauge counting, because the two witnesses agree on every such count yet disagree on measure.
Framework role: a scoped no-go inside the gravity seven-gaps program. It does not close the open measure obligation; it names what any successful derivation must import instead (orientation-carrying ledger refinement, or sites on simplices rather than vertices alone). No direct appeal to T5–T8 or the RCL is needed here; the obstruction is purely combinatorial on the smallest complexes where gauge counting speaks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.