Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Finite Level Generators for Binary Automatic Apwenian Sequences

Abstract

Binary automatic apwenian sequences arise as the parity of successive whole levels of one finite sum-equivalent morphism.

Definition 1.1 (Canonical binary input).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.binaryInput

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.binaryInput (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

The input of a positive integer is its binary expansion in most-significant-first order, obtained by reversing Nat.digits 2 n. A Boolean convention chooses either the one-digit word [0] or the empty word for zero.

Definition 1.2 (Source automaticity).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.IsBinaryAutomatic

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.IsBinaryAutomatic (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

A natural-valued sequence u is binary automatic when every u(n) is less than two and there exist a finite state type Q, a DFAO M with natural-valued outputs, and a choice of the zero-input convention such that M on the canonical binary input of every nonnegative n outputs u(n). Only outputs on these inputs are required to be binary. The machine is not required to be invariant under leading-zero padding.

Definition 1.3 (Sum-equivalent alphabet morphisms).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.AlphabetMorphism

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.AlphabetMorphism (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

For a finite natural-number alphabet Sigma, a morphism is a map tau from natural numbers to finite words. For every s in Sigma, tau(s) has exactly two letters, every letter of tau(s) belongs to Sigma, and the sum of tau(s) is congruent to s modulo two. Its extension to words is concatenation of the letter images, so it is an endomorphism of the free monoid on Sigma. Values outside Sigma have no role.

Definition 1.4 (Successive ordered levels).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.level

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.level (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

For a directive sigma indexed by the nonnegative integers, X(0) is [1] and X(j+1) is obtained by applying sigma(j) to every letter of X(j) and concatenating those images in their original order. This construction is defined for any directive, independently of automaticity and apwenianness.

Definition 1.5 (Concatenated-level prefixes).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.levelPrefix

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.levelPrefix (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

The prefix with parameter j is the concatenation X(0) X(1) … X(j-1). The prefix with parameter zero is empty, and the next prefix appends the next whole level. These are actual words, with their order retained.

Definition 1.6 (Infinite sequence generated by levels).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.Generates

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.Generates (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

A directive generates a sequence v when each concatenated-level prefix is exactly the initial segment of v having that prefix’s length, and for every index n some such prefix has length greater than n. This exact-prefix relation defines the infinite concatenation without a metric-limit construction.

Definition 1.7 (The universal representation statement).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.claim

Formalization. D5/S3/Combinatorics/Apwenian/GuoHanGeneration.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

For every binary automatic u that is apwenian, there exist a finite natural-number alphabet Sigma containing one, a sum-equivalent two-letter morphism tau on every letter of Sigma, and a sequence v generated by the constant directive sigma(j) = tau. Every v(n) belongs to Sigma and satisfies v(n) modulo two = u(n), for all nonnegative n. Any sequence generated by this same directive equals v. Apwenianness is exactly u(0) = 1 and u(n) congruent to u(2n+1) + u(2n+2) modulo two for all nonnegative n. This statement strengthens Conjecture 1 of Guo and Han by allowing a constant directive as its witness.

Theorem 1.8 (Every binary automatic apwenian sequence has a level generator).

Lean statement: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.result

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Apwenian/GuoHanGeneration.result (✓ std3). ∎

Resolves. Problems/guo-han-binary-automatic-apwenian-level-generation (proved) by D5/S3/Combinatorics/Apwenian/GuoHanGeneration.result.

Source. Repository-derived.

Acknowledgement. Ying-Jun Guo, Guo-Niu Han (2025). On a family of automatic apwenian sequences. DOI: 10.1016/j.disc.2025.114399. URL: https://irma.math.unistra.fr/~guoniu/papers/p120autoapw.pdf.

Commentary.

The universal representation statement holds. Adjoin a fresh zero state z with delta(0,z) = z and delta(1,z) equal to the original transition from the start on one. The canonical-input state a(n) then satisfies a(2n+b) = delta(b,a(n)) for b zero or one, including n = b = 0. The finite set of occurring adjacent pairs s(n) = (a(n), a(n+1)) is closed under the ordered children L(q,r) = (delta(1,q), delta(0,r)) and R(q,r) = (delta(0,r), delta(1,r)), with L(s(n)) = s(2n+1) and R(s(n)) = s(2n+2). Enumerate this occurring set with s(0) at index zero, and label a pair by twice its index plus the parity of its first output. The labels are injective, the root label is one, and the apwenian recurrence makes the image [e(L(s)), e(R(s))] sum-equivalent on every alphabet letter. The j-th ordered level is exactly the labels e(s(2^j - 1 + k)) for k from zero through 2^j - 1; its concatenated prefix of j levels contains exactly the first 2^j - 1 values of v. These prefix lengths are unbounded, proving generation, uniqueness, and parity agreement at every index. The alphabet may contain several odd letters, and the generated sequence is not assumed to be a morphism fixed point.

References

  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.AlphabetMorphism
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.Generates
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.IsBinaryAutomatic
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.binaryInput
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.claim
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.level
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.levelPrefix
  • Truth anchor: D5/S3/Combinatorics/Apwenian/GuoHanGeneration.result
  • Dependency: D5/S0/Automata/DFAOStateLowerBound
  • Dependency: D5/S1/Recurrence/Raney/MaximalBlockEvolution
  • Dependency: D5/S3/Combinatorics/Apwenian/GuoHanDefs