Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Iteration-Depth No-Gap for Literal Insertion

Abstract

Literal fixed-degree insertion has a gap-free spectrum of minimum iteration depths.

Hughes defines k-insertion by interleaving k source factors with k+1 base factors, allowing every factor to be empty. Iteration keeps the same positive degree throughout a history. The result below settles the arbitrary-language conjecture stated in Section 10, not the finite-language Theorem 8 or the insertion-degree conjecture in Section 11.

Definition 1.1 (Languages of finite words).

Formalization. D5/S1/Words/IterationDepthNoGap.Language (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

A language over an alphabet is an arbitrary set of finite lists. No finiteness condition is imposed on the language itself.

Definition 1.2 (Literal fixed-degree insertion).

Formalization. D5/S1/Words/IterationDepthNoGap.fixedDegreeInsertion (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

A list of k pairs records x_i and y_i, and the final tail records x_(k+1). The x-pieces concatenate to a base word, the y-pieces concatenate to a source word, and pairwise interleaving followed by the tail is the output. Empty lists are allowed in every position.

Definition 1.3 (Iteration at one fixed degree).

Formalization. D5/S1/Words/IterationDepthNoGap.fixedDegreeIterate (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

Stage zero is B. Every successor inserts A into the preceding stage using the same degree k.

Definition 1.4 (Appearance at an iteration stage).

Formalization. D5/S1/Words/IterationDepthNoGap.appearsAt (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

A word appears at stage m when one positive degree k produces it at that stage. The existential degree may depend on the word and stage.

Definition 1.5 (Minimum iteration depth).

Formalization. D5/S1/Words/IterationDepthNoGap.hasIterationDepth (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

Depth m means appearance at m together with nonappearance at every smaller stage, exactly retaining the minimum convention from the source.

Definition 1.6 (Attained minimum depths).

Formalization. D5/S1/Words/IterationDepthNoGap.iterationDepthSpectrum (✓ std3).

Citation. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

The spectrum contains exactly those natural numbers realized as the minimum iteration depth of some finite word.

Definition 1.7 (The source depth origin).

Formalization. D5/S1/Words/IterationDepthNoGap.closedSourceZero (✓ std3).

Source. Repository-derived.

Commentary.

The published minimum depth is zero-based. This Fin 2 value is the actual source coordinate used by the theorem and its finite information arena.

Definition 1.8 (Spectrum at a selected origin).

Formalization. D5/S1/Words/IterationDepthNoGap.iterationDepthSpectrumAt (✓ std3).

Source. Repository-derived.

Commentary.

Changing the origin adds its natural coordinate to every actual minimum depth. At closedSourceZero this is extensionally equal to the published spectrum.

Theorem 1.9 (No gaps in the arbitrary-language spectrum).

Proof. Machine-checked in Lean as D5/S1/Words/IterationDepthNoGap.result (✓ std3). ∎

Resolves. Problems/hughes-iteration-depth-no-gap (proved) by D5/S1/Words/IterationDepthNoGap.result.

Source. Repository-derived.

Acknowledgement. Charles E. Hughes (2026). Undecidability of Adjacent Equality for Insertion, Shuffle, and Crossover Language Operations. URL: https://arxiv.org/abs/2608.27755v1.

Commentary.

For every alphabet and arbitrary languages A and B, any attained depth r forces every q at most r to be attained. From a minimum-depth successor word, the proof extracts its predecessor. If that predecessor appeared too early at degree j, both histories lift to max(k,j) by padding with empty factor pairs, producing the original word too early. Induction then descends through every smaller depth. The argument includes empty languages, epsilon-only languages, and empty alphabets. No finiteness, countability, or decidable equality assumption on the alphabet is needed.

References