Documentation

LeanPool.PointwiseComposition.FailureOfComposition.PartialRecursiveQuotient

Supporting results for pointwise provable equality.

The generated quotient of a Sigma-one sound PA extension is the monoid of unary partial recursive functions. The target consists of actual partial maps, with partial composition as multiplication and the total identity as its unit.

source
def PointwiseComposition.FailureOfComposition.UnaryPartrec :
Type

Unary partial recursive functions, identified by equality of partial maps.

Equations
Instances For
    source
    @[instance_reducible]
    instance PointwiseComposition.FailureOfComposition.UnaryPartrec.instMul :
    Mul UnaryPartrec
    Equations
    source
    @[instance_reducible]
    instance PointwiseComposition.FailureOfComposition.UnaryPartrec.instOne :
    One UnaryPartrec
    Equations
    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.UnaryPartrec.mul_apply (f g : UnaryPartrec) (x : ℕ) :
    ↑(f * g) x = (↑g x).bind ↑f

    Multiplication is ordinary partial composition, with the right map applied first.

    source
    @[simp]
    theorem PointwiseComposition.FailureOfComposition.UnaryPartrec.one_apply (x : ℕ) :
    ↑1 x = Part.some x
    source
    @[instance_reducible]
    instance PointwiseComposition.FailureOfComposition.UnaryPartrec.instMonoid :
    Monoid UnaryPartrec
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def PointwiseComposition.FailureOfComposition.UnaryPartrec.ofIndex (e : ℕ) :
    UnaryPartrec

    The partial recursive function denoted by a concrete natural-number index.

    Equations
    Instances For
      source
      @[simp]
      theorem PointwiseComposition.FailureOfComposition.UnaryPartrec.ofIndex_val (e : ℕ) :
      ↑(ofIndex e) = Kleene.eval e
      source
      theorem PointwiseComposition.FailureOfComposition.UnaryPartrec.ofIndex_surjective :
      Function.Surjective ofIndex

      Every unary partial recursive function has an index in the fixed numbering.

      source
      noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientDenotation (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) :
      GeneratedQuotient T → UnaryPartrec

      Evaluation descends to the generated quotient of a Sigma-one sound theory.

      Equations
      Instances For
        source
        @[simp]
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientDenotation_mk (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) (e : ℕ) :
        generatedQuotientDenotation T hT (generatedQuotientMk T e) = UnaryPartrec.ofIndex e
        source
        theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientDenotation_bijective (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) :
        Function.Bijective (generatedQuotientDenotation T hT)
        source
        noncomputable def PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientPartialRecursiveEquiv (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) :
        GeneratedQuotient T ≃* UnaryPartrec

        In the sound case, the generated quotient is isomorphic to the monoid of all unary partial recursive functions under partial composition.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem PointwiseComposition.FailureOfComposition.ConcreteIndices.generatedQuotientPartialRecursiveEquiv_mk (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (hT : GeneratedCongruence.SigmaOneSound T) (e : ℕ) :
          (generatedQuotientPartialRecursiveEquiv T hT) (generatedQuotientMk T e) = UnaryPartrec.ofIndex e