Ordered subgroup factorization
Abstract
The actual least-cell producer verifies both fixed-factor products and every finite rejection.
Theorem 1.1 (The prescribed factor and every finite rejection).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/OrderedSubgroupFactorization.ordered_subgroup_factorization_correct (✓ std3). ∎
Source. Repository-derived.
Commentary.
The checker input source22_4Input is the actual upper-right source Proposition 22.4 entry 3e+g in N[C2], ordered e before g, with K=C2 and b=2. Its first coefficient mismatch is (e,g), and source22_4Certificate is the actual inspectAndConstruct result in the coefficient-rejection branch. Applying this theorem’s rejection soundness proves source22_4FixedFactorQuestion: no p satisfies both prescribed fixed-factor equations. The compiled exact application is validation evidence; no separate certified-instance theorem is introduced. This says nothing about unrestricted SSE, including the source’s later two-step construction.
Let H be any finite group with an independently prescribed total order, and let K be any subgroup with decidable membership. The coefficient ring is the natural numbers. The scalar b may be zero. Write q for the number of actual elements of K, uK for subgroupUniform(K), and uH for groupUniform. No normality, commutativity or multiplication-compatible order is assumed.
RightConstancy(K,a) means that a(x)=a(h) for every h and every x in hK. BlockBalance(K,a,b) means that, for each actual double coset D=KhK, the sum of a over its distinct least right-coset representatives equals their number times b. FixedSolution(K,a,b) means that some natural group-ring p satisfies a=p uK and b uH=uK p. The first equivalence characterizes exactly this fixed second factor. Under right-coset constancy, the equation uK a=(q b) uH is equivalent to block balance. Together with a uK=q a it gives the second, purely group-ring, existence criterion.
Every right coset and left coset within one double coset have a nonempty intersection. Left and right subgroup multiplication give bijections between these cells, so their cardinalities agree. Partitioning the original cosets by the actual cells proves that the distinct row and column counts coincide. This converts the original block balance into equality of the original totals supplied to orderedAllocation.
The row and column sums of blockMass equal the corresponding sums of that same allocation table. Distinct cells have distinct least representatives, because each actual group element belongs to exactly one right coset and one left coset. Different double cosets are disjoint as well. Summing blockMass over the sorted double representatives therefore gives orderedFactor with a=orderedFactor uK and b uH=uK orderedFactor. Coefficient multiplication is reindexed separately on each side; group factors are never exchanged.
CellCount(K) is the equality between the sum of the lengths of the actual sorted row-by-column lists and the sum of dD squared over all distinct double-coset representatives, where dD is the number of rows. Every zero allocation is included in this count. CoefficientMismatch and BalanceMismatch are the actual two finders firstCoefficientMismatch and firstBalanceMismatch. A returned pair consists of two unequal coefficients in one actual right coset. A returned double representative has a failed original block balance.
The option constructor some retains its actual pair or double representative, and none is equivalent to the corresponding universal condition. inspectAndConstruct returns inr(p) exactly when p is this orderedFactor and both conditions hold; that returned p satisfies both products and CellCount. If it returns inl(bad), RejectedWitness(bad,K,a,b) records the appropriate actual failed condition, and no fixed-factor solution exists. RejectedWitness uses the pair condition for the inner inl branch and the double-coset condition for the inner inr branch. The rejection concerns only the fixed-uK problem.