postedWeight_tiltedCost_not_sizeWeight
plain-language theorem explainer
For any nonzero tilt t with |t|<1, the posted weight of the tilted letter cost is never a size-blind weight on bound-3 complexes. Gap-2 gravity arguments cite this to separate the labeled posting layer from the size-function residue that gluing constrains. Proof is a short contradiction: every size-blind weight is relabeling-invariant, while the tilted posted weight is not.
Claim. For every real $t$ with $|t|<1$ and $t\neq 0$, there is no size function $f:\mathbb{N}\times\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ such that the posted weight of the tilted letter cost at tilt $t$ equals the size-blind weight induced by $f$ on every bounded complex of bound $3$.
background
Gap 2 asks whether the posting layer together with the carrier gluing law forces unit sector fugacity in the path-sum measure. The closed-form residue of a size-blind weight that glues is inverse gauge volume times one fugacity per index type; unit fugacity is the extra hypothesis that pins the measure.
A size-blind weight is the labeled weight built from a size function $f$ on vertex/edge/tetrahedron counts. Such weights are invariant under complex relabeling. The tilted family is a one-parameter continuum of non-equivariant letter costs that still post the orbit-mean coefficient $\mu$ everywhere (numerator mass equals orbit cardinality). Posting $\mu$ is a class-mass statement; it does not automatically make the labeled posted weight size-blind.
The companion non-invariance result already shows that the tilted posted weight moves under relabeling whenever $t\neq 0$ and $|t|<1$. Size-blindness is therefore the wrong channel for the tilted family at the labeled level: only its class mass (the Gibbs size function) is visible to gluing.
proof idea
Term-mode contradiction. Unpack an alleged size function $f$ that reproduces the tilted posted weight on every bound-3 complex. Feed that equality into the non-invariance theorem for tilted posted weights: it remains only to check that the candidate weight is relabeling-invariant. Rewrite both sides by the assumed equality and apply invariance of size-blind weights under the given relabeling. The resulting invariance contradicts non-invariance of the tilted posted weight for nonzero $t$ inside the unit interval.
why it matters
This is the labeled-level half of the tilted countermodel in Gap 2. Downstream, widening_blocked_by_non_sizeWeight_posting packages it as Obstruction 1: there exist costs that post $\mu$ everywhere whose posted weight is not any size-blind weight, so the A1.4 elimination predicate (unit fugacity on a representing size function) does not apply at the labeled layer. The hostile-probe witness specializes to tilt $1/2$. The module index records the corresponding underivability flag.
Together with the companion fact that the tilted class mass is still the unit Gibbs size function, the picture is sharp: posting plus gluing constrain shape at class-mass level, but the tilted labeled weight escapes the size-function channel (CarrierShuffle is a predicate on size functions). The best-behaved equivariant countermodel (characterCost) shows gluing also fails to force the fugacity value; this theorem shows a different escape route already at posting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.