Multinomial count of general exact-profile addresses
Provedmme_stothers_general_exact_target_subtype_nat_cardExact count of the target addresses at an arbitrary integral profile.
Fix an integral ten-class profile and a scale , and put with . Among the marginal-supported outer addresses of length , those whose -cell joint histogram is exactly the prescribed one are counted by the multinomial coefficient
the product running over the supported ordered grade triples, with the prescribed multiplicity of .
The point is that an address is determined by the word of joint types it realizes, one supported triple per position, and the prescribed histogram says exactly which words are allowed: the number of such words is the multinomial coefficient of the histogram. The two directions of that correspondence use that the prescribed multiplicity of an unsupported triple is zero, so no information is lost in restricting attention to the supported cells, and that an exact-profile address is automatically marginally regular.
Together with the factorization , where is the star degree, this is the numerator of the target-to-ambient ratio that governs how many addresses survive the outer hash. At the fixed witness it specializes to the published count.
import Definitions.Def_mme_stothers_general_outer_profile open MME BigOperators set_option autoImplicit false
theorem mme_stothers_general_exact_target_subtype_nat_card
(base : Fin 10 → ℕ) (m : ℕ) :
Nat.card
{a : MME.StothersFourth.GenMarginalSupportedAddress base m //
MME.StothersFourth.GenHasExactJointProfile a} =
(MME.StothersFourth.genOuterLength base m).factorial /
∏ sigma : MME.StothersFourth.GenHashSupportTriple,
(MME.StothersFourth.genHashTargetJointTable base m sigma).factorial := by
sorry