Marked Input Shape

Abstract

The marker modes recognize positive signed digits at positions separated by three.

Theorem 1.1 (Input language of a completed marker).

$$\forall s\in \mathrm{List}\left(\mathbb{Z}\right),\forall t\in \mathrm{List}\left(\mathbb{Z}\right),\forall xs\in \mathrm{List}\left(\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\right),\forall p\in \mathrm{Path}\left(\mathrm{prefixRawAutomaton},s,t,xs\right),\left(\mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(s\right),\mathrm{some}\left(GetElem.getElem\left(s,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=0\wedge \mathrm{getD}\left(\mathrm{ite}\left(1<List.length\left(t\right),\mathrm{some}\left(GetElem.getElem\left(t,1\right)\right),\mathrm{none}\left(\right)\right),0\right)=4\right)\Rightarrow \left(\exists lower\in \mathrm{List}\left(\mathbb{Z}\right),\exists m\in \mathbb{N},\exists k\in \mathbb{N},0<m\wedge \mathrm{pathOutputs}\left(\lambda [\mathrm{List}\left(\mathbb{Z}\right)][\mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}\times \mathbb{Z}]q:\mathrm{List}\left(\mathbb{Z}\right)\mapsto \mathrm{getD}\left(\mathrm{ite}\left(10<List.length\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(q\right),\mathrm{some}\left(GetElem.getElem\left(q,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right)\right),\mathrm{some}\left(GetElem.getElem\left(\mathrm{fst}\left(\mathrm{baseTable}\left(\mathrm{toNat}\left(\mathrm{getD}\left(\mathrm{ite}\left(0<List.length\left(q\right),\mathrm{some}\left(GetElem.getElem\left(q,0\right)\right),\mathrm{none}\left(\right)\right),0\right)\right)\right)\right),10\right)\right),\mathrm{none}\left(\right)\right),0\right),p\right)=\mathrm{append}\left(\mathrm{append}\left(lower,\mathrm{flatten}\left(\mathrm{replicate}\left(m,[1,0,0]\right)\right)\right),\mathrm{replicate}\left(k+1,0\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Palindromes/PeriodDoubling/PrefixInputShape.prefix_path_input_shape (✓ std3). ∎

Source. Repository-derived.

Commentary.

A path begins in marker mode zero and ends in mode four. Its input coefficients consist of an arbitrary lower tail, a nonempty repetition of the block [1,0,0], and at least one final zero. Coefficients are read least significant first. Modes one and two require the two zeros after a selected positive digit; mode three either starts the next block or ends the marker; mode four accepts only zeros.

References

• Truth anchor: D5/S1/Words/Palindromes/PeriodDoubling/PrefixInputShape.prefix_path_input_shape
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/BaseSignedStreams
• Dependency: D5/S1/Words/Palindromes/PeriodDoubling/PrefixPathRealization