edgeSign_eq_zero_of_nE_le_one
plain-language theorem explainer
On any bounded complex with at most one edge letter, the edge sign is zero. This is the scope clause for the Gap-2 non-equivariant posting witness: the sign stays silent on the empty complex and the three atoms. Anyone citing the twist-flip or the tilted-numerator family needs it. The proof is a one-line case on the definition: the nonzero branch requires strictly more than one edge.
Claim. Let $K$ be a bounded complex over the polarized interface $B$. If the edge-letter count satisfies $n_E(K)\le 1$, then the edge sign of $K$ equals $0$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure $\mu$ with a Boltzmann numerator that is not identically one. The module answers in the witness direction: an edge-label transposition ("twist") splits orbits into cancelling halves, driven by a sign that flips under the twist.
The edge sign is defined by cases on the edge-letter count $n_E$. When $1<n_E$, it compares keys at edge letters $0$ and $1$ via an antisymmetric comparison; otherwise it is defined to be zero. Bounded complexes package the three size data (including $n_E$) that enter the posting normalizations.
The module already proves that posting $\mu$ is exactly orbit-mean-one of the numerator (no equivariance needed). Equivariant costs force the numerator constant on orbits, hence identically one. The remaining case needs a non-constant mean-one numerator; the sign and twist supply it, but only where $n_E\ge 2$.
proof idea
Term-mode case on the definition. Unfold the edge sign: it is an if 1 < n_E then ... else 0. The hypothesis $n_E\le 1$ is exactly $\neg(1<n_E)$, discharged by omega. Rewrite with if_neg to obtain zero. No external lemmas beyond the definition and arithmetic comparison.
why it matters
This is the scope clause named in the doc-comment: the witness puts nothing non-unit where the normalizations look (empty complex and the three atoms). Downstream, edgeSign_twist uses it for the vanishing half of the flip identity (twist preserves edge count, so zero stays zero). tiltedNumer_eq_one_of_nE_le_one applies it directly: the tilted numerator is $1 + t\cdot\mathrm{edgeSign}$, hence identically one when the sign vanishes.
Together those facts let the one-parameter tilted cost post $\mu$ with non-constant numerator on complexes that have enough edges, while remaining inert on the atomic and empty cases. That closes the open non-equivariant branch left by the equivariant posting theorem and by the floor module's exhibition of vertexIndexCost_not_equivariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.