Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Proof of `Polyregular functions are continuous`

groundedproofs/Lax194892Proofs/Results.lean · lax-194892

What this proof establishes

no assumptions

thm✓Lax194892.PolyregularContinuity

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

In the paper

Description

Polyregular functions are continuous (Theorem D.0.2): induction on the composition tree, with Theorem C.1.1 for the regular primes and a direct automaton for marked squaring (Transducers.polyregularcontinuousTransducers.polyregular_continuous).

Proof strategy

The concept's IsPolyregularIsPolyregular is the source's through isPolyregulariffisPolyregular_iff (Part A's compClosureiffcompClosure_iff on the family, whose regular half goes through Part C's isRegularFuniffisRegularFun_iff and whose marked squaring unfolds identically); ContinuousContinuous unfolds identically. The source proves marked squaring continuous by running the input backwards through a deterministic automaton for the output language and reading off the states of the blocks (PartD/MarkedSquare.leanPartD/MarkedSquare.lean).

Attribution

Theorem D.0.2 of Transducers, Part D; formalised by Aristotle (Harmonic), PartD/Statements.leanPartD/Statements.lean, PartD/MarkedSquare.leanPartD/MarkedSquare.lean.