closedForm
plain-language theorem explainer
Under the carrier-shuffle axioms, every size-blind weight on triples with at least one vertex equals three fugacity powers divided by the gauge-volume factorials. Gap-2 gluing and Gibbs-weight derivations cite this collapse of an arbitrary size function to three real couplings. The proof splits on vanishing incidence, then chains dust-row and bouquet-row identities with the factorial recurrence.
Claim. Let $f:\mathbb{N}^3\to\mathbb{R}$ satisfy the carrier-shuffle axioms: strict positivity, $f(0,0,0)=1$, and the dust-bouquet (and sibling) gluing identities on size triples. Then for all $a,b,c\in\mathbb{N}$ with $a\ge 1$, $$f(a,b,c)\,a!\,b!\,c!\,f(1,0,0)^{b+c}=f(1,0,0)^a\,f(1,1,0)^b\,f(1,0,1)^c.$$
background
Gap 2 in the gravity stack asks whether the gluing law must be assumed or can be derived. Gap2GaugeVolume showed that a gluing law forces inverse-factorial gauge counting; this module reverses the arrow. Two premises, neither mentioning measures or automorphism groups, are enough: (i) size-blindness (the labeled weight depends only on the three index sizes) and (ii) multiplicativity of class mass over disjoint union.
Orbit counts contribute a binomial interleaving factor on their own. Cancelling that factor turns (ii) into a three-variable shuffle identity whose positive solutions are $f(a,b,c)=x^a y^b z^c/(a!b!c!)$. The structure CarrierShuffle packages the four concrete gluing instances the carrier supplies (dust-bouquet, dust-edge, and siblings), already transported onto the size function, together with positivity and unit empty weight.
The present statement is the closed-form solution of that shuffle: on every realizable size triple with $a\ge 1$, the weight is inverse gauge volume times three fugacities, one per index type.
proof idea
Write $a=a'+1$ via omega. Split on whether $b+c=0$.
If $b=c=0$, the claim is exactly the dust-row identity for $a'+1$; finish by simpa.
If $b+c\ge 1$, invoke the dust-bouquet instance of CarrierShuffle, rewrite the interleaving prefactor, and bring in dust-row on $a'$ and bouquet-row on $(b,c)$. Expand $(a'+1)!$ by the successor formula. A short calc then: insert the factorial identity and cancel the bouquet weight by field_simp (using positivity); substitute dust-bouquet and bouquet-row; cancel again; apply dust-row; finish by ring to reassemble $(f(1,0,0))^{a'+1}$.
why it matters
This is the theorem that turns two locality-style premises into an explicit three-parameter family. The infinite-dimensional residue left by Gap2GaugeVolume §6c (an arbitrary map $\mathbb{N}^3\to\mathbb{R}$) collapses to three real fugacities. The next result in the module normalizes the three unit cells to weight one and obtains the Gibbs weight, hence gauge counting, so the measure is derived rather than postulated.
Downstream, Gap2FugacityPostingGluing uses the closed form to force unit fugacity when chemical potentials are posted at atoms, and to build character-cost countermodels. In the broader Recognition gravity program this closes the adversarial-panel route for Gap 2: gluing multiplicativity plus size-blindness replace an assumed normalization, aligning the discrete measure with the inverse-factorial gauge volume that feeds later Regge and continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.