Diagonal Distance Profiles

Abstract

Diagonal Hamming-distance profiles and lower tails have exact finite counts.

Theorem 1.1 (Exact distance profiles factor rowwise).

$$\mathrm{card}\left(\mathrm{distanceProfileFiber}\left(f,r\right)\right)=\mathrm{productRows}\left(\mathrm{rowDistanceCount}\left(f,r\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/DistanceProfile.distance_profile_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each row, the diagonal entry contributes either zero or one to the distance. The remaining coordinates form a finite Hamming sphere, whose choice count is a binomial coefficient times a power of one fewer than the value-set cardinality. Summing the fixed and nonfixed diagonal cases gives the explicit rowDistanceCount, and the rows then multiply independently.

Theorem 1.2 (Common distance lower tails are row powers).

$$\mathrm{card}\left(\mathrm{minimumDistanceListings}\left(f,r\right)\right)=\mathrm{sum}{\left(\mathrm{rowDistanceCount}\left(f,j\right),j,r,\mathrm{card}\left(A\right)\right)}^{\mathrm{card}\left(A\right)}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/DistanceProfile.min_distance_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every row distance lies between zero and the address cardinality. Summing the exact row counts over the closed lower-tail interval and then multiplying over all rows yields the stated finite count.

Theorem 1.3 (Positive distance recovers the escape count).

$$\mathrm{card}\left(\mathrm{positiveDistanceListings}\left(f\right)\right)={\left(\mathrm{card}{\left(Y\right)}^{\mathrm{card}\left(A\right)}-\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right)\right)}^{\mathrm{card}\left(A\right)}$$

Proof. Machine-checked in Lean as D5/S0/Diagonal/DistanceProfile.min_distance_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

A listing is escaped exactly when every row has positive distance from the twisted diagonal. The lower-tail formula at one is identified with the previously frozen exact escape count through that equivalence, without recounting escaped listings.

References

• Truth anchor: D5/S0/Diagonal/DistanceProfile.distance_profile_card
• Truth anchor: D5/S0/Diagonal/DistanceProfile.min_distance_one
• Truth anchor: D5/S0/Diagonal/DistanceProfile.min_distance_tail
• Dependency: D5/S0/Diagonal/EscapeCount