Sharp Finite Markov Order in Intrinsic Sofic Dimension

Let $n$ be the real Hankel dimension of the cylinder probabilities of a stationary finite-alphabet process. If its Markov order is finite, then $\operatorname{ord}(\mu)\le \binom n2.$ For every $n\ge2$ , there exists a stationary sofic process with a nonnegative rational presentation of minimal real dimension $n$ and exact Markov order $\binom n2.$ Thus the bound is sharp when the alphabet is allowed to grow.

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Sofic measures
Posed by: Béal, Jugé, Mairesse and Perrin
Year posed: 2026
Years open: 0y
Solved: 2026-09-08
Model: GPT 6 Astra
Vendor: OpenAI
Collaborators: Eugene Gilburg
Verification: Lean-checked, statement unaudited
Publication: Announced
Significance: 12 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

For a stationary finite-alphabet law $\mu$ , let $n=\dim_{\mathbb R}\mathcal H_p$ be the intrinsic real Hankel dimension of its cylinder-probability function. If $\mu$ has any finite Markov order, then $\operatorname{ord}(\mu)\le \binom n2.$
The proof passes to a reduced $n$ -dimensional linear representation and uses Holland's criterion that $k$ -step Markovity is equivalent to every length- $k$ transition product having rank at most one. Applying $\Lambda^2$ turns this into vanishing of products on a space of dimension $\binom n2$ ; a uniform nilpotence argument then forces vanishing after $\binom n2$ steps.

Sharpness is attained for every $n\ge2$ . The construction gives a stationary sofic process with a nonnegative rational presentation of minimal dimension $n$ and exact order $\binom n2$ . One realization uses $\binom n2-1+n^2$ output symbols.

What the AI did

All original mathematical contributions and discoveries in the publication were produced by AI, including the new intrinsic Markov-order theorem, the stochastic sharpness construction, and the exposition. The publisher-supplied default model attribution is OpenAI GPT-6 Astra, but exact runtime model provenance for the individual discovery, formalization, and drafting stages was not retained. The human publisher selected and organized the research and publication but does not claim subject-matter review.

Verification

The accompanying Lean development uses Lean 4.33.1 with a pinned Mathlib commit. The complete project-local import closure is included, and the four advertised formal endpoints were audited with only `propext`, `Classical.choice`, and `Quot.sound`. Reproduction instructions and source hashes are included.

The formal development proves the one-sided stationary-process upper theorem and rational stationary sharpness. No professional human mathematical review is claimed. Lean verification establishes the encoded statements and assumptions, not global novelty, every prose claim, or the separately discussed two-sided extension.

Sources

Lean proofAudit.lean: the printed endpoints and their axioms
CodeGithub

Submitted by VibeGene on 08 Sep 2026

Sharp Finite Markov Order in Intrinsic Sofic Dimension

What was actually shown

What the AI did

Verification

Sources

Discussion1