R10
plain-language theorem explainer
R10 packages the statement that every sector fugacity weight is invariant under combinatorial relabeling of a size-bounded complex. Anyone auditing Gap-2 gauge-counting reasons cites it as the formal content of the “label indifference” candidate. The declaration is pure Prop packaging: the body is the quantified equality, discharged later by the invariance lemma for fugacityWeight.
Claim. For every bound $B\in\mathbb{N}$, every real assignment $a$ of the three index sizes, and every pair of bounded complexes $K,K'$ of size at most $B$, if $K$ and $K'$ are relabeling-equivalent then the fugacity weight of $a$ on $K$ equals that on $K'$: $a(n_V,n_E,n_T)/(|V|!\,|E|!\,|T|!)$ is the same for both.
background
Gap-2 asks for a physical class mass on combinatorial triangulations that obeys the Gauge Counting Principle (GCP): mass of an orbit equals $1/|\mathrm{Aut}|$ (equivalently $\nu=1/|\mathrm{Aut}|$). The module runs a necessary-reasons census: every candidate fact that might force GCP from richer RecognitionLedger or posting-layer structure is listed, then scored THEOREM, OPEN, MODEL, or REFUTED.
A BoundedComplex B is a size-capped abstract triangulation (at most $B$ vertices, edges, tetrahedra) with incidence data only; the substrate fixes edge length at the minimum mesh. Two such complexes are Equivalent when one is a combinatorial relabeling of the other. A sector fugacity is any real map $a$ of the three index sizes $(n_V,n_E,n_T)$; the labeled weight is $a$ divided by the product of factorials of those sizes (the gauge volume).
Upstream, fugacityWeight is exactly that quotient. Its invariance under relabeling is already proved: every sector fugacity yields a relabeling-invariant labeled weight, so label indifference alone does not pin $a$.
proof idea
Definitional packaging only. The body is the universal Prop that, for arbitrary bound $B$, arbitrary fugacity $a$, and equivalent bounded complexes $K\sim K'$, the two fugacity weights agree. No tactics run here; discharge is deferred to R10_indifference_family_underdetermines, which applies the upstream lemma fugacityWeight_invariant, and to the one-line wrapper R10_reason that inhabits this Prop.
why it matters
In the necessary-reasons census this is the formal content of reason R10. Downstream R10_indifference_family_underdetermines proves the Prop and scores it REFUTED as a selecting principle: an entire family of fugacities is label-indifferent, so indifference cannot force the Gibbs numerator $a\equiv 1$. That kill is banked as N-route-gap2-premise-is-label-indifference and appears in correctedFloorPlans and the historical firstAttackBlock.
R10_reason inhabits the Prop; reasonTable records the row. Together with R07 (invariant enrichment uniqueness wall), R08 (equivariant costs contribute no factor), and R18 (rebooking gauge wall), R10 closes the “mere symmetry of labels selects Gibbs” route. The residual open selector named in the module doc is an action-first prior that pins the action independently of the measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.