Lax Lean Archive

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

Proof of `Decidable equivalence of weighted automata over the rationals`

groundedproofs/Lax132576Proofs/Results.lean · lax-132576

What this proof establishes

no assumptions

thm✓Lax132576.WeightedEquivalenceDecidable

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

Decidable equivalence of weighted automata over Qℚ (Theorem B.3.3): the effective Schützenberger bound (Transducers.effectiveWeightedBoundTransducers.effectiveWeightedBound) and the primitive recursive evaluation of a coded automaton (Transducers.EffectiveWeightedEvalEqTransducers.EffectiveWeightedEvalEq), assembled in Transducers.weightedequivalencedecidableTransducers.weighted_equivalence_decidable; the concept's codes are moved to the source's tuples by wcodeEquiv2wcodeEquiv₂.

Attribution

Theorem B.3.3 of Transducers (Schützenberger); Lean proof by Aristotle (PartB/WeightedDec.leanPartB/WeightedDec.lean, PartB/WeightedBound.leanPartB/WeightedBound.lean, PartB/WCodePrimrec.leanPartB/WCodePrimrec.lean).