OAI/Computability/RationalHitting/Model.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.RationalHitting.Formula line 9

    Also declared: ComparatorChallenges/RationalHitting.lean:9 (same declaration text).

  2. def OAI.RationalHitting.Formula.size line 19

    Also declared: ComparatorChallenges/RationalHitting.lean:19 (same declaration text).

  3. inductive OAI.RationalHitting.Formula.Eval line 26

    Source documentation

    Evaluation in any rational algebra; a unary inverse requires an actual two-sided inverse of the evaluated operand, not a totalized inverse.

    Also declared: ComparatorChallenges/RationalHitting.lean:26 (same declaration text).

    inductive Eval {n : ℕ} {R : Type u} [Ring R]
    (c : ℚ →+* R) (X : Fin n → R) : Formula n → R → Prop where
…

    Mentions: OAI.RationalHitting.Formula

  4. abbrev OAI.RationalHitting.Mat line 36

    Also declared: ComparatorChallenges/RationalHitting.lean:36 (same declaration text).

  5. abbrev OAI.RationalHitting.Tuple line 37

    Also declared: ComparatorChallenges/RationalHitting.lean:37 (same declaration text).

  6. def OAI.RationalHitting.Evaluates line 39

    Also declared: ComparatorChallenges/RationalHitting.lean:39 (same declaration text).

  7. def OAI.RationalHitting.Admissible line 42

    Also declared: ComparatorChallenges/RationalHitting.lean:42 (same declaration text).

  8. def OAI.RationalHitting.Nonzero line 45

    Also declared: ComparatorChallenges/RationalHitting.lean:45 (same declaration text).

  9. structure OAI.RationalHitting.Output line 49

    Source documentation

    All output tuples have one common positive dimension.

    Also declared: ComparatorChallenges/RationalHitting.lean:49 (same declaration text).

    structure Output (n : ℕ) where
…
  10. def OAI.RationalHitting.encodeNat line 56

    Source documentation

    Little-endian unsigned binary, prefixed by a unary bit-length and a zero terminator. This is a self-delimiting binary encoding, including zero.

    Also declared: ComparatorChallenges/RationalHitting.lean:56 (same declaration text).

    def encodeNat (a : ℕ) : List Bool :=
…
  11. def OAI.RationalHitting.encodeRat line 62

    Source documentation

    Sign bit, binary numerator magnitude, and positive binary denominator. Rat.num and Rat.den are the canonical reduced numerator and denominator.

    Also declared: ComparatorChallenges/RationalHitting.lean:62 (same declaration text).

    def encodeRat (a : ℚ) : List Bool :=
…
  12. def OAI.RationalHitting.encodeTuple line 65

    Also declared: ComparatorChallenges/RationalHitting.lean:65 (same declaration text).

  13. def OAI.RationalHitting.encodeOutput line 70

    Also declared: ComparatorChallenges/RationalHitting.lean:70 (same declaration text).

  14. abbrev OAI.RationalHitting.Alphabet line 75

    Source documentation

    0 is blank, 1 and 2 are the two literal binary digits, 3 is work space. Fixed finite tape alphabet and finite state space; no advice or oracle.

    Also declared: ComparatorChallenges/RationalHitting.lean:75 (same declaration text).

    abbrev Alphabet := Fin 4
  15. abbrev OAI.RationalHitting.Machine line 76

    Also declared: ComparatorChallenges/RationalHitting.lean:76 (same declaration text).

  16. abbrev OAI.RationalHitting.Config line 77

    Also declared: ComparatorChallenges/RationalHitting.lean:77 (same declaration text).

  17. def OAI.RationalHitting.tapeBit line 79

    Also declared: ComparatorChallenges/RationalHitting.lean:79 (same declaration text).

  18. def OAI.RationalHitting.unaryInput line 81

    Also declared: ComparatorChallenges/RationalHitting.lean:81 (same declaration text).

  19. def OAI.RationalHitting.run line 85

    Source documentation

    Exactly t ordinary deterministic TM0 transitions.

    Also declared: ComparatorChallenges/RationalHitting.lean:85 (same declaration text).

    def run {m : ℕ} (G : Machine m) : ℕ → Config m → Option (Config m)
  | 0, a => some a
  | t + 1, a => (Turing.TM0.step G a).bind (run G t)

    Mentions: OAI.RationalHitting.Machine, OAI.RationalHitting.Config

  20. def OAI.RationalHitting.OutputsWithin line 89

    Also declared: ComparatorChallenges/RationalHitting.lean:89 (same declaration text).

  21. def OAI.RationalHitting.Hits line 95

    Also declared: ComparatorChallenges/RationalHitting.lean:95 (same declaration text).

  22. def OAI.RationalHitting.MainStatement line 101

    Source documentation

    A fixed polynomial bound on bit time, full binary output length, and common positive dimension.

    Also declared: ComparatorChallenges/RationalHitting.lean:101 (same declaration text).

    def MainStatement : Prop :=
…