PositivePairExactDeckAsymptotics

Abstract

Exact k-deck images have the full weighted-Lyndon asymptotic exponent.

The lower estimate comes from actual equal-length positive-word constructions. For the upper estimate, one singleton Lyndon coordinate is erased and recovered from the fixed total source length; unconditional Lyndon-coordinate recovery then identifies the complete exact deck. Thus exactly one degree of freedom is removed, without an additional hypothesis on n or k.

Theorem 1.1 (Full exact k-deck Conjecture 8.1 asymptotics).

$$\forall A,k,\mathrm{FiniteLinearOrder}\left(A\right),\mathrm{card}\left(A\right)\ge 2,k\ge 1\Rightarrow \mathrm{RealIsTheta}\left(atTop,\mathrm{lambda}\left(n,\mathrm{castR}\left(\mathrm{card}\left(\mathrm{exactKDeckImage}\left(A,k,n\right)\right)\right)\right),\mathrm{lambda}\left(n,\mathrm{pow}\left(\mathrm{castR}\left(n\right),\mathrm{weightedLyndonExponent}\left(A,k\right)-1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Complexity/ExactDecks/Asymptotics/PositivePairExactDeckAsymptotics.actual_exactKDeckImage_weightedLyndon_isTheta (✓ std3). ∎

Resolves. Problems/nilforoushan-parvaresh-conjecture-8-1 (proved) by D5/S1/Words/Complexity/ExactDecks/Asymptotics/PositivePairExactDeckAsymptotics.actual_exactKDeckImage_weightedLyndon_isTheta.

Source. Repository-derived.

Acknowledgement. Arman Nilforoushan; Farzad Parvaresh (2026). Improved upper bound on the number of distinct k-decks for any k and alphabet size by counting the independent parameters. DOI: 10.48550/arXiv.2609.23106. URL: https://arxiv.org/html/2609.23106v1.

Commentary.

For every finite linearly ordered type A with 2<=Fintype.card A, every k:N with 1<=k, the real-valued function n |-> (exactKDeckImage A k n).card is Real.IsTheta at Filter.atTop of n |-> (n:R)^(weightedLyndonExponent A k-1). Here weightedLyndonExponent is the weighted sum of the actual length-r Lyndon-word counts, so the theorem has all source quantifiers and no proxy parameter.

References

• Truth anchor: D5/S1/Words/Complexity/ExactDecks/Asymptotics/PositivePairExactDeckAsymptotics.actual_exactKDeckImage_weightedLyndon_isTheta
• Dependency: D5/S1/Words/Complexity/ExactDecks/Growth/ExactDeckCore
• Dependency: D5/S1/Words/Complexity/ExactDecks/Growth/ExactDeckLowerBound
• Dependency: D5/S1/Words/Complexity/ExactDecks/Growth/PositiveWordBall
• Dependency: D5/S1/Words/Complexity/ExactDecks/UpperBound/FullLyndonRecovery
• Dependency: D5/S1/Words/Complexity/LyndonBrackets/LyndonOrder
• Dependency: D5/S1/Words/Complexity/PositivePairs/Digits/ActualLyndonDirections
• Dependency: D5/S1/Words/Complexity/VivionBinomialConverseFails