OAI/Computability/RationalHitting/InputAdapter.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Required reverse interface from a block-coded finite stack simulator to literal Fin4 output digits. All registers of this transducer are finite.

  1. abbrev OAI.RationalHitting.TMTime.InputAdapter.A line 7
  2. abbrev OAI.RationalHitting.TMTime.InputAdapter.Q line 8
  3. abbrev OAI.RationalHitting.TMTime.InputAdapter.V line 9
  4. abbrev OAI.RationalHitting.TMTime.InputAdapter.Cfg line 10
  5. abbrev OAI.RationalHitting.TMTime.InputAdapter.Stmt line 11
  6. def OAI.RationalHitting.TMTime.InputAdapter.raw line 13
  7. def OAI.RationalHitting.TMTime.InputAdapter.bit line 14
  8. def OAI.RationalHitting.TMTime.InputAdapter.jump line 16
  9. def OAI.RationalHitting.TMTime.InputAdapter.move line 17
  10. def OAI.RationalHitting.TMTime.InputAdapter.leftTo line 18
  11. def OAI.RationalHitting.TMTime.InputAdapter.writeBits line 21
  12. def OAI.RationalHitting.TMTime.InputAdapter.M line 25
  13. lemma OAI.RationalHitting.TMTime.InputAdapter.head₂ line 50
  14. lemma OAI.RationalHitting.TMTime.InputAdapter.right₂ line 51
  15. lemma OAI.RationalHitting.TMTime.InputAdapter.left₂ line 53
  16. lemma OAI.RationalHitting.TMTime.InputAdapter.write₂ line 55
  17. lemma OAI.RationalHitting.TMTime.InputAdapter.stepAux_writeBits line 58
  18. lemma OAI.RationalHitting.TMTime.InputAdapter.scan_right line 71
  19. lemma OAI.RationalHitting.TMTime.InputAdapter.scan_left line 83
  20. lemma OAI.RationalHitting.TMTime.InputAdapter.bit_ne_three line 100
  21. lemma OAI.RationalHitting.TMTime.InputAdapter.raw_ne_zero line 101
  22. def OAI.RationalHitting.TMTime.InputAdapter.state line 103
  23. def OAI.RationalHitting.TMTime.InputAdapter.invariant line 105
  24. lemma OAI.RationalHitting.TMTime.InputAdapter.process line 108
  25. def OAI.RationalHitting.TMTime.InputAdapter.emit line 179
  26. def OAI.RationalHitting.TMTime.InputAdapter.cost line 183
  27. lemma OAI.RationalHitting.TMTime.InputAdapter.all_process line 188
  28. lemma OAI.RationalHitting.TMTime.InputAdapter.emit_length line 200
  29. lemma OAI.RationalHitting.TMTime.InputAdapter.cost_bound line 211
  30. lemma OAI.RationalHitting.TMTime.InputAdapter.left_empty line 232
  31. lemma OAI.RationalHitting.TMTime.InputAdapter.clear_blanks line 235
  32. lemma OAI.RationalHitting.TMTime.InputAdapter.scan_six_zero line 245
  33. lemma OAI.RationalHitting.TMTime.InputAdapter.enter_finish line 249
  34. lemma OAI.RationalHitting.TMTime.InputAdapter.finish line 254
  35. lemma OAI.RationalHitting.TMTime.InputAdapter.scan_zero_raw line 307
  36. lemma OAI.RationalHitting.TMTime.InputAdapter.start_markers line 312
  37. lemma OAI.RationalHitting.TMTime.InputAdapter.start line 317
  38. theorem OAI.RationalHitting.TMTime.InputAdapter.prepare line 332

    Source documentation

    Literal Fin4 raw input is physically erased; no hidden encoded-input precondition is used. The macrotransition charge is quadratic; TM1 compilation adds a fixed multiplicative constant for this one fixed adapter machine.

    theorem prepare (code : Bool → Bool → List Bool) (B : ℕ)
    (hb : ∀ f x, (code f x).length≤B) (w : List Bool) (v : V) :
    ∃ t ≤ (4*B+12)*(w.length+1)^2, ∃ v',
      exec (TM1.step (M code)) t (⟨some 0,v,Tape.mk₁ (w.map raw)⟩ : Cfg)=
        some ⟨none,v',Tape.mk₁ ((emit code true w.reverse).map bit)⟩ := by
…

    Mentions: OAI.RationalHitting.TMTime.InputAdapter.V, OAI.RationalHitting.TMTime.exec, OAI.RationalHitting.TMTime.InputAdapter.M, OAI.RationalHitting.TMTime.InputAdapter.raw, OAI.RationalHitting.TMTime.InputAdapter.Cfg, OAI.RationalHitting.TMTime.InputAdapter.emit, OAI.RationalHitting.TMTime.InputAdapter.bit

  39. lemma OAI.RationalHitting.TMTime.InputAdapter.emit_false line 357
  40. lemma OAI.RationalHitting.TMTime.InputAdapter.stack_encoding line 363
  41. theorem OAI.RationalHitting.TMTime.InputAdapter.raw_stack_input line 386

    Source documentation

    Real finite TM0 raw-input adapter, at quadratic bit cost, reaching exactly Mathlib's initial tape for the binary stack simulator, not an assumed encoding.

    theorem raw_stack_input {K : Type} [DecidableEq K] (k : K) (b : ℕ)
    (enc : TM2to1.Γ' K (fun _ => Bool) → List.Vector Bool b) :
    ∃ (m : ℕ) (G : TM0.Machine A (Fin (m+1))) (C : ℕ), 0<C ∧
      ∀ w : List Bool, w≠[] → ∃ t≤C*(w.length+1)^2, ∃ a : TM0.Cfg A (Fin (m+1)),
        exec (TM0.step G) t (TM0.init (w.map raw))=some a ∧ TM0.step G a=none ∧
        a.Tape=Tape.mk₁ (((TM2to1.trInit k w).flatMap (fun z => (enc z).toList)).map bit) := by
…

    Mentions: OAI.RationalHitting.TMTime.InputAdapter.A, OAI.RationalHitting.TMTime.exec, OAI.RationalHitting.TMTime.InputAdapter.raw, OAI.RationalHitting.TMTime.InputAdapter.bit