Canonical projection of lists of binary Nat pairs

TheoremProjected pair lists total at most four times the input length#✓fully proved

Both projected canonical lists together are bounded by four times the original raw list length, including noncanonical input payloads.

theorem projection_length_le {x : List Bool} {as : List (Nat × Nat)}
    (h : bitDecode x = some as) :
    (bitEncode (as.map Prod.fst)).length +
      (bitEncode (as.map Prod.snd)).length ≤ 4 * x.length

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 11 · Used by 2

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks

Proof usesCanonical payloads of a decoded pair are bounded by the raw input · Successful block parsing reconstructs the input · List decoder consumes one raw payload at a time

Used byPair-list projector yields canonical weight and value lists · Four-output decoder output is at most twice the input length

InductiveStacks of the pair-list projector#✓fully proved

Raw outer input, two reversed accumulators, two outputs, and the existing Nat-pair component's workspace.

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

Uses 1 · Used by 21

Statement usesStacks of the number-pair projector

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Stack embedding of the pair normalizer in the pair-list projector · Program of the pair-list projector · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Eleven-stack invariant of the pair-list projector · Four-output pair-list decoder as a host component · List-projector stack embedding in the four-output decoder · Stacks of the four-output pair-list decoder · Final pair-projector stack embedding in the four-output decoder · Program of the four-output pair-list decoder · Four-output decoder reaches exactly the canonical decoding outcome · Embedded four-output decoder preserves outside stacks · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Outer-splitter stack embedding in the four-output decoder · Stack invariant of the four-output pair-list decoder

InductiveControl labels of the pair-list projector#✓fully proved

Read one outer frame, normalize its pair, emit both fields, repeat.

inductive Lab | loop | block | back | pair (l : NatPair.Lab)
  | emit (right : Bool) | finish (right : Bool) | good | bad
  deriving DecidableEq

inductive Lab | pair (l : PairSplit.Lab)
  | norm (second : Bool) (l : NormalizeMachine.Lab) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:40

Uses 1 · Used by 16

Statement usesControl labels of the number-pair projector

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Pair-normalizer halt redirection in the pair-list projector · Program of the pair-list projector · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Four-output pair-list decoder as a host component · Label map from the list projector to the final pair decoder · Control labels of the four-output pair-list decoder · Program of the four-output pair-list decoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Label map from the outer splitter to the list projector

DefinitionStack embedding of the pair normalizer in the pair-list projector#✓fully proved

The Nat-pair component is embedded without changing its alphabets.

def pairEmb : SEmb (fun _ : NatPair.K => Bool) (fun _ : K => Bool) where
  e := K.pair
  inj _ _ h := K.pair.inj h
  ι _ := Equiv.refl Bool

structure SEmb {K K' : Type} (Γ : K → Type) (Γ' : K' → Type) where
  /-- The stack renaming. -/
  e : K → K'
  /-- Distinct sub-machine stacks go to distinct host stacks. -/
  inj : Injective e
  /-- The alphabet of each sub-machine stack, identified with its host stack's. -/
  ι : ∀ k, Γ k ≃ Γ' (e k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:51

inductive K | pair (k : PairSplit.K) | buffer | left | right
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:29

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:71

  inj : Injective e

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:55

  ι : ∀ k, Γ k ≃ Γ' (e k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:57

Uses 3 · Used by 3

Statement usesStacks of the pair-list projector · Stacks of the number-pair projector · Stack embedding

Used byPair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time

DefinitionPair-normalizer halt redirection in the pair-list projector#✓fully proved

Only the pair component's actual halts are redirected.

def pairLabel : NatPair.Lab → Lab
  | .good => .emit false
  | .bad => .bad
  | l => .pair l

inductive Lab | pair (l : PairSplit.Lab)
  | norm (second : Bool) (l : NormalizeMachine.Lab) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:40

inductive Lab | loop | block | back | pair (l : NatPair.Lab)
  | emit (right : Bool) | finish (right : Bool) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:85

Uses 4 · Used by 3

Statement usesControl labels of the payload normalizer machine · Control labels of the pair-list projector · Control labels of the number-pair projector · Control labels of the raw pair-frame splitter

Used byPair-list projector emits one weight and one value frame per item · Program of the pair-list projector · Pair-list projector fails on malformed input in linear time

DefinitionProgram of the pair-list projector#✓fully proved

Concrete outer parsing, pair normalization, and two framed streams.

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
      (.finish right) (if right then .good else .finish true)
  | .good | .bad => .halt

inductive Lab | loop | block | back | pair (l : NatPair.Lab)
  | emit (right : Bool) | finish (right : Bool) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:85

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:71

def read (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b)
    (self good bad : Λ) : TM2.Stmt Γ Λ Bool :=
  .peek a (fun _ o => isBit d o) <| .branch id
    (.pop a (fun _ o => bitOf d o) <| .branch id
      (.peek a (fun _ o => isBit d o) <| .branch id
        (.pop a (fun _ o => bitOf d o) <| .push b g <|
          .goto fun _ => self)
        (.goto fun _ => bad))
      (.goto fun _ => good))
    (.goto fun _ => bad)

CSLibExt/Computability/Complexity/FramedCNF/Block.lean:32

def moveB (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b) (self next : Λ) :
    TM2.Stmt Γ Λ σ :=
  .peek a (fun _ o => Flag.tag (isBit d o))
    (.branch Flag.untag
      (.pop a (fun _ o => Flag.tag (bitOf d o))
        (.branch Flag.untag
          (.push b (fun _ => g true) (.goto fun _ => self))
          (.push b (fun _ => g false) (.goto fun _ => self))))
      (.goto fun _ => next))

MathlibExt/Computability/TuringMachine/BitOps.lean:86

def mapS : TM2.Stmt Γ Λ σ → TM2.Stmt Γ' Λ' σ
  | .push k f q => .push (E.e k) (fun s => E.ι k (f s)) (mapS q)
  | .peek k f q => .peek (E.e k) (fun s o => f s (o.map (E.ι k).symm)) (mapS q)
  | .pop k f q => .pop (E.e k) (fun s o => f s (o.map (E.ι k).symm)) (mapS q)
  | .load a q => .load a (mapS q)
  | .branch f q₁ q₂ => .branch f (mapS q₁) (mapS q₂)
  | .goto f => .goto fun s => φ (f s)
  | .halt => .halt

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:65

def pairEmb : SEmb (fun _ : NatPair.K => Bool) (fun _ : K => Bool) where
  e := K.pair
  inj _ _ h := K.pair.inj h
  ι _ := Equiv.refl Bool

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:99

def pairLabel : NatPair.Lab → Lab
  | .good => .emit false
  | .bad => .bad
  | l => .pair l

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:105

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .pair l => mapS pairEmb pairLabel (PairSplit.prog l)
  | .norm s l => mapS (normEmb s) (normLabel s) (NormalizeMachine.prog l)
  | .good | .bad => .halt

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:84

def emitFrame (a b : K) (d : Γ a → Option Bool) (g : Bool → Γ b)
    (self next : Λ) : TM2.Stmt Γ Λ Bool :=
  .peek a (fun _ o => isBit d o) <| .branch id
    (.pop a (fun _ o => bitOf d o) <|
      .push b (fun _ => g true) <| .push b g <| .goto fun _ => self)
    (.push b (fun _ => g false) <| .goto fun _ => next)

CSLibExt/Computability/Complexity/PolynomialEncoding/Frame.lean:32

Uses 14 · Used by 10

Statement usesMachine step reading one framed payload pair · Stacks of the pair-list projector · Control labels of the pair-list projector · Stack embedding of the pair normalizer in the pair-list projector · Pair-normalizer halt redirection in the pair-list projector · Stacks of the number-pair projector · Control labels of the number-pair projector · Program of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter · Reversed self-delimiting frame emitter · Translating a statement along a stack embedding · Flag bit of a machine state · Bit-moving loop

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector as a host component · Pair-list projector emits one weight and one value frame per item · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Program of the four-output pair-list decoder · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success

DefinitionEleven-stack invariant of the pair-list projector#✓fully proved

The exact eleven-stack invariant, with caller output suffixes.

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

inductive K | pair (k : PairSplit.K) | buffer | left | right
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:29

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:71

Uses 2 · Used by 9

Statement usesStacks of the pair-list projector · Stacks of the number-pair projector

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector emits one weight and one value frame per item · Pair-list projector always terminates at the decoding outcome · Embedded pair-list projector preserves outside stacks · Pair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success · Stack invariant of the four-output pair-list decoder

TheoremPair-list projector emits one weight and one value frame per item#✓fully proved

One successfully decoded item contributes one canonical weight frame and one canonical value frame, with pair scratch emptied again.

theorem element_run {p : List Bool} {m n : Nat}
    (h : bitDecode p = some (m, n)) (r aw av ow ov : List Bool) (v : Bool) :
    RunLe prog (12 * (delimit p).length)
      ⟨some .loop, v, st (delimit p ++ r) aw av ow ov
        (NatPair.st [] [] [] [] [] [])⟩
      ⟨some .loop, false,
        st r ((delimit (Computability.encodeNat m)).reverse ++ aw)
          ((delimit (Computability.encodeNat n)).reverse ++ av) ow ov
          (NatPair.st [] [] [] [] [] [])⟩

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def delimit : List Bool → List Bool
  | [] => [false]
  | b :: l => true :: b :: delimit l

MathlibExt/Computability/Complexity.lean:68

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

Uses 34 · Used by 2

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Runs within a step budget

Proof usesReading a complete framed block · Control labels of the payload normalizer machine · Stack embedding of the pair normalizer in the pair-list projector · Pair-normalizer halt redirection in the pair-list projector · Control labels of the number-pair projector · Canonical payloads of a decoded pair are bounded by the raw input · Program of the number-pair projector · Number-pair projector yields both canonical payloads on success · Control labels of the raw pair-frame splitter · Frame emitter takes one step per payload bit plus one · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byPair-list projector main loop emits both lists in reverse · Pair-list projector fails on malformed input in linear time

TheoremPair-list projector main loop emits both lists in reverse#✓fully proved

The main loop emits both lists in reverse, ready for the two final stack reversals. Order and multiplicity follow the decoded input.

theorem blocks_run (bs : List (List Bool)) (as : List (Nat × Nat))
    (h : bitDecode (bs.map delimit).flatten = some as)
    (aw av ow ov : List Bool) (v : Bool) :
    RunLe prog (12 * ((bs.map delimit).flatten).length + 1)
      ⟨some .loop, v, st (bs.map delimit).flatten aw av ow ov
        (NatPair.st [] [] [] [] [] [])⟩
      ⟨some (.finish false), false,
        st [] ((bitEncode (as.map Prod.fst)).reverse ++ aw)
          ((bitEncode (as.map Prod.snd)).reverse ++ av) ow ov
          (NatPair.st [] [] [] [] [] [])⟩

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def delimit : List Bool → List Bool
  | [] => [false]
  | b :: l => true :: b :: delimit l

MathlibExt/Computability/Complexity.lean:68

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 20 · Used by 1

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesPair-list projector emits one weight and one value frame per item · List decoder consumes one raw payload at a time · Exact-length runs of a TM2 machine · A single step executes the statement at the current label

Used byPair-list projector yields canonical weight and value lists

TheoremPair-list projector yields canonical weight and value lists#✓fully proved

Successful generic decoding yields the canonical weight and value lists on separate stacks. All input and scratch stacks are emptied.

theorem run_some {x : List Bool} {as : List (Nat × Nat)}
    (h : bitDecode x = some as) (ow ov : List Bool) (v : Bool) :
    ∃ w, RunLe prog (16 * x.length + 3)
      ⟨some .loop, v, st x [] [] ow ov (NatPair.st [] [] [] [] [] [])⟩
      ⟨some .good, w, st [] [] [] (bitEncode (as.map Prod.fst) ++ ow)
        (bitEncode (as.map Prod.snd) ++ ov)
        (NatPair.st [] [] [] [] [] [])⟩

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 22 · Used by 3

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesPair-list projector main loop emits both lists in reverse · Projected pair lists total at most four times the input length · Successful block parsing reconstructs the input · Flag bit of a machine state · Exact-length runs of a TM2 machine · Running the bit-moving loop

Used byPair-list projector always terminates at the decoding outcome · Four-output decoder fails on malformed input · Four-output decoder emits four canonical outputs on success

TheoremPair-list projector fails on malformed input in linear time#✓fully proved

Malformed outer framing or any malformed pair reaches bad in linear time. Failed workspaces may contain partial data and need clearing.

theorem run_none {x : List Bool}
    (h : bitDecode (α := List (Nat × Nat)) x = none)
    (aw av ow ov : List Bool) (v : Bool) :
    ∃ w S, RunLe prog (12 * x.length + 2)
      ⟨some .loop, v, st x aw av ow ov (NatPair.st [] [] [] [] [] [])⟩
      ⟨some .bad, w, S⟩

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

Uses 38 · Used by 2

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesReading a complete framed block · Framed block reader fails on truncated framing · Control labels of the payload normalizer machine · Pair-list projector emits one weight and one value frame per item · Stack embedding of the pair normalizer in the pair-list projector · Pair-normalizer halt redirection in the pair-list projector · Control labels of the number-pair projector · Program of the number-pair projector · Number-pair projector fails on malformed framing in linear time · Control labels of the raw pair-frame splitter · List decoder consumes one raw payload at a time · Parsing a self-delimiting block · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Translating a statement along a stack embedding · Run embedding for bounded runs · Flag bit of a machine state · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Running the bit-moving loop

Used byPair-list projector always terminates at the decoding outcome · Four-output decoder fails on malformed input

AbbreviationPair-list projector as a host component#✓fully proved

The concrete eleven-stack projector uses the existing Host model.

Cslib.Complexity.PolynomialEncoding.ListNatPair.component · 17 lines

abbrev component : Host.Comp where
  K := K
  Γ := fun _ => Bool
  L := Lab
  prog := prog
  ks := [.input, .acc false, .acc true, .output false, .output true,
    .pair (.pair .input), .pair (.pair .left), .pair (.pair .scratch),
    .pair .buffer, .pair .left, .pair .right]
  ks_nodup := by decide
  mem_ks k := by
    cases k with
    | input => decide
    | acc b | output b => cases b <;> decide
    | pair k =>
      cases k with
      | pair k => cases k <;> decide
      | buffer | left | right => decide

structure Comp where
  /-- Stack indices. -/
  K : Type
  /-- Decidable equality of stack indices. -/
  [decK : DecidableEq K]
  /-- Finitely many stacks. -/
  [finK : Fintype K]
  /-- Stack alphabets. -/
  Γ : K → Type
  /-- Finite alphabets. -/
  [finΓ : ∀ k, Fintype (Γ k)]
  /-- Labels. -/
  ⋯

CSLibExt/Computability/Complexity/Host.lean:53

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:71

inductive Lab | loop | block | back | pair (l : NatPair.Lab)
  | emit (right : Bool) | finish (right : Bool) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:85

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

Uses 9 · Used by 1

Statement usesControl labels of the payload normalizer machine · Component machine · Stacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Stacks of the number-pair projector · Control labels of the number-pair projector · Stacks of the raw pair-frame splitter · Control labels of the raw pair-frame splitter

Used byFour-output pair-list decoder as a host component

TheoremPair-list projector always terminates at the decoding outcome#✓fully proved

Total decoder outcome. Success projects canonical lists with empty scratch; failure promises termination, not reusable workspace contents.

theorem run (x : List Bool) (v : Bool) :
    ∃ w S, RunLe prog (16 * x.length + 3)
      ⟨some .loop, v, st x [] [] [] [] (NatPair.st [] [] [] [] [] [])⟩
      ⟨some (if (bitDecode (α := List (Nat × Nat)) x).isSome
        then .good else .bad), w, S⟩ ∧
      ∀ as : List (Nat × Nat), bitDecode x = some as →
        S = st [] [] [] (bitEncode (as.map Prod.fst))
          (bitEncode (as.map Prod.snd)) (NatPair.st [] [] [] [] [] [])

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 19 · Used by 1

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Stacks of the number-pair projector · Six-stack invariant of the number-pair projector · Stacks of the raw pair-frame splitter · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Runs within a step budget

Proof usesPair-list projector fails on malformed input in linear time · Pair-list projector yields canonical weight and value lists · Exact-length runs of a TM2 machine

Used byEmbedded pair-list projector preserves outside stacks

TheoremEmbedded pair-list projector preserves outside stacks#✓fully proved

Any stack embedding preserves the external frame on both outcomes. Only mapped-label reachability is promised: callers establish their own continuation-label separation. Failed private workspace needs clearing.

theorem run_embedded {J L : Type} [DecidableEq J] {Γ : J → Type}
    (E : SEmb (fun _ : K => Bool) Γ) (φ : Lab → L)
    {M : L → TM2.Stmt Γ L Bool} (hm : Embeds E φ prog M)
    (x : List Bool) (v : Bool) (S : ∀ j, List (Γ j))
    (hs : Agree E (st x [] [] [] [] (NatPair.st [] [] [] [] [] [])) S) :
    ∃ w T, RunLe M (16 * x.length + 3)
      ⟨some (φ .loop), v, S⟩
      ⟨some (φ (if (bitDecode (α := List (Nat × Nat)) x).isSome
        then .good else .bad)), w, T⟩ ∧ Frame E S T ∧
      ∀ as : List (Nat × Nat), bitDecode x = some as →
        Agree E (st [] [] [] (bitEncode (as.map Prod.fst))
          (bitEncode (as.map Prod.snd)) (NatPair.st [] [] [] [] [] [])) T

structure SEmb {K K' : Type} (Γ : K → Type) (Γ' : K' → Type) where
  /-- The stack renaming. -/
  e : K → K'
  /-- Distinct sub-machine stacks go to distinct host stacks. -/
  inj : Injective e
  /-- The alphabet of each sub-machine stack, identified with its host stack's. -/
  ι : ∀ k, Γ k ≃ Γ' (e k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:51

inductive K | input | acc (right : Bool) | output (right : Bool)
  | pair (k : NatPair.K)
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:71

inductive Lab | loop | block | back | pair (l : NatPair.Lab)
  | emit (right : Bool) | finish (right : Bool) | good | bad
  deriving DecidableEq

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:85

def Embeds (M : Λ → TM2.Stmt Γ Λ σ) (M' : Λ' → TM2.Stmt Γ' Λ' σ) : Prop :=
  ∀ l, M' (φ l) = mapS E φ (M l) ∨ M l = .halt

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:76

def prog : Lab → TM2.Stmt (fun _ : K => Bool) Lab Bool
  | .loop => .peek .input (fun _ o => o.isSome) <| .branch id
      (.goto fun _ => .block) (.goto fun _ => .finish false)
  | .block => FramedCNF.Block.read .input (.pair (.pair .scratch))
      some id .block .back .bad
  | .back => moveB (.pair (.pair .scratch)) (.pair (.pair .input))
      some id .back (.pair (.pair .read))
  | .pair l => mapS pairEmb pairLabel (NatPair.prog l)
  | .emit right => emitFrame
      (if right then .pair .right else .pair .left) (.acc right)
      some id (.emit right) (if right then .loop else .emit true)
  | .finish right => moveB (.acc right) (.output right) some id
  ⋯

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:111

def Agree (S : ∀ k, List (Γ k)) (S' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k, S' (E.e k) = (S k).map (E.ι k)

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:80

def st (input aw av ow ov : List Bool) (P : NatPair.K → List Bool) :
    K → List Bool
  | .input => input
  | .acc right => if right then av else aw
  | .output right => if right then ov else ow
  | .pair k => P k

CSLibExt/Computability/Complexity/PolynomialEncoding/ListNatPair.lean:127

def st (input first scratch buffer left right : List Bool) : K → List Bool
  | .pair .input => input
  | .pair .left => first
  | .pair .scratch => scratch
  | .buffer => buffer
  | .left => left
  | .right => right

CSLibExt/Computability/Complexity/PolynomialEncoding/NatPair.lean:90

def RunLe (M : Λ → TM2.Stmt Γ Λ σ) (B : ℕ) (c d : TM2.Cfg Γ Λ σ) : Prop :=
  ∃ n, n ≤ B ∧ Run M n c d

MathlibExt/Computability/TuringMachine/Program.lean:901

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def Frame (S' S'' : ∀ k', List (Γ' k')) : Prop :=
  ∀ k', (∀ k, E.e k ≠ k') → S'' k' = S' k'

MathlibExt/Computability/TuringMachine/StackEmbedding.lean:84

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 22

Statement usesStacks of the pair-list projector · Control labels of the pair-list projector · Program of the pair-list projector · Eleven-stack invariant of the pair-list projector · Six-stack invariant of the number-pair projector · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Agreement of host and sub-machine stacks · Embedding of a machine in a host · Frame condition for a stack embedding · Stack embedding · Runs within a step budget

Proof usesPair-list projector always terminates at the decoding outcome · Stacks of the number-pair projector · Stacks of the raw pair-frame splitter · Run embedding for bounded runs

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.