twoPointComplex
plain-language theorem explainer
Defines the two-vertex, edgeless, tetrahedron-free bounded complex at any vertex cap B ≥ 2. It is the concrete witness configuration for the Lane D1 no-go: invariance axioms alone do not fix the path-sum measure. Downstream results compute |Aut| = 2 and separate μ = 1/|Aut| from the uniform weight. The body is a pure structure instance with empty edge and tet maps.
Claim. For every natural number $B \ge 2$, there is a bounded complex of cap $B$ with exactly two vertices, zero edges, and zero tetrahedra; the edge- and tetrahedron-vertex maps are the unique maps out of the empty type.
background
Lane D1 of the Seven Gaps program asks whether relabeling invariance, positivity, and normalization alone force the path-sum weight $w(K) = 1/|\mathrm{Aut}(K)|$ on scoped configurations. The module answers no: several distinct weights satisfy the named InvarianceAxioms, so uniqueness fails without extra substrate structure.
A BoundedComplex B packages finite vertex, edge, and tetrahedron counts (each at most $B$) together with incidence maps. The empty complex is the unit for normalization ($w(\emptyset)=1$). The two-point object is the next simplest nontrivial shape: two free vertices and no incidence data, so every permutation of the two vertices (and the empty edge/tet data) is an automorphism candidate.
The construction is an abbreviation so that the numeric fields $n_V=2$, $n_E=0$, $n_T=0$ reduce during typeclass and cardinality elaborations used by later automorphism and measure lemmas.
proof idea
Definitional instance, not a proof. Fill the BoundedComplex B fields: two vertices, zero edges, zero tets; the bound hypotheses are $2 \le B$ for vertices and Nat.zero_le B for the empty edge and tet counts. The incidence maps are elim0 on the empty finite types, so there are no edges or tetrahedra to assign vertices to. As an abbrev, the size fields unfold by definitional equality in downstream rewrites.
why it matters
This is the explicit witness that drives the kernel no-go. autCard_twoPointComplex shows $|\mathrm{Aut}|=2$ via twoPointAutEquiv with the permutation triple; mu_twoPointComplex then gives $\mu=1/2$. From that point the module separates candidates: muMeasure_lt_uniform_at_witness ($1/2 < 1$), muMeasure_ne_uniformMeasure, muSqMeasure_separations, and injectivity of the power family muPowMeasure at the same configuration.
The headline mu_not_determined_by_invariance packages the kill: both $\mu=1/|\mathrm{Aut}|$ and the uniform weight satisfy every named invariance axiom yet disagree at this complex. The positive "mu-from-invariance" claim stays dead; any unique derivation of the path-sum measure must import richer structure (gluing, orbit-stabilizer, substrate) beyond the named axiom set. That uniqueness problem remains the open substrate-derivation frontier for gravity path sums.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.