# Coordinate-sweep contraction constants: selected source audit

The selected trace solution has an existential universal sweep threshold, but this review has not extracted a useful numerical value. The [hashed reading record](../snapshots/2026-10-08-baseline/coordinate-contraction-review-2026-10-09-v2.json) distinguishes these selected module excerpts from a complete imported-proof review. The source commit remains fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. No Lean, Comparator or independent kernel ran.

`TraceModel.lean` imports `Harmonic.Main`, inside `OAI.ThorpNine.Harmonic`. The parallel Casimir module contains similar names but is not the selected import for this path. `TraceDecay.uniform_nonconstant_decay` takes positive level/dimension contraction coefficients a,b and chooses m>=max(14/a,2/b), then u=2m. The regular trace conclusion uses P=2u. This chain provides a proof witness for existence; the preceding finite four-card calibration does not choose the universal witness.

In Harmonic/Main lines 415–478, the eventual level coefficient combines a spectral coefficient and a dimension coefficient. An eventual threshold D is obtained, and the finite part takes a positive lower bound of f(d)=-log(blockGap(d))/2^d over d<D. The resulting all-d coefficient is the minimum of the eventual and finite bounds. In lines 1087–1138, the dimension contraction similarly uses f(d)=-log(blockGap(d))/(1+log((2^d)!)) and a finite positive minimum. Neither numerical D nor the underlying spectral coefficients were selected in this review.

Harmonic/AverageMap lines 271–292 defines a finite convolution minorant. Its exponent is classically chosen from existence of a positive convolution power; its mass is the full-group size times the minimum mass of that selected power. Lines 463–480 give blockGap=1-mass/(2*2^exponent), and lines 687–694 instantiate it for the palindrome shuffle. This is more information than merely saying the gap is positive, but evaluating a literal full-group minimum is a separate finite construction with factorial-sized state space. An explicit sharper minorant or spectral estimate could be an engineering bridge; it is not supplied by these references.

The product decision remains conditional: do not advertise a source-certified sweep schedule from the tiny fixtures or a hand-picked P. Next inspect the spectral-regime numerical dependencies, and consider an exact four-card palindrome minorant as a finite calibration only. A changed proof with quantitative witnesses, a validated independent-bit backend and correspondence to an actual implementation remain separate obligations. [Framework dossier](../opportunities/040-queryable-permutation-framework/2026-10-09-v3.md).

## Exact two/four-slot calibration

The [new finite utility](../tools/palindrome_minorant_reference.py) implements the selected recursive butterfly model, whose child action precedes the root switch. InsertionPerm's physical-sweep lemma identifies the sweep average with the inverse butterfly average; BlockProduct expresses the palindrome as butterfly times its adjoint. Selected excerpts are now included in the reading record, but those lemmas' proof/import closure was not executed. An independent actual-card swap oracle checks all sixteen four-slot coin assignments, including this orientation, before comparing the inverse law with the earlier physical-sweep law.

For four slots the two independent butterfly assignments account for 256 equally weighted coin strings. All 24 permutations occur with counts 8 or 16. The minimum probability is 1/32, so exponent zero and mass 3/4 give an explicit uniform minorant and gap-formula bound 5/8. This constructed minorant is a valid finite reference; it is not an evaluation of the source's classically selected `palindromeMinorant` value.

The [exact four-slot witness](../prototypes/palindrome-minorant-d2-2026-10-09-v1.json) provides the centered 24-by-24 regular operator B=A-J, in a declared permutation order. Rational arithmetic verifies symmetry, zero constant direction and B^2=(1/4)B. Its scaled-projection rank is two, and a displayed nonzero column is a zero-sum eigenvector of eigenvalue 1/4. Thus the palindrome's nonconstant norm is exactly 1/4, and the corresponding physical sweep's nonconstant squared norm is 1/4. The two-slot palindrome is uniform and its centered operator is zero. No floating eigensolver is used.

For a point mass on S_n, the conservative regular norm inequality gives TV^2<=((n!-1)/4)*c^v when c bounds the sweep's nonconstant squared norm. At n=4, c=1/4 reaches the source target squared 1/(4*n^10) at 13 sweeps; using the weaker explicit-minorant c=5/8 reaches it at 37. Both preceding steps fail their respective bound. These are sufficient bounds for the four-slot reference, not its optimal mixing time: direct exact-law enumeration already passes at six sweeps. At n=2 the exact and minorant calibrations are one and ten sweeps respectively.

[50 controls](../snapshots/2026-10-08-baseline/palindrome-minorant-validation-2026-10-09-v1.json) reconstruct the law/transition matrix through separate physical swaps and direct group transitions, verify exact mass/witness/bound arithmetic, and reject dimensions beyond two. This is a usable finite calibration, with a factorial-sized regular matrix and explicit domain cap. It neither computes all small dimensions below an unknown threshold D nor supplies the eventual spectral constants, universal P, fair-bit backend or formal program/proof acceptance. A numerical bridge should expose those remaining witnesses instead of extrapolating the four-slot result.