Lax Lean Archive

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

Lax132576.LengthPreservingDecidable

Deciding length preservation of a rational function

concepts/Lax132576/LengthPreservingDecidable.lean · lax-132576

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    Theorem

    One can decide whether a given rational function is length preserving (Lemma B.4.3 of Transducers). The book's direct argument computes the unique candidate typing τ:Q→Z\tau : Q \to \mathbb{Z} of the automaton — the difference between output and input length of the runs reaching each state — and checks that every transition respects it and that accepting states have type zero (Claim B.4.4).

    Lean source view on GitHub

    1import Lax132576.TransducerCodes
    2
    3/-!
    4---
    5title: Deciding length preservation of a rational function
    6type: theorem
    7---
    8One can decide whether a given rational function is length preserving (Lemma
    9B.4.3 of *Transducers*). The book's direct argument computes the unique
    10candidate typing τ:Q→Z\tau : Q \to \mathbb{Z} of the automaton — the difference
    11between output and input length of the runs reaching each state — and checks
    12that every transition respects it and that accepting states have type zero
    13(Claim B.4.4).
    14
    15# Formalization notes
    16
    17The decided property, that every output of the coded relation has the length
    18of its input, is meaningful for every code, so the decision procedure is
    19correct for every code; the promise that the code is functional is kept for
    20uniformity with the other decidability statements. The procedure of the proof
    21enumerates the transition sequences of length at most three times the number of
    22states and checks the accepting ones, a pumping argument showing the bound
    23sufficient.
    24-/
    25
    26namespace Lax132576.LengthPreservingDecidable
    27
    28open Lax132576.TransducerCodes
    29
    30/-- Length preservation of a coded rational function is decidable. -/
    31axiom decidable_lengthPreserving :
    32 DecidableUnderPromise CodeFunctional
    33 (fun c => ∀ w v, codeRel c w v → v.length = w.length)
    34
    35end Lax132576.LengthPreservingDecidable
    36
    Show Proof

    Formalization notes

    The decided property, that every output of the coded relation has the length of its input, is meaningful for every code, so the decision procedure is correct for every code; the promise that the code is functional is kept for uniformity with the other decidability statements. The procedure of the proof enumerates the transition sequences of length at most three times the number of states and checks the accepting ones, a pumping argument showing the bound sufficient.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…