OAI/Analysis/MatrixSigning/Model.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.frame line 8

    Source documentation

    Escaped binary words.

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

    def frame : List Bool → List Bool
  | [] => [true]
  | b :: bs => false :: b :: frame bs
  2. def OAI.CurrentKS.encodeNat line 12

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:40 (same declaration text).

  3. def OAI.CurrentKS.encodeInt line 14
  4. structure OAI.CurrentKS.RationalEntry line 19

    Source documentation

    The two binary fields are a numerator and a positive denominator.

    structure RationalEntry where
…
  5. def OAI.CurrentKS.RationalEntry.value line 24
  6. def OAI.CurrentKS.RationalEntry.encode line 27
  7. abbrev OAI.CurrentKS.RationalComplex line 30
  8. def OAI.CurrentKS.encodeComplex line 32
  9. def OAI.CurrentKS.toComplex line 34
  10. structure OAI.CurrentKS.Input line 37
  11. def OAI.CurrentKS.Input.encodeMatrix line 45

    Source documentation

    Row-major entries; a matrix-record delimiter retains explicit list length also for order-zero matrices. This constant-per-matrix framing is polynomially equivalent to dense binary matrix listing in positive dimension.

    def Input.encodeMatrix (x : Input) (i : Fin x.N) : List Bool :=
…

    Mentions: OAI.CurrentKS.Input

  12. def OAI.CurrentKS.Input.encode line 49
  13. def OAI.CurrentKS.Input.length line 52
  14. def OAI.CurrentKS.Input.matrix line 54
  15. def OAI.CurrentKS.opNorm line 57
  16. def OAI.CurrentKS.Admissible line 60
  17. def OAI.CurrentKS.signValue line 63
  18. def OAI.CurrentKS.signedSum line 65
  19. def OAI.CurrentKS.variance line 69
  20. def OAI.CurrentKS.GoodOutput line 72
  21. inductive OAI.CurrentKS.StackAction line 75

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

  22. def OAI.CurrentKS.StackAction.apply line 81

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:48 (same declaration text).

  23. structure OAI.CurrentKS.Instruction line 86

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:53 (same declaration text).

  24. def OAI.CurrentKS.Instruction.halt line 90

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:57 (same declaration text).

  25. structure OAI.CurrentKS.Machine line 92

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:59 (same declaration text).

  26. structure OAI.CurrentKS.Config line 100

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:67 (same declaration text).

  27. def OAI.CurrentKS.topCode line 104

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:71 (same declaration text).

  28. def OAI.CurrentKS.headsCode line 109

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

  29. def OAI.CurrentKS.Machine.step line 113

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:80 (same declaration text).

  30. def OAI.CurrentKS.Machine.init line 123

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:90 (same declaration text).

  31. def OAI.CurrentKS.Machine.run line 126

    Also declared: ComparatorChallenges/AlgorithmicThinTrees.lean:93 (same declaration text).

  32. def OAI.CurrentKS.DeterministicRankOneSigning line 129