tiltedNumer
plain-language theorem explainer
The tilted numerator is one plus a real tilt times the edge-label sign of a bounded complex. It is the explicit Boltzmann numerator the Gap-2 non-equivariant witness is built to produce. Anyone working the posting-cost route or the one-parameter witness family cites it as the closed form of exp(-historyCost). The body is a one-line arithmetic definition.
Claim. For a real tilt $t$ and a size-bounded labeled complex $K$, define the tilted numerator by $1 + t\,\sigma(K)$, where $\sigma(K)$ is the sign comparing the endpoint keys of the first two edge letters of $K$ (and $0$ if $K$ has fewer than two edges).
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ with a Boltzmann numerator that is not identically one. The equivariant route already shows that posting $\mu$ is equivalent to the numerator having orbit mean one; equivariance then forces that mean-one numerator to be constantly one. Without equivariance, mean one can hold with non-constant terms if an orbit splits into cancelling halves.
The witness device is a tilt of a label-reading sign. A bounded complex is a combinatorial triangulation with vertex/edge/tetrahedron counts capped by a fixed $B$. The edge sign of such a complex compares the endpoint keys of its first two edge letters (and is zero when there are fewer than two edges). That sign is the only place the witness reads a label rather than a class invariant, which is what breaks equivariance under edge-letter swap.
The module builds a one-parameter family of costs whose Boltzmann numerators are exactly these tilted values, then shows the excess over one is odd under the twist involution, so the orbit sum collapses to the orbit count.
proof idea
Pure definition: return $1 + t$ times the edge sign of $K$. No lemmas, no tactics. Downstream theorems unpack the consequences (positivity for $|t|<1$, history cost equal to $-\log$ of this value, and twist-odd excess).
why it matters
This is the closed-form numerator the entire Gap-2 witness hangs on. Downstream, the history cost of the tilted letter cost equals $-\log$ of this quantity; exponentiating recovers the numerator exactly; the posted weight is therefore this numerator times the Gibbs weight. The numerator mass theorem then shows the excess over one is twist-odd, so the class sum equals the orbit count and the witness posts $\mu$. Injectivity of the family at a fixed complex uses equality of two tilted numerators to force equal tilts, proving a continuum of distinct costs. The five-part non-equivariant verdict cites the construction as the concrete counterexample to "mean one implies identically one" once equivariance is dropped. In the Seven Gaps gravity stack this closes the open non-equivariant posting case in the witness direction: non-unit numerators can still post $\mu$, but the posted weight is no longer relabeling-invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.