Tribonacci Names

Abstract

Binary words avoiding 111 form Tribonacci-sized name layers.

A length-Q Tribonacci name is a binary word with no three consecutive true digits. The empty, one-digit, and two-digit layers contain 1, 2, and 4 names, fixing the sequence offset rather than copying the golden offset.

Definition 1.1 (Tribonacci sequence).

Lean statement: D5/S0/Tower/Tribonacci/Names.tribonacci

Formalization. D5/S0/Tower/Tribonacci/Names.tribonacci (✓ std3).

Source. Repository-derived.

Commentary.

The sequence starts with T(0)=0, T(1)=1, and T(2)=1, then each term is the sum of the preceding three terms.

Theorem 1.2 (Tribonacci three-term recurrence).

$$\forall n\in N,T\left(n+3\right)=T\left(n+2\right)+T\left(n+1\right)+T\left(n\right)$$

Proof. Machine-checked in Lean as D5/S0/Tower/Tribonacci/Names.tribonacci_add_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the public recurrence equation generated by the recursive definition and used by the cardinality induction.

Definition 1.3 (No-three-consecutive-true name).

Lean statement: D5/S0/Tower/Tribonacci/Names.TribonacciName

Formalization. D5/S0/Tower/Tribonacci/Names.TribonacciName (✓ std3).

Source. Repository-derived.

Commentary.

The recursive predicate checks the first three positions and then the tail, so every length-three window is covered.

Definition 1.4 (Tribonacci-name initial-interval equivalence).

Lean statement: D5/S0/Tower/Tribonacci/Names.tribonacciNameEquiv

Formalization. D5/S0/Tower/Tribonacci/Names.tribonacciNameEquiv (✓ std3).

Source. Repository-derived.

Commentary.

Each admissible name layer is equivalent to the finite initial interval with endpoint T(Q+2).

Theorem 1.5 (Tribonacci-name layers have Tribonacci cardinality).

$$\forall Q\in N,\mathrm{card}\left(\mathrm{TribonacciName}\left(Q\right)\right)=T\left(Q+2\right)$$

Proof. Machine-checked in Lean as D5/S0/Tower/Tribonacci/Names.tribonacci_name_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every admissible nonempty word begins uniquely with 0, 10, or 110. Removing that prefix yields the preceding three admissible layers, which gives the three-term count recurrence.

References

• Truth anchor: D5/S0/Tower/Tribonacci/Names.TribonacciName
• Truth anchor: D5/S0/Tower/Tribonacci/Names.tribonacci
• Truth anchor: D5/S0/Tower/Tribonacci/Names.tribonacciNameEquiv
• Truth anchor: D5/S0/Tower/Tribonacci/Names.tribonacci_add_three
• Truth anchor: D5/S0/Tower/Tribonacci/Names.tribonacci_name_card