Unary Gaps of Actual Words

Abstract

Occurrence-indexed unary gaps and complete positional source traces.

Fix a letter a in an arbitrary alphabet. A gap word alternates blocks of a with a list of non-a occurrences. The list preserves repeated letters as separate occurrences. Its gap vector has one more entry than its occurrence list; entries may be zero.

Definition 1.1 (Gap concatenation).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\mathrm{gap}\left(a,cs,h\right):\mathrm{List}\left(alpha\right)$$

Formalization. D5/S1/Words/UnaryGapWords.gap (✓ std3).

Source. Repository-derived.

Commentary.

For an empty occurrence list, take the first gap’s copies of a. For c followed by cs, concatenate the first a block, c, and the remaining gap word. All uses of a gap presentation supply exactly one more mass than occurrences.

Definition 1.2 (Non-a occurrences).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall w\in \mathrm{List}\left(alpha\right),\mathrm{spine}\left(a,w\right)=\mathrm{filter}\left(notEqualToA,w\right)$$

Formalization. D5/S1/Words/UnaryGapWords.spine (✓ std3).

Source. Repository-derived.

Commentary.

Filter the actual word by inequality to a without removing multiplicities.

Definition 1.3 (Canonical gap lengths).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall w\in \mathrm{List}\left(alpha\right),\mathrm{sizes}\left(a,w\right):\mathrm{List}\left(\mathrm{Nat}\left(\right)\right)$$

Formalization. D5/S1/Words/UnaryGapWords.sizes (✓ std3).

Source. Repository-derived.

Commentary.

Scan from the right. An a increments the first gap; a non-a occurrence starts a new zero gap. The empty word has the single gap zero.

Theorem 1.4 (Uniqueness of indexed gap words).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall ds\in \mathrm{List}\left(alpha\right),\forall k\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\left(\forall x\in alpha,x\in ds\Rightarrow x\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \mathrm{length}\left(k\right)=\mathrm{length}\left(ds\right)+1\right)\right)\right)\Rightarrow \left(\mathrm{gap}\left(a,cs,h\right)=\mathrm{gap}\left(a,ds,k\right)\Rightarrow \left(cs=ds\wedge h=k\right)\right)$$

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

Source. Repository-derived.

Commentary.

Recovering the spine and lengths from each actual concatenation proves both equalities, including repeated separators and zero gaps.

Theorem 1.5 (Every word has a canonical presentation).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall w\in \mathrm{List}\left(alpha\right),\exists cs\in \mathrm{List}\left(alpha\right),\exists h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge w=\mathrm{gap}\left(a,cs,h\right)\right)$$

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

Source. Repository-derived.

Commentary.

The canonical spine and gap lengths reconstruct the original word.

Definition 1.6 (Complete gap labels).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall q\in Side,\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{Trace}\left(a,q,cs,h,e,w,M\right):\mathrm{Prop}\left(\right)$$

Formalization. D5/S1/Words/UnaryGapWords.Trace (✓ std3).

Source. Repository-derived.

Commentary.

Every a gap retains its whole label list b. Its q count contributes to h, and its opposite-source count contributes to e. Every non-a occurrence has label q. This is an inductive decomposition of actual letters and labels.

Definition 1.7 (Grouped labels in each gap).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall q\in Side,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\mathrm{grouped}\left(q,cs,h,e\right):\mathrm{List}\left(Side\right)$$

Formalization. D5/S1/Words/UnaryGapWords.grouped (✓ std3).

Source. Repository-derived.

Commentary.

With a unary inserted source, place its gap mass together after the base copies. With a unary base source, place base copies before the inserted copies in each nonterminal gap, and after them in the terminal gap.

Theorem 1.8 (Unique extra masses and actual masks).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall q\in Side,\forall m\in \mathrm{Nat}\left(\right),\forall w\in \mathrm{List}\left(alpha\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\right)\Rightarrow \left(\left(\exists M\in \mathrm{List}\left(Side\right),\mathrm{length}\left(M\right)=\mathrm{length}\left(w\right)\wedge \left(\mathrm{projection}\left(q,w,M\right)=\mathrm{gap}\left(a,cs,h\right)\wedge \mathrm{projection}\left(\mathrm{opposite}\left(q\right),w,M\right)=\mathrm{replicate}\left(m,a\right)\right)\right)\iff \left(\exists e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(e\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)\right)\wedge \left(\forall f\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\mathrm{length}\left(f\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(f\right)=m\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,f\right)\right)\right)\right)\Rightarrow f=e\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For each native projection pair, non-a letters are forced to q. Splitting at those occurrences gives every label gap and both projected words. Conversely, grouped gap labels realize every permitted mass vector. Canonical word recovery makes the extra vector unique. No alphabet order, decidable equality premise or distinctness between separators is assumed.

Theorem 1.9 (Canonical recovery of a presented gap word).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\right)\Rightarrow \left(\mathrm{spine}\left(a,\mathrm{gap}\left(a,cs,h\right)\right)=cs\wedge \mathrm{sizes}\left(a,\mathrm{gap}\left(a,cs,h\right)\right)=h\right)$$

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

Source. Repository-derived.

Commentary.

Filtering recovers exactly the occurrence list, and the canonical gap scan recovers exactly the supplied lengths.

Theorem 1.10 (Both projections of a positional trace).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall q\in Side,\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\mathrm{Trace}\left(a,q,cs,h,e,w,M\right)\Rightarrow \left(\mathrm{length}\left(M\right)=\mathrm{length}\left(w\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\mathrm{projection}\left(q,w,M\right)=\mathrm{gap}\left(a,cs,h\right)\wedge \left(\mathrm{projection}\left(\mathrm{opposite}\left(q\right),w,M\right)=\mathrm{replicate}\left(\mathrm{sum}\left(e\right),a\right)\wedge w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The trace gives matching word and mask lengths, both ordered source projections, all vector lengths and the actual enlarged gap word.

Theorem 1.11 (Extracting the full trace).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall q\in Side,\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\left(\mathrm{length}\left(M\right)=\mathrm{length}\left(w\right)\wedge \left(\forall x\in alpha,x\in \mathrm{projection}\left(\mathrm{opposite}\left(q\right),w,M\right)\Rightarrow x=a\right)\right)\Rightarrow \left(\exists cs\in \mathrm{List}\left(alpha\right),\exists h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\exists e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\mathrm{Trace}\left(a,q,cs,h,e,w,M\right)\right)$$

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

Source. Repository-derived.

Commentary.

At each non-a occurrence the opposite projection excludes its label. Splitting there retains every intervening label and all zero gaps.

Theorem 1.12 (Realizing every extra vector).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall q\in Side,\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\right)\right)\Rightarrow \mathrm{Trace}\left(a,q,cs,h,e,\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right),\mathrm{grouped}\left(q,cs,h,e\right)\right)$$

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

Source. Repository-derived.

Commentary.

The grouped mask realizes each permitted vector on an actual gap word, including the no-separator case and both exterior masses.

Theorem 1.13 (Recovering prescribed gap masses).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall q\in Side,\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall w\in \mathrm{List}\left(alpha\right),\forall M\in \mathrm{List}\left(Side\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \left(w=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\wedge \left(\mathrm{length}\left(M\right)=\mathrm{length}\left(w\right)\wedge \left(\mathrm{projection}\left(q,w,M\right)=\mathrm{gap}\left(a,cs,h\right)\wedge \left(\forall x\in alpha,x\in \mathrm{projection}\left(\mathrm{opposite}\left(q\right),w,M\right)\Rightarrow x=a\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{Trace}\left(a,q,cs,h,e,w,M\right)$$

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

Source. Repository-derived.

Commentary.

Actual word uniqueness identifies the extracted original and extra gaps with their prescribed vectors, without identifying repeated separators.

Theorem 1.14 (Transport at an actual word cut).

$$\forall alpha\in \mathrm{Type}\left(\right),\forall a\in alpha,\forall cs\in \mathrm{List}\left(alpha\right),\forall h\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall e\in \mathrm{List}\left(\mathrm{Nat}\left(\right)\right),\forall X\in \mathrm{List}\left(alpha\right),\forall Y\in \mathrm{List}\left(alpha\right),\forall k\in \mathrm{Nat}\left(\right),\left(\left(\forall x\in alpha,x\in cs\Rightarrow x\ne a\right)\wedge \left(\mathrm{length}\left(h\right)=\mathrm{length}\left(cs\right)+1\wedge \left(\mathrm{length}\left(e\right)=\mathrm{length}\left(h\right)\wedge \mathrm{append}\left(X,Y\right)=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,e\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{length}\left(\mathrm{spine}\left(a,X\right)\right)<\mathrm{length}\left(e\right)\wedge \left(\mathrm{length}\left(\mathrm{modify}\left(e,\mathrm{length}\left(\mathrm{spine}\left(a,X\right)\right),\mathrm{add}\left(k\right)\right)\right)=\mathrm{length}\left(h\right)\wedge \left(\mathrm{sum}\left(\mathrm{modify}\left(e,\mathrm{length}\left(\mathrm{spine}\left(a,X\right)\right),\mathrm{add}\left(k\right)\right)\right)=\mathrm{sum}\left(e\right)+k\wedge \mathrm{append}\left(\mathrm{append}\left(X,\mathrm{replicate}\left(k,a\right)\right),Y\right)=\mathrm{gap}\left(a,cs,\mathrm{zipWith}\left(add,h,\mathrm{modify}\left(e,\mathrm{length}\left(\mathrm{spine}\left(a,X\right)\right),\mathrm{add}\left(k\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Let i count the non-a occurrences in X. Then i is a valid gap index. Inserting k copies of a at X|Y adds k only to e[i], preserves vector length, increases its sum by k, and gives exactly the concatenated word X followed by a^k followed by Y. This is an identity on actual words.

References

• Truth anchor: D5/S1/Words/UnaryGapWords.Trace
• Truth anchor: D5/S1/Words/UnaryGapWords.gap
• Truth anchor: D5/S1/Words/UnaryGapWords.gap_exists
• Truth anchor: D5/S1/Words/UnaryGapWords.gap_injective
• Truth anchor: D5/S1/Words/UnaryGapWords.gap_insert
• Truth anchor: D5/S1/Words/UnaryGapWords.grouped
• Truth anchor: D5/S1/Words/UnaryGapWords.native_gap_iff
• Truth anchor: D5/S1/Words/UnaryGapWords.profile_gap
• Truth anchor: D5/S1/Words/UnaryGapWords.sizes
• Truth anchor: D5/S1/Words/UnaryGapWords.spine
• Truth anchor: D5/S1/Words/UnaryGapWords.trace_construct
• Truth anchor: D5/S1/Words/UnaryGapWords.trace_exists
• Truth anchor: D5/S1/Words/UnaryGapWords.trace_of_projections
• Truth anchor: D5/S1/Words/UnaryGapWords.trace_projections
• Dependency: D5/S1/Words/HughesBlockExchange