tiltedNumer_loopAndBridge
plain-language theorem explainer
At the distinguished loop-and-bridge complex, the tilted Boltzmann numerator equals $1+t$ for every real tilt $t$. Anyone citing the Gap-2 non-equivariant posting witness needs this evaluation: it is the explicit non-unit value that shows orbit-mean-one without pointwise one. The proof unfolds the numerator and rewrites by the edge-sign at that complex plus $r\cdot 1=r$.
Claim. For every real tilt $t$, the tilted numerator evaluated on the loop-and-bridge complex equals $1+t$.
background
Gap 2 asks whether a letter cost that is not gauge-equivariant can still post the measure $\mu$ while its Boltzmann numerator is not identically one. The equivariant route reduces posting to a unit numerator; without equivariance the sharp condition is only orbit-mean one (class mass of the posted weight equals $\mu$ exactly when the numerator totals the orbit cardinality on each gauge class).
The witness is a one-parameter tilted letter cost. Its Boltzmann numerator is assembled from a base factor and an edge-sign that flips under the edge-label transposition twist (swap of letters 0 and 1). The complex loopAndBridge is the concrete labeled 3-complex where that sign is $+1$, so the tilt enters as a plain additive shift.
Sibling facts record that class mass factors as Gibbs weight times numerator mass, and that $\mu$ is orbit cardinality times the same Gibbs weight; posting $\mu$ is therefore numerator orbit-mean one. This lemma supplies the pointwise value of that numerator on the witness complex.
proof idea
Term-style unfold-and-rewrite. Unfold the definition of the tilted numerator (structurally $1$ plus tilt times the edge sign). Rewrite by the specialized fact that the edge sign on loop-and-bridge is $+1$, then cancel the trivial factor via multiplication by one. No case split and no analysis beyond that algebraic identity.
why it matters
This is the arithmetic pin of the Gap-2 witness family. Downstream, numerator_ne_one_at_loopAndBridge rewrites the exponential of minus history cost through this identity and concludes the numerator is not $1$ for any nonzero admissible tilt. The continuum statement nonequivariant_posting_family and the concrete open-case closer nonequivariant_cost_posts_mu_with_nonunit_numerator (tilt $1/2$, numerator $3/2$) both quote it. Injectivity of the family at this complex, non-equivariance of the tilted cost, and non-invariance of the posted weight likewise reduce to comparing $1+t$ against $1-t$ on a twist pair.
In the Recognition gravity stack this settles the case left open by the equivariant posting theorem and exhibited but undecided in the posting-layer floor: non-equivariant costs can post $\mu$ by orbit-sum cancellation. It does not touch the uniqueness wall for relabeling-invariant weights; the posted weight of the witness is deliberately non-invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.