numerator_ne_one_at_loopAndBridge
plain-language theorem explainer
For any nonzero tilt t with |t|<1, the Boltzmann numerator of the tilted witness cost at the loop-and-bridge complex is not one. Gravity workers on the Gap 2 posting-cost route cite this to place the witness outside the equivariant class, where unit numerator is forced. The proof rewrites the exponential history cost to 1+t and contradicts t≠0 by linear arithmetic.
Claim. Let $t\in\mathbb{R}$ satisfy $|t|<1$ and $t\neq 0$. Write $C_t$ for the one-parameter tilted letter cost and $\gamma$ for the loop-and-bridge labeled complex. Then $\exp(-\mathrm{historyCost}(C_t,3,\gamma))\neq 1$. Equivalently, the Boltzmann numerator of $C_t$ at $\gamma$ equals $1+t$ and is therefore non-unit.
background
Gap 2 asks when a letter cost posts the class mass $\mu$. For equivariant costs the answer is sharp: posting $\mu$ holds exactly when the Boltzmann numerator $\exp(-\mathrm{historyCost})$ is identically one, so the cost layer contributes no factor. The open residue is whether a non-equivariant cost can still post $\mu$ while its individual numerators are not constantly one, by having orbit means equal one without pointwise constancy.
This module answers that residue in the witness direction. It builds a one-parameter tilted cost $C_t$ whose numerator varies on gauge orbits. The complex $\gamma$ called loop-and-bridge is a concrete labeled carrier used as a test point: at $\gamma$ the tilted numerator evaluates to $1+t$. The history cost is the cumulative letter cost along a presentation of fixed size three; the Boltzmann factor is its negative exponential.
The surrounding lemmas already give the orbit-mean characterization of posting $\mu$ for arbitrary (not necessarily equivariant) costs, and show that equivariance forces constancy on orbits. The present statement is the elementary non-unit evaluation that feeds the later asymmetry argument.
proof idea
Term-mode proof in three beats. First rewrite the left-hand side by the identity that converts the exponential of minus the tilted history cost (under $|t|<1$) into the explicit tilted numerator. Second, specialize that numerator at loop-and-bridge, obtaining the algebraic value $1+t$. Third, assume $1+t=1$ and discharge $t=0$ by linarith, contradicting the hypothesis $t\neq 0$. No induction or case split is required; the work is entirely in the two rewrite lemmas plus linear arithmetic.
why it matters
The equivariant posting theorem already closes the route for costs constant on gauge orbits: unit numerator is forced. The module docstring flags the complementary case, non-equivariant costs whose orbit-sum of Boltzmann factors equals the orbit count while individual terms differ. This theorem supplies the first half of the witness: at loop-and-bridge the tilted numerator is $1+t\neq 1$ whenever the tilt is nonzero.
Together with the companion evaluation on the twist of loop-and-bridge, it shows the witness is label-asymmetric on a gauge pair, hence not equivariant, while still able to post $\mu$ by orbit-mean one. That settles Gap 2 in the witness direction and confirms that the sharp condition is orbit-mean one, not identical one. In the broader Recognition gravity stack this keeps the posting-layer floor honest: the wall quantifies over a class the witness deliberately exits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.