equivariance_is_load_bearing

Gap 2 asks how a letter cost posts the scalar measure $\mu$ on gauge classes of bounded complexes. For equivariant costs the answer is sharp: the cost posts $\mu$ exactly when its Boltzmann numerator $\exp(-\mathrm{historyCost})$ is identically one, so the cost layer contributes no nontrivial factor. That equivalence is the content of the equivariant posting theorem; its docstring leaves open the non-equivariant case.

The module first isolates the true condition with no equivariance hypothesis: class mass of a posted weight equals the Gibbs weight times the total of the numerator over the class, while $\mu$ is orbit cardinality times the same Gibbs weight. Hence posting $\mu$ is exactly the statement that the numerator has orbit mean one. Equivariance upgrades mean one to identically one only because it forces the numerator to be constant on each orbit.

The remaining question is whether mean one can hold with non-constant terms. The device is a tilt of the letter cost that reads edge labels and flips sign under a transposition of two edge letters, splitting orbits into cancelling halves.

Concrete witness: the tilted letter cost at tilt $1/2$. First check $|1/2|<1$ and $1/2\neq 0$ by absolute-value splitting and norm_num. Package the witness with refine:

• non-equivariance from tiltedCost_not_equivariant;
• exact posting of $\mu$ on every class of bound $3$ from tiltedCost_posts_mu;
• failure of the numerator to be identically one by contradiction: if it were, evaluation at the fixed complex loopAndBridge would contradict numerator_ne_one_at_loopAndBridge.

Thirteen lines, all discharged by the tilted-cost API already built in the module.

This is the witness half of Gap 2. Downstream, nonequivariant_case_verdict packages the five-part resolution: posting $\mu$ is always orbit mean one; equivariance upgrades mean one to identically one; without equivariance the upgrade fails (this theorem); the posted weight need not be relabeling-invariant, so the uniqueness wall is escaped. The sibling continuum statement strengthens the point: every nonzero tilt of size less than one works, so the non-equivariant class contains a one-parameter family, not a single accident.

In the Recognition gravity stack this closes the posting-cost route for the open non-equivariant branch named by the equivariant iff and exhibited (but not decided) by the vertex-index cost in the floor module. It does not by itself derive the physical measure; it shows that the equivariance hypothesis in the earlier equivalence is load-bearing and cannot be dropped.