tiltedNumer_pos
plain-language theorem explainer
For tilt parameter |t|<1, the tilted numerator of any bounded complex is strictly positive. Anyone citing the non-equivariant Gap-2 witness needs this as the domain side of exp/log. The proof is three-way case split on edge sign, then linear arithmetic from the |t|<1 bounds.
Claim. Let $t\in\mathbb{R}$ satisfy $|t|<1$, and let $K$ be a bounded complex. Then the tilted numerator at $(t,K)$ is strictly positive: $0 < N_{\mathrm{tilt}}(t,K)$.
background
Gap 2 asks whether a non-equivariant letter cost can still post the measure factor $\mu$ without a Boltzmann numerator that is identically one. The equivariant route forces the numerator to be constantly one on each orbit; the open case is mean-one with non-constant terms.
This module builds a one-parameter witness: a tilted cost whose Boltzmann numerator varies across an orbit (via an edge-label transposition twist) yet averages to one. The tilted numerator $N_{\mathrm{tilt}}(t,K)$ is the closed-form expression for that Boltzmann factor; it is assembled from the edge sign of $K$ and the tilt $t$.
Positivity is the analytic prerequisite for writing the history cost as $-\log N_{\mathrm{tilt}}$, so that $\exp(-\mathrm{historyCost})=N_{\mathrm{tilt}}$ holds on the nose.
proof idea
Unpack $|t|<1$ into the two strict inequalities $-1<t$ and $t<1$. Unfold the definition of the tilted numerator. Case on the three exhaustive edge-sign values of $K$ (via edgeSign_cases). In each branch rewrite the numerator to the corresponding linear expression in $t$, then finish by linarith against the two bounds on $t$. No measure or Gibbs data enters.
why it matters
Parent theorem exp_neg_historyCost_tiltedCost quotes this result directly: after rewriting the tilted history cost, it applies Real.exp_log at tiltedNumer_pos to identify the Boltzmann numerator of the witness with $N_{\mathrm{tilt}}(t,K)$. That identification is the concrete content of the Gap-2 witness in the non-equivariant posting case.
Within the Seven Gaps gravity stack, Gap 2 is the remaining posting-layer obstruction after the equivariant route is closed. Establishing a positive, explicitly tilted numerator lets the orbit-mean-one condition hold without forcing the numerator to be identically one, which is exactly the case the equivariant theorem left open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.