# 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-v1.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-v2.md).