Structural arithmetic of a general integral profile
Provedmme_stothers_general_outer_profile_arithmeticStructural arithmetic of an arbitrary integral ten-class profile.
Four facts underlying the general-profile outer data. The first is about the ten Table-1 symmetry classes alone and involves no profile; the other three hold for every integral profile .
-
The Equation (5.2) matrix counts orbit members by coordinate. For every class , every mode and every grade , the number of grade triples in the permutation orbit of the class representative whose -th coordinate equals is exactly the entry of the integer matrix of Equation (5.2). In particular the count does not depend on the mode , as it must, the orbit being permutation-closed.
-
Row sums. , where are the nine-grade marginal numerators and . Equivalently: each row of the Equation (5.2) matrix sums to , so the three mode words of an address of length do use every position.
-
Agreement with . as real numbers, i.e. the integer marginal numerators are literally the Equation (5.2) map applied to the unnormalized profile. This is what connects the integral outer data to the real-valued marginal used by
globalRate. -
The -cell histogram has the prescribed marginals. For every mode and grade ,
Together these say that the exact target histogram at any integral profile really is a joint distribution on the supported grade triples with the prescribed nine-grade marginals, which is the hypothesis under which the Lemma 5.2 entropy comparison applies. Item 1 is also an independent consistency check between Table 1's ten permutation classes and the integer matrix printed in Equation (5.2).
import Definitions.Def_mme_stothers_general_outer_profile open MME BigOperators set_option autoImplicit false
theorem mme_stothers_general_outer_profile_arithmetic :
(∀ (r : Fin 10) (s : Fin 3) (j : Fin 9),
((MME.StothersFourth.genClassOrbit r).filter
(fun sigma ↦ sigma s = j)).card =
MME.StothersFourth.genClassMarginalMultiplicity r j) ∧
(∀ base : Fin 10 → ℕ,
∑ j : Fin 9, MME.StothersFourth.genMarginalBaseCount base j =
3 * MME.StothersFourth.genProfileScale base) ∧
(∀ (base : Fin 10 → ℕ) (j : Fin 9),
(MME.StothersFourth.genMarginalBaseCount base j : ℝ) =
MME.StothersFourth.Q (fun i ↦ (base i : ℝ)) j) ∧
(∀ (base : Fin 10 → ℕ) (m : ℕ) (i : Fin 3) (j : Fin 9),
(∑ sigma : {sigma : MME.StothersFourth.GenHashSupportTriple //
sigma.1 i = j},
MME.StothersFourth.genHashTargetJointTable base m sigma.1) =
MME.StothersFourth.genMarginalCount base m j) := by
sorry