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

Lax765601.MapLiftingDecomposition

Map lifting preserves decompositions into primes

concepts/Lax765601/MapLiftingDecomposition.lean · lax-765601

proven

Loading review…

Sign in with ORCID

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

    If a Mealy machine decomposes into prime Mealy machines, then so does its map lifting (Lemma A.2.4 of Transducers). Since map lifting commutes with composition, it suffices to lift a single prime. A flip-flop is lifted by resetting its state at every separator. A reversible machine needs more care, because resetting would break reversibility: the book computes, by a reversible machine, the state transformation γw\gamma_w of every prefix in the variant where the separator does nothing, stores the value at the last separator by a flip-flop delay machine, and recovers the state transformation of the current block by the cancellation law δw=γv1γvw\delta_w = \gamma_v^{-1} \cdot \gamma_{vw}, all of which is a one-state machine's work.

    Lean source view on GitHub

    1import Lax765601.PrimeMealyMachines
    2import Lax765601.MapLifting
    3
    4/-!
    5---
    6title: Map lifting preserves decompositions into primes
    7type: theorem
    8---
    9If a Mealy machine decomposes into prime Mealy machines, then so does its map
    10lifting (Lemma A.2.4 of *Transducers*). Since map lifting commutes with
    11composition, it suffices to lift a single prime. A flip-flop is lifted by
    12resetting its state at every separator. A reversible machine needs more care,
    13because resetting would break reversibility: the book computes, by a reversible
    14machine, the state transformation γw\gamma_w of every prefix in the variant
    15where the separator does nothing, stores the value at the last separator by a
    16flip-flop delay machine, and recovers the state transformation of the current
    17block by the cancellation law δw=γv1γvw\delta_w = \gamma_v^{-1} \cdot \gamma_{vw},
    18all of which is a one-state machine's work.
    19
    20# Formalization notes
    21
    22Finiteness of the input alphabet is assumed; the finiteness of the output
    23alphabet, which the book assumes globally, is not needed here and is dropped.
    24The map lifting is `MapLifting.mapLift`, over the alphabets `Option A` and
    25`Option B`.
    26-/
    27
    28namespace Lax765601.MapLiftingDecomposition
    29
    30open Lax765601.CompositionClosure Lax765601.PrimeMealyMachines Lax765601.MapLifting
    31
    32/-- The map lifting of a composition of prime Mealy machines is a composition of
    33prime Mealy machines. -/
    34axiom compClosure_mapLift {A B : Type} [Finite A] {f : List A → List B}
    35 (hf : CompClosure PrimeMealyFam A B f) :
    36 CompClosure PrimeMealyFam (Option A) (Option B) (mapLift f)
    37
    38end Lax765601.MapLiftingDecomposition
    39
    Show Proof

    Formalization notes

    Finiteness of the input alphabet is assumed; the finiteness of the output alphabet, which the book assumes globally, is not needed here and is dropped. The map lifting is MapLifting.mapLiftMapLifting.mapLift, over the alphabets OptionAOption A and OptionBOption B.

    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…