BalancedBordersHalfFrequency

Abstract

Balanced borders force exact half frequency; short unbalanced words exclude it.

Theorem 1.1 (rho_nonneg).

$$\forall w\in \mathrm{List}\left(Bool\right),\forall m\in \mathbb{N},0\le \mathrm{rho}\left(w,m\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.rho_nonneg (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.2 (rho_le_one).

$$\forall w\in \mathrm{List}\left(Bool\right),\forall m\in \mathbb{N},(w\ne [])\Rightarrow ((0<m)\Rightarrow (\mathrm{rho}\left(w,m\right)\le 1))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.rho_le_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.3 (singleton_not_tendsto_half).

$$\forall b\in Bool,\neg \mathrm{Tendsto}\left(\mathrm{rho}\left([b]\right),atTop,\mathrm{nhds}\left(\frac{1}{2}\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.singleton_not_tendsto_half (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.4 (flip_tendsto_half_iff).

$$\forall w\in \mathrm{List}\left(Bool\right),(w\ne [])\Rightarrow ((\mathrm{Tendsto}\left(\mathrm{rho}\left(\mathrm{List}.\mathrm{map}(\mathrm{Bool}.\mathrm{not},w)\right),atTop,\mathrm{nhds}\left(\frac{1}{2}\right)\right))\iff (\mathrm{Tendsto}\left(\mathrm{rho}\left(w\right),atTop,\mathrm{nhds}\left(\frac{1}{2}\right)\right)))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.flip_tendsto_half_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Complementing every bit bijects the avoiding words and replaces each positive-length average by one minus that average. Half-frequency convergence is preserved.

Theorem 1.5 (onesTotal11_bound).

$$\forall k\in \mathbb{N},(3\cdot \mathrm{avoidOnes}\left([true,true],k+2\right)\le (k+2:\mathbb{R})\cdot \mathrm{avoidCount}\left([true,true],k+2\right))\wedge (3\cdot \mathrm{avoidOnes}\left([true,true],k+3\right)\le (k+3:\mathbb{R})\cdot \mathrm{avoidCount}\left([true,true],k+3\right))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.onesTotal11_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The avoiding words for 11 split into a word prefixed by 0 and a shorter word prefixed by 10. Their disjoint count and one-count recurrences give the two inequalities simultaneously by induction.

Theorem 1.6 (not_tendsto_half_11).

$$\neg \mathrm{Tendsto}\left(\mathrm{rho}\left([true,true]\right),atTop,\mathrm{nhds}\left(\frac{1}{2}\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.not_tendsto_half_11 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The recurrence estimate bounds all positive-length averages from length two onward by 1/3, excluding convergence to 1/2.

Definition 1.7 (signedMoment).

$$\forall f\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\mathrm{signedMoment}\left(f\right)=\mathrm{PowerSeries}.\mathrm{mk}((n:\mathbb{N})\mapsto (2\cdot \mathrm{Polynomial}.\mathrm{eval}(1,\mathrm{Polynomial}.\mathrm{derivative}(\mathrm{PowerSeries}.\mathrm{coeff}(n,f)))-(n:\mathbb{Q})\cdot \mathrm{Polynomial}.\mathrm{eval}(1,\mathrm{PowerSeries}.\mathrm{coeff}(n,f))))$$

Formalization. D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment (✓ std3).

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.8 (signedMoment_add).

$$\forall f\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\forall g\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\mathrm{signedMoment}\left(f+g\right)=\mathrm{signedMoment}\left(f\right)+\mathrm{signedMoment}\left(g\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_add (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.9 (signedMoment_sub).

$$\forall f\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\forall g\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\mathrm{signedMoment}\left(f-g\right)=\mathrm{signedMoment}\left(f\right)-\mathrm{signedMoment}\left(g\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_sub (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.10 (signedMoment_mul).

$$\forall f\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\forall g\in \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\mathrm{signedMoment}\left(f\cdot g\right)=\mathrm{signedMoment}\left(f\right)\cdot \mathrm{PowerSeries}.\mathrm{map}(\mathrm{Polynomial}.\mathrm{evalRingHom}(1),g)+\mathrm{PowerSeries}.\mathrm{map}(\mathrm{Polynomial}.\mathrm{evalRingHom}(1),f)\cdot \mathrm{signedMoment}\left(g\right)$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_mul (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.11 (signedMoment_one).

$$\mathrm{signedMoment}\left(1\right)=0$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.12 (signedMoment_monomial).

$$\forall n\in \mathbb{N},\forall k\in \mathbb{N},\mathrm{signedMoment}\left(\mathrm{PowerSeries}.\mathrm{monomial}(n,\mathrm{Polynomial}.X^k)\right)=\mathrm{PowerSeries}.\mathrm{monomial}(n,2\cdot (k:\mathbb{Q})-(n:\mathbb{Q}))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_monomial (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.13 (signedMoment_letterSeries).

$$\mathrm{signedMoment}\left(\mathrm{letterSeries}\left(\right)\right)=0$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_letterSeries (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.14 (signedMoment_sum).

$$\forall I\in Type,\forall S\in \mathrm{Finset}\left(I\right),\forall f\in I\to \mathrm{PowerSeries}\left(\mathrm{Polynomial}\left(\mathbb{Q}\right)\right),\mathrm{signedMoment}\left(\sum _{i\in S}(f\left(i\right))\right)=\sum _{i\in S}(\mathrm{signedMoment}\left(f\left(i\right)\right))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Definition 1.15 (avoidDenominator).

$$\forall w\in \mathrm{List}\left(Bool\right),\mathrm{avoidDenominator}\left(w\right)=\left(1-\mathrm{letterSeries}\left(\right)\right)\cdot \mathrm{overlapSeries}\left(w\right)+\mathrm{wordMonomial}\left(w\right)$$

Formalization. D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.avoidDenominator (✓ std3).

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.16 (balanced_signedMoment_avoidSeries).

$$\forall w\in \mathrm{List}\left(Bool\right),(w\ne [])\Rightarrow ((\mathrm{BalancedBorders}\left(w\right))\Rightarrow (\mathrm{signedMoment}\left(\mathrm{avoidSeries}\left(w\right)\right)=0))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.balanced_signedMoment_avoidSeries (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed statement uses the literal binary-word counts and border operations. All counts in real or rational arithmetic carry the displayed coercions. Nat.sub denotes truncated subtraction. All hypotheses and parameters have their displayed domains.

Theorem 1.17 (balanced_tendsto_half).

$$\forall w\in \mathrm{List}\left(Bool\right),(w\ne [])\Rightarrow ((\mathrm{BalancedBorders}\left(w\right))\Rightarrow (\mathrm{Tendsto}\left(\mathrm{rho}\left(w\right),atTop,\mathrm{nhds}\left(\frac{1}{2}\right)\right)))$$

Proof. Machine-checked in Lean as D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.balanced_tendsto_half (✓ std3). ∎

Citation. Miklós Bóna, Balázs Maga, Jacob Richey (2026). Letter frequency in shifts of finite type with one forbidden word. URL: https://arxiv.org/abs/2606.06655v2.

Commentary.

“In particular, if $w$ has balanced borders, then ${\rho }^w=q^w=\frac{1}{2}$.” (Proposition 3.3, p. 9.)

Only the rho consequence is displayed. The proof gives rho w m = 1/2 for every positive m.

References

• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.avoidDenominator
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.balanced_signedMoment_avoidSeries
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.balanced_tendsto_half
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.flip_tendsto_half_iff
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.not_tendsto_half_11
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.onesTotal11_bound
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.rho_le_one
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.rho_nonneg
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_add
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_letterSeries
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_monomial
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_mul
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_one
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_sub
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.signedMoment_sum
• Truth anchor: D5/S1/Words/Forbidden/BalancedBordersHalfFrequency.singleton_not_tendsto_half
• Dependency: D5/S1/Words/Forbidden/BorderImbalanceExclusion
• Dependency: D5/S1/Words/Forbidden/ForbiddenWordGrowth