SingleRunDegrees

Abstract

Degree enumeration for labelled circular run-constrained words.

Theorem 1.1 (run interior delete illegal).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (a:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),\forall (p:\mathrm{Nat}),(\mathrm{IsOneRunStart}war)\to ((0<p)\to ((p+1<r)\to (\neg \mathrm{Admissible}(\mathrm{CircularWords}.\mathrm{flip}w(\mathrm{cycAdd}ap)))))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/SingleRunDegrees.run_interior_delete_illegal (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

Deleting an interior one splits its run around a zero gap too short for the preceding run.

Definition 1.2 (singleRun).

$$\forall (n:\mathrm{Nat}),\forall (r:\mathrm{Nat}),\mathrm{singleRun}nr=(\mathrm{fun}j\mapsto \mathrm{decide}(j.\mathrm{val}<r))$$

Formalization. D5/S1/Words/AssociatedMersenne/SingleRunDegrees.singleRun (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The first r labelled positions are ones and the remaining positions are zeros.

Theorem 1.3 (singleRun degree).

$$\forall (r:\mathrm{Nat}),\forall (s:\mathrm{Nat}),(0<r)\to (\mathrm{degree}(\mathrm{singleRun}(2\cdot r+1+s)r)=\min r2+\mathrm{if}2\le s\mathrm{then}s\mathrm{else}0)$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/SingleRunDegrees.singleRun_degree (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

Endpoint deletions and the admissible insertions in the shared circular gap give the exact single-run degree.

Theorem 1.4 (degree raw singleton).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),\forall (z:\mathrm{Nat}),(0<r)\to ((r<z)\to ((\mathrm{linearize}wi=\mathrm{rawWord}[(r,z)])\to (\mathrm{degree}w=\min r2+\mathrm{if}2\le z-r-1\mathrm{then}z-r-1\mathrm{else}0)))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/SingleRunDegrees.degree_raw_singleton (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

Rotating to the mark identifies a singleton raw-pair encoding with the single-run degree calculation.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/SingleRunDegrees.degree_raw_singleton
• Truth anchor: D5/S1/Words/AssociatedMersenne/SingleRunDegrees.run_interior_delete_illegal
• Truth anchor: D5/S1/Words/AssociatedMersenne/SingleRunDegrees.singleRun
• Truth anchor: D5/S1/Words/AssociatedMersenne/SingleRunDegrees.singleRun_degree
• Dependency: D5/S1/Words/AssociatedMersenne/RunTupleBijection