Lax Lean Archive

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

Proof of `Precomputing the answers of MSO formulas by a rational function`

groundedproofs/Lax314295Proofs/Results.lean · lax-314295

What this proof establishes

no assumptions

thm✓Lax314295.LogicPrecomputation

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

The answers of finitely many mso formulas with one or two free variables are read off a letter-to-letter rational function (Lemma C.4.10): a product of the automata of Lemma C.4.2 run from both ends, as a bimachine (Transducers.msoformulasviarationalTransducers.mso_formulas_via_rational).

Proof strategy

The source's statement is about finite sets of source formulas; the concept's sets Φ1Φ₁, Φ2Φ₂ are sent to their images under toSrctoSrc, finite by Set.Finite.imageSet.Finite.image, and the answers are transported back along sattoSrcsat_toSrc. Rational functions come from Part B's bridge; LengthPreservingLengthPreserving unfolds identically.

Attribution

Lemma C.4.10 of Transducers, Part C; formalised by Aristotle (Harmonic), PartC/MSOPrecomp.leanPartC/MSOPrecomp.lean, PartC/MarkBimach.leanPartC/MarkBimach.lean, PartC/MSO.leanPartC/MSO.lean.