normalizedAtTheAtoms_tiltedCost
plain-language theorem explainer
For any tilt parameter t with absolute value less than one, the posted weight of the tilted letter cost is normalized at the empty complex and at the three atomic complexes. Anyone citing the non-equivariant Gap-2 witness needs this to keep the witness inside the admissible posting class. The proof rewrites the posted weight, forces unit numerator on complexes with at most one edge letter, and applies the atom Gibbs-weight identity.
Claim. If $|t| < 1$, then the posted weight of the tilted letter cost at tilt $t$ is normalized at the atoms: on the empty complex and on every complex with at most one edge letter, that posted weight equals $1$.
background
Gap 2 asks whether a non-gauge-equivariant letter cost can still post the projector coefficient $\mu$ while its Boltzmann numerator is not identically one. The equivariant route forces numerator one; the open case is orbit-mean one without constancy. This module builds a one-parameter tilted cost whose sign flips under an edge-letter transposition, so orbit halves cancel.
NormalizedAtTheAtoms is the admissibility filter on posted weights: they must equal one on the empty complex and on the three atomic complexes (at most one edge letter). Without it the witness would be excluded before the class-mass comparison begins.
Posted weight factors as numerator over gauge volume times a Gibbs factor. On atoms the numerator of the tilted cost is forced to one (nothing for the sign to compare), and the Gibbs weight is one, so normalization is structural rather than a numerical accident.
proof idea
Term-mode proof by introduction on the complex data, then a short rewrite chain. First replace the posted weight of the tilted cost by its explicit formula (postedWeight_tiltedCost, using $|t|<1$). Next apply tiltedNumer_eq_one_of_nE_le_one: any complex with at most one edge letter has tilted numerator one (proved by a size bound via omega). Cancel the resulting 1 * _ with one_mul. Finish with gibbsWeight_eq_one_at_atoms, which supplies unit Gibbs weight on the empty complex and the three atoms under the atom hypotheses.
why it matters
This is the normalization half of the Gap-2 witness package. Downstream, nonequivariant_cost_posts_mu_with_nonunit_numerator packages four facts at tilt $1/2$: non-equivariance, class mass exactly $\mu$ at every complex and cap, Boltzmann numerator $3/2$ (not $1$) at loopAndBridge, and this atom normalization. Without the present theorem the witness would fail the posting-layer floor's admissibility gate.
It shows the open case left by equivariant_posts_mu_iff_numerator_one is inhabited in the witness direction: orbit-sum cancellation is real, and the forward implication of that equivariant theorem is false once equivariance is dropped. The sibling index_premise_still_open records that a separate index-measure premise remains unresolved; this lemma closes only the normalization side of the posting witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.