Proof of `Hadamard automata and Hadamard-finite series` (3rd statement)

groundedproofs/Lax619925Proofs/Hadamard.lean · lax-619925

What this proof establishes

no assumptions

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

The Hadamard coincidence theorem (paper §5): a series is Hadamard-finite if and only if it is Hadamard-recognisable. The "recognisable implies finite" direction reads off the generator tuple A.sem(Xi)A.sem (X_i); the "finite implies recognisable" direction extends the witnessing tuple by the series itself and builds the automaton from the closure under left derivatives.