Section 5 and Table 1: fourth-power support and ten classes
Provedmme_stothers_fourth_support_and_classesLet be an arbitrary field. In the canonical nine-grading of the literal fourth power :
- every block whose three mode grades do not sum to has zero block tensor;
- exactly grade triples sum to ;
- every such triple belongs to a unique permutation orbit represented by one of ; and
- the orbit represented by class has cardinality , where .
This is the literal fourth-power decomposition underlying Section 5 and Table 1; it does not replace overlapping blocks by an external direct sum.
import Definitions.Def_mme_stothers_fourth_data open MME BigOperators universe u set_option autoImplicit false
theorem mme_stothers_fourth_support_and_classes
{K : Type u} [Field K] :
(∀ sigma : Fin 3 → Fin 9,
(MME.StothersFourth.cwFourthCanonicalGrading K 6).blockTensor sigma = 0 ↔
(∑ s, (sigma s).val) ≠ 8) ∧
Fintype.card
{sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8} = 45 ∧
(∀ sigma : {sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8},
∃! r : Fin 10,
MME.StothersFourth.sameOrbit sigma.1
(MME.StothersFourth.classRep r)) ∧
(∀ r : Fin 10,
Fintype.card
{sigma : {sigma : Fin 3 → Fin 9 // (∑ s, (sigma s).val) = 8} //
MME.StothersFourth.sameOrbit sigma.1
(MME.StothersFourth.classRep r)} =
3 * MME.StothersFourth.classMultiplicity r) := by
sorryRead-back
What the Lean code literally says, in plain math · gpt-5
For an arbitrary universe and every type in that universe equipped with a field structure, with no further restriction on , let , put , and form the three-slot tensor object . At each slot , the “fourth canonical” basis of is, literally, the tensor-product basis of two copies of the square canonical basis for and ; its indices are pairs with . If denotes the supplied square-pair grade at , the fourth pair grade is the element whose underlying natural number is . The grading used below is the internal nine-part basis grading whose decomposition at each slot is the basis grading induced by and ; for a function , write for the block tensor selected by the three grades . Also define ten representative functions , displayed as ordered triples of their values at , and ten natural-number multiplicities by and . The theorem asserts all four of the following simultaneously: first, for every one of the functions , including functions with repeated values and values or , if and only if the natural-number sum is not ; both directions are asserted—zero implies that the sum is not , and a sum different from implies zero—so a sum equal to forces the selected block tensor to be nonzero. Second, the set has exactly elements. Third, for every , there exists exactly one class index such that there exists a permutation of satisfying for every ; this is the literal direction of the equality, and only is unique—the permutation is merely existential and need not be unique, in particular when a representative has repeated coordinates. Fourth, for every , the number of distinct for which such a permutation exists is exactly , hence is respectively for ; this cardinality counts the functions , not the possible witnessing permutations.
Confirmed by the mission captain (proposal self-audit).