Documentation

LeanPool.SmallUndecidableGroups.Thue.FixedSeed

FixedSeed #

Part of the dependency closure of the small undecidable group constructions.

source
noncomputable def Undecidability.FixedMachine.thueBinaryCode :
TM1BinaryAdapter.Code TapeSymbol

The canonical binary block code used to feed the finite Post bridge.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev Undecidability.FixedMachine.ThueAlphabet (c : Turing.ToPartrec.Code) :
    Type

    The finite alphabet of the Thue system simulating a specified partial recursive code.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Undecidability.FixedMachine.thuePostMachine (c : Turing.ToPartrec.Code) :
      PostMachine.Machine (TM0PostAdapter.Phase ↥(SupportedTM1Thue.State thueBinaryCode oneTapeProgram (oneTapeSupport c)))

      The finitely supported Post machine simulating a specified partial recursive code.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Undecidability.FixedMachine.thueSystem (c : Turing.ToPartrec.Code) :
        ThueSystem (ThueAlphabet c)

        The Thue system simulating a specified partial recursive code.

        Equations
        Instances For
          source
          noncomputable def Undecidability.FixedMachine.thueStart (c : Turing.ToPartrec.Code) (input : List TapeSymbol) :
          List (ThueAlphabet c)

          The encoded initial configuration for a specified code and tape input.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Undecidability.FixedMachine.thue_iff_oneTape_eval_dom (c : Turing.ToPartrec.Code) (input : List TapeSymbol) :
            ThueEq (thueSystem c) (thueStart c input) PostMachine.target ↔ (Turing.TM1.eval oneTapeProgram input).Dom
            source
            theorem Undecidability.FixedMachine.thueSystem_finite (c : Turing.ToPartrec.Code) :
            Set.Finite (thueSystem c)
            source
            @[instance_reducible]
            noncomputable instance Undecidability.FixedMachine.thueAlphabetFintype (c : Turing.ToPartrec.Code) :
            Fintype (ThueAlphabet c)
            Equations
            source
            instance Undecidability.FixedMachine.thueAlphabetNonempty (c : Turing.ToPartrec.Code) :
            Nonempty (ThueAlphabet c)
            source
            @[instance_reducible]
            noncomputable instance Undecidability.FixedMachine.thueAlphabetPrimcodable (c : Turing.ToPartrec.Code) :
            Primcodable (ThueAlphabet c)
            Equations
            • One or more equations did not get rendered due to their size.
            source
            theorem Undecidability.FixedMachine.thueStart_computable (c : Turing.ToPartrec.Code) :
            Computable (thueStart c)
            source
            theorem Undecidability.FixedMachine.thue_target_not_computable (c : Turing.ToPartrec.Code) (hc : ∀ (n : ℕ), (c.eval [n]).Dom ↔ (fixedUniversalEval n).Dom) :
            ¬ComputablePred fun (Q : List (ThueAlphabet c)) => ThueEq (thueSystem c) Q PostMachine.target
            source
            theorem Undecidability.FixedMachine.exists_finiteFixedTargetSeed :
            Nonempty Thue.Matiyasevich1993.FiniteFixedTargetSeed

            A finite fixed-target Thue seed obtained from Mathlib's universal partial-recursive evaluator and the explicit Post simulation.