The σ-grading count from a coincidence count #
R324GradeLedger reduces clause A to the permutation layer count
#{τ : grade τ = j} ≤ A^m·(m-j)!. This file reduces that to the
elementary gluing count
#{τ : τ realises all coincidences in S} ≤ B^m·(m-|S|)!,
for a prescribed set S of coincidences — which is the shape one
actually proves, by gluing the |S| coincident pairs into blocks and
permuting the m-|S| blocks.
The mechanism #
Power counting on the collapsed lattice sum
∑_q ∏ᵢ‖ρ̂(εqᵢ)‖²·∏ⱼ⟨Sⱼ⟩⁻²⟨Sⱼ^τ⟩⁻² produces one factor L per member
of a maximal refinement chain of partitions of {1,…,m} whose blocks
are intervals for the identity order and for the τ order. Every
proper step of such a chain merges two blocks that are adjacent in both
orders, so the chain length is controlled by the coincidences of τ:
the positions i at which i and i+1 are also neighbours in the
τ order. The trivial chain (the all-singletons partition alone) is
always present, which is the reason for the + 1 in hdom: the
generic bijection has no coincidence at all and still has grade 1
(the m = 4 example τ = (2,4,1,3) of R324CappedCrossGrading).
That +1 is affordable: one unit of grade costs one factor m, and
m ≤ 2^m. The subset-count constant B is likewise affordable: a
prescribed set of |S| coincidences may be realised with either
orientation of each glued block, which is a 2^m overhead at worst.
Both are absorbed into the final constant 4B.
Alignment with the proved §5 machine #
The factorial layer criterion is not an ad hoc device: the proved
permSumRHS of Proposition 5.7 (PermSum/Statements.lean) already has
the shape
C^n·∑_{W ⊆ branches} (n - |W|)!·∏ₗ √(mult l)!·(scale ratios),
i.e. a sum over subsets W weighted by exactly (n-|W|)!, each
element of W paying for its factorial with a scale-ratio gain. So
(m-j)! per grade level is the same bookkeeping the paper's §5 uses,
and the downstream of clause A is built to absorb it.
Factorial bookkeeping for the +1 offset #
The reduction #
The σ-grading layer count from a prescribed-coincidence count.
coin τ is the finite set of coincidences of τ. If
- the grade never exceeds
#coincidences + 1, and - for every prescribed set
Sof coincidences at mostB^m·(m-|S|)!bijections realise all of them,
then the permutation layer count holds with constant 4B, hence — via
r324Grade_layeredAt_of_collapse — clause A.
The proof is the union bound over the ≤ 2^m candidate coincidence
sets of the right size, followed by r324Grade_factorial_pred_le.
The concrete coincidence family #
The position of i in the τ-order (junk outside the range).
Equations
- Anderson4D.r324GradePos τ i = if h : i < m then ↑((Equiv.symm τ) ⟨i, h⟩) else 0
Instances For
The coincidences of a bijection: the positions i < m-1 at
which the neighbouring pair {i, i+1} of the identity order is also a
neighbouring pair of the τ order. These are exactly the two-block
merges available at the finest level of the common-interval chain, so
they control the grade.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The remaining combinatorial obligation. A prescribed set S
of coincidences is realised by at most 2^m·(m-|S|)! bijections: glue
the |S| coincident pairs into blocks (at most 2^m orientations) and
permute the ≤ m-|S| blocks. S = ∅ is the equality case m!.
Equations
- Anderson4D.R324GradeCoincidenceCount m = ∀ (S : Finset (Fin m)), ↑{τ : Equiv.Perm (Fin m) | S ⊆ Anderson4D.r324GradeCoincidence τ}.card ≤ 2 ^ m * ↑(m - S.card).factorial
Instances For
The σ-grading count, packaged. A grade dominated by the
coincidence count, together with the gluing count, gives the
permutation layer count at constant 8, hence clause A through
r324Grade_layeredAt_of_collapse.